author  paulson 
Thu, 08 Jan 1998 18:10:34 +0100  
changeset 4537  4e835bd9fada 
parent 4509  828148415197 
child 4831  dae4d63a1318 
permissions  rwrr 
1934  1 
(* Title: HOL/Auth/NS_Shared 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1996 University of Cambridge 

5 

6 
Inductive relation "ns_shared" for NeedhamSchroeder SharedKey protocol. 

7 

8 
From page 247 of 

9 
Burrows, Abadi and Needham. A Logic of Authentication. 

10 
Proc. Royal Soc. 426 (1989) 

11 
*) 

12 

13 
open NS_Shared; 

14 

4449  15 
set proof_timing; 
1997  16 
HOL_quantifiers := false; 
17 

4470  18 
AddEs spies_partsEs; 
19 
AddDs [impOfSubs analz_subset_parts]; 

20 
AddDs [impOfSubs Fake_parts_insert]; 

21 

1997  22 

2323  23 
(*A "possibility property": there are traces that reach the end*) 
1997  24 
goal thy 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

25 
"!!A B. [ A ~= B; A ~= Server; B ~= Server ] \ 
4237
fb01353e363b
The dtac was discarding information, though apparently no proofs were hurt
paulson
parents:
4091
diff
changeset

26 
\ ==> EX N K. EX evs: ns_shared. \ 
3465  27 
\ Says A B (Crypt K {Nonce N, Nonce N}) : set evs"; 
1997  28 
by (REPEAT (resolve_tac [exI,bexI] 1)); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

29 
by (rtac (ns_shared.Nil RS ns_shared.NS1 RS ns_shared.NS2 RS 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

30 
ns_shared.NS3 RS ns_shared.NS4 RS ns_shared.NS5) 2); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

31 
by possibility_tac; 
2015  32 
result(); 
33 

3675
70dd312b70b2
Deleted the redundant simprule not_parts_not_analz
paulson
parents:
3651
diff
changeset

34 
goal thy 
70dd312b70b2
Deleted the redundant simprule not_parts_not_analz
paulson
parents:
3651
diff
changeset

35 
"!!A B. [ A ~= B; A ~= Server; B ~= Server ] \ 
70dd312b70b2
Deleted the redundant simprule not_parts_not_analz
paulson
parents:
3651
diff
changeset

36 
\ ==> EX evs: ns_shared. \ 
70dd312b70b2
Deleted the redundant simprule not_parts_not_analz
paulson
parents:
3651
diff
changeset

37 
\ Says A B (Crypt ?K {Nonce ?N, Nonce ?N}) : set evs"; 
70dd312b70b2
Deleted the redundant simprule not_parts_not_analz
paulson
parents:
3651
diff
changeset

38 
by (REPEAT (resolve_tac [exI,bexI] 1)); 
70dd312b70b2
Deleted the redundant simprule not_parts_not_analz
paulson
parents:
3651
diff
changeset

39 
by (rtac (ns_shared.Nil RS ns_shared.NS1 RS ns_shared.NS2 RS 
70dd312b70b2
Deleted the redundant simprule not_parts_not_analz
paulson
parents:
3651
diff
changeset

40 
ns_shared.NS3 RS ns_shared.NS4 RS ns_shared.NS5) 2); 
70dd312b70b2
Deleted the redundant simprule not_parts_not_analz
paulson
parents:
3651
diff
changeset

41 
by possibility_tac; 
1943  42 

1934  43 
(**** Inductive proofs about ns_shared ****) 
44 

45 
(*Nobody sends themselves messages*) 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

46 
goal thy "!!evs. evs : ns_shared ==> ALL A X. Says A A X ~: set evs"; 
2032  47 
by (etac ns_shared.induct 1); 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4470
diff
changeset

48 
by Auto_tac; 
1934  49 
qed_spec_mp "not_Says_to_self"; 
50 
Addsimps [not_Says_to_self]; 

51 
AddSEs [not_Says_to_self RSN (2, rev_notE)]; 

52 

1943  53 
(*For reasoning about the encrypted portion of message NS3*) 
3465  54 
goal thy "!!evs. Says S A (Crypt KA {N, B, K, X}) : set evs \ 
3683  55 
\ ==> X : parts (spies evs)"; 
4470  56 
by (Blast_tac 1); 
3683  57 
qed "NS3_msg_in_parts_spies"; 
2032  58 

2070  59 
goal thy 
3465  60 
"!!evs. Says Server A (Crypt (shrK A) {NA, B, K, X}) : set evs \ 
3683  61 
\ ==> K : parts (spies evs)"; 
4470  62 
by (Blast_tac 1); 
3683  63 
qed "Oops_parts_spies"; 
2070  64 

3683  65 
(*For proving the easier theorems about X ~: parts (spies evs).*) 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

66 
fun parts_induct_tac i = 
4331  67 
EVERY [etac ns_shared.induct i, 
68 
REPEAT (FIRSTGOAL analz_mono_contra_tac), 

69 
forward_tac [Oops_parts_spies] (i+7), 

70 
forward_tac [NS3_msg_in_parts_spies] (i+4), 

71 
prove_simple_subgoals_tac i]; 

2070  72 

1934  73 

3683  74 
(** Theorems of the form X ~: parts (spies evs) imply that NOBODY 
2015  75 
sends messages containing X! **) 
1934  76 

3683  77 
(*Spy never sees another agent's shared key! (unless it's bad at start)*) 
1934  78 
goal thy 
3683  79 
"!!evs. evs : ns_shared ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

80 
by (parts_induct_tac 1); 
3961  81 
by (ALLGOALS Blast_tac); 
2131  82 
qed "Spy_see_shrK"; 
83 
Addsimps [Spy_see_shrK]; 

1934  84 

2131  85 
goal thy 
3683  86 
"!!evs. evs : ns_shared ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4470
diff
changeset

87 
by Auto_tac; 
2131  88 
qed "Spy_analz_shrK"; 
89 
Addsimps [Spy_analz_shrK]; 

1934  90 

4470  91 
AddSDs [Spy_see_shrK RSN (2, rev_iffD1), 
92 
Spy_analz_shrK RSN (2, rev_iffD1)]; 

1934  93 

2070  94 

2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

95 
(*Nobody can have used nonexistent keys!*) 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

96 
goal thy "!!evs. evs : ns_shared ==> \ 
3683  97 
\ Key K ~: used evs > K ~: keysFor (parts (spies evs))"; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

98 
by (parts_induct_tac 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

99 
(*Fake*) 
4509
828148415197
Making proofs faster, especially using keysFor_parts_insert
paulson
parents:
4477
diff
changeset

100 
by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

101 
(*NS2, NS4, NS5*) 
4470  102 
by (ALLGOALS (Blast_tac)); 
2160  103 
qed_spec_mp "new_keys_not_used"; 
1934  104 

105 
bind_thm ("new_keys_not_analzd", 

2032  106 
[analz_subset_parts RS keysFor_mono, 
107 
new_keys_not_used] MRS contra_subsetD); 

1934  108 

109 
Addsimps [new_keys_not_used, new_keys_not_analzd]; 

110 

111 

112 
(** Lemmas concerning the form of items passed in messages **) 

113 

2015  114 
(*Describes the form of K, X and K' when the Server sends this message.*) 
1934  115 
goal thy 
3683  116 
"!!evs. [ Says Server A (Crypt K' {N, Agent B, Key K, X}) : set evs; \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

117 
\ evs : ns_shared ] \ 
4267  118 
\ ==> K ~: range shrK & \ 
119 
\ X = (Crypt (shrK B) {Key K, Agent A}) & \ 

2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

120 
\ K' = shrK A"; 
2032  121 
by (etac rev_mp 1); 
122 
by (etac ns_shared.induct 1); 

4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4470
diff
changeset

123 
by Auto_tac; 
1934  124 
qed "Says_Server_message_form"; 
125 

126 

2070  127 
(*If the encrypted message appears then it originated with the Server*) 
1934  128 
goal thy 
3683  129 
"!!evs. [ Crypt (shrK A) {NA, Agent B, Key K, X} : parts (spies evs); \ 
4267  130 
\ A ~: bad; evs : ns_shared ] \ 
131 
\ ==> Says Server A (Crypt (shrK A) {NA, Agent B, Key K, X}) \ 

3651  132 
\ : set evs"; 
2070  133 
by (etac rev_mp 1); 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

134 
by (parts_induct_tac 1); 
4470  135 
by (Blast_tac 1); 
2323  136 
qed "A_trusts_NS2"; 
1934  137 

1965  138 

4331  139 
goal thy 
140 
"!!evs. [ Crypt (shrK A) {NA, Agent B, Key K, X} : parts (spies evs); \ 

141 
\ A ~: bad; evs : ns_shared ] \ 

142 
\ ==> K ~: range shrK & X = (Crypt (shrK B) {Key K, Agent A})"; 

143 
by (blast_tac (claset() addSDs [A_trusts_NS2, Says_Server_message_form]) 1); 

144 
qed "cert_A_form"; 

145 

146 

1965  147 
(*EITHER describes the form of X when the following message is sent, 
148 
OR reduces it to the Fake case. 

149 
Use Says_Server_message_form if applicable.*) 

1934  150 
goal thy 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

151 
"!!evs. [ Says S A (Crypt (shrK A) {Nonce NA, Agent B, Key K, X}) \ 
3651  152 
\ : set evs; \ 
153 
\ evs : ns_shared ] \ 

3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

154 
\ ==> (K ~: range shrK & X = (Crypt (shrK B) {Key K, Agent A})) \ 
3683  155 
\  X : analz (spies evs)"; 
156 
by (case_tac "A : bad" 1); 

4091  157 
by (fast_tac (claset() addSDs [Says_imp_spies RS analz.Inj] 
4237
fb01353e363b
The dtac was discarding information, though apparently no proofs were hurt
paulson
parents:
4091
diff
changeset

158 
addss (simpset())) 1); 
4470  159 
by (blast_tac (claset() addSDs [cert_A_form]) 1); 
1934  160 
qed "Says_S_message_form"; 
161 

162 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

163 
(*For proofs involving analz.*) 
3683  164 
val analz_spies_tac = 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

165 
forward_tac [Says_Server_message_form] 8 THEN 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

166 
forward_tac [Says_S_message_form] 5 THEN 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

167 
REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] ORELSE' hyp_subst_tac); 
2131  168 

1934  169 

170 
(**** 

171 
The following is to prove theorems of the form 

172 

3683  173 
Key K : analz (insert (Key KAB) (spies evs)) ==> 
174 
Key K : analz (spies evs) 

1934  175 

176 
A more general formula must be proved inductively. 

177 
****) 

178 

179 

180 
(*NOT useful in this form, but it says that session keys are not used 

181 
to encrypt messages containing other keys, in the actual protocol. 

182 
We require that agents should behave like this subsequently also.*) 

183 
goal thy 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

184 
"!!evs. [ evs : ns_shared; Kab ~: range shrK ] ==> \ 
4237
fb01353e363b
The dtac was discarding information, though apparently no proofs were hurt
paulson
parents:
4091
diff
changeset

185 
\ (Crypt KAB X) : parts (spies evs) & \ 
3683  186 
\ Key K : parts {X} > Key K : parts (spies evs)"; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

187 
by (parts_induct_tac 1); 
4470  188 
(*Fake*) 
4091  189 
by (blast_tac (claset() addSEs partsEs 
4237
fb01353e363b
The dtac was discarding information, though apparently no proofs were hurt
paulson
parents:
4091
diff
changeset

190 
addDs [impOfSubs parts_insert_subset_Un]) 1); 
1965  191 
(*Base, NS4 and NS5*) 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4470
diff
changeset

192 
by Auto_tac; 
1934  193 
result(); 
194 

195 

196 
(** Session keys are not used to encrypt other session keys **) 

197 

2015  198 
(*The equality makes the induction hypothesis easier to apply*) 
1934  199 
goal thy 
4237
fb01353e363b
The dtac was discarding information, though apparently no proofs were hurt
paulson
parents:
4091
diff
changeset

200 
"!!evs. evs : ns_shared ==> \ 
fb01353e363b
The dtac was discarding information, though apparently no proofs were hurt
paulson
parents:
4091
diff
changeset

201 
\ ALL K KK. KK <= Compl (range shrK) > \ 
3683  202 
\ (Key K : analz (Key``KK Un (spies evs))) = \ 
203 
\ (K : KK  Key K : analz (spies evs))"; 

2032  204 
by (etac ns_shared.induct 1); 
3683  205 
by analz_spies_tac; 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

206 
by (REPEAT_FIRST (resolve_tac [allI, impI])); 
3961  207 
by (REPEAT_FIRST (rtac analz_image_freshK_lemma)); 
208 
(*Takes 9 secs*) 

2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

209 
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); 
3451
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3441
diff
changeset

210 
(*Fake*) 
4422
21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4331
diff
changeset

211 
by (spy_analz_tac 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

212 
qed_spec_mp "analz_image_freshK"; 
1934  213 

214 

215 
goal thy 

4237
fb01353e363b
The dtac was discarding information, though apparently no proofs were hurt
paulson
parents:
4091
diff
changeset

216 
"!!evs. [ evs : ns_shared; KAB ~: range shrK ] ==> \ 
3683  217 
\ Key K : analz (insert (Key KAB) (spies evs)) = \ 
218 
\ (K = KAB  Key K : analz (spies evs))"; 

2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

219 
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

220 
qed "analz_insert_freshK"; 
1934  221 

222 

2558  223 
(** The session key K uniquely identifies the message **) 
1965  224 

1934  225 
goal thy 
4267  226 
"!!evs. evs : ns_shared ==> \ 
4237
fb01353e363b
The dtac was discarding information, though apparently no proofs were hurt
paulson
parents:
4091
diff
changeset

227 
\ EX A' NA' B' X'. ALL A NA B X. \ 
3683  228 
\ Says Server A (Crypt (shrK A) {NA, Agent B, Key K, X}) : set evs \ 
229 
\ > A=A' & NA=NA' & B=B' & X=X'"; 

2032  230 
by (etac ns_shared.induct 1); 
4091  231 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); 
3730  232 
by Safe_tac; 
2070  233 
(*NS3*) 
234 
by (ex_strip_tac 2); 

3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

235 
by (Blast_tac 2); 
2070  236 
(*NS2: it can't be a new key*) 
237 
by (expand_case_tac "K = ?y" 1); 

238 
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2)); 

4470  239 
by (Blast_tac 1); 
1934  240 
val lemma = result(); 
241 

242 
(*In messages of this form, the session key uniquely identifies the rest*) 

243 
goal thy 

4237
fb01353e363b
The dtac was discarding information, though apparently no proofs were hurt
paulson
parents:
4091
diff
changeset

244 
"!!evs. [ Says Server A \ 
fb01353e363b
The dtac was discarding information, though apparently no proofs were hurt
paulson
parents:
4091
diff
changeset

245 
\ (Crypt (shrK A) {NA, Agent B, Key K, X}) : set evs; \ 
fb01353e363b
The dtac was discarding information, though apparently no proofs were hurt
paulson
parents:
4091
diff
changeset

246 
\ Says Server A' \ 
3683  247 
\ (Crypt (shrK A') {NA', Agent B', Key K, X'}) : set evs; \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

248 
\ evs : ns_shared ] ==> A=A' & NA=NA' & B=B' & X = X'"; 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2374
diff
changeset

249 
by (prove_unique_tac lemma 1); 
1934  250 
qed "unique_session_keys"; 
251 

252 

2032  253 
(** Crucial secrecy property: Spy does not see the keys sent in msg NS2 **) 
2015  254 

1934  255 
goal thy 
3961  256 
"!!evs. [ A ~: bad; B ~: bad; evs : ns_shared ] \ 
2015  257 
\ ==> Says Server A \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

258 
\ (Crypt (shrK A) {NA, Agent B, Key K, \ 
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

259 
\ Crypt (shrK B) {Key K, Agent A}}) \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

260 
\ : set evs > \ 
4537
4e835bd9fada
Expressed most Oops rules using Notes instead of Says, and other tidying
paulson
parents:
4509
diff
changeset

261 
\ (ALL NB. Notes Spy {NA, NB, Key K} ~: set evs) > \ 
3683  262 
\ Key K ~: analz (spies evs)"; 
2032  263 
by (etac ns_shared.induct 1); 
3683  264 
by analz_spies_tac; 
1934  265 
by (ALLGOALS 
2015  266 
(asm_simp_tac 
4091  267 
(simpset() addsimps ([analz_insert_eq, analz_insert_freshK] @ 
4237
fb01353e363b
The dtac was discarding information, though apparently no proofs were hurt
paulson
parents:
4091
diff
changeset

268 
pushes @ expand_ifs)))); 
3451
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3441
diff
changeset

269 
(*Oops*) 
4509
828148415197
Making proofs faster, especially using keysFor_parts_insert
paulson
parents:
4477
diff
changeset

270 
by (blast_tac (claset() addSDs [unique_session_keys]) 5); 
3679  271 
(*NS3, replay subcase*) 
3451
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3441
diff
changeset

272 
by (Blast_tac 4); 
1934  273 
(*NS2*) 
4470  274 
by (Blast_tac 2); 
3451
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3441
diff
changeset

275 
(*Fake*) 
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3441
diff
changeset

276 
by (spy_analz_tac 1); 
3679  277 
(*NS3, Server subcase*) (**LEVEL 6 **) 
4091  278 
by (clarify_tac (claset() delrules [impCE]) 1); 
3683  279 
by (forward_tac [Says_imp_spies RS parts.Inj RS A_trusts_NS2] 1); 
2170  280 
by (assume_tac 2); 
4091  281 
by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj RS 
4470  282 
Crypt_Spy_analz_bad]) 1); 
4091  283 
by (blast_tac (claset() addDs [unique_session_keys]) 1); 
2070  284 
val lemma = result() RS mp RS mp RSN(2,rev_notE); 
2015  285 

286 

287 
(*Final version: Server's message in the most abstract form*) 

288 
goal thy 

4237
fb01353e363b
The dtac was discarding information, though apparently no proofs were hurt
paulson
parents:
4091
diff
changeset

289 
"!!evs. [ Says Server A \ 
4331  290 
\ (Crypt K' {NA, Agent B, Key K, X}) : set evs; \ 
4537
4e835bd9fada
Expressed most Oops rules using Notes instead of Says, and other tidying
paulson
parents:
4509
diff
changeset

291 
\ ALL NB. Notes Spy {NA, NB, Key K} ~: set evs; \ 
3683  292 
\ A ~: bad; B ~: bad; evs : ns_shared \ 
293 
\ ] ==> Key K ~: analz (spies evs)"; 

2015  294 
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); 
4091  295 
by (blast_tac (claset() addSDs [lemma]) 1); 
2032  296 
qed "Spy_not_see_encrypted_key"; 
297 

298 

2070  299 
(**** Guarantees available at various stages of protocol ***) 
300 

3651  301 
A_trusts_NS2 RS Spy_not_see_encrypted_key; 
2070  302 

303 

304 
(*If the encrypted message appears then it originated with the Server*) 

305 
goal thy 

4237
fb01353e363b
The dtac was discarding information, though apparently no proofs were hurt
paulson
parents:
4091
diff
changeset

306 
"!!evs. [ Crypt (shrK B) {Key K, Agent A} : parts (spies evs); \ 
fb01353e363b
The dtac was discarding information, though apparently no proofs were hurt
paulson
parents:
4091
diff
changeset

307 
\ B ~: bad; evs : ns_shared ] \ 
2070  308 
\ ==> EX NA. Says Server A \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

309 
\ (Crypt (shrK A) {NA, Agent B, Key K, \ 
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

310 
\ Crypt (shrK B) {Key K, Agent A}}) \ 
3465  311 
\ : set evs"; 
2070  312 
by (etac rev_mp 1); 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

313 
by (parts_induct_tac 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

314 
by (ALLGOALS Blast_tac); 
2323  315 
qed "B_trusts_NS3"; 
2070  316 

317 

318 
goal thy 

4331  319 
"!!evs. [ Crypt K (Nonce NB) : parts (spies evs); \ 
320 
\ Says Server A (Crypt (shrK A) {NA, Agent B, Key K, X}) \ 

321 
\ : set evs; \ 

322 
\ Key K ~: analz (spies evs); \ 

323 
\ evs : ns_shared ] \ 

324 
\ ==> Says B A (Crypt K (Nonce NB)) : set evs"; 

325 
by (etac rev_mp 1); 

326 
by (etac rev_mp 1); 

327 
by (etac rev_mp 1); 

328 
by (parts_induct_tac 1); 

4267  329 
(*NS3*) 
330 
by (Blast_tac 3); 

4470  331 
by (Blast_tac 1); 
4267  332 
(*NS2: contradiction from the assumptions 
4331  333 
Key K ~: used evs2 and Crypt K (Nonce NB) : parts (spies evs2) *) 
334 
by (blast_tac (claset() addSEs [new_keys_not_used RSN (2,rev_notE)] 

335 
addSDs [Crypt_imp_keysFor]) 1); 

336 
(**LEVEL 7**) 

337 
(*NS4*) 

338 
by (Clarify_tac 1); 

339 
by (not_bad_tac "Ba" 1); 

4470  340 
by (blast_tac (claset() addDs [B_trusts_NS3, unique_session_keys]) 1); 
4331  341 
qed "A_trusts_NS4_lemma"; 
2103  342 

4331  343 

344 
(*This version no longer assumes that K is secure*) 

2103  345 
goal thy 
4267  346 
"!!evs. [ Crypt K (Nonce NB) : parts (spies evs); \ 
4331  347 
\ Crypt (shrK A) {NA, Agent B, Key K, X} : parts (spies evs); \ 
4537
4e835bd9fada
Expressed most Oops rules using Notes instead of Says, and other tidying
paulson
parents:
4509
diff
changeset

348 
\ ALL NB. Notes Spy {NA, NB, Key K} ~: set evs; \ 
4267  349 
\ A ~: bad; B ~: bad; evs : ns_shared ] \ 
3465  350 
\ ==> Says B A (Crypt K (Nonce NB)) : set evs"; 
4331  351 
by (blast_tac (claset() addSIs [A_trusts_NS2, A_trusts_NS4_lemma] 
4267  352 
addSEs [Spy_not_see_encrypted_key RSN (2,rev_notE)]) 1); 
2323  353 
qed "A_trusts_NS4"; 
4331  354 

355 

356 
(*If the session key has been used in NS4 then somebody has forwarded 

357 
component X in some instance of NS4. Perhaps an interesting property, 

358 
but not needed (after all) for the proofs below.*) 

359 
goal thy 

360 
"!!evs. [ Crypt K (Nonce NB) : parts (spies evs); \ 

361 
\ Says Server A (Crypt (shrK A) {NA, Agent B, Key K, X}) \ 

362 
\ : set evs; \ 

363 
\ Key K ~: analz (spies evs); \ 

364 
\ evs : ns_shared ] \ 

365 
\ ==> EX A'. Says A' B X : set evs"; 

366 
by (etac rev_mp 1); 

367 
by (etac rev_mp 1); 

368 
by (etac rev_mp 1); 

369 
by (parts_induct_tac 1); 

370 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib]))); 

371 
by (ALLGOALS Clarify_tac); 

4470  372 
by (Blast_tac 1); 
4331  373 
(**LEVEL 7**) 
374 
(*NS2*) 

375 
by (blast_tac (claset() addSEs [new_keys_not_used RSN (2,rev_notE)] 

376 
addSDs [Crypt_imp_keysFor]) 1); 

377 
(*NS4*) 

378 
by (not_bad_tac "Ba" 1); 

379 
by (Asm_full_simp_tac 1); 

380 
by (forward_tac [Says_imp_spies RS parts.Inj RS B_trusts_NS3] 1); 

381 
by (ALLGOALS Clarify_tac); 

382 
by (blast_tac (claset() addDs [unique_session_keys]) 1); 

383 
qed "NS4_implies_NS3"; 

384 

385 

386 
goal thy 

387 
"!!evs. [ B ~: bad; evs : ns_shared ] \ 

388 
\ ==> Key K ~: analz (spies evs) > \ 

389 
\ Says Server A \ 

390 
\ (Crypt (shrK A) {NA, Agent B, Key K, \ 

391 
\ Crypt (shrK B) {Key K, Agent A}}) \ 

392 
\ : set evs > \ 

393 
\ Says B A (Crypt K (Nonce NB)) : set evs > \ 

394 
\ Crypt K {Nonce NB, Nonce NB} : parts (spies evs) > \ 

395 
\ Says A B (Crypt K {Nonce NB, Nonce NB}) : set evs"; 

396 
by (parts_induct_tac 1); 

397 
(*NS4*) 

4470  398 
by (Blast_tac 4); 
4331  399 
(*NS3*) 
4470  400 
by (blast_tac (claset() addSDs [cert_A_form]) 3); 
4331  401 
(*NS2*) 
402 
by (blast_tac (claset() addSEs [new_keys_not_used RSN (2,rev_notE)] 

403 
addSDs [Crypt_imp_keysFor]) 2); 

4470  404 
by (Blast_tac 1); 
4331  405 
(**LEVEL 5**) 
406 
(*NS5*) 

407 
by (Clarify_tac 1); 

408 
by (not_bad_tac "Aa" 1); 

4470  409 
by (blast_tac (claset() addDs [A_trusts_NS2, unique_session_keys]) 1); 
4331  410 
val lemma = result(); 
411 

412 

413 
(*Very strong Oops condition reveals protocol's weakness*) 

414 
goal thy 

415 
"!!evs. [ Crypt K {Nonce NB, Nonce NB} : parts (spies evs); \ 

416 
\ Says B A (Crypt K (Nonce NB)) : set evs; \ 

417 
\ Crypt (shrK B) {Key K, Agent A} : parts (spies evs); \ 

4537
4e835bd9fada
Expressed most Oops rules using Notes instead of Says, and other tidying
paulson
parents:
4509
diff
changeset

418 
\ ALL NA NB. Notes Spy {NA, NB, Key K} ~: set evs; \ 
4331  419 
\ A ~: bad; B ~: bad; evs : ns_shared ] \ 
420 
\ ==> Says A B (Crypt K {Nonce NB, Nonce NB}) : set evs"; 

421 
by (dtac B_trusts_NS3 1); 

422 
by (ALLGOALS Clarify_tac); 

423 
by (blast_tac (claset() addSIs [normalize_thm [RSspec, RSmp] lemma] 

424 
addSEs [Spy_not_see_encrypted_key RSN (2,rev_notE)]) 1); 

425 
qed "B_trusts_NS5"; 