60 by (fast_tac (!claset addSEs partsEs |
60 by (fast_tac (!claset addSEs partsEs |
61 addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1); |
61 addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1); |
62 qed "OR5_parts_sees_Enemy"; |
62 qed "OR5_parts_sees_Enemy"; |
63 |
63 |
64 (*OR2_analz... and OR4_analz... let us treat those cases using the same |
64 (*OR2_analz... and OR4_analz... let us treat those cases using the same |
65 argument as for the Fake case.*) |
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 |
|
67 messages originate from the Enemy. *) |
|
68 |
66 val OR2_OR4_tac = |
69 val OR2_OR4_tac = |
67 dtac (OR2_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 4 THEN |
70 dtac (OR2_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 4 THEN |
68 dtac (OR4_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 6; |
71 dtac (OR4_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 6; |
69 |
72 |
70 |
73 |
71 (*** Shared keys are not betrayed ***) |
74 (*** Shared keys are not betrayed ***) |
72 |
75 |
73 (*Enemy never sees another agent's shared key!*) |
76 (*Enemy never sees another agent's shared key! (unless it is leaked at start)*) |
74 goal thy |
77 goal thy |
75 "!!evs. [| evs : otway; A ~= Enemy |] ==> \ |
78 "!!evs. [| evs : otway; A ~= Enemy; A ~: Friend``leaked |] ==> \ |
76 \ Key (shrK A) ~: parts (sees Enemy evs)"; |
79 \ Key (shrK A) ~: parts (sees Enemy evs)"; |
77 be otway.induct 1; |
80 be otway.induct 1; |
78 by OR2_OR4_tac; |
81 by OR2_OR4_tac; |
79 by (Auto_tac()); |
82 by (Auto_tac()); |
80 (*Deals with Fake message*) |
83 (*Deals with Fake message*) |
88 Addsimps [Enemy_not_see_shrK, |
91 Addsimps [Enemy_not_see_shrK, |
89 not_sym RSN (2, Enemy_not_see_shrK), |
92 not_sym RSN (2, Enemy_not_see_shrK), |
90 Enemy_not_analz_shrK, |
93 Enemy_not_analz_shrK, |
91 not_sym RSN (2, Enemy_not_analz_shrK)]; |
94 not_sym RSN (2, Enemy_not_analz_shrK)]; |
92 |
95 |
93 (*We go to some trouble to preserve R in the 3rd subgoal*) |
96 (*We go to some trouble to preserve R in the 3rd and 4th subgoals |
|
97 As usual fast_tac cannot be used because it uses the equalities too soon*) |
94 val major::prems = |
98 val major::prems = |
95 goal thy "[| Key (shrK A) : parts (sees Enemy evs); \ |
99 goal thy "[| Key (shrK A) : parts (sees Enemy evs); \ |
96 \ evs : otway; \ |
100 \ evs : otway; \ |
97 \ A=Enemy ==> R \ |
101 \ A=Enemy ==> R; \ |
|
102 \ !!i. [| A = Friend i; i: leaked |] ==> R \ |
98 \ |] ==> R"; |
103 \ |] ==> R"; |
99 br ccontr 1; |
104 br ccontr 1; |
100 br ([major, Enemy_not_see_shrK] MRS rev_notE) 1; |
105 br ([major, Enemy_not_see_shrK] MRS rev_notE) 1; |
|
106 br notI 3; |
|
107 be imageE 3; |
101 by (swap_res_tac prems 2); |
108 by (swap_res_tac prems 2); |
102 by (ALLGOALS (fast_tac (!claset addIs prems))); |
109 by (swap_res_tac prems 3 THEN ALLGOALS (fast_tac (!claset addIs prems))); |
103 qed "Enemy_see_shrK_E"; |
110 qed "Enemy_see_shrK_E"; |
104 |
111 |
105 bind_thm ("Enemy_analz_shrK_E", |
112 bind_thm ("Enemy_analz_shrK_E", |
106 analz_subset_parts RS subsetD RS Enemy_see_shrK_E); |
113 analz_subset_parts RS subsetD RS Enemy_see_shrK_E); |
107 |
114 |
108 (*Classical reasoner doesn't need the not_sym versions (with swapped ~=) *) |
115 (*Classical reasoner doesn't need the not_sym versions (with swapped ~=) *) |
109 AddSEs [Enemy_see_shrK_E, Enemy_analz_shrK_E]; |
116 AddSEs [Enemy_see_shrK_E, Enemy_analz_shrK_E]; |
110 |
|
111 |
|
112 (*No Friend will ever see another agent's shared key |
|
113 (excluding the Enemy, who might transmit his). |
|
114 The Server, of course, knows all shared keys.*) |
|
115 goal thy |
|
116 "!!evs. [| evs : otway; A ~= Enemy; A ~= Friend j |] ==> \ |
|
117 \ Key (shrK A) ~: parts (sees (Friend j) evs)"; |
|
118 br (sees_agent_subset_sees_Enemy RS parts_mono RS contra_subsetD) 1; |
|
119 by (ALLGOALS Asm_simp_tac); |
|
120 qed "Friend_not_see_shrK"; |
|
121 |
|
122 |
|
123 (*Not for Addsimps -- it can cause goals to blow up!*) |
|
124 goal thy |
|
125 "!!evs. evs : otway ==> \ |
|
126 \ (Key (shrK A) : analz (insert (Key (shrK B)) (sees Enemy evs))) = \ |
|
127 \ (A=B | A=Enemy)"; |
|
128 by (best_tac (!claset addDs [impOfSubs analz_subset_parts] |
|
129 addIs [impOfSubs (subset_insertI RS analz_mono)] |
|
130 addss (!simpset)) 1); |
|
131 qed "shrK_mem_analz"; |
|
132 |
117 |
133 |
118 |
134 (*** Future keys can't be seen or used! ***) |
119 (*** Future keys can't be seen or used! ***) |
135 |
120 |
136 (*Nobody can have SEEN keys that will be generated in the future. |
121 (*Nobody can have SEEN keys that will be generated in the future. |
241 by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes))); |
225 by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes))); |
242 (*Deals with Faked messages*) |
226 (*Deals with Faked messages*) |
243 by (best_tac (!claset addSEs partsEs |
227 by (best_tac (!claset addSEs partsEs |
244 addDs [impOfSubs analz_subset_parts, |
228 addDs [impOfSubs analz_subset_parts, |
245 impOfSubs parts_insert_subset_Un] |
229 impOfSubs parts_insert_subset_Un] |
246 addss (!simpset)) 1); |
230 addss (!simpset)) 2); |
247 (*OR5*) |
231 (*Base case and OR5*) |
248 by (fast_tac (!claset addss (!simpset)) 1); |
232 by (Auto_tac()); |
249 result(); |
233 result(); |
250 |
234 |
251 |
235 |
252 (** Specialized rewriting for this proof **) |
236 (** Specialized rewriting for this proof **) |
253 |
237 |
254 Delsimps [image_insert]; |
238 Delsimps [image_insert]; |
255 Addsimps [image_insert RS sym]; |
239 Addsimps [image_insert RS sym]; |
|
240 |
|
241 Delsimps [image_Un]; |
|
242 Addsimps [image_Un RS sym]; |
256 |
243 |
257 goal thy "insert (Key (newK x)) (sees A evs) = \ |
244 goal thy "insert (Key (newK x)) (sees A evs) = \ |
258 \ Key `` (newK``{x}) Un (sees A evs)"; |
245 \ Key `` (newK``{x}) Un (sees A evs)"; |
259 by (Fast_tac 1); |
246 by (Fast_tac 1); |
260 val insert_Key_singleton = result(); |
247 val insert_Key_singleton = result(); |
292 ]); |
279 ]); |
293 |
280 |
294 |
281 |
295 (*Lemma for the trivial direction of the if-and-only-if*) |
282 (*Lemma for the trivial direction of the if-and-only-if*) |
296 goal thy |
283 goal thy |
297 "!!evs. (Key K : analz (insert KsC (Key``nE Un sEe))) --> \ |
284 "!!evs. (Key K : analz (Key``nE Un sEe)) --> \ |
298 \ (K : nE | Key K : analz (insert KsC sEe)) ==> \ |
285 \ (K : nE | Key K : analz sEe) ==> \ |
299 \ (Key K : analz (insert KsC (Key``nE Un sEe))) = \ |
286 \ (Key K : analz (Key``nE Un sEe)) = (K : nE | Key K : analz sEe)"; |
300 \ (K : nE | Key K : analz (insert KsC sEe))"; |
|
301 by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1); |
287 by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1); |
302 val lemma = result(); |
288 val lemma = result(); |
303 |
289 |
|
290 |
304 goal thy |
291 goal thy |
305 "!!evs. evs : otway ==> \ |
292 "!!evs. evs : otway ==> \ |
306 \ ALL K E. (Key K : analz (insert (Key (shrK C)) \ |
293 \ ALL K E. (Key K : analz (Key``(newK``E) Un (sees Enemy evs))) = \ |
307 \ (Key``(newK``E) Un (sees Enemy evs)))) = \ |
294 \ (K : newK``E | Key K : analz (sees Enemy evs))"; |
308 \ (K : newK``E | \ |
|
309 \ Key K : analz (insert (Key (shrK C)) \ |
|
310 \ (sees Enemy evs)))"; |
|
311 be otway.induct 1; |
295 be otway.induct 1; |
312 bd OR2_analz_sees_Enemy 4; |
296 bd OR2_analz_sees_Enemy 4; |
313 bd OR4_analz_sees_Enemy 6; |
297 bd OR4_analz_sees_Enemy 6; |
314 by (REPEAT_FIRST (resolve_tac [allI, lemma])); |
298 by (REPEAT_FIRST (resolve_tac [allI, lemma])); |
315 by (ALLGOALS (*Takes 40 secs*) |
299 by (ALLGOALS (*Takes 35 secs*) |
316 (asm_simp_tac |
300 (asm_simp_tac |
317 (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK] |
301 (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK] |
318 @ pushes) |
302 @ pushes) |
319 setloop split_tac [expand_if]))); |
303 setloop split_tac [expand_if]))); |
320 (*OR4*) |
304 (*OR4*) |
321 by (enemy_analz_tac 5); |
305 by (enemy_analz_tac 5); |
322 (*OR3*) |
306 (*OR3*) |
323 by (Fast_tac 4); |
307 by (Fast_tac 4); |
324 (*OR2*) (** LEVEL 11 **) |
308 (*OR2*) (** LEVEL 7 **) |
325 by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")] |
309 by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")] |
326 (insert_commute RS ssubst) 3); |
310 (insert_commute RS ssubst) 3); |
327 by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")] |
311 by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")] |
328 (insert_commute RS ssubst) 3); |
312 (insert_commute RS ssubst) 3); |
329 by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 3); |
313 by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 3); |
330 by (enemy_analz_tac 3); |
314 by (enemy_analz_tac 3); |
331 (*Fake case*) (** LEVEL 6 **) |
315 (*Fake case*) (** LEVEL 11 **) |
332 by (res_inst_tac [("y1","X"), ("A1", "?G Un (?H::msg set)")] |
316 by (res_inst_tac [("y1","X"), ("A1", "?G Un (?H::msg set)")] |
333 (insert_commute RS ssubst) 2); |
317 (insert_commute RS ssubst) 2); |
334 by (enemy_analz_tac 2); |
318 by (enemy_analz_tac 2); |
335 (*Base case*) |
319 (*Base case*) |
336 by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1); |
320 by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1); |
337 qed_spec_mp "analz_image_newK"; |
321 qed_spec_mp "analz_image_newK"; |
338 |
322 |
339 |
323 |
340 goal thy |
324 goal thy |
341 "!!evs. evs : otway ==> \ |
325 "!!evs. evs : otway ==> \ |
342 \ Key K : analz (insert (Key (newK evt)) \ |
326 \ Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) = \ |
343 \ (insert (Key (shrK C)) \ |
327 \ (K = newK evt | Key K : analz (sees Enemy evs))"; |
344 \ (sees Enemy evs))) = \ |
|
345 \ (K = newK evt | \ |
|
346 \ Key K : analz (insert (Key (shrK C)) \ |
|
347 \ (sees Enemy evs)))"; |
|
348 by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, |
328 by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, |
349 insert_Key_singleton]) 1); |
329 insert_Key_singleton]) 1); |
350 by (Fast_tac 1); |
330 by (Fast_tac 1); |
351 qed "analz_insert_Key_newK"; |
331 qed "analz_insert_Key_newK"; |
352 |
332 |
369 (*Crucial secrecy property: Enemy does not see the keys sent in msg OR3*) |
349 (*Crucial secrecy property: Enemy does not see the keys sent in msg OR3*) |
370 goal thy |
350 goal thy |
371 "!!evs. [| Says Server (Friend j) \ |
351 "!!evs. [| Says Server (Friend j) \ |
372 \ {|Ni, Crypt {|Ni, K|} (shrK (Friend i)), \ |
352 \ {|Ni, Crypt {|Ni, K|} (shrK (Friend i)), \ |
373 \ Crypt {|Nj, K|} (shrK (Friend j))|} : set_of_list evs; \ |
353 \ Crypt {|Nj, K|} (shrK (Friend j))|} : set_of_list evs; \ |
374 \ evs : otway; Friend i ~= C; Friend j ~= C \ |
354 \ i ~: leaked; j ~: leaked; evs : otway |] ==> \ |
375 \ |] ==> \ |
355 \ K ~: analz (sees Enemy evs)"; |
376 \ K ~: analz (insert (Key (shrK C)) (sees Enemy evs))"; |
|
377 be rev_mp 1; |
356 be rev_mp 1; |
378 be otway.induct 1; |
357 be otway.induct 1; |
379 bd OR2_analz_sees_Enemy 4; |
358 bd OR2_analz_sees_Enemy 4; |
380 bd OR4_analz_sees_Enemy 6; |
359 bd OR4_analz_sees_Enemy 6; |
381 by (ALLGOALS Asm_simp_tac); |
360 by (ALLGOALS Asm_simp_tac); |
382 (*Next 3 steps infer that K has the form "Key (newK evs'" ... *) |
361 (*Next 3 steps infer that K has the form "Key (newK evs'" ... *) |
383 by (REPEAT_FIRST (resolve_tac [conjI, impI])); |
362 by (REPEAT_FIRST (resolve_tac [conjI, impI])); |
384 by (TRYALL (forward_tac [Says_Server_message_form] THEN' assume_tac)); |
363 by (TRYALL (forward_tac [Says_Server_message_form] THEN' assume_tac)); |
385 by (REPEAT_FIRST (eresolve_tac [bexE, exE, conjE] ORELSE' hyp_subst_tac)); |
364 by (REPEAT_FIRST (eresolve_tac [bexE, exE, conjE] ORELSE' hyp_subst_tac)); |
386 by (ALLGOALS |
365 by (ALLGOALS |
387 (asm_full_simp_tac |
366 (asm_full_simp_tac |
388 (!simpset addsimps ([analz_subset_parts RS contra_subsetD, |
367 (!simpset addsimps ([analz_subset_parts RS contra_subsetD, |
389 analz_insert_Key_newK] @ pushes) |
368 analz_insert_Key_newK] @ pushes) |
390 setloop split_tac [expand_if]))); |
369 setloop split_tac [expand_if]))); |
391 (*OR3*) |
370 (*OR3*) |
392 by (fast_tac (!claset addSEs [less_irrefl]) 3); |
371 by (fast_tac (!claset addSEs [less_irrefl]) 3); |
393 (*Fake*) (** LEVEL 8 **) |
372 (*Fake*) (** LEVEL 10 **) |
394 by (res_inst_tac [("y1","X"), ("x1", "Key ?K")] (insert_commute RS ssubst) 1); |
373 by (res_inst_tac [("y1","X"), ("x1", "Key ?K")] (insert_commute RS ssubst) 1); |
395 by (enemy_analz_tac 1); |
374 by (enemy_analz_tac 1); |
396 (*OR4*) |
375 (*OR4*) |
397 by (mp_tac 2); |
376 by (mp_tac 2); |
398 by (enemy_analz_tac 2); |
377 by (enemy_analz_tac 2); |
409 (*** Session keys are issued at most once, and identify the principals ***) |
388 (*** Session keys are issued at most once, and identify the principals ***) |
410 |
389 |
411 (** First, two lemmas for the Fake, OR2 and OR4 cases **) |
390 (** First, two lemmas for the Fake, OR2 and OR4 cases **) |
412 |
391 |
413 goal thy |
392 goal thy |
414 "!!evs. [| X : synth (analz (sees Enemy evs)); \ |
393 "!!evs. [| X : synth (analz (sees Enemy evs)); \ |
415 \ Crypt X' (shrK C) : parts{X}; \ |
394 \ Crypt X' (shrK C) : parts{X}; \ |
416 \ C ~= Enemy; evs : otway |] \ |
395 \ C ~= Enemy; C ~: Friend``leaked; evs : otway |] \ |
417 \ ==> Crypt X' (shrK C) : parts (sees Enemy evs)"; |
396 \ ==> Crypt X' (shrK C) : parts (sees Enemy evs)"; |
418 by (best_tac (!claset addSEs [impOfSubs analz_subset_parts] |
397 by (best_tac (!claset addSEs [impOfSubs analz_subset_parts] |
419 addDs [impOfSubs parts_insert_subset_Un] |
398 addDs [impOfSubs parts_insert_subset_Un] |
420 addss (!simpset)) 1); |
399 addss (!simpset)) 1); |
421 qed "Crypt_Fake_parts"; |
400 qed "Crypt_Fake_parts"; |
431 fun ex_strip_tac i = REPEAT (ares_tac [exI, conjI] i) THEN assume_tac (i+1); |
410 fun ex_strip_tac i = REPEAT (ares_tac [exI, conjI] i) THEN assume_tac (i+1); |
432 |
411 |
433 (*The Key K uniquely identifies a pair of senders in the message encrypted by |
412 (*The Key K uniquely identifies a pair of senders in the message encrypted by |
434 C, but if C=Enemy then he could send all sorts of nonsense.*) |
413 C, but if C=Enemy then he could send all sorts of nonsense.*) |
435 goal thy |
414 goal thy |
436 "!!evs. evs : otway ==> \ |
415 "!!evs. evs : otway ==> \ |
437 \ EX A B. ALL C. \ |
416 \ EX A B. ALL C. \ |
438 \ C ~= Enemy --> \ |
417 \ C ~= Enemy & C ~: Friend``leaked --> \ |
439 \ (ALL S S' X. Says S S' X : set_of_list evs --> \ |
418 \ (ALL S S' X. Says S S' X : set_of_list evs --> \ |
440 \ (EX NA. Crypt {|NA, Key K|} (shrK C) : parts{X}) --> C=A | C=B)"; |
419 \ (EX NA. Crypt {|NA, Key K|} (shrK C) : parts{X}) --> C=A | C=B)"; |
441 by (Simp_tac 1); |
420 by (Simp_tac 1); |
442 be otway.induct 1; |
421 be otway.induct 1; |
443 bd OR2_analz_sees_Enemy 4; |
422 bd OR2_analz_sees_Enemy 4; |