src/HOL/Auth/Yahalom.ML
changeset 4537 4e835bd9fada
parent 4509 828148415197
child 4598 649bf14debe7
     1.1 --- a/src/HOL/Auth/Yahalom.ML	Thu Jan 08 18:09:47 1998 +0100
     1.2 +++ b/src/HOL/Auth/Yahalom.ML	Thu Jan 08 18:10:34 1998 +0100
     1.3 @@ -202,12 +202,12 @@
     1.4  (** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
     1.5  
     1.6  goal thy 
     1.7 - "!!evs. [| A ~: bad;  B ~: bad;  evs : yahalom |]         \
     1.8 + "!!evs. [| A ~: bad;  B ~: bad;  evs : yahalom |]                \
     1.9  \        ==> Says Server A                                        \
    1.10  \              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
    1.11  \                Crypt (shrK B) {|Agent A, Key K|}|}              \
    1.12  \             : set evs -->                                       \
    1.13 -\            Says A Spy {|na, nb, Key K|} ~: set evs -->          \
    1.14 +\            Notes Spy {|na, nb, Key K|} ~: set evs -->           \
    1.15  \            Key K ~: analz (spies evs)";
    1.16  by (etac yahalom.induct 1);
    1.17  by analz_spies_tac;
    1.18 @@ -232,8 +232,8 @@
    1.19  \              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
    1.20  \                Crypt (shrK B) {|Agent A, Key K|}|}              \
    1.21  \             : set evs;                                          \
    1.22 -\           Says A Spy {|na, nb, Key K|} ~: set evs;              \
    1.23 -\           A ~: bad;  B ~: bad;  evs : yahalom |]         \
    1.24 +\           Notes Spy {|na, nb, Key K|} ~: set evs;               \
    1.25 +\           A ~: bad;  B ~: bad;  evs : yahalom |]                \
    1.26  \        ==> Key K ~: analz (spies evs)";
    1.27  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
    1.28  by (blast_tac (claset() addSEs [lemma]) 1);
    1.29 @@ -322,6 +322,12 @@
    1.30  qed "KeyWithNonce_Says";
    1.31  Addsimps [KeyWithNonce_Says];
    1.32  
    1.33 +goalw thy [KeyWithNonce_def]
    1.34 +   "KeyWithNonce K NB (Notes A X # evs) = KeyWithNonce K NB evs";
    1.35 +by (Simp_tac 1);
    1.36 +qed "KeyWithNonce_Notes";
    1.37 +Addsimps [KeyWithNonce_Notes];
    1.38 +
    1.39  (*A fresh key cannot be associated with any nonce 
    1.40    (with respect to a given trace). *)
    1.41  goalw thy [KeyWithNonce_def]
    1.42 @@ -372,7 +378,8 @@
    1.43       (analz_image_freshK_ss 
    1.44         addsimps expand_ifs
    1.45         addsimps [all_conj_distrib, analz_image_freshK,
    1.46 -		 KeyWithNonce_Says, fresh_not_KeyWithNonce, 
    1.47 +		 KeyWithNonce_Says, KeyWithNonce_Notes,
    1.48 +		 fresh_not_KeyWithNonce, 
    1.49  		 imp_disj_not1,		     (*Moves NBa~=NB to the front*)
    1.50  		 Says_Server_KeyWithNonce])));
    1.51  (*Fake*) 
    1.52 @@ -478,7 +485,7 @@
    1.53  \ ==> Says B Server                                                    \
    1.54  \          {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \
    1.55  \     : set evs -->                                                    \
    1.56 -\     (ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs) -->     \
    1.57 +\     (ALL k. Notes Spy {|Nonce NA, Nonce NB, k|} ~: set evs) -->      \
    1.58  \     Nonce NB ~: analz (spies evs)";
    1.59  by (etac yahalom.induct 1);
    1.60  by analz_spies_tac;
    1.61 @@ -529,7 +536,7 @@
    1.62  
    1.63  
    1.64  (*B's session key guarantee from YM4.  The two certificates contribute to a
    1.65 -  single conclusion about the Server's message.  Note that the "Says A Spy"
    1.66 +  single conclusion about the Server's message.  Note that the "Notes Spy"
    1.67    assumption must quantify over ALL POSSIBLE keys instead of our particular K.
    1.68    If this run is broken and the spy substitutes a certificate containing an
    1.69    old key, B has no means of telling.*)
    1.70 @@ -539,7 +546,7 @@
    1.71  \             : set evs;                                                    \
    1.72  \           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
    1.73  \                       Crypt K (Nonce NB)|} : set evs;                     \
    1.74 -\           ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs;         \
    1.75 +\           ALL k. Notes Spy {|Nonce NA, Nonce NB, k|} ~: set evs;          \
    1.76  \           A ~: bad;  B ~: bad;  evs : yahalom |]       \
    1.77  \         ==> Says Server A                                                 \
    1.78  \                     {|Crypt (shrK A) {|Agent B, Key K,                    \
    1.79 @@ -636,7 +643,7 @@
    1.80  \             : set evs;                                                    \
    1.81  \           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
    1.82  \                       Crypt K (Nonce NB)|} : set evs;                     \
    1.83 -\           (ALL NA k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs);    \
    1.84 +\           (ALL NA k. Notes Spy {|Nonce NA, Nonce NB, k|} ~: set evs);     \
    1.85  \           A ~: bad;  B ~: bad;  evs : yahalom |]       \
    1.86  \        ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
    1.87  by (dtac B_trusts_YM4 1);