356 (*A is uncompromised because NB is secure*) |
356 (*A is uncompromised because NB is secure*) |
357 by (not_lost_tac "A" 1); |
357 by (not_lost_tac "A" 1); |
358 (*A's certificate guarantees the existence of the Server message*) |
358 (*A's certificate guarantees the existence of the Server message*) |
359 by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj RS parts.Fst RS |
359 by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj RS parts.Fst RS |
360 A_trusts_YM3]) 1); |
360 A_trusts_YM3]) 1); |
361 val B_trusts_YM4_newK = result() RS mp RSN (2, rev_mp); |
361 bind_thm ("B_trusts_YM4_newK", result() RS mp RSN (2, rev_mp)); |
362 |
362 |
363 |
363 |
364 (**** Towards proving secrecy of Nonce NB ****) |
364 (**** Towards proving secrecy of Nonce NB ****) |
365 |
365 |
366 (** Lemmas about the predicate KeyWithNonce **) |
366 (** Lemmas about the predicate KeyWithNonce **) |
380 by (Simp_tac 1); |
380 by (Simp_tac 1); |
381 by (Blast_tac 1); |
381 by (Blast_tac 1); |
382 qed "KeyWithNonce_Says"; |
382 qed "KeyWithNonce_Says"; |
383 Addsimps [KeyWithNonce_Says]; |
383 Addsimps [KeyWithNonce_Says]; |
384 |
384 |
|
385 (*A fresh key cannot be associated with any nonce |
|
386 (with respect to a given trace). *) |
385 goalw thy [KeyWithNonce_def] |
387 goalw thy [KeyWithNonce_def] |
386 "!!evs. Key K ~: used evs ==> ~ KeyWithNonce K NB evs"; |
388 "!!evs. Key K ~: used evs ==> ~ KeyWithNonce K NB evs"; |
387 by (blast_tac (!claset addSEs sees_Spy_partsEs) 1); |
389 by (blast_tac (!claset addSEs sees_Spy_partsEs) 1); |
388 qed "fresh_not_KeyWithNonce"; |
390 qed "fresh_not_KeyWithNonce"; |
389 |
391 |
508 |
510 |
509 |
511 |
510 (** A nonce value is never used both as NA and as NB **) |
512 (** A nonce value is never used both as NA and as NB **) |
511 |
513 |
512 goal thy |
514 goal thy |
513 "!!evs. [| B ~: lost; evs : yahalom lost |] \ |
515 "!!evs. [| B ~: lost; evs : yahalom lost |] \ |
514 \ ==> Nonce NB ~: analz (sees lost Spy evs) --> \ |
516 \ ==> Nonce NB ~: analz (sees lost Spy evs) --> \ |
515 \ Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}: parts(sees lost Spy evs)\ |
517 \ Crypt (shrK B') {|Agent A', Nonce NB, NB'|} \ |
516 \ --> Crypt (shrK B') {|Agent A', Nonce NB, NB'|} ~: parts(sees lost Spy evs)"; |
518 \ : parts(sees lost Spy evs) \ |
|
519 \ --> Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|} \ |
|
520 \ ~: parts(sees lost Spy evs)"; |
517 by analz_mono_parts_induct_tac; |
521 by analz_mono_parts_induct_tac; |
518 by (Fake_parts_insert_tac 1); |
522 by (Fake_parts_insert_tac 1); |
519 by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS analz.Inj] |
523 by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS analz.Inj] |
520 addSIs [parts_insertI] |
524 addSIs [parts_insertI] |
521 addSEs partsEs) 1); |
525 addSEs partsEs) 1); |
522 bind_thm ("no_nonce_YM1_YM2", result() RS mp RSN (2, rev_mp) RS notE); |
526 bind_thm ("no_nonce_YM1_YM2", result() RS mp RSN (2,rev_mp) RSN (2,rev_notE)); |
523 |
527 |
524 (*YM3 can only be triggered by YM2*) |
528 (*The Server sends YM3 only in response to YM2.*) |
525 goal thy |
529 goal thy |
526 "!!evs. [| Says Server A \ |
530 "!!evs. [| Says Server A \ |
527 \ {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} : set_of_list evs; \ |
531 \ {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} : set_of_list evs; \ |
528 \ evs : yahalom lost |] \ |
532 \ evs : yahalom lost |] \ |
529 \ ==> EX B'. Says B' Server \ |
533 \ ==> EX B'. Says B' Server \ |
534 by (ALLGOALS Asm_simp_tac); |
538 by (ALLGOALS Asm_simp_tac); |
535 by (ALLGOALS Blast_tac); |
539 by (ALLGOALS Blast_tac); |
536 qed "Says_Server_imp_YM2"; |
540 qed "Says_Server_imp_YM2"; |
537 |
541 |
538 |
542 |
539 (*Basic theorem for B: Nonce NB remains secure from the Spy. |
543 (*A vital theorem for B, that nonce NB remains secure from the Spy. |
540 Unusually, the Fake case requires Spy:lost.*) |
544 Unusually, the Fake case requires Spy:lost.*) |
541 goal thy |
545 goal thy |
542 "!!evs. [| A ~: lost; B ~: lost; Spy: lost; evs : yahalom lost |] \ |
546 "!!evs. [| A ~: lost; B ~: lost; Spy: lost; evs : yahalom lost |] \ |
543 \ ==> Says B Server \ |
547 \ ==> Says B Server \ |
544 \ {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \ |
548 \ {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \ |
592 addDs [Says_imp_sees_Spy' RS parts.Inj, |
596 addDs [Says_imp_sees_Spy' RS parts.Inj, |
593 no_nonce_YM1_YM2 (*to prove NB~=NAa*) ]) 1); |
597 no_nonce_YM1_YM2 (*to prove NB~=NAa*) ]) 1); |
594 bind_thm ("Spy_not_see_NB", result() RSN(2,rev_mp) RSN(2,rev_mp)); |
598 bind_thm ("Spy_not_see_NB", result() RSN(2,rev_mp) RSN(2,rev_mp)); |
595 |
599 |
596 |
600 |
597 (*What can B deduce from receipt of YM4? Note how the two components of |
601 (*B's session key guarantee from YM4. The two certificates contribute to a |
598 the message contribute to a single conclusion about the Server's message. |
602 single conclusion about the Server's message. Note that the "Says A Spy" |
599 Note that the "Says A Spy" assumption must quantify over |
603 assumption must quantify over ALL POSSIBLE keys instead of our particular K. |
600 ALL POSSIBLE keys instead of our particular K. If this run is broken and |
604 If this run is broken and the spy substitutes a certificate containing an |
601 the spy has a certificate for an old key, B has no means of telling.*) |
605 old key, B has no means of telling.*) |
602 goal thy |
606 goal thy |
603 "!!evs. [| Says B Server \ |
607 "!!evs. [| Says B Server \ |
604 \ {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \ |
608 \ {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \ |
605 \ : set_of_list evs; \ |
609 \ : set_of_list evs; \ |
606 \ Says A' B {|Crypt (shrK B) {|Agent A, Key K|}, \ |
610 \ Says A' B {|Crypt (shrK B) {|Agent A, Key K|}, \ |