# HG changeset patch # User paulson # Date 867319085 -7200 # Node ID 315694e22856a4d7aba897d4df3e139555ba0365 # Parent 8ea594a5ae53fef4b4336b8db6e609872c7d3fb8 Trivial changes in connection with the Yahalom paper. Changed the order of the premises in no_nonce_YM1_YM2. Installed B_trusts_YM4_newK using bind_thm. Improved some comments. diff -r 8ea594a5ae53 -r 315694e22856 src/HOL/Auth/Yahalom.ML --- a/src/HOL/Auth/Yahalom.ML Thu Jun 26 11:15:55 1997 +0200 +++ b/src/HOL/Auth/Yahalom.ML Thu Jun 26 11:58:05 1997 +0200 @@ -358,7 +358,7 @@ (*A's certificate guarantees the existence of the Server message*) by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj RS parts.Fst RS A_trusts_YM3]) 1); -val B_trusts_YM4_newK = result() RS mp RSN (2, rev_mp); +bind_thm ("B_trusts_YM4_newK", result() RS mp RSN (2, rev_mp)); (**** Towards proving secrecy of Nonce NB ****) @@ -382,6 +382,8 @@ qed "KeyWithNonce_Says"; Addsimps [KeyWithNonce_Says]; +(*A fresh key cannot be associated with any nonce + (with respect to a given trace). *) goalw thy [KeyWithNonce_def] "!!evs. Key K ~: used evs ==> ~ KeyWithNonce K NB evs"; by (blast_tac (!claset addSEs sees_Spy_partsEs) 1); @@ -510,18 +512,20 @@ (** A nonce value is never used both as NA and as NB **) goal thy - "!!evs. [| B ~: lost; evs : yahalom lost |] \ -\ ==> Nonce NB ~: analz (sees lost Spy evs) --> \ -\ Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}: parts(sees lost Spy evs)\ -\ --> Crypt (shrK B') {|Agent A', Nonce NB, NB'|} ~: parts(sees lost Spy evs)"; + "!!evs. [| B ~: lost; evs : yahalom lost |] \ +\ ==> Nonce NB ~: analz (sees lost Spy evs) --> \ +\ Crypt (shrK B') {|Agent A', Nonce NB, NB'|} \ +\ : parts(sees lost Spy evs) \ +\ --> Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|} \ +\ ~: parts(sees lost Spy evs)"; by analz_mono_parts_induct_tac; by (Fake_parts_insert_tac 1); by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS analz.Inj] addSIs [parts_insertI] addSEs partsEs) 1); -bind_thm ("no_nonce_YM1_YM2", result() RS mp RSN (2, rev_mp) RS notE); +bind_thm ("no_nonce_YM1_YM2", result() RS mp RSN (2,rev_mp) RSN (2,rev_notE)); -(*YM3 can only be triggered by YM2*) +(*The Server sends YM3 only in response to YM2.*) goal thy "!!evs. [| Says Server A \ \ {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} : set_of_list evs; \ @@ -536,7 +540,7 @@ qed "Says_Server_imp_YM2"; -(*Basic theorem for B: Nonce NB remains secure from the Spy. +(*A vital theorem for B, that nonce NB remains secure from the Spy. Unusually, the Fake case requires Spy:lost.*) goal thy "!!evs. [| A ~: lost; B ~: lost; Spy: lost; evs : yahalom lost |] \ @@ -594,11 +598,11 @@ bind_thm ("Spy_not_see_NB", result() RSN(2,rev_mp) RSN(2,rev_mp)); -(*What can B deduce from receipt of YM4? Note how the two components of - the message contribute to a single conclusion about the Server's message. - Note that the "Says A Spy" assumption must quantify over - ALL POSSIBLE keys instead of our particular K. If this run is broken and - the spy has a certificate for an old key, B has no means of telling.*) +(*B's session key guarantee from YM4. The two certificates contribute to a + single conclusion about the Server's message. Note that the "Says A Spy" + assumption must quantify over ALL POSSIBLE keys instead of our particular K. + If this run is broken and the spy substitutes a certificate containing an + old key, B has no means of telling.*) goal thy "!!evs. [| Says B Server \ \ {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \