author  paulson 
Tue, 21 Oct 1997 10:39:27 +0200  
changeset 3961  6a8996fb7d99 
parent 3919  c036caebfc75 
child 4091  771b1f6422a8 
permissions  rwrr 
2002  1 
(* Title: HOL/Auth/OtwayRees_Bad 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1996 University of Cambridge 

5 

6 
Inductive relation "otway" for the OtwayRees protocol. 

7 

8 
The FAULTY version omitting encryption of Nonce NB, as suggested on page 247 of 

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

10 
Proc. Royal Soc. 426 (1989) 

11 

12 
This file illustrates the consequences of such errors. We can still prove 

2032  13 
impressivelooking properties such as Spy_not_see_encrypted_key, yet the 
2002  14 
protocol is open to a middleperson attack. Attempting to prove some key lemmas 
15 
indicates the possibility of this attack. 

16 
*) 

17 

18 
open OtwayRees_Bad; 

19 

20 
proof_timing:=true; 

21 
HOL_quantifiers := false; 

22 

23 

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

24 
(*A "possibility property": there are traces that reach the end*) 
2002  25 
goal thy 
26 
"!!A B. [ A ~= B; A ~= Server; B ~= Server ] \ 

27 
\ ==> EX K. EX NA. EX evs: otway. \ 

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

28 
\ Says B A {Nonce NA, Crypt (shrK A) {Nonce NA, Key K}} \ 
3465  29 
\ : set evs"; 
2002  30 
by (REPEAT (resolve_tac [exI,bexI] 1)); 
2032  31 
by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

32 
by possibility_tac; 
2002  33 
result(); 
34 

35 

36 
(**** Inductive proofs about otway ****) 

37 

38 
(*Nobody sends themselves messages*) 

3465  39 
goal thy "!!evs. evs : otway ==> ALL A X. Says A A X ~: set evs"; 
2032  40 
by (etac otway.induct 1); 
2002  41 
by (Auto_tac()); 
42 
qed_spec_mp "not_Says_to_self"; 

43 
Addsimps [not_Says_to_self]; 

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

45 

46 

47 
(** For reasoning about the encrypted portion of messages **) 

48 

3465  49 
goal thy "!!evs. Says A' B {N, Agent A, Agent B, X} : set evs ==> \ 
3683  50 
\ X : analz (spies evs)"; 
51 
by (blast_tac (!claset addSDs [Says_imp_spies RS analz.Inj]) 1); 

52 
qed "OR2_analz_spies"; 

2002  53 

3465  54 
goal thy "!!evs. Says S' B {N, X, Crypt (shrK B) X'} : set evs ==> \ 
3683  55 
\ X : analz (spies evs)"; 
56 
by (blast_tac (!claset addSDs [Says_imp_spies RS analz.Inj]) 1); 

57 
qed "OR4_analz_spies"; 

2002  58 

3465  59 
goal thy "!!evs. Says Server B {NA, X, Crypt K' {NB,K}} : set evs \ 
3683  60 
\ ==> K : parts (spies evs)"; 
61 
by (blast_tac (!claset addSEs spies_partsEs) 1); 

62 
qed "Oops_parts_spies"; 

2002  63 

64 
(*OR2_analz... and OR4_analz... let us treat those cases using the same 

65 
argument as for the Fake case. This is possible for most, but not all, 

66 
proofs: Fake does not invent new nonces (as in OR2), and of course Fake 

2032  67 
messages originate from the Spy. *) 
2002  68 

3683  69 
bind_thm ("OR2_parts_spies", 
70 
OR2_analz_spies RS (impOfSubs analz_subset_parts)); 

71 
bind_thm ("OR4_parts_spies", 

72 
OR4_analz_spies RS (impOfSubs analz_subset_parts)); 

2052  73 

3683  74 
(*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:
3466
diff
changeset

75 
fun parts_induct_tac i = 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

76 
etac otway.induct i THEN 
3683  77 
forward_tac [Oops_parts_spies] (i+6) THEN 
78 
forward_tac [OR4_parts_spies] (i+5) THEN 

79 
forward_tac [OR2_parts_spies] (i+3) THEN 

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

80 
prove_simple_subgoals_tac i; 
2002  81 

82 

3683  83 
(** Theorems of the form X ~: parts (spies evs) imply that NOBODY 
2002  84 
sends messages containing X! **) 
85 

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

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

90 
by (Fake_parts_insert_tac 1); 
3961  91 
by (ALLGOALS Blast_tac); 
2131  92 
qed "Spy_see_shrK"; 
93 
Addsimps [Spy_see_shrK]; 

2002  94 

2131  95 
goal thy 
3683  96 
"!!evs. evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; 
2131  97 
by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset)); 
98 
qed "Spy_analz_shrK"; 

99 
Addsimps [Spy_analz_shrK]; 

2002  100 

3683  101 
goal thy "!!A. [ Key (shrK A) : parts (spies evs); evs : otway ] ==> A:bad"; 
3102  102 
by (blast_tac (!claset addDs [Spy_see_shrK]) 1); 
2131  103 
qed "Spy_see_shrK_D"; 
2002  104 

2131  105 
bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D); 
106 
AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; 

2002  107 

108 

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

109 
(*Nobody can have used nonexistent keys!*) 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

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

113 
(*Fake*) 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

114 
by (best_tac 
3961  115 
(!claset addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)] 
116 
addIs [impOfSubs analz_subset_parts] 

117 
addDs [impOfSubs (analz_subset_parts RS keysFor_mono)] 

118 
addss (!simpset)) 1); 

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

119 
(*OR13*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

120 
by (ALLGOALS Blast_tac); 
2160  121 
qed_spec_mp "new_keys_not_used"; 
2002  122 

123 
bind_thm ("new_keys_not_analzd", 

2032  124 
[analz_subset_parts RS keysFor_mono, 
125 
new_keys_not_used] MRS contra_subsetD); 

2002  126 

127 
Addsimps [new_keys_not_used, new_keys_not_analzd]; 

128 

129 

2131  130 

131 
(*** Proofs involving analz ***) 

132 

133 
(*Describes the form of K and NA when the Server sends this message. Also 

134 
for Oops case.*) 

135 
goal thy 

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

136 
"!!evs. [ Says Server B \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

137 
\ {NA, X, Crypt (shrK B) {NB, Key K}} : set evs; \ 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

138 
\ evs : otway ] \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

139 
\ ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)"; 
2131  140 
by (etac rev_mp 1); 
141 
by (etac otway.induct 1); 

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

142 
by (prove_simple_subgoals_tac 1); 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

143 
by (Blast_tac 1); 
2131  144 
qed "Says_Server_message_form"; 
145 

146 

147 
(*For proofs involving analz.*) 

3683  148 
val analz_spies_tac = 
149 
dtac OR2_analz_spies 4 THEN 

150 
dtac OR4_analz_spies 6 THEN 

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

151 
forward_tac [Says_Server_message_form] 7 THEN assume_tac 7 THEN 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2417
diff
changeset

152 
REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7); 
2002  153 

154 

155 
(**** 

156 
The following is to prove theorems of the form 

157 

3683  158 
Key K : analz (insert (Key KAB) (spies evs)) ==> 
159 
Key K : analz (spies evs) 

2002  160 

161 
A more general formula must be proved inductively. 

162 
****) 

163 

164 

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

166 

167 
(*The equality makes the induction hypothesis easier to apply*) 

168 
goal thy 

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

169 
"!!evs. evs : otway ==> \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

170 
\ ALL K KK. KK <= Compl (range shrK) > \ 
3683  171 
\ (Key K : analz (Key``KK Un (spies evs))) = \ 
172 
\ (K : KK  Key K : analz (spies evs))"; 

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

175 
by (REPEAT_FIRST (resolve_tac [allI, impI])); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

176 
by (REPEAT_FIRST (rtac analz_image_freshK_lemma )); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

177 
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:
3207
diff
changeset

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

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

180 
(*Base*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

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

182 
qed_spec_mp "analz_image_freshK"; 
2002  183 

184 

185 
goal thy 

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

186 
"!!evs. [ evs : otway; KAB ~: range shrK ] ==> \ 
3683  187 
\ Key K : analz (insert (Key KAB) (spies evs)) = \ 
188 
\ (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

189 
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

190 
qed "analz_insert_freshK"; 
2002  191 

192 

2131  193 
(*** The Key K uniquely identifies the Server's message. **) 
2002  194 

195 
goal thy 

3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

196 
"!!evs. evs : otway ==> \ 
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

197 
\ EX B' NA' NB' X'. ALL B NA NB X. \ 
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

198 
\ Says Server B {NA, X, Crypt (shrK B) {NB, K}} : set evs > \ 
2131  199 
\ B=B' & NA=NA' & NB=NB' & X=X'"; 
2032  200 
by (etac otway.induct 1); 
2002  201 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib]))); 
3730  202 
by (ALLGOALS Clarify_tac); 
2002  203 
(*Remaining cases: OR3 and OR4*) 
204 
by (ex_strip_tac 2); 

3102  205 
by (Blast_tac 2); 
2107
23e8f15ec95f
The new proof of the lemma for new_nonces_not_seen is faster
paulson
parents:
2052
diff
changeset

206 
by (expand_case_tac "K = ?y" 1); 
23e8f15ec95f
The new proof of the lemma for new_nonces_not_seen is faster
paulson
parents:
2052
diff
changeset

207 
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2)); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

208 
(*...we assume X is a recent message, and handle this case by contradiction*) 
3683  209 
by (blast_tac (!claset addSEs spies_partsEs 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

210 
delrules [conjI] (*no splitup to 4 subgoals*)) 1); 
2002  211 
val lemma = result(); 
212 

213 
goal thy 

3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

214 
"!!evs. [ Says Server B {NA, X, Crypt (shrK B) {NB, K}} : set evs; \ 
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

215 
\ Says Server B' {NA',X',Crypt (shrK B') {NB',K}} : set evs; \ 
2131  216 
\ evs : otway ] ==> X=X' & B=B' & NA=NA' & NB=NB'"; 
2417  217 
by (prove_unique_tac lemma 1); 
2002  218 
qed "unique_session_keys"; 
219 

220 

2131  221 
(*Crucial security property, but not itself enough to guarantee correctness!*) 
222 
goal thy 

3683  223 
"!!evs. [ A ~: bad; B ~: bad; evs : otway ] \ 
2166  224 
\ ==> Says Server B \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

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

226 
\ Crypt (shrK B) {NB, Key K}} : set evs > \ 
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

227 
\ Says B Spy {NA, NB, Key K} ~: set evs > \ 
3683  228 
\ Key K ~: analz (spies evs)"; 
2131  229 
by (etac otway.induct 1); 
3683  230 
by analz_spies_tac; 
2131  231 
by (ALLGOALS 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

232 
(asm_simp_tac (!simpset addcongs [conj_cong] 
3674
65ec38fbb265
Deleted the redundant simprule not_parts_not_analz
paulson
parents:
3519
diff
changeset

233 
addsimps [analz_insert_eq, analz_insert_freshK] 
3961  234 
addsimps (pushes@expand_ifs)))); 
3451
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3207
diff
changeset

235 
(*Oops*) 
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3207
diff
changeset

236 
by (blast_tac (!claset addSDs [unique_session_keys]) 4); 
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3207
diff
changeset

237 
(*OR4*) 
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3207
diff
changeset

238 
by (Blast_tac 3); 
2131  239 
(*OR3*) 
3683  240 
by (blast_tac (!claset addSEs spies_partsEs 
3451
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3207
diff
changeset

241 
addIs [impOfSubs analz_subset_parts]) 2); 
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3207
diff
changeset

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

243 
by (spy_analz_tac 1); 
2131  244 
val lemma = result() RS mp RS mp RSN(2,rev_notE); 
245 

246 
goal thy 

3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

247 
"!!evs. [ Says Server B \ 
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

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

249 
\ Crypt (shrK B) {NB, Key K}} : set evs; \ 
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

250 
\ Says B Spy {NA, NB, Key K} ~: set evs; \ 
3683  251 
\ A ~: bad; B ~: bad; evs : otway ] \ 
252 
\ ==> Key K ~: analz (spies evs)"; 

2131  253 
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); 
3102  254 
by (blast_tac (!claset addSEs [lemma]) 1); 
2131  255 
qed "Spy_not_see_encrypted_key"; 
256 

257 

258 
(*** Attempting to prove stronger properties ***) 

259 

2052  260 
(*Only OR1 can have caused such a part of a message to appear. 
261 
I'm not sure why A ~= B premise is needed: OtwayRees.ML doesn't need it. 

262 
Perhaps it's because OR2 has two similarlooking encrypted messages in 

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

263 
this version.*) 
2002  264 
goal thy 
3683  265 
"!!evs. [ A ~: bad; A ~= B; evs : otway ] \ 
266 
\ ==> Crypt (shrK A) {NA, Agent A, Agent B} : parts (spies evs) > \ 

2131  267 
\ Says A B {NA, Agent A, Agent B, \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

268 
\ Crypt (shrK A) {NA, Agent A, Agent B}} : set evs"; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

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

270 
by (Fake_parts_insert_tac 1); 
3102  271 
by (Blast_tac 1); 
2002  272 
qed_spec_mp "Crypt_imp_OR1"; 
273 

274 

2131  275 
(*Crucial property: If the encrypted message appears, and A has used NA 
276 
to start a run, then it originated with the Server!*) 

277 
(*Only it is FALSE. Somebody could make a fake message to Server 

2002  278 
substituting some other nonce NA' for NB.*) 
279 
goal thy 

3683  280 
"!!evs. [ A ~: bad; A ~= Spy; evs : otway ] \ 
281 
\ ==> Crypt (shrK A) {NA, Key K} : parts (spies evs) > \ 

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

282 
\ Says A B {NA, Agent A, Agent B, \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

283 
\ Crypt (shrK A) {NA, Agent A, Agent B}} \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

284 
\ : set evs > \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

285 
\ (EX B NB. Says Server B \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

286 
\ {NA, \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

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

288 
\ Crypt (shrK B) {NB, Key K}} : set evs)"; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

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

290 
by (Fake_parts_insert_tac 1); 
2002  291 
(*OR1: it cannot be a new Nonce, contradiction.*) 
3102  292 
by (blast_tac (!claset addSIs [parts_insertI] 
3730  293 
addSEs spies_partsEs) 1); 
294 
(*OR3 and OR4*) 

295 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib]))); 

296 
by (ALLGOALS Clarify_tac); 

2002  297 
(*OR4*) 
3102  298 
by (blast_tac (!claset addSIs [Crypt_imp_OR1] 
3683  299 
addEs spies_partsEs) 2); 
2131  300 
(*OR3*) (** LEVEL 5 **) 
3730  301 
(*The hypotheses at this point suggest an attack in which nonce NB is used 
2052  302 
in two different roles: 
303 
Says B' Server 

3730  304 
{Nonce NA, Agent Aa, Agent A, 
305 
Crypt (shrK Aa) {Nonce NA, Agent Aa, Agent A}, Nonce NB, 

306 
Crypt (shrK A) {Nonce NA, Agent Aa, Agent A}} 

307 
: set evs3; 

2052  308 
Says A B 
3730  309 
{Nonce NB, Agent A, Agent B, 
310 
Crypt (shrK A) {Nonce NB, Agent A, Agent B}} 

311 
: set evs3; 

2052  312 
*) 
2131  313 
writeln "GIVE UP! on NA_Crypt_imp_Server_msg"; 
2002  314 

315 

2052  316 
(*Thus the key property A_can_trust probably fails too.*) 