changeset 1942 | 6c9c1a42a869 |
parent 1933 | 8b24773de6db |
child 2032 | 1bbf1bdcaf56 |
1941:f97a6e5b6375 | 1942:6c9c1a42a869 |
---|---|
26 |
26 |
27 goal List.thy "!!x. xs = x#xs' ==> x : set_of_list xs"; |
27 goal List.thy "!!x. xs = x#xs' ==> x : set_of_list xs"; |
28 by (Asm_simp_tac 1); |
28 by (Asm_simp_tac 1); |
29 qed "set_of_list_eqI1"; |
29 qed "set_of_list_eqI1"; |
30 |
30 |
31 goal List.thy "set_of_list l <= set_of_list (x#l)"; |
|
32 by (Simp_tac 1); |
|
33 by (Fast_tac 1); |
|
34 qed "set_of_list_subset_Cons"; |
|
35 |
|
36 (*Not for Addsimps -- it can cause goals to blow up!*) |
|
37 goal Set.thy "(a : (if Q then x else y)) = ((Q --> a:x) & (~Q --> a : y))"; |
|
38 by (simp_tac (!simpset setloop split_tac [expand_if]) 1); |
|
39 qed "mem_if"; |
|
40 |
|
41 (*FUN.ML?? WE NEED A NOTION OF INVERSE IMAGE, OR GRAPH!!*) |
31 (*FUN.ML?? WE NEED A NOTION OF INVERSE IMAGE, OR GRAPH!!*) |
42 goal Set.thy "!!f. B <= range f = (B = f`` {x. f x: B})"; |
32 goal Set.thy "!!f. B <= range f = (B = f`` {x. f x: B})"; |
43 by (fast_tac (!claset addEs [equalityE]) 1); |
33 by (fast_tac (!claset addEs [equalityE]) 1); |
44 val subset_range_iff = result(); |
34 val subset_range_iff = result(); |
45 |
35 |
51 (*By default only o_apply is built-in. But in the presence of eta-expansion |
41 (*By default only o_apply is built-in. But in the presence of eta-expansion |
52 this means that some terms displayed as (f o g) will be rewritten, and others |
42 this means that some terms displayed as (f o g) will be rewritten, and others |
53 will not!*) |
43 will not!*) |
54 Addsimps [o_def]; |
44 Addsimps [o_def]; |
55 |
45 |
56 (*** Basic properties of serverKey and newK ***) |
46 (*** Basic properties of shrK and newK ***) |
57 |
47 |
58 (* invKey (serverKey A) = serverKey A *) |
48 (* invKey (shrK A) = shrK A *) |
59 bind_thm ("invKey_serverKey", rewrite_rule [isSymKey_def] isSym_serverKey); |
49 bind_thm ("invKey_shrK", rewrite_rule [isSymKey_def] isSym_shrK); |
60 |
50 |
61 (* invKey (newK evs) = newK evs *) |
51 (* invKey (newK evs) = newK evs *) |
62 bind_thm ("invKey_newK", rewrite_rule [isSymKey_def] isSym_newK); |
52 bind_thm ("invKey_newK", rewrite_rule [isSymKey_def] isSym_newK); |
63 Addsimps [invKey_serverKey, invKey_newK]; |
53 Addsimps [invKey_shrK, invKey_newK]; |
64 |
54 |
65 |
55 |
66 (*New keys and nonces are fresh*) |
56 (*New keys and nonces are fresh*) |
67 val serverKey_inject = inj_serverKey RS injD; |
57 val shrK_inject = inj_shrK RS injD; |
68 val newN_inject = inj_newN RS injD |
58 val newN_inject = inj_newN RS injD |
69 and newK_inject = inj_newK RS injD; |
59 and newK_inject = inj_newK RS injD; |
70 AddSEs [serverKey_inject, newN_inject, newK_inject, |
60 AddSEs [shrK_inject, newN_inject, newK_inject, |
71 fresh_newK RS notE, fresh_newN RS notE]; |
61 fresh_newK RS notE, fresh_newN RS notE]; |
72 Addsimps [inj_serverKey RS inj_eq, inj_newN RS inj_eq, inj_newK RS inj_eq]; |
62 Addsimps [inj_shrK RS inj_eq, inj_newN RS inj_eq, inj_newK RS inj_eq]; |
73 Addsimps [fresh_newN, fresh_newK]; |
63 Addsimps [fresh_newN, fresh_newK]; |
74 |
64 |
75 goal thy "newK evs ~= serverKey B"; |
65 goal thy "newK evs ~= shrK B"; |
76 by (subgoal_tac "newK evs = serverKey B --> \ |
66 by (subgoal_tac "newK evs = shrK B --> \ |
77 \ Key (newK evs) : parts (initState B)" 1); |
67 \ Key (newK evs) : parts (initState B)" 1); |
78 by (Fast_tac 1); |
68 by (Fast_tac 1); |
79 by (agent.induct_tac "B" 1); |
69 by (agent.induct_tac "B" 1); |
80 by (auto_tac (!claset addIs [range_eqI], !simpset)); |
70 by (auto_tac (!claset addIs [range_eqI], !simpset)); |
81 qed "newK_neq_serverKey"; |
71 qed "newK_neq_shrK"; |
82 |
72 |
83 Addsimps [newK_neq_serverKey, newK_neq_serverKey RS not_sym]; |
73 Addsimps [newK_neq_shrK, newK_neq_shrK RS not_sym]; |
84 |
74 |
85 (*Good for talking about Server's initial state*) |
75 (*Good for talking about Server's initial state*) |
86 goal thy "!!H. H <= Key``E ==> parts H = H"; |
76 goal thy "!!H. H <= Key``E ==> parts H = H"; |
87 by (Auto_tac ()); |
77 by (Auto_tac ()); |
88 be parts.induct 1; |
78 be parts.induct 1; |
110 goalw thy [keysFor_def] "keysFor (Key``E) = {}"; |
100 goalw thy [keysFor_def] "keysFor (Key``E) = {}"; |
111 by (Auto_tac ()); |
101 by (Auto_tac ()); |
112 qed "keysFor_image_Key"; |
102 qed "keysFor_image_Key"; |
113 Addsimps [keysFor_image_Key]; |
103 Addsimps [keysFor_image_Key]; |
114 |
104 |
115 goal thy "serverKey A ~: newK``E"; |
105 goal thy "shrK A ~: newK``E"; |
116 by (agent.induct_tac "A" 1); |
106 by (agent.induct_tac "A" 1); |
117 by (Auto_tac ()); |
107 by (Auto_tac ()); |
118 qed "serverKey_notin_image_newK"; |
108 qed "shrK_notin_image_newK"; |
119 Addsimps [serverKey_notin_image_newK]; |
109 Addsimps [shrK_notin_image_newK]; |
120 |
110 |
121 |
111 |
122 (*Agents see their own serverKeys!*) |
112 (*Agents see their own shrKs!*) |
123 goal thy "Key (serverKey A) : analz (sees A evs)"; |
113 goal thy "Key (shrK A) : analz (sees A evs)"; |
124 by (list.induct_tac "evs" 1); |
114 by (list.induct_tac "evs" 1); |
125 by (asm_simp_tac (!simpset addsimps [impOfSubs(Un_upper2 RS analz_mono)]) 2); |
115 by (asm_simp_tac (!simpset addsimps [impOfSubs(Un_upper2 RS analz_mono)]) 2); |
126 by (agent.induct_tac "A" 1); |
116 by (agent.induct_tac "A" 1); |
127 by (auto_tac (!claset addIs [range_eqI], !simpset)); |
117 by (auto_tac (!claset addIs [range_eqI], !simpset)); |
128 qed "analz_own_serverKey"; |
118 qed "analz_own_shrK"; |
129 |
119 |
130 bind_thm ("parts_own_serverKey", |
120 bind_thm ("parts_own_shrK", |
131 [analz_subset_parts, analz_own_serverKey] MRS subsetD); |
121 [analz_subset_parts, analz_own_shrK] MRS subsetD); |
132 |
122 |
133 Addsimps [analz_own_serverKey, parts_own_serverKey]; |
123 Addsimps [analz_own_shrK, parts_own_shrK]; |
134 |
124 |
135 |
125 |
136 |
126 |
137 (**** Inductive relation "traces" -- basic properties ****) |
127 (**** Inductive relation "traces" -- basic properties ****) |
138 |
128 |
200 qed_spec_mp "Says_imp_sees_Enemy"; |
190 qed_spec_mp "Says_imp_sees_Enemy"; |
201 |
191 |
202 Addsimps [Says_imp_sees_Enemy]; |
192 Addsimps [Says_imp_sees_Enemy]; |
203 AddIs [Says_imp_sees_Enemy]; |
193 AddIs [Says_imp_sees_Enemy]; |
204 |
194 |
205 goal thy "initState C <= Key `` range serverKey"; |
195 goal thy "initState C <= Key `` range shrK"; |
206 by (agent.induct_tac "C" 1); |
196 by (agent.induct_tac "C" 1); |
207 by (Auto_tac ()); |
197 by (Auto_tac ()); |
208 qed "initState_subset"; |
198 qed "initState_subset"; |
209 |
199 |
210 goal thy "X : sees C evs --> \ |
200 goal thy "X : sees C evs --> \ |
211 \ (EX A B. Says A B X : set_of_list evs) | \ |
201 \ (EX A B. Says A B X : set_of_list evs) | \ |
212 \ (EX A. Notes A X : set_of_list evs) | \ |
202 \ (EX A. Notes A X : set_of_list evs) | \ |
213 \ (EX A. X = Key (serverKey A))"; |
203 \ (EX A. X = Key (shrK A))"; |
214 by (list.induct_tac "evs" 1); |
204 by (list.induct_tac "evs" 1); |
215 by (ALLGOALS Asm_simp_tac); |
205 by (ALLGOALS Asm_simp_tac); |
216 by (fast_tac (!claset addDs [impOfSubs initState_subset]) 1); |
206 by (fast_tac (!claset addDs [impOfSubs initState_subset]) 1); |
217 br conjI 1; |
207 br conjI 1; |
218 by (Fast_tac 2); |
208 by (Fast_tac 2); |
264 (*** Server keys are not betrayed ***) |
254 (*** Server keys are not betrayed ***) |
265 |
255 |
266 (*Enemy never sees another agent's server key!*) |
256 (*Enemy never sees another agent's server key!*) |
267 goal thy |
257 goal thy |
268 "!!evs. [| evs : traces; A ~= Enemy |] ==> \ |
258 "!!evs. [| evs : traces; A ~= Enemy |] ==> \ |
269 \ Key (serverKey A) ~: parts (sees Enemy evs)"; |
259 \ Key (shrK A) ~: parts (sees Enemy evs)"; |
270 be traces.induct 1; |
260 be traces.induct 1; |
271 bd NS3_msg_in_parts_sees_Enemy 5; |
261 bd NS3_msg_in_parts_sees_Enemy 5; |
272 by (Auto_tac()); |
262 by (Auto_tac()); |
273 (*Deals with Fake message*) |
263 (*Deals with Fake message*) |
274 by (best_tac (!claset addDs [impOfSubs analz_subset_parts, |
264 by (best_tac (!claset addDs [impOfSubs analz_subset_parts, |
275 impOfSubs synth_analz_parts_insert_subset_Un]) 1); |
265 impOfSubs synth_analz_parts_insert_subset_Un]) 1); |
276 qed "Enemy_not_see_serverKey"; |
266 qed "Enemy_not_see_shrK"; |
277 |
267 |
278 bind_thm ("Enemy_not_analz_serverKey", |
268 bind_thm ("Enemy_not_analz_shrK", |
279 [analz_subset_parts, Enemy_not_see_serverKey] MRS contra_subsetD); |
269 [analz_subset_parts, Enemy_not_see_shrK] MRS contra_subsetD); |
280 |
270 |
281 Addsimps [Enemy_not_see_serverKey, |
271 Addsimps [Enemy_not_see_shrK, |
282 not_sym RSN (2, Enemy_not_see_serverKey), |
272 not_sym RSN (2, Enemy_not_see_shrK), |
283 Enemy_not_analz_serverKey, |
273 Enemy_not_analz_shrK, |
284 not_sym RSN (2, Enemy_not_analz_serverKey)]; |
274 not_sym RSN (2, Enemy_not_analz_shrK)]; |
285 |
275 |
286 (*We go to some trouble to preserve R in the 3rd subgoal*) |
276 (*We go to some trouble to preserve R in the 3rd subgoal*) |
287 val major::prems = |
277 val major::prems = |
288 goal thy "[| Key (serverKey A) : parts (sees Enemy evs); \ |
278 goal thy "[| Key (shrK A) : parts (sees Enemy evs); \ |
289 \ evs : traces; \ |
279 \ evs : traces; \ |
290 \ A=Enemy ==> R \ |
280 \ A=Enemy ==> R \ |
291 \ |] ==> R"; |
281 \ |] ==> R"; |
292 br ccontr 1; |
282 br ccontr 1; |
293 br ([major, Enemy_not_see_serverKey] MRS rev_notE) 1; |
283 br ([major, Enemy_not_see_shrK] MRS rev_notE) 1; |
294 by (swap_res_tac prems 2); |
284 by (swap_res_tac prems 2); |
295 by (ALLGOALS (fast_tac (!claset addIs prems))); |
285 by (ALLGOALS (fast_tac (!claset addIs prems))); |
296 qed "Enemy_see_serverKey_E"; |
286 qed "Enemy_see_shrK_E"; |
297 |
287 |
298 bind_thm ("Enemy_analz_serverKey_E", |
288 bind_thm ("Enemy_analz_shrK_E", |
299 analz_subset_parts RS subsetD RS Enemy_see_serverKey_E); |
289 analz_subset_parts RS subsetD RS Enemy_see_shrK_E); |
300 |
290 |
301 (*Classical reasoner doesn't need the not_sym versions (with swapped ~=) *) |
291 (*Classical reasoner doesn't need the not_sym versions (with swapped ~=) *) |
302 AddSEs [Enemy_see_serverKey_E, Enemy_analz_serverKey_E]; |
292 AddSEs [Enemy_see_shrK_E, Enemy_analz_shrK_E]; |
303 |
293 |
304 |
294 |
305 (*No Friend will ever see another agent's server key |
295 (*No Friend will ever see another agent's server key |
306 (excluding the Enemy, who might transmit his). |
296 (excluding the Enemy, who might transmit his). |
307 The Server, of course, knows all server keys.*) |
297 The Server, of course, knows all server keys.*) |
308 goal thy |
298 goal thy |
309 "!!evs. [| evs : traces; A ~= Enemy; A ~= Friend j |] ==> \ |
299 "!!evs. [| evs : traces; A ~= Enemy; A ~= Friend j |] ==> \ |
310 \ Key (serverKey A) ~: parts (sees (Friend j) evs)"; |
300 \ Key (shrK A) ~: parts (sees (Friend j) evs)"; |
311 br (sees_agent_subset_sees_Enemy RS parts_mono RS contra_subsetD) 1; |
301 br (sees_agent_subset_sees_Enemy RS parts_mono RS contra_subsetD) 1; |
312 by (ALLGOALS Asm_simp_tac); |
302 by (ALLGOALS Asm_simp_tac); |
313 qed "Friend_not_see_serverKey"; |
303 qed "Friend_not_see_shrK"; |
314 |
304 |
315 |
305 |
316 (*Not for Addsimps -- it can cause goals to blow up!*) |
306 (*Not for Addsimps -- it can cause goals to blow up!*) |
317 goal thy |
307 goal thy |
318 "!!evs. evs : traces ==> \ |
308 "!!evs. evs : traces ==> \ |
319 \ (Key (serverKey A) \ |
309 \ (Key (shrK A) \ |
320 \ : analz (insert (Key (serverKey B)) (sees Enemy evs))) = \ |
310 \ : analz (insert (Key (shrK B)) (sees Enemy evs))) = \ |
321 \ (A=B | A=Enemy)"; |
311 \ (A=B | A=Enemy)"; |
322 by (best_tac (!claset addDs [impOfSubs analz_subset_parts] |
312 by (best_tac (!claset addDs [impOfSubs analz_subset_parts] |
323 addIs [impOfSubs (subset_insertI RS analz_mono)] |
313 addIs [impOfSubs (subset_insertI RS analz_mono)] |
324 addss (!simpset)) 1); |
314 addss (!simpset)) 1); |
325 qed "serverKey_mem_analz"; |
315 qed "shrK_mem_analz"; |
326 |
316 |
327 |
317 |
328 |
318 |
329 |
319 |
330 (*** Future keys can't be seen or used! ***) |
320 (*** Future keys can't be seen or used! ***) |
427 ["Agent ?C", "Nonce ?N", "MPair ?X' ?Y"]; |
417 ["Agent ?C", "Nonce ?N", "MPair ?X' ?Y"]; |
428 |
418 |
429 (*Cannot be added with Addsimps -- we don't always want to re-order messages*) |
419 (*Cannot be added with Addsimps -- we don't always want to re-order messages*) |
430 val pushes = pushKeys@pushCrypts; |
420 val pushes = pushKeys@pushCrypts; |
431 |
421 |
432 val pushKey_newK = insComm "Key (newK ?evs)" "Key (serverKey ?C)"; |
422 val pushKey_newK = insComm "Key (newK ?evs)" "Key (shrK ?C)"; |
433 |
423 |
434 |
424 |
435 (** Lemmas concerning the form of items passed in messages **) |
425 (** Lemmas concerning the form of items passed in messages **) |
436 |
426 |
437 (*Describes the form *and age* of K, and the form of X, |
427 (*Describes the form *and age* of K, and the form of X, |
439 goal thy |
429 goal thy |
440 "!!evs. [| Says Server A (Crypt {|N, Agent B, K, X|} K') : set_of_list evs; \ |
430 "!!evs. [| Says Server A (Crypt {|N, Agent B, K, X|} K') : set_of_list evs; \ |
441 \ evs : traces \ |
431 \ evs : traces \ |
442 \ |] ==> (EX evt:traces. \ |
432 \ |] ==> (EX evt:traces. \ |
443 \ K = Key(newK evt) & \ |
433 \ K = Key(newK evt) & \ |
444 \ X = (Crypt {|K, Agent A|} (serverKey B)) & \ |
434 \ X = (Crypt {|K, Agent A|} (shrK B)) & \ |
445 \ K' = serverKey A & \ |
435 \ K' = shrK A & \ |
446 \ length evt < length evs)"; |
436 \ length evt < length evs)"; |
447 be rev_mp 1; |
437 be rev_mp 1; |
448 be traces.induct 1; |
438 be traces.induct 1; |
449 by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset)))); |
439 by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset)))); |
450 qed "Says_Server_message_form"; |
440 qed "Says_Server_message_form"; |
459 goal thy |
449 goal thy |
460 "!!evs. [| evs = Says Server (Friend i) \ |
450 "!!evs. [| evs = Says Server (Friend i) \ |
461 \ (Crypt {|N, Agent(Friend j), K, X|} K') # evs'; \ |
451 \ (Crypt {|N, Agent(Friend j), K, X|} K') # evs'; \ |
462 \ evs : traces; i~=k \ |
452 \ evs : traces; i~=k \ |
463 \ |] ==> \ |
453 \ |] ==> \ |
464 \ K ~: analz (insert (Key (serverKey (Friend k))) (sees Enemy evs))"; |
454 \ K ~: analz (insert (Key (shrK (Friend k))) (sees Enemy evs))"; |
465 be rev_mp 1; |
455 be rev_mp 1; |
466 be traces.induct 1; |
456 be traces.induct 1; |
467 by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes))); |
457 by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes))); |
468 by (Step_tac 1); |
458 by (Step_tac 1); |
469 by (asm_full_simp_tac (!simpset addsimps[analz_subset_parts RS contra_subsetD]) 1); |
459 by (asm_full_simp_tac (!simpset addsimps[analz_subset_parts RS contra_subsetD]) 1); |
473 |
463 |
474 (*Describes the form of X when the following message is sent*) |
464 (*Describes the form of X when the following message is sent*) |
475 goal thy |
465 goal thy |
476 "!!evs. evs : traces ==> \ |
466 "!!evs. evs : traces ==> \ |
477 \ ALL A NA B K X. \ |
467 \ ALL A NA B K X. \ |
478 \ (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \ |
468 \ (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) \ |
479 \ : parts (sees Enemy evs) & A ~= Enemy --> \ |
469 \ : parts (sees Enemy evs) & A ~= Enemy --> \ |
480 \ (EX evt:traces. K = newK evt & \ |
470 \ (EX evt:traces. K = newK evt & \ |
481 \ X = (Crypt {|Key K, Agent A|} (serverKey B)))"; |
471 \ X = (Crypt {|Key K, Agent A|} (shrK B)))"; |
482 be traces.induct 1; |
472 be traces.induct 1; |
483 bd NS3_msg_in_parts_sees_Enemy 5; |
473 bd NS3_msg_in_parts_sees_Enemy 5; |
484 by (Step_tac 1); |
474 by (Step_tac 1); |
485 by (ALLGOALS Asm_full_simp_tac); |
475 by (ALLGOALS Asm_full_simp_tac); |
486 (*Remaining cases are Fake and NS2*) |
476 (*Remaining cases are Fake and NS2*) |
494 |
484 |
495 (*For eliminating the A ~= Enemy condition from the previous result*) |
485 (*For eliminating the A ~= Enemy condition from the previous result*) |
496 goal thy |
486 goal thy |
497 "!!evs. evs : traces ==> \ |
487 "!!evs. evs : traces ==> \ |
498 \ ALL S A NA B K X. \ |
488 \ ALL S A NA B K X. \ |
499 \ Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \ |
489 \ Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) \ |
500 \ : set_of_list evs --> \ |
490 \ : set_of_list evs --> \ |
501 \ S = Server | S = Enemy"; |
491 \ S = Server | S = Enemy"; |
502 be traces.induct 1; |
492 be traces.induct 1; |
503 by (ALLGOALS Asm_simp_tac); |
493 by (ALLGOALS Asm_simp_tac); |
504 (*We are left with NS3*) |
494 (*We are left with NS3*) |
517 |
507 |
518 |
508 |
519 (*Describes the form of X when the following message is sent; |
509 (*Describes the form of X when the following message is sent; |
520 use Says_Server_message_form if applicable*) |
510 use Says_Server_message_form if applicable*) |
521 goal thy |
511 goal thy |
522 "!!evs. [| Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \ |
512 "!!evs. [| Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) \ |
523 \ : set_of_list evs; \ |
513 \ : set_of_list evs; \ |
524 \ evs : traces \ |
514 \ evs : traces \ |
525 \ |] ==> (EX evt:traces. K = newK evt & length evt < length evs & \ |
515 \ |] ==> (EX evt:traces. K = newK evt & length evt < length evs & \ |
526 \ X = (Crypt {|Key K, Agent A|} (serverKey B)))"; |
516 \ X = (Crypt {|Key K, Agent A|} (shrK B)))"; |
527 by (forward_tac [Server_or_Enemy] 1); |
517 by (forward_tac [Server_or_Enemy] 1); |
528 ba 1; |
518 ba 1; |
529 by (Step_tac 1); |
519 by (Step_tac 1); |
530 by (fast_tac (!claset addSDs [Says_Server_message_form] addss (!simpset)) 1); |
520 by (fast_tac (!claset addSDs [Says_Server_message_form] addss (!simpset)) 1); |
531 by (forward_tac [encrypted_form] 1); |
521 by (forward_tac [encrypted_form] 1); |
534 qed "Says_S_message_form"; |
524 qed "Says_S_message_form"; |
535 |
525 |
536 (*Currently unused. Needed only to reason about the VERY LAST message.*) |
526 (*Currently unused. Needed only to reason about the VERY LAST message.*) |
537 goal thy |
527 goal thy |
538 "!!evs. [| evs = Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} \ |
528 "!!evs. [| evs = Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} \ |
539 \ (serverKey A)) # evs'; \ |
529 \ (shrK A)) # evs'; \ |
540 \ evs : traces \ |
530 \ evs : traces \ |
541 \ |] ==> (EX evt:traces. evs' : traces & length evt < length evs & \ |
531 \ |] ==> (EX evt:traces. evs' : traces & length evt < length evs & \ |
542 \ K = newK evt & \ |
532 \ K = newK evt & \ |
543 \ X = (Crypt {|Key K, Agent A|} (serverKey B)))"; |
533 \ X = (Crypt {|Key K, Agent A|} (shrK B)))"; |
544 by (forward_tac [traces_eq_ConsE] 1); |
534 by (forward_tac [traces_eq_ConsE] 1); |
545 by (dtac (set_of_list_eqI1 RS Says_S_message_form) 2); |
535 by (dtac (set_of_list_eqI1 RS Says_S_message_form) 2); |
546 by (Auto_tac()); |
536 by (Auto_tac()); |
547 qed "Says_S_message_form_eq"; |
537 qed "Says_S_message_form_eq"; |
548 |
538 |
550 |
540 |
551 (**** |
541 (**** |
552 The following is to prove theorems of the form |
542 The following is to prove theorems of the form |
553 |
543 |
554 Key K : analz (insert (Key (newK evt)) |
544 Key K : analz (insert (Key (newK evt)) |
555 (insert (Key (serverKey C)) (sees Enemy evs))) ==> |
545 (insert (Key (shrK C)) (sees Enemy evs))) ==> |
556 Key K : analz (insert (Key (serverKey C)) (sees Enemy evs)) |
546 Key K : analz (insert (Key (shrK C)) (sees Enemy evs)) |
557 |
547 |
558 A more general formula must be proved inductively. |
548 A more general formula must be proved inductively. |
559 |
549 |
560 ****) |
550 ****) |
561 |
551 |
598 |
588 |
599 (** Session keys are not used to encrypt other session keys **) |
589 (** Session keys are not used to encrypt other session keys **) |
600 |
590 |
601 goal thy |
591 goal thy |
602 "!!evs. evs : traces ==> \ |
592 "!!evs. evs : traces ==> \ |
603 \ ALL K E. (Key K : analz (insert (Key (serverKey C)) \ |
593 \ ALL K E. (Key K : analz (insert (Key (shrK C)) \ |
604 \ (Key``(newK``E) Un (sees Enemy evs)))) = \ |
594 \ (Key``(newK``E) Un (sees Enemy evs)))) = \ |
605 \ (K : newK``E | \ |
595 \ (K : newK``E | \ |
606 \ Key K : analz (insert (Key (serverKey C)) \ |
596 \ Key K : analz (insert (Key (shrK C)) \ |
607 \ (sees Enemy evs)))"; |
597 \ (sees Enemy evs)))"; |
608 be traces.induct 1; |
598 be traces.induct 1; |
609 by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5); |
599 by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5); |
610 by (REPEAT ((eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac) 5)); |
600 by (REPEAT ((eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac) 5)); |
611 by (ALLGOALS |
601 by (ALLGOALS |
622 by (REPEAT (Safe_step_tac 1)); |
612 by (REPEAT (Safe_step_tac 1)); |
623 by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 2); |
613 by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 2); |
624 by (subgoal_tac |
614 by (subgoal_tac |
625 "Key K : analz \ |
615 "Key K : analz \ |
626 \ (synth \ |
616 \ (synth \ |
627 \ (analz (insert (Key (serverKey C)) \ |
617 \ (analz (insert (Key (shrK C)) \ |
628 \ (Key``(newK``E) Un (sees Enemy evsa)))))" 1); |
618 \ (Key``(newK``E) Un (sees Enemy evsa)))))" 1); |
629 (*First, justify this subgoal*) |
619 (*First, justify this subgoal*) |
630 (*Discard formulae for better speed*) |
620 (*Discard formulae for better speed*) |
631 by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2); |
621 by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2); |
632 by (eres_inst_tac [("V","?Q ~: ?QQ")] thin_rl 2); |
622 by (eres_inst_tac [("V","?Q ~: ?QQ")] thin_rl 2); |
638 |
628 |
639 |
629 |
640 goal thy |
630 goal thy |
641 "!!evs. evs : traces ==> \ |
631 "!!evs. evs : traces ==> \ |
642 \ Key K : analz (insert (Key (newK evt)) \ |
632 \ Key K : analz (insert (Key (newK evt)) \ |
643 \ (insert (Key (serverKey C)) \ |
633 \ (insert (Key (shrK C)) \ |
644 \ (sees Enemy evs))) = \ |
634 \ (sees Enemy evs))) = \ |
645 \ (K = newK evt | \ |
635 \ (K = newK evt | \ |
646 \ Key K : analz (insert (Key (serverKey C)) \ |
636 \ Key K : analz (insert (Key (shrK C)) \ |
647 \ (sees Enemy evs)))"; |
637 \ (sees Enemy evs)))"; |
648 by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, |
638 by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, |
649 insert_Key_singleton]) 1); |
639 insert_Key_singleton]) 1); |
650 by (Fast_tac 1); |
640 by (Fast_tac 1); |
651 qed "analz_insert_Key_newK"; |
641 qed "analz_insert_Key_newK"; |
657 goal thy |
647 goal thy |
658 "!!evs. evs : traces ==> \ |
648 "!!evs. evs : traces ==> \ |
659 \ EX X'. ALL C S A Y N B X. \ |
649 \ EX X'. ALL C S A Y N B X. \ |
660 \ C ~= Enemy --> \ |
650 \ C ~= Enemy --> \ |
661 \ Says S A Y : set_of_list evs --> \ |
651 \ Says S A Y : set_of_list evs --> \ |
662 \ ((Crypt {|N, Agent B, Key K, X|} (serverKey C)) : parts{Y} --> \ |
652 \ ((Crypt {|N, Agent B, Key K, X|} (shrK C)) : parts{Y} --> \ |
663 \ (X = X'))"; |
653 \ (X = X'))"; |
664 be traces.induct 1; |
654 be traces.induct 1; |
665 by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5); |
655 by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5); |
666 by (ALLGOALS |
656 by (ALLGOALS |
667 (asm_simp_tac (!simpset addsimps [all_conj_distrib, imp_conj_distrib]))); |
657 (asm_simp_tac (!simpset addsimps [all_conj_distrib, imp_conj_distrib]))); |
680 br exI 1; |
670 br exI 1; |
681 br conjI 1; |
671 br conjI 1; |
682 ba 2; |
672 ba 2; |
683 by (Step_tac 1); |
673 by (Step_tac 1); |
684 (** LEVEL 12 **) |
674 (** LEVEL 12 **) |
685 by (subgoal_tac "Crypt {|N, Agent Ba, Key K, Xa|} (serverKey C) \ |
675 by (subgoal_tac "Crypt {|N, Agent Ba, Key K, Xa|} (shrK C) \ |
686 \ : parts (sees Enemy evsa)" 1); |
676 \ : parts (sees Enemy evsa)" 1); |
687 by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2); |
677 by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2); |
688 by (best_tac (!claset addSEs [impOfSubs analz_subset_parts] |
678 by (best_tac (!claset addSEs [impOfSubs analz_subset_parts] |
689 addDs [impOfSubs parts_insert_subset_Un] |
679 addDs [impOfSubs parts_insert_subset_Un] |
690 addss (!simpset)) 2); |
680 addss (!simpset)) 2); |
699 |
689 |
700 |
690 |
701 (*In messages of this form, the session key uniquely identifies the rest*) |
691 (*In messages of this form, the session key uniquely identifies the rest*) |
702 goal thy |
692 goal thy |
703 "!!evs. [| Says S A \ |
693 "!!evs. [| Says S A \ |
704 \ (Crypt {|N, Agent B, Key K, X|} (serverKey C)) \ |
694 \ (Crypt {|N, Agent B, Key K, X|} (shrK C)) \ |
705 \ : set_of_list evs; \ |
695 \ : set_of_list evs; \ |
706 \ Says S' A' \ |
696 \ Says S' A' \ |
707 \ (Crypt {|N', Agent B', Key K, X'|} (serverKey C')) \ |
697 \ (Crypt {|N', Agent B', Key K, X'|} (shrK C')) \ |
708 \ : set_of_list evs; \ |
698 \ : set_of_list evs; \ |
709 \ evs : traces; C ~= Enemy; C' ~= Enemy |] ==> X = X'"; |
699 \ evs : traces; C ~= Enemy; C' ~= Enemy |] ==> X = X'"; |
710 bd lemma 1; |
700 bd lemma 1; |
711 be exE 1; |
701 be exE 1; |
712 by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1); |
702 by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1); |
720 goal thy |
710 goal thy |
721 "!!evs. [| Says Server (Friend i) \ |
711 "!!evs. [| Says Server (Friend i) \ |
722 \ (Crypt {|N, Agent(Friend j), K, X|} K') : set_of_list evs; \ |
712 \ (Crypt {|N, Agent(Friend j), K, X|} K') : set_of_list evs; \ |
723 \ evs : traces; Friend i ~= C; Friend j ~= C \ |
713 \ evs : traces; Friend i ~= C; Friend j ~= C \ |
724 \ |] ==> \ |
714 \ |] ==> \ |
725 \ K ~: analz (insert (Key (serverKey C)) (sees Enemy evs))"; |
715 \ K ~: analz (insert (Key (shrK C)) (sees Enemy evs))"; |
726 be rev_mp 1; |
716 be rev_mp 1; |
727 be traces.induct 1; |
717 be traces.induct 1; |
728 by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes))); |
718 by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes))); |
729 (*Next 3 steps infer that K has the form "Key (newK evs'" ... *) |
719 (*Next 3 steps infer that K has the form "Key (newK evs'" ... *) |
730 by (REPEAT_FIRST (resolve_tac [conjI, impI])); |
720 by (REPEAT_FIRST (resolve_tac [conjI, impI])); |
740 (** LEVEL 8 **) |
730 (** LEVEL 8 **) |
741 (*Now for the Fake case*) |
731 (*Now for the Fake case*) |
742 br notI 1; |
732 br notI 1; |
743 by (subgoal_tac |
733 by (subgoal_tac |
744 "Key (newK evt) : \ |
734 "Key (newK evt) : \ |
745 \ analz (synth (analz (insert (Key (serverKey C)) \ |
735 \ analz (synth (analz (insert (Key (shrK C)) \ |
746 \ (sees Enemy evsa))))" 1); |
736 \ (sees Enemy evsa))))" 1); |
747 be (impOfSubs analz_mono) 2; |
737 be (impOfSubs analz_mono) 2; |
748 by (deepen_tac (!claset addIs [analz_mono RS synth_mono RSN (2,rev_subsetD), |
738 by (deepen_tac (!claset addIs [analz_mono RS synth_mono RSN (2,rev_subsetD), |
749 impOfSubs synth_increasing, |
739 impOfSubs synth_increasing, |
750 impOfSubs analz_increasing]) 0 2); |
740 impOfSubs analz_increasing]) 0 2); |
762 (**LEVEL 18 **) |
752 (**LEVEL 18 **) |
763 bd unique_session_keys 1; |
753 bd unique_session_keys 1; |
764 by (REPEAT_FIRST assume_tac); |
754 by (REPEAT_FIRST assume_tac); |
765 by (ALLGOALS Full_simp_tac); |
755 by (ALLGOALS Full_simp_tac); |
766 by (Step_tac 1); |
756 by (Step_tac 1); |
767 by (asm_full_simp_tac (!simpset addsimps [serverKey_mem_analz]) 1); |
757 by (asm_full_simp_tac (!simpset addsimps [shrK_mem_analz]) 1); |
768 qed "Enemy_not_see_encrypted_key"; |
758 qed "Enemy_not_see_encrypted_key"; |
769 |
759 |
770 |
760 |
771 |
761 |
772 |
762 |
825 goal thy |
815 goal thy |
826 "!!evs. [| evs = Says S (Friend i) \ |
816 "!!evs. [| evs = Says S (Friend i) \ |
827 \ (Crypt {|N, Agent(Friend j), K, X|} K') # evs'; \ |
817 \ (Crypt {|N, Agent(Friend j), K, X|} K') # evs'; \ |
828 \ evs : traces; i~=k \ |
818 \ evs : traces; i~=k \ |
829 \ |] ==> \ |
819 \ |] ==> \ |
830 \ K ~: analz (insert (Key (serverKey (Friend k))) (sees Enemy evs))"; |
820 \ K ~: analz (insert (Key (shrK (Friend k))) (sees Enemy evs))"; |
831 be rev_mp 1; |
821 be rev_mp 1; |
832 be traces.induct 1; |
822 be traces.induct 1; |
833 by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes))); |
823 by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes))); |
834 by (Step_tac 1); |
824 by (Step_tac 1); |
835 by (asm_full_simp_tac (!simpset addsimps[analz_subset_parts RS contra_subsetD]) 1); |
825 by (asm_full_simp_tac (!simpset addsimps[analz_subset_parts RS contra_subsetD]) 1); |
844 (*Precisely formulated as needed below. Perhaps redundant, as simplification |
834 (*Precisely formulated as needed below. Perhaps redundant, as simplification |
845 with the aid of analz_subset_parts RS contra_subsetD might do the |
835 with the aid of analz_subset_parts RS contra_subsetD might do the |
846 same thing.*) |
836 same thing.*) |
847 goal thy |
837 goal thy |
848 "!!evs. [| evs : traces; A ~= Enemy; A ~= Friend j |] ==> \ |
838 "!!evs. [| evs : traces; A ~= Enemy; A ~= Friend j |] ==> \ |
849 \ Key (serverKey A) ~: \ |
839 \ Key (shrK A) ~: \ |
850 \ analz (insert (Key (serverKey (Friend j))) (sees Enemy evs))"; |
840 \ analz (insert (Key (shrK (Friend j))) (sees Enemy evs))"; |
851 br (analz_subset_parts RS contra_subsetD) 1; |
841 br (analz_subset_parts RS contra_subsetD) 1; |
852 by (Asm_simp_tac 1); |
842 by (Asm_simp_tac 1); |
853 qed "insert_not_analz_serverKey"; |
843 qed "insert_not_analz_shrK"; |
854 |
844 |
855 |
845 |
856 |
846 |
857 |
847 |
858 XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX; |
848 XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX; |
866 |
856 |
867 (*If a message is sent, encrypted with a Friend's server key, then either |
857 (*If a message is sent, encrypted with a Friend's server key, then either |
868 that Friend or the Server originally sent it.*) |
858 that Friend or the Server originally sent it.*) |
869 goal thy |
859 goal thy |
870 "!!evs. evs : traces ==> \ |
860 "!!evs. evs : traces ==> \ |
871 \ ALL A B X i. Says A B (Crypt X (serverKey (Friend i))) \ |
861 \ ALL A B X i. Says A B (Crypt X (shrK (Friend i))) \ |
872 \ : set_of_list evs --> \ |
862 \ : set_of_list evs --> \ |
873 \ (EX B'. Says Server B' (Crypt X (serverKey (Friend i))) : set_of_list evs | \ |
863 \ (EX B'. Says Server B' (Crypt X (shrK (Friend i))) : set_of_list evs | \ |
874 \ Says (Friend i) B' (Crypt X (serverKey (Friend i))) : set_of_list evs)"; |
864 \ Says (Friend i) B' (Crypt X (shrK (Friend i))) : set_of_list evs)"; |
875 be traces.induct 1; |
865 be traces.induct 1; |
876 by (Step_tac 1); |
866 by (Step_tac 1); |
877 by (ALLGOALS Asm_full_simp_tac); |
867 by (ALLGOALS Asm_full_simp_tac); |
878 (*Remaining cases are Fake, NS2 and NS3*) |
868 (*Remaining cases are Fake, NS2 and NS3*) |
879 by (Fast_tac 2); (*Proves the NS2 case*) |
869 by (Fast_tac 2); (*Proves the NS2 case*) |
892 be conjE 2; |
882 be conjE 2; |
893 by ((dtac spec THEN' dtac spec THEN' dtac spec THEN' dtac spec)2); |
883 by ((dtac spec THEN' dtac spec THEN' dtac spec THEN' dtac spec)2); |
894 |
884 |
895 (*The NS3 case needs the induction hypothesis twice! |
885 (*The NS3 case needs the induction hypothesis twice! |
896 One application is to the X component of the most recent message.*) |
886 One application is to the X component of the most recent message.*) |
897 by (subgoal_tac "? evs'. X = Crypt {|Key (newK evs'), Agent A|} (serverKey B)" 2); |
887 by (subgoal_tac "? evs'. X = Crypt {|Key (newK evs'), Agent A|} (shrK B)" 2); |
898 by (Fast_tac 3); |
888 by (Fast_tac 3); |
899 by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2); |
889 by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2); |
900 be conjE 2; |
890 be conjE 2; |
901 (*DELETE the first quantified formula: it's now useless*) |
891 (*DELETE the first quantified formula: it's now useless*) |
902 by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2); |
892 by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2); |