src/HOL/Auth/Yahalom.ML
changeset 2032 1bbf1bdcaf56
parent 2026 0df5a96bf77e
child 2045 ae1030e66745
     1.1 --- a/src/HOL/Auth/Yahalom.ML	Thu Sep 26 12:47:47 1996 +0200
     1.2 +++ b/src/HOL/Auth/Yahalom.ML	Thu Sep 26 12:50:48 1996 +0200
     1.3 @@ -20,10 +20,10 @@
     1.4  
     1.5  goal thy 
     1.6   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
     1.7 -\        ==> EX X NB K. EX evs: yahalom.          \
     1.8 +\        ==> EX X NB K. EX evs: yahalom lost.          \
     1.9  \               Says A B {|X, Crypt (Nonce NB) K|} : set_of_list evs";
    1.10  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.11 -br (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS yahalom.YM4) 2;
    1.12 +by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS yahalom.YM4) 2);
    1.13  by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
    1.14  by (ALLGOALS Fast_tac);
    1.15  result();
    1.16 @@ -31,19 +31,19 @@
    1.17  
    1.18  (**** Inductive proofs about yahalom ****)
    1.19  
    1.20 -(*The Enemy can see more than anybody else, except for their initial state*)
    1.21 +(*The Spy can see more than anybody else, except for their initial state*)
    1.22  goal thy 
    1.23 - "!!evs. evs : yahalom ==> \
    1.24 -\     sees A evs <= initState A Un sees Enemy evs";
    1.25 -be yahalom.induct 1;
    1.26 + "!!evs. evs : yahalom lost ==> \
    1.27 +\     sees lost A evs <= initState lost A Un sees lost Spy evs";
    1.28 +by (etac yahalom.induct 1);
    1.29  by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] 
    1.30 -			        addss (!simpset))));
    1.31 -qed "sees_agent_subset_sees_Enemy";
    1.32 +                                addss (!simpset))));
    1.33 +qed "sees_agent_subset_sees_Spy";
    1.34  
    1.35  
    1.36  (*Nobody sends themselves messages*)
    1.37 -goal thy "!!evs. evs : yahalom ==> ALL A X. Says A A X ~: set_of_list evs";
    1.38 -be yahalom.induct 1;
    1.39 +goal thy "!!evs. evs : yahalom lost ==> ALL A X. Says A A X ~: set_of_list evs";
    1.40 +by (etac yahalom.induct 1);
    1.41  by (Auto_tac());
    1.42  qed_spec_mp "not_Says_to_self";
    1.43  Addsimps [not_Says_to_self];
    1.44 @@ -54,58 +54,58 @@
    1.45  
    1.46  (*Lets us treat YM4 using a similar argument as for the Fake case.*)
    1.47  goal thy "!!evs. Says S A {|Crypt Y (shrK A), X|} : set_of_list evs ==> \
    1.48 -\                X : analz (sees Enemy evs)";
    1.49 -by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]) 1);
    1.50 -qed "YM4_analz_sees_Enemy";
    1.51 +\                X : analz (sees lost Spy evs)";
    1.52 +by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    1.53 +qed "YM4_analz_sees_Spy";
    1.54  
    1.55  goal thy "!!evs. Says S A {|Crypt {|B, K, NA, NB|} (shrK A), X|} \
    1.56  \                  : set_of_list evs ==> \
    1.57 -\                K : parts (sees Enemy evs)";
    1.58 +\                K : parts (sees lost Spy evs)";
    1.59  by (fast_tac (!claset addSEs partsEs
    1.60 -	              addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
    1.61 -qed "YM4_parts_sees_Enemy";
    1.62 +                      addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
    1.63 +qed "YM4_parts_sees_Spy";
    1.64  
    1.65  
    1.66  
    1.67 -(** Theorems of the form X ~: parts (sees Enemy evs) imply that NOBODY
    1.68 +(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
    1.69      sends messages containing X! **)
    1.70  
    1.71 -(*Enemy never sees another agent's shared key! (unless it is leaked at start)*)
    1.72 +(*Spy never sees lost another agent's shared key! (unless it is leaked at start)*)
    1.73  goal thy 
    1.74 - "!!evs. [| evs : yahalom;  A ~: bad |]    \
    1.75 -\        ==> Key (shrK A) ~: parts (sees Enemy evs)";
    1.76 -be yahalom.induct 1;
    1.77 -bd (YM4_analz_sees_Enemy RS synth.Inj) 6;
    1.78 + "!!evs. [| evs : yahalom lost;  A ~: lost |]    \
    1.79 +\        ==> Key (shrK A) ~: parts (sees lost Spy evs)";
    1.80 +by (etac yahalom.induct 1);
    1.81 +by (dtac (YM4_analz_sees_Spy RS synth.Inj) 6);
    1.82  by (ALLGOALS Asm_simp_tac);
    1.83  by (stac insert_commute 3);
    1.84  by (Auto_tac());
    1.85  (*Fake and YM4 are similar*)
    1.86  by (ALLGOALS (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
    1.87 -					impOfSubs Fake_parts_insert])));
    1.88 -qed "Enemy_not_see_shrK";
    1.89 +                                        impOfSubs Fake_parts_insert])));
    1.90 +qed "Spy_not_see_shrK";
    1.91  
    1.92 -bind_thm ("Enemy_not_analz_shrK",
    1.93 -	  [analz_subset_parts, Enemy_not_see_shrK] MRS contra_subsetD);
    1.94 +bind_thm ("Spy_not_analz_shrK",
    1.95 +          [analz_subset_parts, Spy_not_see_shrK] MRS contra_subsetD);
    1.96  
    1.97 -Addsimps [Enemy_not_see_shrK, Enemy_not_analz_shrK];
    1.98 +Addsimps [Spy_not_see_shrK, Spy_not_analz_shrK];
    1.99  
   1.100  (*We go to some trouble to preserve R in the 3rd and 4th subgoals
   1.101    As usual fast_tac cannot be used because it uses the equalities too soon*)
   1.102  val major::prems = 
   1.103 -goal thy  "[| Key (shrK A) : parts (sees Enemy evs);       \
   1.104 -\             evs : yahalom;                               \
   1.105 -\             A:bad ==> R                                  \
   1.106 +goal thy  "[| Key (shrK A) : parts (sees lost Spy evs);       \
   1.107 +\             evs : yahalom lost;                               \
   1.108 +\             A:lost ==> R                                  \
   1.109  \           |] ==> R";
   1.110 -br ccontr 1;
   1.111 -br ([major, Enemy_not_see_shrK] MRS rev_notE) 1;
   1.112 +by (rtac ccontr 1);
   1.113 +by (rtac ([major, Spy_not_see_shrK] MRS rev_notE) 1);
   1.114  by (swap_res_tac prems 2);
   1.115  by (ALLGOALS (fast_tac (!claset addIs prems)));
   1.116 -qed "Enemy_see_shrK_E";
   1.117 +qed "Spy_see_shrK_E";
   1.118  
   1.119 -bind_thm ("Enemy_analz_shrK_E", 
   1.120 -	  analz_subset_parts RS subsetD RS Enemy_see_shrK_E);
   1.121 +bind_thm ("Spy_analz_shrK_E", 
   1.122 +          analz_subset_parts RS subsetD RS Spy_see_shrK_E);
   1.123  
   1.124 -AddSEs [Enemy_see_shrK_E, Enemy_analz_shrK_E];
   1.125 +AddSEs [Spy_see_shrK_E, Spy_analz_shrK_E];
   1.126  
   1.127  
   1.128  (*** Future keys can't be seen or used! ***)
   1.129 @@ -116,21 +116,21 @@
   1.130    standard Fake rule.  
   1.131        The length comparison, and Union over C, are essential for the 
   1.132    induction! *)
   1.133 -goal thy "!!evs. evs : yahalom ==> \
   1.134 +goal thy "!!evs. evs : yahalom lost ==> \
   1.135  \                length evs <= length evs' --> \
   1.136 -\                          Key (newK evs') ~: (UN C. parts (sees C evs))";
   1.137 -be yahalom.induct 1;
   1.138 -bd (YM4_analz_sees_Enemy RS synth.Inj) 6;
   1.139 +\                          Key (newK evs') ~: (UN C. parts (sees lost C evs))";
   1.140 +by (etac yahalom.induct 1);
   1.141 +by (dtac (YM4_analz_sees_Spy RS synth.Inj) 6);
   1.142  by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   1.143 -					   impOfSubs parts_insert_subset_Un,
   1.144 -					   Suc_leD]
   1.145 -			            addss (!simpset))));
   1.146 +                                           impOfSubs parts_insert_subset_Un,
   1.147 +                                           Suc_leD]
   1.148 +                                    addss (!simpset))));
   1.149  val lemma = result();
   1.150  
   1.151  (*Variant needed for the main theorem below*)
   1.152  goal thy 
   1.153 - "!!evs. [| evs : yahalom;  length evs <= length evs' |]    \
   1.154 -\        ==> Key (newK evs') ~: parts (sees C evs)";
   1.155 + "!!evs. [| evs : yahalom lost;  length evs <= length evs' |]    \
   1.156 +\        ==> Key (newK evs') ~: parts (sees lost C evs)";
   1.157  by (fast_tac (!claset addDs [lemma]) 1);
   1.158  qed "new_keys_not_seen";
   1.159  Addsimps [new_keys_not_seen];
   1.160 @@ -139,23 +139,23 @@
   1.161  goal thy 
   1.162   "!!evs. [| Says A B X : set_of_list evs;  \
   1.163  \           Key (newK evt) : parts {X};    \
   1.164 -\           evs : yahalom                 \
   1.165 +\           evs : yahalom lost                 \
   1.166  \        |] ==> length evt < length evs";
   1.167 -br ccontr 1;
   1.168 -bd leI 1;
   1.169 -by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Enemy]
   1.170 +by (rtac ccontr 1);
   1.171 +by (dtac leI 1);
   1.172 +by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
   1.173                        addIs  [impOfSubs parts_mono]) 1);
   1.174  qed "Says_imp_old_keys";
   1.175  
   1.176  
   1.177  (*Nobody can have USED keys that will be generated in the future.
   1.178    ...very like new_keys_not_seen*)
   1.179 -goal thy "!!evs. evs : yahalom ==> \
   1.180 +goal thy "!!evs. evs : yahalom lost ==> \
   1.181  \                length evs <= length evs' --> \
   1.182 -\                newK evs' ~: keysFor (UN C. parts (sees C evs))";
   1.183 -be yahalom.induct 1;
   1.184 -by (forward_tac [YM4_parts_sees_Enemy] 6);
   1.185 -bd (YM4_analz_sees_Enemy RS synth.Inj) 6;
   1.186 +\                newK evs' ~: keysFor (UN C. parts (sees lost C evs))";
   1.187 +by (etac yahalom.induct 1);
   1.188 +by (forward_tac [YM4_parts_sees_Spy] 6);
   1.189 +by (dtac (YM4_analz_sees_Spy RS synth.Inj) 6);
   1.190  by (ALLGOALS Asm_full_simp_tac);
   1.191  (*YM1, YM2 and YM3*)
   1.192  by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,3,2]));
   1.193 @@ -167,22 +167,22 @@
   1.194  by (ALLGOALS
   1.195       (best_tac
   1.196        (!claset addDs [impOfSubs analz_subset_parts,
   1.197 -		      impOfSubs (analz_subset_parts RS keysFor_mono),
   1.198 -		      impOfSubs (parts_insert_subset_Un RS keysFor_mono),
   1.199 -		      Suc_leD]
   1.200 -	       addEs [new_keys_not_seen RSN(2,rev_notE)]
   1.201 -	       addss (!simpset))));
   1.202 +                      impOfSubs (analz_subset_parts RS keysFor_mono),
   1.203 +                      impOfSubs (parts_insert_subset_Un RS keysFor_mono),
   1.204 +                      Suc_leD]
   1.205 +               addEs [new_keys_not_seen RSN(2,rev_notE)]
   1.206 +               addss (!simpset))));
   1.207  val lemma = result();
   1.208  
   1.209  goal thy 
   1.210 - "!!evs. [| evs : yahalom;  length evs <= length evs' |]    \
   1.211 -\        ==> newK evs' ~: keysFor (parts (sees C evs))";
   1.212 + "!!evs. [| evs : yahalom lost;  length evs <= length evs' |]    \
   1.213 +\        ==> newK evs' ~: keysFor (parts (sees lost C evs))";
   1.214  by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
   1.215  qed "new_keys_not_used";
   1.216  
   1.217  bind_thm ("new_keys_not_analzd",
   1.218 -	  [analz_subset_parts RS keysFor_mono,
   1.219 -	   new_keys_not_used] MRS contra_subsetD);
   1.220 +          [analz_subset_parts RS keysFor_mono,
   1.221 +           new_keys_not_used] MRS contra_subsetD);
   1.222  
   1.223  Addsimps [new_keys_not_used, new_keys_not_analzd];
   1.224  
   1.225 @@ -193,8 +193,8 @@
   1.226  (****
   1.227   The following is to prove theorems of the form
   1.228  
   1.229 -          Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) ==>
   1.230 -          Key K : analz (sees Enemy evs)
   1.231 +          Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) ==>
   1.232 +          Key K : analz (sees lost Spy evs)
   1.233  
   1.234   A more general formula must be proved inductively.
   1.235  
   1.236 @@ -205,17 +205,17 @@
   1.237    to encrypt messages containing other keys, in the actual protocol.
   1.238    We require that agents should behave like this subsequently also.*)
   1.239  goal thy 
   1.240 - "!!evs. evs : yahalom ==> \
   1.241 -\        (Crypt X (newK evt)) : parts (sees Enemy evs) & \
   1.242 -\        Key K : parts {X} --> Key K : parts (sees Enemy evs)";
   1.243 -be yahalom.induct 1;
   1.244 -bd (YM4_analz_sees_Enemy RS synth.Inj) 6;
   1.245 + "!!evs. evs : yahalom lost ==> \
   1.246 +\        (Crypt X (newK evt)) : parts (sees lost Spy evs) & \
   1.247 +\        Key K : parts {X} --> Key K : parts (sees lost Spy evs)";
   1.248 +by (etac yahalom.induct 1);
   1.249 +by (dtac (YM4_analz_sees_Spy RS synth.Inj) 6);
   1.250  by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes)));
   1.251  (*Deals with Faked messages*)
   1.252  by (EVERY 
   1.253      (map (best_tac (!claset addSEs partsEs
   1.254 -			    addDs [impOfSubs parts_insert_subset_Un]
   1.255 -			    addss (!simpset)))
   1.256 +                            addDs [impOfSubs parts_insert_subset_Un]
   1.257 +                            addss (!simpset)))
   1.258       [3,2]));
   1.259  (*Base case*)
   1.260  by (Auto_tac());
   1.261 @@ -230,8 +230,8 @@
   1.262  Delsimps [image_Un];
   1.263  Addsimps [image_Un RS sym];
   1.264  
   1.265 -goal thy "insert (Key (newK x)) (sees A evs) = \
   1.266 -\         Key `` (newK``{x}) Un (sees A evs)";
   1.267 +goal thy "insert (Key (newK x)) (sees lost A evs) = \
   1.268 +\         Key `` (newK``{x}) Un (sees lost A evs)";
   1.269  by (Fast_tac 1);
   1.270  val insert_Key_singleton = result();
   1.271  
   1.272 @@ -243,10 +243,10 @@
   1.273  
   1.274  (*This lets us avoid analyzing the new message -- unless we have to!*)
   1.275  (*NEEDED??*)
   1.276 -goal thy "synth (analz (sees Enemy evs)) <=   \
   1.277 -\         synth (analz (sees Enemy (Says A B X # evs)))";
   1.278 +goal thy "synth (analz (sees lost Spy evs)) <=   \
   1.279 +\         synth (analz (sees lost Spy (Says A B X # evs)))";
   1.280  by (Simp_tac 1);
   1.281 -br (subset_insertI RS analz_mono RS synth_mono) 1;
   1.282 +by (rtac (subset_insertI RS analz_mono RS synth_mono) 1);
   1.283  qed "synth_analz_thin";
   1.284  
   1.285  AddIs [impOfSubs synth_analz_thin];
   1.286 @@ -265,33 +265,33 @@
   1.287  
   1.288  
   1.289  goal thy  
   1.290 - "!!evs. evs : yahalom ==> \
   1.291 -\  ALL K E. (Key K : analz (Key``(newK``E) Un (sees Enemy evs))) = \
   1.292 -\           (K : newK``E | Key K : analz (sees Enemy evs))";
   1.293 -be yahalom.induct 1;
   1.294 -bd YM4_analz_sees_Enemy 6;
   1.295 + "!!evs. evs : yahalom lost ==> \
   1.296 +\  ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \
   1.297 +\           (K : newK``E | Key K : analz (sees lost Spy evs))";
   1.298 +by (etac yahalom.induct 1);
   1.299 +by (dtac YM4_analz_sees_Spy 6);
   1.300  by (REPEAT_FIRST (resolve_tac [allI, lemma]));
   1.301  by (ALLGOALS 
   1.302      (asm_simp_tac 
   1.303       (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
   1.304 -			 @ pushes)
   1.305 +                         @ pushes)
   1.306                 setloop split_tac [expand_if])));
   1.307  (*YM4*) 
   1.308 -by (enemy_analz_tac 4);
   1.309 +by (spy_analz_tac 4);
   1.310  (*YM3*)
   1.311  by (Fast_tac 3);
   1.312  (*Fake case*)
   1.313 -by (enemy_analz_tac 2);
   1.314 +by (spy_analz_tac 2);
   1.315  (*Base case*)
   1.316  by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
   1.317  qed_spec_mp "analz_image_newK";
   1.318  
   1.319  goal thy
   1.320 - "!!evs. evs : yahalom ==>                               \
   1.321 -\        Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) = \
   1.322 -\        (K = newK evt | Key K : analz (sees Enemy evs))";
   1.323 + "!!evs. evs : yahalom lost ==>                               \
   1.324 +\        Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) = \
   1.325 +\        (K = newK evt | Key K : analz (sees lost Spy evs))";
   1.326  by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
   1.327 -				   insert_Key_singleton]) 1);
   1.328 +                                   insert_Key_singleton]) 1);
   1.329  by (Fast_tac 1);
   1.330  qed "analz_insert_Key_newK";
   1.331  
   1.332 @@ -301,39 +301,39 @@
   1.333   "!!evs. [| Says Server A                                           \
   1.334  \            {|Crypt {|Agent B, K, NA, NB|} (shrK A),               \
   1.335  \              Crypt {|Agent A, K|} (shrK B)|} : set_of_list evs;   \
   1.336 -\           evs : yahalom |]                                        \
   1.337 -\        ==> (EX evt:yahalom. K = Key(newK evt))";
   1.338 -be rev_mp 1;
   1.339 -be yahalom.induct 1;
   1.340 +\           evs : yahalom lost |]                                        \
   1.341 +\        ==> (EX evt: yahalom lost. K = Key(newK evt))";
   1.342 +by (etac rev_mp 1);
   1.343 +by (etac yahalom.induct 1);
   1.344  by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   1.345  qed "Says_Server_message_form";
   1.346  
   1.347  
   1.348 -(** Crucial secrecy property: Enemy does not see the keys sent in msg YM3
   1.349 +(** Crucial secrecy property: Spy does not see the keys sent in msg YM3
   1.350      As with Otway-Rees, proof does not need uniqueness of session keys. **)
   1.351  
   1.352  goal thy 
   1.353 - "!!evs. [| A ~: bad;  B ~: bad;  evs : yahalom;  evt : yahalom |]        \
   1.354 + "!!evs. [| A ~: lost;  B ~: lost;  evs : yahalom lost;  evt : yahalom lost |]        \
   1.355  \        ==> Says Server A                                                \
   1.356  \              {|Crypt {|Agent B, Key(newK evt), NA, NB|} (shrK A),       \
   1.357  \                Crypt {|Agent A, Key(newK evt)|} (shrK B)|}              \
   1.358  \             : set_of_list evs -->    \
   1.359 -\            Key(newK evt) ~: analz (sees Enemy evs)";
   1.360 -be yahalom.induct 1;
   1.361 -bd YM4_analz_sees_Enemy 6;
   1.362 +\            Key(newK evt) ~: analz (sees lost Spy evs)";
   1.363 +by (etac yahalom.induct 1);
   1.364 +by (dtac YM4_analz_sees_Spy 6);
   1.365  by (ALLGOALS
   1.366      (asm_simp_tac 
   1.367       (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
   1.368 -			  analz_insert_Key_newK] @ pushes)
   1.369 +                          analz_insert_Key_newK] @ pushes)
   1.370                 setloop split_tac [expand_if])));
   1.371  (*YM4*)
   1.372 -by (enemy_analz_tac 3);
   1.373 +by (spy_analz_tac 3);
   1.374  (*YM3*)
   1.375  by (fast_tac (!claset addIs [parts_insertI]
   1.376 -		      addEs [Says_imp_old_keys RS less_irrefl]
   1.377 -	              addss (!simpset)) 2);
   1.378 +                      addEs [Says_imp_old_keys RS less_irrefl]
   1.379 +                      addss (!simpset)) 2);
   1.380  (*Fake*) (** LEVEL 10 **)
   1.381 -by (enemy_analz_tac 1);
   1.382 +by (spy_analz_tac 1);
   1.383  val lemma = result() RS mp RSN(2,rev_notE);
   1.384  
   1.385  
   1.386 @@ -342,26 +342,26 @@
   1.387   "!!evs. [| Says Server A \
   1.388  \            {|Crypt {|Agent B, K, NA, NB|} (shrK A),                   \
   1.389  \              Crypt {|Agent A, K|} (shrK B)|} : set_of_list evs;       \
   1.390 -\           A ~: bad;  B ~: bad;  evs : yahalom |] ==>                  \
   1.391 -\     K ~: analz (sees Enemy evs)";
   1.392 +\           A ~: lost;  B ~: lost;  evs : yahalom lost |] ==>                  \
   1.393 +\     K ~: analz (sees lost Spy evs)";
   1.394  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   1.395  by (fast_tac (!claset addSEs [lemma]) 1);
   1.396 -qed "Enemy_not_see_encrypted_key";
   1.397 +qed "Spy_not_see_encrypted_key";
   1.398  
   1.399  
   1.400  (** Towards proofs of stronger authenticity properties **)
   1.401  
   1.402  goal thy 
   1.403 - "!!evs. [| Crypt {|Agent A, Key K|} (shrK B) : parts (sees Enemy evs); \
   1.404 -\           B ~: bad;  evs : yahalom |]                                 \
   1.405 + "!!evs. [| Crypt {|Agent A, Key K|} (shrK B) : parts (sees lost Spy evs); \
   1.406 +\           B ~: lost;  evs : yahalom lost |]                                 \
   1.407  \        ==> EX NA NB. Says Server A                                    \
   1.408  \                        {|Crypt {|Agent B, Key K,                      \
   1.409  \                                  Nonce NA, Nonce NB|} (shrK A),       \
   1.410  \                          Crypt {|Agent A, Key K|} (shrK B)|}          \
   1.411  \                       : set_of_list evs";
   1.412 -be rev_mp 1;
   1.413 -be yahalom.induct 1;
   1.414 -bd (YM4_analz_sees_Enemy RS synth.Inj) 6;
   1.415 +by (etac rev_mp 1);
   1.416 +by (etac yahalom.induct 1);
   1.417 +by (dtac (YM4_analz_sees_Spy RS synth.Inj) 6);
   1.418  by (ALLGOALS Asm_simp_tac);
   1.419  (*YM3*)
   1.420  by (Fast_tac 3);
   1.421 @@ -371,28 +371,28 @@
   1.422  by (stac insert_commute 2 THEN Simp_tac 2);
   1.423  (*Fake and YM4 are similar*)
   1.424  by (ALLGOALS (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
   1.425 -					impOfSubs Fake_parts_insert])));
   1.426 +                                        impOfSubs Fake_parts_insert])));
   1.427  qed "Crypt_imp_Server_msg";
   1.428  
   1.429  
   1.430  (*What can B deduce from receipt of YM4?  
   1.431    NOT THAT THE NONCES AGREE (in this version).  But what does the Nonce
   1.432 -	give us??*)
   1.433 +        give us??*)
   1.434  goal thy 
   1.435   "!!evs. [| Says A' B {|Crypt {|Agent A, Key K|} (shrK B),              \
   1.436  \                       Crypt (Nonce NB) K|} : set_of_list evs;         \
   1.437 -\           B ~: bad;  evs : yahalom |]                                 \
   1.438 +\           B ~: lost;  evs : yahalom lost |]                                 \
   1.439  \        ==> EX NA NB. Says Server A                                    \
   1.440  \                     {|Crypt {|Agent B, Key K,                         \
   1.441  \                               Nonce NA, Nonce NB|} (shrK A),          \
   1.442  \                       Crypt {|Agent A, Key K|} (shrK B)|}             \
   1.443  \                   : set_of_list evs";
   1.444 -be rev_mp 1;
   1.445 -be yahalom.induct 1;
   1.446 -by (dresolve_tac [YM4_analz_sees_Enemy] 6);
   1.447 +by (etac rev_mp 1);
   1.448 +by (etac yahalom.induct 1);
   1.449 +by (dtac YM4_analz_sees_Spy 6);
   1.450  by (ALLGOALS Asm_simp_tac);
   1.451  by (ALLGOALS (fast_tac (!claset addSDs [impOfSubs analz_subset_parts RS
   1.452 -					Crypt_imp_Server_msg])));
   1.453 +                                        Crypt_imp_Server_msg])));
   1.454  qed "YM4_imp_Says_Server_A";
   1.455  
   1.456  
   1.457 @@ -400,8 +400,8 @@
   1.458  goal thy 
   1.459   "!!evs. [| Says A' B {|Crypt {|Agent A, Key K|} (shrK B),              \
   1.460  \                       Crypt (Nonce NB) K|} : set_of_list evs;         \
   1.461 -\           A ~: bad;  B ~: bad;  evs : yahalom |]                      \
   1.462 -\        ==> Key K ~: analz (sees Enemy evs)";
   1.463 +\           A ~: lost;  B ~: lost;  evs : yahalom lost |]                      \
   1.464 +\        ==> Key K ~: analz (sees lost Spy evs)";
   1.465  by (fast_tac (!claset addSDs [YM4_imp_Says_Server_A,
   1.466 -			      Enemy_not_see_encrypted_key]) 1);
   1.467 +                              Spy_not_see_encrypted_key]) 1);
   1.468  qed "B_gets_secure_key";