src/HOL/Auth/Yahalom.ML
changeset 3464 315694e22856
parent 3450 cd73bc206d87
child 3465 e85c24717cad
     1.1 --- a/src/HOL/Auth/Yahalom.ML	Thu Jun 26 11:15:55 1997 +0200
     1.2 +++ b/src/HOL/Auth/Yahalom.ML	Thu Jun 26 11:58:05 1997 +0200
     1.3 @@ -358,7 +358,7 @@
     1.4  (*A's certificate guarantees the existence of the Server message*)
     1.5  by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj RS parts.Fst RS
     1.6  			      A_trusts_YM3]) 1);
     1.7 -val B_trusts_YM4_newK = result() RS mp RSN (2, rev_mp);
     1.8 +bind_thm ("B_trusts_YM4_newK", result() RS mp RSN (2, rev_mp));
     1.9  
    1.10  
    1.11  (**** Towards proving secrecy of Nonce NB ****)
    1.12 @@ -382,6 +382,8 @@
    1.13  qed "KeyWithNonce_Says";
    1.14  Addsimps [KeyWithNonce_Says];
    1.15  
    1.16 +(*A fresh key cannot be associated with any nonce 
    1.17 +  (with respect to a given trace). *)
    1.18  goalw thy [KeyWithNonce_def]
    1.19   "!!evs. Key K ~: used evs ==> ~ KeyWithNonce K NB evs";
    1.20  by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
    1.21 @@ -510,18 +512,20 @@
    1.22  (** A nonce value is never used both as NA and as NB **)
    1.23  
    1.24  goal thy 
    1.25 - "!!evs. [| B ~: lost;  evs : yahalom lost  |]               \
    1.26 -\ ==> Nonce NB ~: analz (sees lost Spy evs) -->              \
    1.27 -\     Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}: parts(sees lost Spy evs)\
    1.28 -\ --> Crypt (shrK B') {|Agent A', Nonce NB, NB'|} ~: parts(sees lost Spy evs)";
    1.29 + "!!evs. [| B ~: lost;  evs : yahalom lost  |]       \
    1.30 +\ ==> Nonce NB ~: analz (sees lost Spy evs) -->      \
    1.31 +\     Crypt (shrK B') {|Agent A', Nonce NB, NB'|}    \
    1.32 +\       : parts(sees lost Spy evs)                   \
    1.33 +\ --> Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|} \
    1.34 +\       ~: parts(sees lost Spy evs)";
    1.35  by analz_mono_parts_induct_tac;
    1.36  by (Fake_parts_insert_tac 1);
    1.37  by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS analz.Inj]
    1.38                         addSIs [parts_insertI]
    1.39                         addSEs partsEs) 1);
    1.40 -bind_thm ("no_nonce_YM1_YM2", result() RS mp RSN (2, rev_mp) RS notE);
    1.41 +bind_thm ("no_nonce_YM1_YM2", result() RS mp RSN (2,rev_mp) RSN (2,rev_notE));
    1.42  
    1.43 -(*YM3 can only be triggered by YM2*)
    1.44 +(*The Server sends YM3 only in response to YM2.*)
    1.45  goal thy 
    1.46   "!!evs. [| Says Server A                                           \
    1.47  \            {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} : set_of_list evs; \
    1.48 @@ -536,7 +540,7 @@
    1.49  qed "Says_Server_imp_YM2";
    1.50  
    1.51  
    1.52 -(*Basic theorem for B: Nonce NB remains secure from the Spy.
    1.53 +(*A vital theorem for B, that nonce NB remains secure from the Spy.
    1.54    Unusually, the Fake case requires Spy:lost.*)
    1.55  goal thy 
    1.56   "!!evs. [| A ~: lost;  B ~: lost;  Spy: lost;  evs : yahalom lost |]  \
    1.57 @@ -594,11 +598,11 @@
    1.58  bind_thm ("Spy_not_see_NB", result() RSN(2,rev_mp) RSN(2,rev_mp));
    1.59  
    1.60  
    1.61 -(*What can B deduce from receipt of YM4?  Note how the two components of
    1.62 -  the message contribute to a single conclusion about the Server's message.
    1.63 -  Note that the "Says A Spy" assumption must quantify over 
    1.64 -  ALL POSSIBLE keys instead of our particular K.  If this run is broken and
    1.65 -  the spy has a certificate for an old key, B has no means of telling.*)
    1.66 +(*B's session key guarantee from YM4.  The two certificates contribute to a
    1.67 +  single conclusion about the Server's message.  Note that the "Says A Spy"
    1.68 +  assumption must quantify over ALL POSSIBLE keys instead of our particular K.
    1.69 +  If this run is broken and the spy substitutes a certificate containing an
    1.70 +  old key, B has no means of telling.*)
    1.71  goal thy 
    1.72   "!!evs. [| Says B Server                                                   \
    1.73  \             {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}   \