author  paulson 
Mon, 28 Oct 1996 12:55:24 +0100  
changeset 2131  3106a99d30a5 
parent 2107  23e8f15ec95f 
child 2160  ad4382e546fc 
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 

24 
(*Weak liveness: there are traces that reach the end*) 

25 
goal thy 

26 
"!!A B. [ A ~= B; A ~= Server; B ~= Server ] \ 

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

28 
\ Says B A {Nonce NA, Crypt {Nonce NA, Key K} (shrK A)} \ 

29 
\ : set_of_list evs"; 

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); 
2002  32 
by (ALLGOALS (simp_tac (!simpset setsolver safe_solver))); 
33 
by (REPEAT_FIRST (resolve_tac [refl, conjI])); 

34 
by (ALLGOALS (fast_tac (!claset addss (!simpset setsolver safe_solver)))); 

35 
result(); 

36 

37 

38 
(**** Inductive proofs about otway ****) 

39 

2032  40 
(*The Spy can see more than anybody else, except for their initial state*) 
2002  41 
goal thy 
42 
"!!evs. evs : otway ==> \ 

2052  43 
\ sees lost A evs <= initState lost A Un sees lost Spy evs"; 
2032  44 
by (etac otway.induct 1); 
2002  45 
by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] 
2032  46 
addss (!simpset)))); 
47 
qed "sees_agent_subset_sees_Spy"; 

2002  48 

49 

50 
(*Nobody sends themselves messages*) 

51 
goal thy "!!evs. evs : otway ==> ALL A X. Says A A X ~: set_of_list evs"; 

2032  52 
by (etac otway.induct 1); 
2002  53 
by (Auto_tac()); 
54 
qed_spec_mp "not_Says_to_self"; 

55 
Addsimps [not_Says_to_self]; 

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

57 

58 

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

60 

61 
goal thy "!!evs. Says A' B {N, Agent A, Agent B, X} : set_of_list evs ==> \ 

2052  62 
\ X : analz (sees lost Spy evs)"; 
2032  63 
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1); 
64 
qed "OR2_analz_sees_Spy"; 

2002  65 

66 
goal thy "!!evs. Says S B {N, X, X'} : set_of_list evs ==> \ 

2052  67 
\ X : analz (sees lost Spy evs)"; 
2032  68 
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1); 
69 
qed "OR4_analz_sees_Spy"; 

2002  70 

2131  71 
goal thy "!!evs. Says Server B {NA, X, Crypt {NB,K} K'} : set_of_list evs \ 
72 
\ ==> K : parts (sees lost Spy evs)"; 

2002  73 
by (fast_tac (!claset addSEs partsEs 
2032  74 
addSDs [Says_imp_sees_Spy RS parts.Inj]) 1); 
2131  75 
qed "Oops_parts_sees_Spy"; 
2002  76 

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

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

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

2032  80 
messages originate from the Spy. *) 
2002  81 

2052  82 
bind_thm ("OR2_parts_sees_Spy", 
83 
OR2_analz_sees_Spy RS (impOfSubs analz_subset_parts)); 

84 
bind_thm ("OR4_parts_sees_Spy", 

85 
OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts)); 

86 

2002  87 
val parts_Fake_tac = 
2052  88 
forward_tac [OR2_parts_sees_Spy] 4 THEN 
89 
forward_tac [OR4_parts_sees_Spy] 6 THEN 

2131  90 
forward_tac [Oops_parts_sees_Spy] 7; 
91 

92 
(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *) 

93 
fun parts_induct_tac i = SELECT_GOAL 

94 
(DETERM (etac otway.induct 1 THEN parts_Fake_tac THEN 

95 
(*Fake message*) 

96 
TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts, 

97 
impOfSubs Fake_parts_insert] 

98 
addss (!simpset)) 2)) THEN 

99 
(*Base case*) 

100 
fast_tac (!claset addss (!simpset)) 1 THEN 

101 
ALLGOALS Asm_simp_tac) i; 

2002  102 

103 

2052  104 
(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY 
2002  105 
sends messages containing X! **) 
106 

2131  107 
(*Spy never sees another agent's shared key! (unless it's lost at start)*) 
2002  108 
goal thy 
2131  109 
"!!evs. evs : otway \ 
110 
\ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)"; 

111 
by (parts_induct_tac 1); 

2002  112 
by (Auto_tac()); 
2131  113 
qed "Spy_see_shrK"; 
114 
Addsimps [Spy_see_shrK]; 

2002  115 

2131  116 
goal thy 
117 
"!!evs. evs : otway \ 

118 
\ ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)"; 

119 
by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset)); 

120 
qed "Spy_analz_shrK"; 

121 
Addsimps [Spy_analz_shrK]; 

2002  122 

2131  123 
goal thy "!!A. [ Key (shrK A) : parts (sees lost Spy evs); \ 
124 
\ evs : otway ] ==> A:lost"; 

125 
by (fast_tac (!claset addDs [Spy_see_shrK]) 1); 

126 
qed "Spy_see_shrK_D"; 

2002  127 

2131  128 
bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D); 
129 
AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; 

2002  130 

131 

132 
(*** Future keys can't be seen or used! ***) 

133 

134 
(*Nobody can have SEEN keys that will be generated in the future. 

135 
This has to be proved anew for each protocol description, 

136 
but should go by similar reasoning every time. Hardest case is the 

137 
standard Fake rule. 

138 
The Union over C is essential for the induction! *) 

139 
goal thy "!!evs. evs : otway ==> \ 

140 
\ length evs <= length evs' > \ 

2052  141 
\ Key (newK evs') ~: (UN C. parts (sees lost C evs))"; 
2131  142 
by (parts_induct_tac 1); 
2002  143 
by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts, 
2032  144 
impOfSubs parts_insert_subset_Un, 
145 
Suc_leD] 

146 
addss (!simpset)))); 

2002  147 
val lemma = result(); 
148 

149 
(*Variant needed for the main theorem below*) 

150 
goal thy 

151 
"!!evs. [ evs : otway; length evs <= length evs' ] \ 

2052  152 
\ ==> Key (newK evs') ~: parts (sees lost C evs)"; 
2002  153 
by (fast_tac (!claset addDs [lemma]) 1); 
154 
qed "new_keys_not_seen"; 

155 
Addsimps [new_keys_not_seen]; 

156 

157 
(*Another variant: old messages must contain old keys!*) 

158 
goal thy 

159 
"!!evs. [ Says A B X : set_of_list evs; \ 

160 
\ Key (newK evt) : parts {X}; \ 

161 
\ evs : otway \ 

162 
\ ] ==> length evt < length evs"; 

2032  163 
by (rtac ccontr 1); 
2052  164 
by (dtac leI 1); 
2032  165 
by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy] 
2052  166 
addIs [impOfSubs parts_mono]) 1); 
2002  167 
qed "Says_imp_old_keys"; 
168 

169 

170 
(*** Future nonces can't be seen or used! [proofs resemble those above] ***) 

171 

172 
goal thy "!!evs. evs : otway ==> \ 

173 
\ length evs <= length evs' > \ 

2052  174 
\ Nonce (newN evs') ~: (UN C. parts (sees lost C evs))"; 
2032  175 
by (etac otway.induct 1); 
2002  176 
(*auto_tac does not work here, as it performs safe_tac first*) 
2107
23e8f15ec95f
The new proof of the lemma for new_nonces_not_seen is faster
paulson
parents:
2052
diff
changeset

177 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert2] 
23e8f15ec95f
The new proof of the lemma for new_nonces_not_seen is faster
paulson
parents:
2052
diff
changeset

178 
addcongs [disj_cong]))); 
23e8f15ec95f
The new proof of the lemma for new_nonces_not_seen is faster
paulson
parents:
2052
diff
changeset

179 
by (REPEAT_FIRST (fast_tac (!claset 
23e8f15ec95f
The new proof of the lemma for new_nonces_not_seen is faster
paulson
parents:
2052
diff
changeset

180 
addSEs partsEs 
23e8f15ec95f
The new proof of the lemma for new_nonces_not_seen is faster
paulson
parents:
2052
diff
changeset

181 
addSDs [Says_imp_sees_Spy RS parts.Inj] 
23e8f15ec95f
The new proof of the lemma for new_nonces_not_seen is faster
paulson
parents:
2052
diff
changeset

182 
addDs [impOfSubs analz_subset_parts, 
2032  183 
impOfSubs parts_insert_subset_Un, 
184 
Suc_leD] 

185 
addss (!simpset)))); 

2002  186 
val lemma = result(); 
187 

188 
(*Variant needed for the main theorem below*) 

189 
goal thy 

190 
"!!evs. [ evs : otway; length evs <= length evs' ] \ 

2052  191 
\ ==> Nonce (newN evs') ~: parts (sees lost C evs)"; 
2002  192 
by (fast_tac (!claset addDs [lemma]) 1); 
193 
qed "new_nonces_not_seen"; 

194 
Addsimps [new_nonces_not_seen]; 

195 

196 
(*Another variant: old messages must contain old nonces!*) 

197 
goal thy 

198 
"!!evs. [ Says A B X : set_of_list evs; \ 

199 
\ Nonce (newN evt) : parts {X}; \ 

200 
\ evs : otway \ 

201 
\ ] ==> length evt < length evs"; 

2032  202 
by (rtac ccontr 1); 
2052  203 
by (dtac leI 1); 
2032  204 
by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Spy] 
2052  205 
addIs [impOfSubs parts_mono]) 1); 
2002  206 
qed "Says_imp_old_nonces"; 
207 

208 

209 
(*Nobody can have USED keys that will be generated in the future. 

210 
...very like new_keys_not_seen*) 

211 
goal thy "!!evs. evs : otway ==> \ 

212 
\ length evs <= length evs' > \ 

2052  213 
\ newK evs' ~: keysFor (UN C. parts (sees lost C evs))"; 
2131  214 
by (parts_induct_tac 1); 
2002  215 
(*OR1 and OR3*) 
216 
by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2])); 

217 
(*Fake, OR2, OR4: these messages send unknown (X) components*) 

2107
23e8f15ec95f
The new proof of the lemma for new_nonces_not_seen is faster
paulson
parents:
2052
diff
changeset

218 
by (REPEAT 
23e8f15ec95f
The new proof of the lemma for new_nonces_not_seen is faster
paulson
parents:
2052
diff
changeset

219 
(best_tac 
2002  220 
(!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono), 
2032  221 
impOfSubs (parts_insert_subset_Un RS keysFor_mono), 
222 
Suc_leD] 

223 
addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)] 

2107
23e8f15ec95f
The new proof of the lemma for new_nonces_not_seen is faster
paulson
parents:
2052
diff
changeset

224 
addss (!simpset)) 1)); 
2002  225 
val lemma = result(); 
226 

227 
goal thy 

228 
"!!evs. [ evs : otway; length evs <= length evs' ] \ 

2052  229 
\ ==> newK evs' ~: keysFor (parts (sees lost C evs))"; 
2002  230 
by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1); 
231 
qed "new_keys_not_used"; 

232 

233 
bind_thm ("new_keys_not_analzd", 

2032  234 
[analz_subset_parts RS keysFor_mono, 
235 
new_keys_not_used] MRS contra_subsetD); 

2002  236 

237 
Addsimps [new_keys_not_used, new_keys_not_analzd]; 

238 

239 

2131  240 

241 
(*** Proofs involving analz ***) 

242 

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

244 
for Oops case.*) 

245 
goal thy 

246 
"!!evs. [ Says Server B \ 

247 
\ {NA, X, Crypt {NB, K} (shrK B)} : set_of_list evs; \ 

248 
\ evs : otway ] \ 

249 
\ ==> (EX evt: otway. K = Key(newK evt)) & \ 

250 
\ (EX i. NA = Nonce i) & (EX j. NB = Nonce j)"; 

251 
by (etac rev_mp 1); 

252 
by (etac otway.induct 1); 

253 
by (ALLGOALS (fast_tac (!claset addss (!simpset)))); 

254 
qed "Says_Server_message_form"; 

255 

256 

257 
(*For proofs involving analz.*) 

258 
val analz_Fake_tac = 

259 
dtac OR2_analz_sees_Spy 4 THEN 

260 
dtac OR4_analz_sees_Spy 6 THEN 

261 
forward_tac [Says_Server_message_form] 7 THEN 

262 
assume_tac 7 THEN Full_simp_tac 7 THEN 

263 
REPEAT ((eresolve_tac [bexE, exE, conjE] ORELSE' hyp_subst_tac) 7); 

2002  264 

265 

266 
(**** 

267 
The following is to prove theorems of the form 

268 

2052  269 
Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) ==> 
270 
Key K : analz (sees lost Spy evs) 

2002  271 

272 
A more general formula must be proved inductively. 

273 

274 
****) 

275 

276 

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

278 

279 
(*Lemma for the trivial direction of the ifandonlyif*) 

280 
goal thy 

281 
"!!evs. (Key K : analz (Key``nE Un sEe)) > \ 

282 
\ (K : nE  Key K : analz sEe) ==> \ 

283 
\ (Key K : analz (Key``nE Un sEe)) = (K : nE  Key K : analz sEe)"; 

284 
by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1); 

285 
val lemma = result(); 

286 

287 

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

289 
goal thy 

290 
"!!evs. evs : otway ==> \ 

2052  291 
\ ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \ 
292 
\ (K : newK``E  Key K : analz (sees lost Spy evs))"; 

2032  293 
by (etac otway.induct 1); 
2131  294 
by analz_Fake_tac; 
2002  295 
by (REPEAT_FIRST (ares_tac [allI, lemma])); 
2131  296 
by (ALLGOALS 
2002  297 
(asm_simp_tac 
298 
(!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK] 

2032  299 
@ pushes) 
2002  300 
setloop split_tac [expand_if]))); 
301 
(** LEVEL 7 **) 

2131  302 
(*OR4, OR2, Fake*) 
303 
by (EVERY (map spy_analz_tac [5,3,2])); 

304 
(*Oops, OR3, Base*) 

305 
by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1)); 

2002  306 
qed_spec_mp "analz_image_newK"; 
307 

308 

309 
goal thy 

310 
"!!evs. evs : otway ==> \ 

2052  311 
\ Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) = \ 
312 
\ (K = newK evt  Key K : analz (sees lost Spy evs))"; 

2002  313 
by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
2032  314 
insert_Key_singleton]) 1); 
2002  315 
by (Fast_tac 1); 
316 
qed "analz_insert_Key_newK"; 

317 

318 

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

321 
goal thy 

2131  322 
"!!evs. evs : otway ==> \ 
323 
\ EX B' NA' NB' X'. ALL B NA NB X. \ 

324 
\ Says Server B {NA, X, Crypt {NB, K} (shrK B)} : set_of_list evs > \ 

325 
\ B=B' & NA=NA' & NB=NB' & X=X'"; 

2032  326 
by (etac otway.induct 1); 
2002  327 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib]))); 
328 
by (Step_tac 1); 

329 
(*Remaining cases: OR3 and OR4*) 

330 
by (ex_strip_tac 2); 

331 
by (Fast_tac 2); 

2107
23e8f15ec95f
The new proof of the lemma for new_nonces_not_seen is faster
paulson
parents:
2052
diff
changeset

332 
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

333 
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2)); 
2002  334 
(*...we assume X is a very new message, and handle this case by contradiction*) 
335 
by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl] 

2032  336 
delrules [conjI] (*prevent splitup into 4 subgoals*) 
337 
addss (!simpset addsimps [parts_insertI])) 1); 

2002  338 
val lemma = result(); 
339 

340 
goal thy 

2131  341 
"!!evs. [ Says Server B {NA, X, Crypt {NB, K} (shrK B)} \ 
2002  342 
\ : set_of_list evs; \ 
2131  343 
\ Says Server B' {NA',X',Crypt {NB',K} (shrK B')} \ 
2002  344 
\ : set_of_list evs; \ 
2131  345 
\ evs : otway ] ==> X=X' & B=B' & NA=NA' & NB=NB'"; 
2032  346 
by (dtac lemma 1); 
2002  347 
by (REPEAT (etac exE 1)); 
348 
(*Duplicate the assumption*) 

349 
by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1); 

350 
by (fast_tac (!claset addSDs [spec]) 1); 

351 
qed "unique_session_keys"; 

352 

353 

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

356 
"!!evs. [ A ~: lost; B ~: lost; evs : otway; evt : otway ] \ 

357 
\ ==> Says Server B \ 

358 
\ {NA, Crypt {NA, Key K} (shrK A), \ 

359 
\ Crypt {NB, Key K} (shrK B)} : set_of_list evs > \ 

360 
\ Says B Spy {NA, NB, Key K} ~: set_of_list evs > \ 

361 
\ Key K ~: analz (sees lost Spy evs)"; 

362 
by (etac otway.induct 1); 

363 
by analz_Fake_tac; 

364 
by (ALLGOALS 

365 
(asm_full_simp_tac 

366 
(!simpset addsimps ([analz_subset_parts RS contra_subsetD, 

367 
analz_insert_Key_newK] @ pushes) 

368 
setloop split_tac [expand_if]))); 

369 
(*OR3*) 

370 
by (fast_tac (!claset addSIs [parts_insertI] 

371 
addEs [Says_imp_old_keys RS less_irrefl] 

372 
addss (!simpset addsimps [parts_insert2])) 3); 

373 
(*OR4, OR2, Fake*) 

374 
by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac)); 

375 
(*Oops*) (** LEVEL 5 **) 

376 
by (fast_tac (!claset delrules [disjE] 

377 
addDs [unique_session_keys] addss (!simpset)) 1); 

378 
val lemma = result() RS mp RS mp RSN(2,rev_notE); 

379 

380 

381 
goal thy 

382 
"!!evs. [ Says Server B \ 

383 
\ {NA, Crypt {NA, K} (shrK A), \ 

384 
\ Crypt {NB, K} (shrK B)} : set_of_list evs; \ 

385 
\ Says B Spy {NA, NB, K} ~: set_of_list evs; \ 

386 
\ A ~: lost; B ~: lost; evs : otway ] \ 

387 
\ ==> K ~: analz (sees lost Spy evs)"; 

388 
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); 

389 
by (fast_tac (!claset addSEs [lemma]) 1); 

390 
qed "Spy_not_see_encrypted_key"; 

391 

392 

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

394 

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

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

398 
this version.*) 

2002  399 
goal thy 
2131  400 
"!!evs. [ A ~: lost; A ~= B; evs : otway ] \ 
401 
\ ==> Crypt {NA, Agent A, Agent B} (shrK A) \ 

2052  402 
\ : parts (sees lost Spy evs) > \ 
2131  403 
\ Says A B {NA, Agent A, Agent B, \ 
2002  404 
\ Crypt {NA, Agent A, Agent B} (shrK A)} \ 
405 
\ : set_of_list evs"; 

2131  406 
by (parts_induct_tac 1); 
407 
by (Fast_tac 1); 

2002  408 
qed_spec_mp "Crypt_imp_OR1"; 
409 

410 

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

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

2002  414 
substituting some other nonce NA' for NB.*) 
415 
goal thy 

2052  416 
"!!evs. [ A ~: lost; A ~= Spy; evs : otway ] \ 
417 
\ ==> Crypt {NA, Key K} (shrK A) : parts (sees lost Spy evs) > \ 

2131  418 
\ Says A B {NA, Agent A, Agent B, \ 
2052  419 
\ Crypt {NA, Agent A, Agent B} (shrK A)} \ 
2131  420 
\ : set_of_list evs > \ 
421 
\ (EX B NB. Says Server B \ 

422 
\ {NA, \ 

2052  423 
\ Crypt {NA, Key K} (shrK A), \ 
424 
\ Crypt {NB, Key K} (shrK B)} \ 

2002  425 
\ : set_of_list evs)"; 
2131  426 
by (parts_induct_tac 1); 
2002  427 
(*OR1: it cannot be a new Nonce, contradiction.*) 
428 
by (fast_tac (!claset addSIs [parts_insertI] 

2032  429 
addSEs partsEs 
430 
addEs [Says_imp_old_nonces RS less_irrefl] 

431 
addss (!simpset)) 1); 

2002  432 
(*OR4*) 
433 
by (REPEAT (Safe_step_tac 2)); 

2052  434 
by (REPEAT (best_tac (!claset addSDs [parts_cut]) 3)); 
435 
by (fast_tac (!claset addSIs [Crypt_imp_OR1] 

436 
addEs partsEs 

437 
addDs [Says_imp_sees_Spy RS parts.Inj]) 2); 

2131  438 
(*OR3*) (** LEVEL 5 **) 
2002  439 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib]))); 
2052  440 
by (step_tac (!claset delrules [disjCI, impCE]) 1); 
2002  441 
(*The hypotheses at this point suggest an attack in which nonce NA is used 
2052  442 
in two different roles: 
443 
Says B' Server 

444 
{Nonce NAa, Agent Aa, Agent A, 

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

446 
Crypt {Nonce NAa, Agent Aa, Agent A} (shrK A)} 

447 
: set_of_list evsa; 

448 
Says A B 

449 
{Nonce NA, Agent A, Agent B, 

450 
Crypt {Nonce NA, Agent A, Agent B} (shrK A)} 

451 
: set_of_list evsa 

452 
*) 

2131  453 
writeln "GIVE UP! on NA_Crypt_imp_Server_msg"; 
2002  454 

455 

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