Addition of Yahalom protocol
authorpaulson
Fri Sep 13 13:16:57 1996 +0200 (1996-09-13)
changeset 1995c80e58e78d9c
parent 1994 4ddfafdeefa4
child 1996 33c42cae3dd0
Addition of Yahalom protocol
src/HOL/Auth/ROOT.ML
src/HOL/Auth/Yahalom.ML
src/HOL/Auth/Yahalom.thy
     1.1 --- a/src/HOL/Auth/ROOT.ML	Fri Sep 13 13:15:48 1996 +0200
     1.2 +++ b/src/HOL/Auth/ROOT.ML	Fri Sep 13 13:16:57 1996 +0200
     1.3 @@ -14,4 +14,5 @@
     1.4  use_thy "Shared";
     1.5  use_thy "NS_Shared";
     1.6  use_thy "OtwayRees";
     1.7 +use_thy "Yahalom";
     1.8  
     2.1 --- a/src/HOL/Auth/Yahalom.ML	Fri Sep 13 13:15:48 1996 +0200
     2.2 +++ b/src/HOL/Auth/Yahalom.ML	Fri Sep 13 13:16:57 1996 +0200
     2.3 @@ -1,4 +1,4 @@
     2.4 -(*  Title:      HOL/Auth/OtwayRees
     2.5 +(*  Title:      HOL/Auth/Yahalom
     2.6      ID:         $Id$
     2.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.8      Copyright   1996  University of Cambridge
     2.9 @@ -10,11 +10,25 @@
    2.10    Proc. Royal Soc. 426 (1989)
    2.11  *)
    2.12  
    2.13 -open OtwayRees;
    2.14 +open Yahalom;
    2.15  
    2.16  proof_timing:=true;
    2.17  HOL_quantifiers := false;
    2.18  
    2.19 +
    2.20 +(** Weak liveness: there are traces that reach the end **)
    2.21 +
    2.22 +goal thy 
    2.23 + "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
    2.24 +\        ==> EX X NB K. EX evs: yahalom.          \
    2.25 +\               Says A B {|X, Crypt (Nonce NB) K|} : set_of_list evs";
    2.26 +by (REPEAT (resolve_tac [exI,bexI] 1));
    2.27 +br (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS yahalom.YM4) 2;
    2.28 +by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
    2.29 +by (ALLGOALS Fast_tac);
    2.30 +qed "weak_liveness";
    2.31 +
    2.32 +
    2.33  (**** Inductive proofs about yahalom ****)
    2.34  
    2.35  (*The Enemy can see more than anybody else, except for their initial state*)
    2.36 @@ -45,30 +59,19 @@
    2.37  
    2.38  (** For reasoning about the encrypted portion of messages **)
    2.39  
    2.40 -goal thy "!!evs. (Says A' B {|N, Agent A, Agent B, X|}) : set_of_list evs ==> \
    2.41 -\                X : analz (sees Enemy evs)";
    2.42 -by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]) 1);
    2.43 -qed "YM2_analz_sees_Enemy";
    2.44 -
    2.45 -goal thy "!!evs. (Says S B {|N, X, X'|}) : set_of_list evs ==> \
    2.46 +(*Lets us treat YM4 using a similar argument as for the Fake case.*)
    2.47 +goal thy "!!evs. Says S A {|Crypt Y (shrK A), X|} : set_of_list evs ==> \
    2.48  \                X : analz (sees Enemy evs)";
    2.49  by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]) 1);
    2.50  qed "YM4_analz_sees_Enemy";
    2.51  
    2.52 -goal thy "!!evs. (Says B' A {|N, Crypt {|N,K|} K'|}) : set_of_list evs ==> \
    2.53 +goal thy "!!evs. Says S A {|Crypt {|B, K, NA, NB|} (shrK A), X|} \
    2.54 +\                  : set_of_list evs ==> \
    2.55  \                K : parts (sees Enemy evs)";
    2.56  by (fast_tac (!claset addSEs partsEs
    2.57  	              addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
    2.58 -qed "YM5_parts_sees_Enemy";
    2.59 +qed "YM4_parts_sees_Enemy";
    2.60  
    2.61 -(*YM2_analz... and YM4_analz... let us treat those cases using the same 
    2.62 -  argument as for the Fake case.  This is possible for most, but not all,
    2.63 -  proofs: Fake does not invent new nonces (as in YM2), and of course Fake
    2.64 -  messages originate from the Enemy. *)
    2.65 -
    2.66 -val YM2_YM4_tac = 
    2.67 -    dtac (YM2_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 4 THEN
    2.68 -    dtac (YM4_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 6;
    2.69  
    2.70  
    2.71  (*** Shared keys are not betrayed ***)
    2.72 @@ -78,11 +81,13 @@
    2.73   "!!evs. [| evs : yahalom;  A ~: bad |] ==> \
    2.74  \        Key (shrK A) ~: parts (sees Enemy evs)";
    2.75  be yahalom.induct 1;
    2.76 -by YM2_YM4_tac;
    2.77 +bd (YM4_analz_sees_Enemy RS synth.Inj) 6;
    2.78 +by (ALLGOALS Asm_simp_tac);
    2.79 +by (stac insert_commute 3);
    2.80  by (Auto_tac());
    2.81 -(*Deals with Fake message*)
    2.82 -by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    2.83 -			     impOfSubs Fake_parts_insert]) 1);
    2.84 +(*Fake and YM4 are similar*)
    2.85 +by (ALLGOALS (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
    2.86 +					impOfSubs Fake_parts_insert])));
    2.87  qed "Enemy_not_see_shrK";
    2.88  
    2.89  bind_thm ("Enemy_not_analz_shrK",
    2.90 @@ -94,7 +99,7 @@
    2.91    As usual fast_tac cannot be used because it uses the equalities too soon*)
    2.92  val major::prems = 
    2.93  goal thy  "[| Key (shrK A) : parts (sees Enemy evs);       \
    2.94 -\             evs : yahalom;                                 \
    2.95 +\             evs : yahalom;                               \
    2.96  \             A:bad ==> R                                  \
    2.97  \           |] ==> R";
    2.98  br ccontr 1;
    2.99 @@ -121,13 +126,11 @@
   2.100  \                length evs <= length evs' --> \
   2.101  \                          Key (newK evs') ~: (UN C. parts (sees C evs))";
   2.102  be yahalom.induct 1;
   2.103 -by YM2_YM4_tac;
   2.104 -(*auto_tac does not work here, as it performs safe_tac first*)
   2.105 -by (ALLGOALS Asm_simp_tac);
   2.106 +bd (YM4_analz_sees_Enemy RS synth.Inj) 6;
   2.107  by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   2.108 -				       impOfSubs parts_insert_subset_Un,
   2.109 -				       Suc_leD]
   2.110 -			        addss (!simpset))));
   2.111 +					   impOfSubs parts_insert_subset_Un,
   2.112 +					   Suc_leD]
   2.113 +			            addss (!simpset))));
   2.114  val lemma = result();
   2.115  
   2.116  (*Variant needed for the main theorem below*)
   2.117 @@ -156,27 +159,24 @@
   2.118  \                length evs <= length evs' --> \
   2.119  \                newK evs' ~: keysFor (UN C. parts (sees C evs))";
   2.120  be yahalom.induct 1;
   2.121 -by YM2_YM4_tac;
   2.122 -bd YM5_parts_sees_Enemy 7;
   2.123 -by (ALLGOALS Asm_simp_tac);
   2.124 -(*YM1 and YM3*)
   2.125 -by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2]));
   2.126 -(*Fake, YM2, YM4: these messages send unknown (X) components*)
   2.127 -by (EVERY 
   2.128 -    (map
   2.129 +by (forward_tac [YM4_parts_sees_Enemy] 6);
   2.130 +bd (YM4_analz_sees_Enemy RS synth.Inj) 6;
   2.131 +by (ALLGOALS Asm_full_simp_tac);
   2.132 +(*YM1, YM2 and YM3*)
   2.133 +by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,3,2]));
   2.134 +(*Fake and YM4: these messages send unknown (X) components*)
   2.135 +by (stac insert_commute 2);
   2.136 +by (Simp_tac 2);
   2.137 +(*YM4: the only way K could have been used is if it had been seen,
   2.138 +  contradicting new_keys_not_seen*)
   2.139 +by (ALLGOALS
   2.140       (best_tac
   2.141 -      (!claset addSDs [newK_invKey]
   2.142 -	       addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   2.143 +      (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   2.144  		      impOfSubs (parts_insert_subset_Un RS keysFor_mono),
   2.145  		      Suc_leD]
   2.146 -	       addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
   2.147 -	       addss (!simpset)))
   2.148 -     [3,2,1]));
   2.149 -(*YM5: dummy message*)
   2.150 -by (best_tac (!claset addSDs [newK_invKey]
   2.151 -		        addEs  [new_keys_not_seen RSN(2,rev_notE)]
   2.152 -			addIs  [less_SucI, impOfSubs keysFor_mono]
   2.153 -			addss (!simpset addsimps [le_def])) 1);
   2.154 +	       addDs [impOfSubs analz_subset_parts]
   2.155 +	       addEs [new_keys_not_seen RSN(2,rev_notE)]
   2.156 +	       addss (!simpset))));
   2.157  val lemma = result();
   2.158  
   2.159  goal thy 
   2.160 @@ -214,14 +214,16 @@
   2.161  \        (Crypt X (newK evt)) : parts (sees Enemy evs) & \
   2.162  \        Key K : parts {X} --> Key K : parts (sees Enemy evs)";
   2.163  be yahalom.induct 1;
   2.164 -by YM2_YM4_tac;
   2.165 +bd (YM4_analz_sees_Enemy RS synth.Inj) 6;
   2.166  by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes)));
   2.167  (*Deals with Faked messages*)
   2.168 -by (best_tac (!claset addSEs partsEs
   2.169 -		      addDs [impOfSubs analz_subset_parts,
   2.170 -                             impOfSubs parts_insert_subset_Un]
   2.171 -                      addss (!simpset)) 2);
   2.172 -(*Base case and YM5*)
   2.173 +by (EVERY 
   2.174 +    (map (best_tac (!claset addSEs partsEs
   2.175 +			    addDs [impOfSubs analz_subset_parts,
   2.176 +				   impOfSubs parts_insert_subset_Un]
   2.177 +			    addss (!simpset)))
   2.178 +     [3,2]));
   2.179 +(*Base case*)
   2.180  by (Auto_tac());
   2.181  result();
   2.182  
   2.183 @@ -259,19 +261,6 @@
   2.184  
   2.185  (** Session keys are not used to encrypt other session keys **)
   2.186  
   2.187 -(*Could generalize this so that the X component doesn't have to be first
   2.188 -  in the message?*)
   2.189 -val enemy_analz_tac =
   2.190 -  SELECT_GOAL 
   2.191 -   (EVERY [REPEAT (resolve_tac [impI,notI] 1),
   2.192 -	   dtac (impOfSubs Fake_analz_insert) 1,
   2.193 -	   eresolve_tac [asm_rl, synth.Inj] 1,
   2.194 -	   Fast_tac 1,
   2.195 -	   Asm_full_simp_tac 1,
   2.196 -	   IF_UNSOLVED (deepen_tac (!claset addIs [impOfSubs analz_mono]) 0 1)
   2.197 -	   ]);
   2.198 -
   2.199 -
   2.200  (*Lemma for the trivial direction of the if-and-only-if*)
   2.201  goal thy  
   2.202   "!!evs. (Key K : analz (Key``nE Un sEe)) --> \
   2.203 @@ -286,34 +275,23 @@
   2.204  \  ALL K E. (Key K : analz (Key``(newK``E) Un (sees Enemy evs))) = \
   2.205  \           (K : newK``E | Key K : analz (sees Enemy evs))";
   2.206  be yahalom.induct 1;
   2.207 -bd YM2_analz_sees_Enemy 4;
   2.208  bd YM4_analz_sees_Enemy 6;
   2.209  by (REPEAT_FIRST (resolve_tac [allI, lemma]));
   2.210 -by (ALLGOALS (*Takes 35 secs*)
   2.211 +by (ALLGOALS 
   2.212      (asm_simp_tac 
   2.213       (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
   2.214  			 @ pushes)
   2.215                 setloop split_tac [expand_if])));
   2.216  (*YM4*) 
   2.217 -by (enemy_analz_tac 5);
   2.218 +by (enemy_analz_tac 4);
   2.219  (*YM3*)
   2.220 -by (Fast_tac 4);
   2.221 -(*YM2*) (** LEVEL 7 **)
   2.222 -by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")] 
   2.223 -    (insert_commute RS ssubst) 3);
   2.224 -by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")]
   2.225 -    (insert_commute RS ssubst) 3);
   2.226 -by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 3);
   2.227 -by (enemy_analz_tac 3);
   2.228 -(*Fake case*) (** LEVEL 11 **)
   2.229 -by (res_inst_tac [("y1","X"), ("A1", "?G Un (?H::msg set)")] 
   2.230 -    (insert_commute RS ssubst) 2);
   2.231 +by (Fast_tac 3);
   2.232 +(*Fake case*)
   2.233  by (enemy_analz_tac 2);
   2.234  (*Base case*)
   2.235  by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
   2.236  qed_spec_mp "analz_image_newK";
   2.237  
   2.238 -
   2.239  goal thy
   2.240   "!!evs. evs : yahalom ==>                               \
   2.241  \        Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) = \
   2.242 @@ -326,29 +304,28 @@
   2.243  
   2.244  (*Describes the form *and age* of K when the following message is sent*)
   2.245  goal thy 
   2.246 - "!!evs. [| Says Server B \
   2.247 -\            {|NA, Crypt {|NA, K|} (shrK A),                      \
   2.248 -\                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs;  \
   2.249 + "!!evs. [| Says Server A                                           \
   2.250 +\            {|Crypt {|Agent B, K, NA, NB|} (shrK A),               \
   2.251 +\              Crypt {|Agent A, K|} (shrK B)|} : set_of_list evs;   \
   2.252  \           evs : yahalom |]                                        \
   2.253 -\        ==> (EX evt:yahalom. K = Key(newK evt) & \
   2.254 -\                           length evt < length evs) &            \
   2.255 -\            (EX i. NA = Nonce i)";
   2.256 +\        ==> (EX evt:yahalom. K = Key(newK evt) &                   \
   2.257 +\                           length evt < length evs)";
   2.258  be rev_mp 1;
   2.259  be yahalom.induct 1;
   2.260  by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset))));
   2.261  qed "Says_Server_message_form";
   2.262  
   2.263  
   2.264 -(*Crucial secrecy property: Enemy does not see the keys sent in msg YM3*)
   2.265 +(*Crucial secrecy property: Enemy does not see the keys sent in msg YM3
   2.266 +  As with Otway-Rees, proof does not need uniqueness of session keys.*)
   2.267  goal thy 
   2.268   "!!evs. [| Says Server A \
   2.269 -\            {|NA, Crypt {|NA, K|} (shrK B),                      \
   2.270 -\                  Crypt {|NB, K|} (shrK A)|} : set_of_list evs;  \
   2.271 -\           A ~: bad;  B ~: bad;  evs : yahalom |] ==>              \
   2.272 +\            {|Crypt {|Agent B, K, NA, NB|} (shrK A),                   \
   2.273 +\              Crypt {|Agent A, K|} (shrK B)|} : set_of_list evs;       \
   2.274 +\           A ~: bad;  B ~: bad;  evs : yahalom |] ==>                  \
   2.275  \     K ~: analz (sees Enemy evs)";
   2.276  be rev_mp 1;
   2.277  be yahalom.induct 1;
   2.278 -bd YM2_analz_sees_Enemy 4;
   2.279  bd YM4_analz_sees_Enemy 6;
   2.280  by (ALLGOALS Asm_simp_tac);
   2.281  (*Next 3 steps infer that K has the form "Key (newK evs'" ... *)
   2.282 @@ -360,87 +337,10 @@
   2.283       (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
   2.284  			  analz_insert_Key_newK] @ pushes)
   2.285                 setloop split_tac [expand_if])));
   2.286 +(*YM4*)
   2.287 +by (enemy_analz_tac 3);
   2.288  (*YM3*)
   2.289 -by (fast_tac (!claset addSEs [less_irrefl]) 3);
   2.290 +by (fast_tac (!claset addSEs [less_irrefl]) 2);
   2.291  (*Fake*) (** LEVEL 10 **)
   2.292 -by (res_inst_tac [("y1","X"), ("x1", "Key ?K")] (insert_commute RS ssubst) 1);
   2.293 -by (enemy_analz_tac 1);
   2.294 -(*YM4*)
   2.295 -by (mp_tac 2);
   2.296 -by (enemy_analz_tac 2);
   2.297 -(*YM2*)
   2.298 -by (mp_tac 1);
   2.299 -by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")]
   2.300 -    (insert_commute RS ssubst) 1);
   2.301 -by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
   2.302  by (enemy_analz_tac 1);
   2.303  qed "Enemy_not_see_encrypted_key";
   2.304 -
   2.305 -
   2.306 -
   2.307 -(*** Session keys are issued at most once, and identify the principals ***)
   2.308 -
   2.309 -(** First, two lemmas for the Fake, YM2 and YM4 cases **)
   2.310 -
   2.311 -goal thy 
   2.312 - "!!evs. [| X : synth (analz (sees Enemy evs));                \
   2.313 -\           Crypt X' (shrK C) : parts{X};                      \
   2.314 -\           C ~: bad;  evs : yahalom |]  \
   2.315 -\        ==> Crypt X' (shrK C) : parts (sees Enemy evs)";
   2.316 -by (best_tac (!claset addSEs [impOfSubs analz_subset_parts]
   2.317 -	              addDs [impOfSubs parts_insert_subset_Un]
   2.318 -                      addss (!simpset)) 1);
   2.319 -qed "Crypt_Fake_parts";
   2.320 -
   2.321 -goal thy 
   2.322 - "!!evs. [| Crypt X' K : parts (sees A evs);  evs : yahalom |]  \
   2.323 -\        ==> EX S S' Y. Says S S' Y : set_of_list evs &       \
   2.324 -\            Crypt X' K : parts {Y}";
   2.325 -bd parts_singleton 1;
   2.326 -by (fast_tac (!claset addSDs [seesD] addss (!simpset)) 1);
   2.327 -qed "Crypt_parts_singleton";
   2.328 -
   2.329 -fun ex_strip_tac i = REPEAT (ares_tac [exI, conjI] i) THEN assume_tac (i+1);
   2.330 -
   2.331 -(*The Key K uniquely identifies a pair of senders in the message encrypted by
   2.332 -  C, but if C=Enemy then he could send all sorts of nonsense.*)
   2.333 -goal thy 
   2.334 - "!!evs. evs : yahalom ==>                                     \
   2.335 -\      EX A B. ALL C.                                        \
   2.336 -\         C ~: bad -->                                       \
   2.337 -\         (ALL S S' X. Says S S' X : set_of_list evs -->     \
   2.338 -\           (EX NA. Crypt {|NA, Key K|} (shrK C) : parts{X}) --> C=A | C=B)";
   2.339 -by (Simp_tac 1);
   2.340 -be yahalom.induct 1;
   2.341 -bd YM2_analz_sees_Enemy 4;
   2.342 -bd YM4_analz_sees_Enemy 6;
   2.343 -by (ALLGOALS 
   2.344 -    (asm_simp_tac (!simpset addsimps [all_conj_distrib, imp_conj_distrib])));
   2.345 -by (REPEAT_FIRST (etac exE));
   2.346 -(*YM4*)
   2.347 -by (ex_strip_tac 4);
   2.348 -by (fast_tac (!claset addSDs [synth.Inj RS Crypt_Fake_parts, 
   2.349 -			      Crypt_parts_singleton]) 4);
   2.350 -(*YM3: Case split propagates some context to other subgoal...*)
   2.351 -	(** LEVEL 8 **)
   2.352 -by (excluded_middle_tac "K = newK evsa" 3);
   2.353 -by (Asm_simp_tac 3);
   2.354 -by (REPEAT (ares_tac [exI] 3));
   2.355 -(*...we prove this case by contradiction: the key is too new!*)
   2.356 -by (fast_tac (!claset addIs [impOfSubs (subset_insertI RS parts_mono)]
   2.357 -		      addSEs partsEs
   2.358 -		      addEs [Says_imp_old_keys RS less_irrefl]
   2.359 -	              addss (!simpset)) 3);
   2.360 -(*YM2*) (** LEVEL 12 **)
   2.361 -by (ex_strip_tac 2);
   2.362 -by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")]
   2.363 -    (insert_commute RS ssubst) 2);
   2.364 -by (Simp_tac 2);
   2.365 -by (fast_tac (!claset addSDs [synth.Inj RS Crypt_Fake_parts, 
   2.366 -			      Crypt_parts_singleton]) 2);
   2.367 -(*Fake*) (** LEVEL 16 **)
   2.368 -by (ex_strip_tac 1);
   2.369 -by (fast_tac (!claset addSDs [Crypt_Fake_parts, Crypt_parts_singleton]) 1);
   2.370 -qed "unique_session_keys";
   2.371 -
   2.372 -(*It seems strange but this theorem is NOT needed to prove the main result!*)
     3.1 --- a/src/HOL/Auth/Yahalom.thy	Fri Sep 13 13:15:48 1996 +0200
     3.2 +++ b/src/HOL/Auth/Yahalom.thy	Fri Sep 13 13:16:57 1996 +0200
     3.3 @@ -1,4 +1,4 @@
     3.4 -(*  Title:      HOL/Auth/OtwayRees
     3.5 +(*  Title:      HOL/Auth/Yahalom
     3.6      ID:         $Id$
     3.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.8      Copyright   1996  University of Cambridge
     3.9 @@ -10,7 +10,7 @@
    3.10    Proc. Royal Soc. 426 (1989)
    3.11  *)
    3.12  
    3.13 -OtwayRees = Shared + 
    3.14 +Yahalom = Shared + 
    3.15  
    3.16  consts  yahalom   :: "event list set"
    3.17  inductive yahalom
    3.18 @@ -26,13 +26,12 @@
    3.19  
    3.20           (*Alice initiates a protocol run*)
    3.21      YM1  "[| evs: yahalom;  A ~= B |]
    3.22 -          ==> Says A B {|Nonce (newN evs), Agent A |} # evs : yahalom"
    3.23 +          ==> Says A B {|Agent A, Nonce (newN evs)|} # evs : yahalom"
    3.24  
    3.25           (*Bob's response to Alice's message.  Bob doesn't know who 
    3.26 -	   the sender is, hence the A' in the sender field.
    3.27 -           We modify the published protocol by NOT encrypting NB.*)
    3.28 +	   the sender is, hence the A' in the sender field.*)
    3.29      YM2  "[| evs: yahalom;  B ~= Server;
    3.30 -             Says A' B {|Nonce NA, Agent A|} : set_of_list evs |]
    3.31 +             Says A' B {|Agent A, Nonce NA|} : set_of_list evs |]
    3.32            ==> Says B Server 
    3.33                    {|Agent B, 
    3.34                      Crypt {|Agent A, Nonce NA, Nonce (newN evs)|} (shrK B)|}
    3.35 @@ -40,34 +39,23 @@
    3.36  
    3.37           (*The Server receives Bob's message.  He responds by sending a
    3.38              new session key to Alice, with a packet for forwarding to Bob.*)
    3.39 -    YM3  "[| evs: yahalom;  B ~= Server;
    3.40 +    YM3  "[| evs: yahalom;  A ~= Server;
    3.41               Says B' Server 
    3.42 -                  {|Nonce NA, Agent A, Agent B, 
    3.43 -                    Crypt {|Nonce NA, Agent A, Agent B|} (shrK A), 
    3.44 -                    Nonce NB, 
    3.45 -                    Crypt {|Nonce NA, Agent A, Agent B|} (shrK B)|}
    3.46 +                  {|Agent B, Crypt {|Agent A, Nonce NA, Nonce NB|} (shrK B)|}
    3.47                 : set_of_list evs |]
    3.48 -          ==> Says Server B 
    3.49 -                  {|Nonce NA, 
    3.50 -                    Crypt {|Nonce NA, Key (newK evs)|} (shrK A),
    3.51 -                    Crypt {|Nonce NB, Key (newK evs)|} (shrK B)|}
    3.52 +          ==> Says Server A
    3.53 +                  {|Crypt {|Agent B, Key (newK evs), 
    3.54 +                            Nonce NA, Nonce NB|} (shrK A),
    3.55 +                    Crypt {|Agent A, Key (newK evs)|} (shrK B)|}
    3.56                   # evs : yahalom"
    3.57  
    3.58 -         (*Bob receives the Server's (?) message and compares the Nonces with
    3.59 -	   those in the message he previously sent the Server.*)
    3.60 +         (*Alice receives the Server's (?) message, checks her Nonce, and
    3.61 +           uses the new session key to send Bob his Nonce.*)
    3.62      YM4  "[| evs: yahalom;  A ~= B;  
    3.63 -             Says S B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|}
    3.64 +             Says S A {|Crypt {|Agent B, Key K, Nonce NA, Nonce NB|} (shrK A),
    3.65 +                        X|}
    3.66                 : set_of_list evs;
    3.67 -             Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, X''|}
    3.68 -               : set_of_list evs |]
    3.69 -          ==> (Says B A {|Nonce NA, X|}) # evs : yahalom"
    3.70 -
    3.71 -         (*Alice checks her Nonce, then sends a dummy message to Bob,
    3.72 -           using the new session key.*)
    3.73 -    YM5  "[| evs: yahalom;  
    3.74 -             Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|}
    3.75 -               : set_of_list evs;
    3.76 -             Says A  B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |]
    3.77 -          ==> Says A B (Crypt (Agent A) K)  # evs : yahalom"
    3.78 +             Says A B {|Agent A, Nonce NA|} : set_of_list evs |]
    3.79 +          ==> Says A B {|X, Crypt (Nonce NB) K|} # evs : yahalom"
    3.80  
    3.81  end