53 |
53 |
54 (*Relates to both YM4 and Oops*) |
54 (*Relates to both YM4 and Oops*) |
55 goal thy "!!evs. Says S A {|Crypt (shrK A) {|B,K,NA,NB|}, X|} : set evs ==> \ |
55 goal thy "!!evs. Says S A {|Crypt (shrK A) {|B,K,NA,NB|}, X|} : set evs ==> \ |
56 \ K : parts (spies evs)"; |
56 \ K : parts (spies evs)"; |
57 by (blast_tac (claset() addSEs partsEs |
57 by (blast_tac (claset() addSEs partsEs |
58 addSDs [Says_imp_spies RS parts.Inj]) 1); |
58 addSDs [Says_imp_spies RS parts.Inj]) 1); |
59 qed "YM4_Key_parts_spies"; |
59 qed "YM4_Key_parts_spies"; |
60 |
60 |
61 (*For proving the easier theorems about X ~: parts (spies evs).*) |
61 (*For proving the easier theorems about X ~: parts (spies evs).*) |
62 fun parts_spies_tac i = |
62 fun parts_spies_tac i = |
63 forward_tac [YM4_Key_parts_spies] (i+6) THEN |
63 forward_tac [YM4_Key_parts_spies] (i+6) THEN |
106 \ Key K ~: used evs --> K ~: keysFor (parts (spies evs))"; |
106 \ Key K ~: used evs --> K ~: keysFor (parts (spies evs))"; |
107 by (parts_induct_tac 1); |
107 by (parts_induct_tac 1); |
108 (*Fake*) |
108 (*Fake*) |
109 by (best_tac |
109 by (best_tac |
110 (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)] |
110 (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)] |
111 addIs [impOfSubs analz_subset_parts] |
111 addIs [impOfSubs analz_subset_parts] |
112 addDs [impOfSubs (analz_subset_parts RS keysFor_mono)] |
112 addDs [impOfSubs (analz_subset_parts RS keysFor_mono)] |
113 addss (simpset())) 1); |
113 addss (simpset())) 1); |
114 (*YM2-4: Because Key K is not fresh, etc.*) |
114 (*YM2-4: Because Key K is not fresh, etc.*) |
115 by (REPEAT (blast_tac (claset() addSEs spies_partsEs) 1)); |
115 by (REPEAT (blast_tac (claset() addSEs spies_partsEs) 1)); |
116 qed_spec_mp "new_keys_not_used"; |
116 qed_spec_mp "new_keys_not_used"; |
117 |
117 |
118 bind_thm ("new_keys_not_analzd", |
118 bind_thm ("new_keys_not_analzd", |
194 (*Remaining case: YM3*) |
194 (*Remaining case: YM3*) |
195 by (expand_case_tac "K = ?y" 1); |
195 by (expand_case_tac "K = ?y" 1); |
196 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2)); |
196 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2)); |
197 (*...we assume X is a recent message and handle this case by contradiction*) |
197 (*...we assume X is a recent message and handle this case by contradiction*) |
198 by (blast_tac (claset() addSEs spies_partsEs |
198 by (blast_tac (claset() addSEs spies_partsEs |
199 delrules [conjI] (*no split-up to 4 subgoals*)) 1); |
199 delrules [conjI] (*no split-up to 4 subgoals*)) 1); |
200 val lemma = result(); |
200 val lemma = result(); |
201 |
201 |
202 goal thy |
202 goal thy |
203 "!!evs. [| Says Server A \ |
203 "!!evs. [| Says Server A \ |
204 \ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} : set evs; \ |
204 \ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} : set evs; \ |
223 by (etac yahalom.induct 1); |
223 by (etac yahalom.induct 1); |
224 by analz_spies_tac; |
224 by analz_spies_tac; |
225 by (ALLGOALS |
225 by (ALLGOALS |
226 (asm_simp_tac |
226 (asm_simp_tac |
227 (simpset() addsimps (expand_ifs@pushes) |
227 (simpset() addsimps (expand_ifs@pushes) |
228 addsimps [analz_insert_eq, analz_insert_freshK]))); |
228 addsimps [analz_insert_eq, analz_insert_freshK]))); |
229 (*Oops*) |
229 (*Oops*) |
230 by (blast_tac (claset() addDs [unique_session_keys]) 3); |
230 by (blast_tac (claset() addDs [unique_session_keys]) 3); |
231 (*YM3*) |
231 (*YM3*) |
232 by (blast_tac (claset() delrules [impCE] |
232 by (blast_tac (claset() delrules [impCE] |
233 addSEs spies_partsEs |
233 addSEs spies_partsEs |
234 addIs [impOfSubs analz_subset_parts]) 2); |
234 addIs [impOfSubs analz_subset_parts]) 2); |
235 (*Fake*) |
235 (*Fake*) |
236 by (spy_analz_tac 1); |
236 by (spy_analz_tac 1); |
237 val lemma = result() RS mp RS mp RSN(2,rev_notE); |
237 val lemma = result() RS mp RS mp RSN(2,rev_notE); |
238 |
238 |
239 |
239 |
306 (*YM4*) |
306 (*YM4*) |
307 (*A is uncompromised because NB is secure*) |
307 (*A is uncompromised because NB is secure*) |
308 by (not_bad_tac "A" 1); |
308 by (not_bad_tac "A" 1); |
309 (*A's certificate guarantees the existence of the Server message*) |
309 (*A's certificate guarantees the existence of the Server message*) |
310 by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS parts.Fst RS |
310 by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS parts.Fst RS |
311 A_trusts_YM3]) 1); |
311 A_trusts_YM3]) 1); |
312 bind_thm ("B_trusts_YM4_newK", result() RS mp RSN (2, rev_mp)); |
312 bind_thm ("B_trusts_YM4_newK", result() RS mp RSN (2, rev_mp)); |
313 |
313 |
314 |
314 |
315 (**** Towards proving secrecy of Nonce NB ****) |
315 (**** Towards proving secrecy of Nonce NB ****) |
316 |
316 |
449 \ : set evs; \ |
449 \ : set evs; \ |
450 \ nb ~: analz (spies evs); evs : yahalom |] \ |
450 \ nb ~: analz (spies evs); evs : yahalom |] \ |
451 \ ==> NA' = NA & A' = A & B' = B"; |
451 \ ==> NA' = NA & A' = A & B' = B"; |
452 by (not_bad_tac "B'" 1); |
452 by (not_bad_tac "B'" 1); |
453 by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj] |
453 by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj] |
454 addSEs [MPair_parts] |
454 addSEs [MPair_parts] |
455 addDs [unique_NB]) 1); |
455 addDs [unique_NB]) 1); |
456 qed "Says_unique_NB"; |
456 qed "Says_unique_NB"; |
457 |
457 |
458 |
458 |
459 (** A nonce value is never used both as NA and as NB **) |
459 (** A nonce value is never used both as NA and as NB **) |
460 |
460 |
464 \ Crypt (shrK B') {|Agent A', Nonce NB, nb'|} : parts(spies evs) --> \ |
464 \ Crypt (shrK B') {|Agent A', Nonce NB, nb'|} : parts(spies evs) --> \ |
465 \ Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|} ~: parts(spies evs)"; |
465 \ Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|} ~: parts(spies evs)"; |
466 by (parts_induct_tac 1); |
466 by (parts_induct_tac 1); |
467 by (Fake_parts_insert_tac 1); |
467 by (Fake_parts_insert_tac 1); |
468 by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj] |
468 by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj] |
469 addSIs [parts_insertI] |
469 addSIs [parts_insertI] |
470 addSEs partsEs) 1); |
470 addSEs partsEs) 1); |
471 bind_thm ("no_nonce_YM1_YM2", result() RS mp RSN (2,rev_mp) RSN (2,rev_notE)); |
471 bind_thm ("no_nonce_YM1_YM2", result() RS mp RSN (2,rev_mp) RSN (2,rev_notE)); |
472 |
472 |
473 (*The Server sends YM3 only in response to YM2.*) |
473 (*The Server sends YM3 only in response to YM2.*) |
474 goal thy |
474 goal thy |
475 "!!evs. [| Says Server A \ |
475 "!!evs. [| Says Server A \ |
496 by (etac yahalom.induct 1); |
496 by (etac yahalom.induct 1); |
497 by analz_spies_tac; |
497 by analz_spies_tac; |
498 by (ALLGOALS |
498 by (ALLGOALS |
499 (asm_simp_tac |
499 (asm_simp_tac |
500 (simpset() addsimps (expand_ifs@pushes) |
500 (simpset() addsimps (expand_ifs@pushes) |
501 addsimps [analz_insert_eq, analz_insert_freshK]))); |
501 addsimps [analz_insert_eq, analz_insert_freshK]))); |
502 (*Prove YM3 by showing that no NB can also be an NA*) |
502 (*Prove YM3 by showing that no NB can also be an NA*) |
503 by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj] |
503 by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj] |
504 addSEs [MPair_parts] |
504 addSEs [MPair_parts] |
505 addDs [no_nonce_YM1_YM2, Says_unique_NB]) 4 |
505 addDs [no_nonce_YM1_YM2, Says_unique_NB]) 4 |
506 THEN flexflex_tac); |
506 THEN flexflex_tac); |
507 (*YM2: similar freshness reasoning*) |
507 (*YM2: similar freshness reasoning*) |
508 by (blast_tac (claset() addSEs partsEs |
508 by (blast_tac (claset() addSEs partsEs |
509 addDs [Says_imp_spies RS analz.Inj, |
509 addDs [Says_imp_spies RS analz.Inj, |
510 impOfSubs analz_subset_parts]) 3); |
510 impOfSubs analz_subset_parts]) 3); |
511 (*YM1: NB=NA is impossible anyway, but NA is secret because it is fresh!*) |
511 (*YM1: NB=NA is impossible anyway, but NA is secret because it is fresh!*) |
512 by (blast_tac (claset() addSIs [parts_insertI] |
512 by (blast_tac (claset() addSIs [parts_insertI] |
513 addSEs spies_partsEs) 2); |
513 addSEs spies_partsEs) 2); |
514 (*Fake*) |
514 (*Fake*) |
515 by (spy_analz_tac 1); |
515 by (spy_analz_tac 1); |
516 (** LEVEL 7: YM4 and Oops remain **) |
516 (** LEVEL 7: YM4 and Oops remain **) |
517 by (ALLGOALS Clarify_tac); |
517 by (ALLGOALS Clarify_tac); |
518 (*YM4: key K is visible to Spy, contradicting session key secrecy theorem*) |
518 (*YM4: key K is visible to Spy, contradicting session key secrecy theorem*) |
521 by (forward_tac [Says_Server_message_form] 3); |
521 by (forward_tac [Says_Server_message_form] 3); |
522 by (forward_tac [Says_Server_imp_YM2] 4); |
522 by (forward_tac [Says_Server_imp_YM2] 4); |
523 by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, exE, disjE])); |
523 by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, exE, disjE])); |
524 (* use Says_unique_NB to identify message components: Aa=A, Ba=B, NAa=NA *) |
524 (* use Says_unique_NB to identify message components: Aa=A, Ba=B, NAa=NA *) |
525 by (blast_tac (claset() addDs [Says_unique_NB, Spy_not_see_encrypted_key, |
525 by (blast_tac (claset() addDs [Says_unique_NB, Spy_not_see_encrypted_key, |
526 impOfSubs Fake_analz_insert]) 1); |
526 impOfSubs Fake_analz_insert]) 1); |
527 (** LEVEL 14 **) |
527 (** LEVEL 14 **) |
528 (*Oops case: if the nonce is betrayed now, show that the Oops event is |
528 (*Oops case: if the nonce is betrayed now, show that the Oops event is |
529 covered by the quantified Oops assumption.*) |
529 covered by the quantified Oops assumption.*) |
530 by (full_simp_tac (simpset() addsimps [all_conj_distrib]) 1); |
530 by (full_simp_tac (simpset() addsimps [all_conj_distrib]) 1); |
531 by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1 THEN etac exE 1); |
531 by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1 THEN etac exE 1); |
533 (*If NB=NBa then all other components of the Oops message agree*) |
533 (*If NB=NBa then all other components of the Oops message agree*) |
534 by (blast_tac (claset() addDs [Says_unique_NB]) 1 THEN flexflex_tac); |
534 by (blast_tac (claset() addDs [Says_unique_NB]) 1 THEN flexflex_tac); |
535 (*case NB ~= NBa*) |
535 (*case NB ~= NBa*) |
536 by (asm_simp_tac (simpset() addsimps [single_Nonce_secrecy]) 1); |
536 by (asm_simp_tac (simpset() addsimps [single_Nonce_secrecy]) 1); |
537 by (blast_tac (claset() addSEs [MPair_parts] |
537 by (blast_tac (claset() addSEs [MPair_parts] |
538 addDs [Says_imp_spies RS parts.Inj, |
538 addDs [Says_imp_spies RS parts.Inj, |
539 no_nonce_YM1_YM2 (*to prove NB~=NAa*) ]) 1); |
539 no_nonce_YM1_YM2 (*to prove NB~=NAa*) ]) 1); |
540 bind_thm ("Spy_not_see_NB", result() RSN(2,rev_mp) RSN(2,rev_mp)); |
540 bind_thm ("Spy_not_see_NB", result() RSN(2,rev_mp) RSN(2,rev_mp)); |
541 |
541 |
542 |
542 |
543 (*B's session key guarantee from YM4. The two certificates contribute to a |
543 (*B's session key guarantee from YM4. The two certificates contribute to a |
544 single conclusion about the Server's message. Note that the "Says A Spy" |
544 single conclusion about the Server's message. Note that the "Says A Spy" |
595 by (ALLGOALS Asm_simp_tac); |
595 by (ALLGOALS Asm_simp_tac); |
596 (*YM4*) |
596 (*YM4*) |
597 by (Blast_tac 2); |
597 by (Blast_tac 2); |
598 (*YM3*) |
598 (*YM3*) |
599 by (best_tac (claset() addSDs [B_Said_YM2, Says_imp_spies RS parts.Inj] |
599 by (best_tac (claset() addSDs [B_Said_YM2, Says_imp_spies RS parts.Inj] |
600 addSEs [MPair_parts]) 1); |
600 addSEs [MPair_parts]) 1); |
601 val lemma = result() RSN (2, rev_mp) RS mp |> standard; |
601 val lemma = result() RSN (2, rev_mp) RS mp |> standard; |
602 |
602 |
603 (*If A receives YM3 then B has used nonce NA (and therefore is alive)*) |
603 (*If A receives YM3 then B has used nonce NA (and therefore is alive)*) |
604 goal thy |
604 goal thy |
605 "!!evs. [| Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \ |
605 "!!evs. [| Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \ |
606 \ : set evs; \ |
606 \ : set evs; \ |
607 \ A ~: bad; B ~: bad; evs : yahalom |] \ |
607 \ A ~: bad; B ~: bad; evs : yahalom |] \ |
608 \ ==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \ |
608 \ ==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \ |
609 \ : set evs"; |
609 \ : set evs"; |
610 by (blast_tac (claset() addSDs [A_trusts_YM3, lemma] |
610 by (blast_tac (claset() addSDs [A_trusts_YM3, lemma] |
611 addEs spies_partsEs) 1); |
611 addEs spies_partsEs) 1); |
612 qed "YM3_auth_B_to_A"; |
612 qed "YM3_auth_B_to_A"; |
613 |
613 |
614 |
614 |
615 (*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***) |
615 (*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***) |
616 |
616 |
626 \ (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs)"; |
626 \ (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs)"; |
627 by (parts_induct_tac 1); |
627 by (parts_induct_tac 1); |
628 (*Fake*) |
628 (*Fake*) |
629 by (Fake_parts_insert_tac 1); |
629 by (Fake_parts_insert_tac 1); |
630 (*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*) |
630 (*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*) |
631 by (fast_tac (claset() addSDs [Crypt_imp_invKey_keysFor] addss (simpset())) 1); |
631 by (fast_tac (claset() addSDs [Crypt_imp_keysFor] addss (simpset())) 1); |
632 (*YM4: was Crypt K (Nonce NB) the very last message? If not, use ind. hyp.*) |
632 (*YM4: was Crypt K (Nonce NB) the very last message? If not, use ind. hyp.*) |
633 by (asm_simp_tac (simpset() addsimps [ex_disj_distrib]) 1); |
633 by (asm_simp_tac (simpset() addsimps [ex_disj_distrib]) 1); |
634 (*yes: apply unicity of session keys*) |
634 (*yes: apply unicity of session keys*) |
635 by (not_bad_tac "Aa" 1); |
635 by (not_bad_tac "Aa" 1); |
636 by (blast_tac (claset() addSEs [MPair_parts] |
636 by (blast_tac (claset() addSEs [MPair_parts] |
637 addSDs [A_trusts_YM3, B_trusts_YM4_shrK] |
637 addSDs [A_trusts_YM3, B_trusts_YM4_shrK] |
638 addDs [Says_imp_spies RS parts.Inj, |
638 addDs [Says_imp_spies RS parts.Inj, |
639 unique_session_keys]) 1); |
639 unique_session_keys]) 1); |
640 val lemma = normalize_thm [RSspec, RSmp] (result()) |> standard; |
640 val lemma = normalize_thm [RSspec, RSmp] (result()) |> standard; |
641 |
641 |
642 (*If B receives YM4 then A has used nonce NB (and therefore is alive). |
642 (*If B receives YM4 then A has used nonce NB (and therefore is alive). |
643 Moreover, A associates K with NB (thus is talking about the same run). |
643 Moreover, A associates K with NB (thus is talking about the same run). |
644 Other premises guarantee secrecy of K.*) |
644 Other premises guarantee secrecy of K.*) |
656 by (etac (Says_imp_spies RS parts.Inj RS MPair_parts) 1); |
656 by (etac (Says_imp_spies RS parts.Inj RS MPair_parts) 1); |
657 by (rtac lemma 1); |
657 by (rtac lemma 1); |
658 by (rtac Spy_not_see_encrypted_key 2); |
658 by (rtac Spy_not_see_encrypted_key 2); |
659 by (REPEAT_FIRST assume_tac); |
659 by (REPEAT_FIRST assume_tac); |
660 by (blast_tac (claset() addSEs [MPair_parts] |
660 by (blast_tac (claset() addSEs [MPair_parts] |
661 addDs [Says_imp_spies RS parts.Inj]) 1); |
661 addDs [Says_imp_spies RS parts.Inj]) 1); |
662 qed_spec_mp "YM4_imp_A_Said_YM3"; |
662 qed_spec_mp "YM4_imp_A_Said_YM3"; |