src/HOL/Auth/OtwayRees.ML
changeset 2032 1bbf1bdcaf56
parent 2026 0df5a96bf77e
child 2045 ae1030e66745
     1.1 --- a/src/HOL/Auth/OtwayRees.ML	Thu Sep 26 12:47:47 1996 +0200
     1.2 +++ b/src/HOL/Auth/OtwayRees.ML	Thu Sep 26 12:50:48 1996 +0200
     1.3 @@ -22,11 +22,11 @@
     1.4  (*Weak liveness: there are traces that reach the end*)
     1.5  goal thy 
     1.6   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
     1.7 -\        ==> EX K. EX NA. EX evs: otway.          \
     1.8 +\        ==> EX K. EX NA. EX evs: otway lost.          \
     1.9  \               Says B A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|} \
    1.10  \                 : set_of_list evs";
    1.11  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.12 -br (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2;
    1.13 +by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
    1.14  by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
    1.15  by (REPEAT_FIRST (resolve_tac [refl, conjI]));
    1.16  by (ALLGOALS (fast_tac (!claset addss (!simpset setsolver safe_solver))));
    1.17 @@ -35,19 +35,37 @@
    1.18  
    1.19  (**** Inductive proofs about otway ****)
    1.20  
    1.21 -(*The Enemy can see more than anybody else, except for their initial state*)
    1.22 +goal thy "!!evs. lost' <= lost ==> otway lost' <= otway lost";
    1.23 +by (rtac subsetI 1);
    1.24 +by (etac otway.induct 1);
    1.25 +by (REPEAT_FIRST
    1.26 +    (best_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
    1.27 +                              :: otway.intrs))));
    1.28 +qed "otway_mono";
    1.29 +
    1.30 +
    1.31 +(*The Spy can see more than anybody else, except for their initial state*)
    1.32  goal thy 
    1.33 - "!!evs. evs : otway ==> \
    1.34 -\     sees A evs <= initState A Un sees Enemy evs";
    1.35 -be otway.induct 1;
    1.36 + "!!evs. evs : otway lost ==> \
    1.37 +\     sees lost A evs <= initState lost A Un sees lost Spy evs";
    1.38 +by (etac otway.induct 1);
    1.39  by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] 
    1.40 -			        addss (!simpset))));
    1.41 -qed "sees_agent_subset_sees_Enemy";
    1.42 +                                addss (!simpset))));
    1.43 +qed "sees_agent_subset_sees_Spy";
    1.44 +
    1.45 +(*The Spy can see more than anybody else who's lost their key!*)
    1.46 +goal thy 
    1.47 + "!!evs. evs : otway lost ==> \
    1.48 +\        A: lost --> A ~= Server --> sees lost A evs <= sees lost Spy evs";
    1.49 +by (etac otway.induct 1);
    1.50 +by (agent.induct_tac "A" 1);
    1.51 +by (auto_tac (!claset addDs [sees_Says_subset_insert RS subsetD], (!simpset)));
    1.52 +qed_spec_mp "sees_lost_agent_subset_sees_Spy";
    1.53  
    1.54  
    1.55  (*Nobody sends themselves messages*)
    1.56 -goal thy "!!evs. evs : otway ==> ALL A X. Says A A X ~: set_of_list evs";
    1.57 -be otway.induct 1;
    1.58 +goal thy "!!evs. evs : otway lost ==> ALL A X. Says A A X ~: set_of_list evs";
    1.59 +by (etac otway.induct 1);
    1.60  by (Auto_tac());
    1.61  qed_spec_mp "not_Says_to_self";
    1.62  Addsimps [not_Says_to_self];
    1.63 @@ -57,69 +75,78 @@
    1.64  (** For reasoning about the encrypted portion of messages **)
    1.65  
    1.66  goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set_of_list evs ==> \
    1.67 -\                X : analz (sees Enemy evs)";
    1.68 -by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]) 1);
    1.69 -qed "OR2_analz_sees_Enemy";
    1.70 +\                X : analz (sees lost Spy evs)";
    1.71 +by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    1.72 +qed "OR2_analz_sees_Spy";
    1.73  
    1.74  goal thy "!!evs. Says S B {|N, X, X'|} : set_of_list evs ==> \
    1.75 -\                X : analz (sees Enemy evs)";
    1.76 -by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]) 1);
    1.77 -qed "OR4_analz_sees_Enemy";
    1.78 +\                X : analz (sees lost Spy evs)";
    1.79 +by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    1.80 +qed "OR4_analz_sees_Spy";
    1.81  
    1.82  goal thy "!!evs. Says B' A {|N, Crypt {|N,K|} K'|} : set_of_list evs ==> \
    1.83 -\                K : parts (sees Enemy evs)";
    1.84 +\                K : parts (sees lost Spy evs)";
    1.85  by (fast_tac (!claset addSEs partsEs
    1.86 -	              addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
    1.87 -qed "Reveal_parts_sees_Enemy";
    1.88 +                      addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
    1.89 +qed "Reveal_parts_sees_Spy";
    1.90  
    1.91  (*OR2_analz... and OR4_analz... let us treat those cases using the same 
    1.92    argument as for the Fake case.  This is possible for most, but not all,
    1.93    proofs: Fake does not invent new nonces (as in OR2), and of course Fake
    1.94 -  messages originate from the Enemy. *)
    1.95 +  messages originate from the Spy. *)
    1.96  
    1.97 +bind_thm ("OR2_parts_sees_Spy",
    1.98 +          OR2_analz_sees_Spy RS (impOfSubs analz_subset_parts));
    1.99 +bind_thm ("OR4_parts_sees_Spy",
   1.100 +          OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
   1.101 +
   1.102 +(*We instantiate the variable to "lost".  Leaving it as a Var makes proofs
   1.103 +  harder to complete, since simplification does less for us.*)
   1.104  val parts_Fake_tac = 
   1.105 -    forward_tac [OR2_analz_sees_Enemy RS (impOfSubs analz_subset_parts)] 4 THEN
   1.106 -    forward_tac [OR4_analz_sees_Enemy RS (impOfSubs analz_subset_parts)] 6 THEN
   1.107 -    forward_tac [Reveal_parts_sees_Enemy] 7;
   1.108 +    let val tac = forw_inst_tac [("lost","lost")] 
   1.109 +    in  tac OR2_parts_sees_Spy 4 THEN 
   1.110 +        tac OR4_parts_sees_Spy 6 THEN
   1.111 +        tac Reveal_parts_sees_Spy 7
   1.112 +    end;
   1.113  
   1.114  
   1.115 -(** Theorems of the form X ~: parts (sees Enemy evs) imply that NOBODY
   1.116 +(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
   1.117      sends messages containing X! **)
   1.118  
   1.119 -(*Enemy never sees another agent's shared key! (unless it is leaked at start)*)
   1.120 +(*Spy never sees lost another agent's shared key! (unless it is leaked at start)*)
   1.121  goal thy 
   1.122 - "!!evs. [| evs : otway;  A ~: bad |]    \
   1.123 -\        ==> Key (shrK A) ~: parts (sees Enemy evs)";
   1.124 -be otway.induct 1;
   1.125 + "!!evs. [| evs : otway lost;  A ~: lost |]    \
   1.126 +\        ==> Key (shrK A) ~: parts (sees lost Spy evs)";
   1.127 +by (etac otway.induct 1);
   1.128  by parts_Fake_tac;
   1.129  by (Auto_tac());
   1.130  (*Deals with Fake message*)
   1.131  by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   1.132 -			     impOfSubs Fake_parts_insert]) 1);
   1.133 -qed "Enemy_not_see_shrK";
   1.134 +                             impOfSubs Fake_parts_insert]) 1);
   1.135 +qed "Spy_not_see_shrK";
   1.136  
   1.137 -bind_thm ("Enemy_not_analz_shrK",
   1.138 -	  [analz_subset_parts, Enemy_not_see_shrK] MRS contra_subsetD);
   1.139 +bind_thm ("Spy_not_analz_shrK",
   1.140 +          [analz_subset_parts, Spy_not_see_shrK] MRS contra_subsetD);
   1.141  
   1.142 -Addsimps [Enemy_not_see_shrK, Enemy_not_analz_shrK];
   1.143 +Addsimps [Spy_not_see_shrK, Spy_not_analz_shrK];
   1.144  
   1.145  (*We go to some trouble to preserve R in the 3rd and 4th subgoals
   1.146    As usual fast_tac cannot be used because it uses the equalities too soon*)
   1.147  val major::prems = 
   1.148 -goal thy  "[| Key (shrK A) : parts (sees Enemy evs);       \
   1.149 -\             evs : otway;                                 \
   1.150 -\             A:bad ==> R                                  \
   1.151 +goal thy  "[| Key (shrK A) : parts (sees lost Spy evs);       \
   1.152 +\             evs : otway lost;                                 \
   1.153 +\             A:lost ==> R                                  \
   1.154  \           |] ==> R";
   1.155 -br ccontr 1;
   1.156 -br ([major, Enemy_not_see_shrK] MRS rev_notE) 1;
   1.157 +by (rtac ccontr 1);
   1.158 +by (rtac ([major, Spy_not_see_shrK] MRS rev_notE) 1);
   1.159  by (swap_res_tac prems 2);
   1.160  by (ALLGOALS (fast_tac (!claset addIs prems)));
   1.161 -qed "Enemy_see_shrK_E";
   1.162 +qed "Spy_see_shrK_E";
   1.163  
   1.164 -bind_thm ("Enemy_analz_shrK_E", 
   1.165 -	  analz_subset_parts RS subsetD RS Enemy_see_shrK_E);
   1.166 +bind_thm ("Spy_analz_shrK_E", 
   1.167 +          analz_subset_parts RS subsetD RS Spy_see_shrK_E);
   1.168  
   1.169 -AddSEs [Enemy_see_shrK_E, Enemy_analz_shrK_E];
   1.170 +AddSEs [Spy_see_shrK_E, Spy_analz_shrK_E];
   1.171  
   1.172  
   1.173  (*** Future keys can't be seen or used! ***)
   1.174 @@ -129,23 +156,23 @@
   1.175    but should go by similar reasoning every time.  Hardest case is the
   1.176    standard Fake rule.  
   1.177        The Union over C is essential for the induction! *)
   1.178 -goal thy "!!evs. evs : otway ==> \
   1.179 +goal thy "!!evs. evs : otway lost ==> \
   1.180  \                length evs <= length evs' --> \
   1.181 -\                          Key (newK evs') ~: (UN C. parts (sees C evs))";
   1.182 -be otway.induct 1;
   1.183 +\                          Key (newK evs') ~: (UN C. parts (sees lost C evs))";
   1.184 +by (etac otway.induct 1);
   1.185  by parts_Fake_tac;
   1.186  (*auto_tac does not work here, as it performs safe_tac first*)
   1.187  by (ALLGOALS Asm_simp_tac);
   1.188  by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   1.189 -					   impOfSubs parts_insert_subset_Un,
   1.190 -					   Suc_leD]
   1.191 -			            addss (!simpset))));
   1.192 +                                           impOfSubs parts_insert_subset_Un,
   1.193 +                                           Suc_leD]
   1.194 +                                    addss (!simpset))));
   1.195  val lemma = result();
   1.196  
   1.197  (*Variant needed for the main theorem below*)
   1.198  goal thy 
   1.199 - "!!evs. [| evs : otway;  length evs <= length evs' |]    \
   1.200 -\        ==> Key (newK evs') ~: parts (sees C evs)";
   1.201 + "!!evs. [| evs : otway lost;  length evs <= length evs' |]    \
   1.202 +\        ==> Key (newK evs') ~: parts (sees lost C evs)";
   1.203  by (fast_tac (!claset addDs [lemma]) 1);
   1.204  qed "new_keys_not_seen";
   1.205  Addsimps [new_keys_not_seen];
   1.206 @@ -154,37 +181,37 @@
   1.207  goal thy 
   1.208   "!!evs. [| Says A B X : set_of_list evs;  \
   1.209  \           Key (newK evt) : parts {X};    \
   1.210 -\           evs : otway                 \
   1.211 +\           evs : otway lost                 \
   1.212  \        |] ==> length evt < length evs";
   1.213 -br ccontr 1;
   1.214 -bd leI 1;
   1.215 -by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Enemy]
   1.216 +by (rtac ccontr 1);
   1.217 +by (dtac leI 1);
   1.218 +by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
   1.219                        addIs  [impOfSubs parts_mono]) 1);
   1.220  qed "Says_imp_old_keys";
   1.221  
   1.222  
   1.223  (*** Future nonces can't be seen or used! [proofs resemble those above] ***)
   1.224  
   1.225 -goal thy "!!evs. evs : otway ==> \
   1.226 +goal thy "!!evs. evs : otway lost ==> \
   1.227  \                length evs <= length evt --> \
   1.228 -\                          Nonce (newN evt) ~: (UN C. parts (sees C evs))";
   1.229 -be otway.induct 1;
   1.230 +\                Nonce (newN evt) ~: (UN C. parts (sees lost C evs))";
   1.231 +by (etac otway.induct 1);
   1.232  (*auto_tac does not work here, as it performs safe_tac first*)
   1.233 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [ parts_insert2]
   1.234 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert2]
   1.235                                       addcongs [disj_cong])));
   1.236  by (REPEAT_FIRST (fast_tac (!claset 
   1.237 -			      addSEs partsEs
   1.238 -			      addSDs  [Says_imp_sees_Enemy RS parts.Inj]
   1.239 -			      addDs  [impOfSubs analz_subset_parts,
   1.240 -				      impOfSubs parts_insert_subset_Un,
   1.241 -				      Suc_leD]
   1.242 -			      addss (!simpset))));
   1.243 +                              addSEs partsEs
   1.244 +                              addSDs  [Says_imp_sees_Spy RS parts.Inj]
   1.245 +                              addDs  [impOfSubs analz_subset_parts,
   1.246 +                                      impOfSubs parts_insert_subset_Un,
   1.247 +                                      Suc_leD]
   1.248 +                              addss (!simpset))));
   1.249  val lemma = result();
   1.250  
   1.251  (*Variant needed for the main theorem below*)
   1.252  goal thy 
   1.253 - "!!evs. [| evs : otway;  length evs <= length evs' |]    \
   1.254 -\        ==> Nonce (newN evs') ~: parts (sees C evs)";
   1.255 + "!!evs. [| evs : otway lost;  length evs <= length evs' |]    \
   1.256 +\        ==> Nonce (newN evs') ~: parts (sees lost C evs)";
   1.257  by (fast_tac (!claset addDs [lemma]) 1);
   1.258  qed "new_nonces_not_seen";
   1.259  Addsimps [new_nonces_not_seen];
   1.260 @@ -193,21 +220,21 @@
   1.261  goal thy 
   1.262   "!!evs. [| Says A B X : set_of_list evs;  \
   1.263  \           Nonce (newN evt) : parts {X};    \
   1.264 -\           evs : otway                 \
   1.265 +\           evs : otway lost                 \
   1.266  \        |] ==> length evt < length evs";
   1.267 -br ccontr 1;
   1.268 -bd leI 1;
   1.269 -by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Enemy]
   1.270 -	              addIs  [impOfSubs parts_mono]) 1);
   1.271 +by (rtac ccontr 1);
   1.272 +by (dtac leI 1);
   1.273 +by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Spy]
   1.274 +                      addIs  [impOfSubs parts_mono]) 1);
   1.275  qed "Says_imp_old_nonces";
   1.276  
   1.277  
   1.278  (*Nobody can have USED keys that will be generated in the future.
   1.279    ...very like new_keys_not_seen*)
   1.280 -goal thy "!!evs. evs : otway ==> \
   1.281 +goal thy "!!evs. evs : otway lost ==> \
   1.282  \                length evs <= length evs' --> \
   1.283 -\                newK evs' ~: keysFor (UN C. parts (sees C evs))";
   1.284 -be otway.induct 1;
   1.285 +\                newK evs' ~: keysFor (UN C. parts (sees lost C evs))";
   1.286 +by (etac otway.induct 1);
   1.287  by parts_Fake_tac;
   1.288  by (ALLGOALS Asm_simp_tac);
   1.289  (*OR1 and OR3*)
   1.290 @@ -217,26 +244,26 @@
   1.291      (map
   1.292       (best_tac
   1.293        (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   1.294 -		      impOfSubs (parts_insert_subset_Un RS keysFor_mono),
   1.295 -		      Suc_leD]
   1.296 -	       addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
   1.297 -	       addss (!simpset)))
   1.298 +                      impOfSubs (parts_insert_subset_Un RS keysFor_mono),
   1.299 +                      Suc_leD]
   1.300 +               addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
   1.301 +               addss (!simpset)))
   1.302       [3,2,1]));
   1.303  (*Reveal: dummy message*)
   1.304  by (best_tac (!claset addEs  [new_keys_not_seen RSN(2,rev_notE)]
   1.305 -		      addIs  [less_SucI, impOfSubs keysFor_mono]
   1.306 -		      addss (!simpset addsimps [le_def])) 1);
   1.307 +                      addIs  [less_SucI, impOfSubs keysFor_mono]
   1.308 +                      addss (!simpset addsimps [le_def])) 1);
   1.309  val lemma = result();
   1.310  
   1.311  goal thy 
   1.312 - "!!evs. [| evs : otway;  length evs <= length evs' |]    \
   1.313 -\        ==> newK evs' ~: keysFor (parts (sees C evs))";
   1.314 + "!!evs. [| evs : otway lost;  length evs <= length evs' |]    \
   1.315 +\        ==> newK evs' ~: keysFor (parts (sees lost C evs))";
   1.316  by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
   1.317  qed "new_keys_not_used";
   1.318  
   1.319  bind_thm ("new_keys_not_analzd",
   1.320 -	  [analz_subset_parts RS keysFor_mono,
   1.321 -	   new_keys_not_used] MRS contra_subsetD);
   1.322 +          [analz_subset_parts RS keysFor_mono,
   1.323 +           new_keys_not_used] MRS contra_subsetD);
   1.324  
   1.325  Addsimps [new_keys_not_used, new_keys_not_analzd];
   1.326  
   1.327 @@ -247,8 +274,8 @@
   1.328  (****
   1.329   The following is to prove theorems of the form
   1.330  
   1.331 -          Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) ==>
   1.332 -          Key K : analz (sees Enemy evs)
   1.333 +          Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) ==>
   1.334 +          Key K : analz (sees lost Spy evs)
   1.335  
   1.336   A more general formula must be proved inductively.
   1.337  
   1.338 @@ -259,15 +286,15 @@
   1.339    to encrypt messages containing other keys, in the actual protocol.
   1.340    We require that agents should behave like this subsequently also.*)
   1.341  goal thy 
   1.342 - "!!evs. evs : otway ==> \
   1.343 -\        (Crypt X (newK evt)) : parts (sees Enemy evs) & \
   1.344 -\        Key K : parts {X} --> Key K : parts (sees Enemy evs)";
   1.345 -be otway.induct 1;
   1.346 + "!!evs. evs : otway lost ==> \
   1.347 +\        (Crypt X (newK evt)) : parts (sees lost Spy evs) & \
   1.348 +\        Key K : parts {X} --> Key K : parts (sees lost Spy evs)";
   1.349 +by (etac otway.induct 1);
   1.350  by parts_Fake_tac;
   1.351 -by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes)));
   1.352 +by (ALLGOALS Asm_simp_tac);
   1.353  (*Deals with Faked messages*)
   1.354  by (best_tac (!claset addSEs partsEs
   1.355 -		      addDs [impOfSubs parts_insert_subset_Un]
   1.356 +                      addDs [impOfSubs parts_insert_subset_Un]
   1.357                        addss (!simpset)) 2);
   1.358  (*Base case and Reveal*)
   1.359  by (Auto_tac());
   1.360 @@ -282,8 +309,8 @@
   1.361  Delsimps [image_Un];
   1.362  Addsimps [image_Un RS sym];
   1.363  
   1.364 -goal thy "insert (Key (newK x)) (sees A evs) = \
   1.365 -\         Key `` (newK``{x}) Un (sees A evs)";
   1.366 +goal thy "insert (Key (newK x)) (sees lost A evs) = \
   1.367 +\         Key `` (newK``{x}) Un (sees lost A evs)";
   1.368  by (Fast_tac 1);
   1.369  val insert_Key_singleton = result();
   1.370  
   1.371 @@ -295,10 +322,10 @@
   1.372  
   1.373  (*This lets us avoid analyzing the new message -- unless we have to!*)
   1.374  (*NEEDED??*)
   1.375 -goal thy "synth (analz (sees Enemy evs)) <=   \
   1.376 -\         synth (analz (sees Enemy (Says A B X # evs)))";
   1.377 +goal thy "synth (analz (sees lost Spy evs)) <=   \
   1.378 +\         synth (analz (sees lost Spy (Says A B X # evs)))";
   1.379  by (Simp_tac 1);
   1.380 -br (subset_insertI RS analz_mono RS synth_mono) 1;
   1.381 +by (rtac (subset_insertI RS analz_mono RS synth_mono) 1);
   1.382  qed "synth_analz_thin";
   1.383  
   1.384  AddIs [impOfSubs synth_analz_thin];
   1.385 @@ -312,16 +339,17 @@
   1.386    assumptions on A are needed to prevent its being a Faked message.  (Based
   1.387    on NS_Shared/Says_S_message_form) *)
   1.388  goal thy
   1.389 - "!!evs. evs: otway ==>                                           \
   1.390 -\          Crypt {|N, Key K|} (shrK A) : parts (sees Enemy evs) & \
   1.391 -\          A ~: bad -->                                           \
   1.392 -\        (EX evt:otway. K = newK evt)";
   1.393 -be otway.induct 1;
   1.394 + "!!evs. evs: otway lost ==>                                           \
   1.395 +\          Crypt {|N, Key K|} (shrK A) : parts (sees lost Spy evs) & \
   1.396 +\          A ~: lost -->                                           \
   1.397 +\        (EX evt: otway lost. K = newK evt)";
   1.398 +by (etac otway.induct 1);
   1.399  by parts_Fake_tac;
   1.400 -by (Auto_tac());
   1.401 +by (ALLGOALS Asm_simp_tac);
   1.402  (*Deals with Fake message*)
   1.403  by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   1.404 -			     impOfSubs Fake_parts_insert]) 1);
   1.405 +                             impOfSubs Fake_parts_insert]) 2);
   1.406 +by (Auto_tac());
   1.407  val lemma = result() RS mp;
   1.408  
   1.409  
   1.410 @@ -329,14 +357,14 @@
   1.411    OR     reduces it to the Fake case.*)
   1.412  goal thy 
   1.413   "!!evs. [| Says B' A {|N, Crypt {|N, Key K|} (shrK A)|} : set_of_list evs;  \
   1.414 -\           evs : otway |]                      \
   1.415 -\        ==> (EX evt:otway. K = newK evt) | Key K : analz (sees Enemy evs)";
   1.416 -by (excluded_middle_tac "A : bad" 1);
   1.417 -by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]
   1.418 -	              addss (!simpset)) 2);
   1.419 +\           evs : otway lost |]                      \
   1.420 +\        ==> (EX evt: otway lost. K = newK evt) | Key K : analz (sees lost Spy evs)";
   1.421 +by (excluded_middle_tac "A : lost" 1);
   1.422 +by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
   1.423 +                      addss (!simpset)) 2);
   1.424  by (forward_tac [lemma] 1);
   1.425  by (fast_tac (!claset addEs  partsEs
   1.426 -	              addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
   1.427 +                      addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
   1.428  by (Fast_tac 1);
   1.429  qed "Reveal_message_form";
   1.430  
   1.431 @@ -352,34 +380,34 @@
   1.432  
   1.433  (*The equality makes the induction hypothesis easier to apply*)
   1.434  goal thy  
   1.435 - "!!evs. evs : otway ==> \
   1.436 -\  ALL K E. (Key K : analz (Key``(newK``E) Un (sees Enemy evs))) = \
   1.437 -\           (K : newK``E | Key K : analz (sees Enemy evs))";
   1.438 -be otway.induct 1;
   1.439 -bd OR2_analz_sees_Enemy 4;
   1.440 -bd OR4_analz_sees_Enemy 6;
   1.441 -bd Reveal_message_form 7;
   1.442 + "!!evs. evs : otway lost ==> \
   1.443 +\  ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \
   1.444 +\           (K : newK``E | Key K : analz (sees lost Spy evs))";
   1.445 +by (etac otway.induct 1);
   1.446 +by (dtac OR2_analz_sees_Spy 4);
   1.447 +by (dtac OR4_analz_sees_Spy 6);
   1.448 +by (dtac Reveal_message_form 7);
   1.449  by (REPEAT_FIRST (ares_tac [allI, lemma]));
   1.450  by (REPEAT ((eresolve_tac [bexE, disjE] ORELSE' hyp_subst_tac) 7));
   1.451  by (ALLGOALS (*Takes 28 secs*)
   1.452      (asm_simp_tac 
   1.453       (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
   1.454 -			 @ pushes)
   1.455 +                         @ pushes)
   1.456                 setloop split_tac [expand_if])));
   1.457  (** LEVEL 7 **)
   1.458  (*Reveal case 2, OR4, OR2, Fake*) 
   1.459 -by (EVERY (map enemy_analz_tac [7,5,3,2]));
   1.460 +by (EVERY (map spy_analz_tac [7,5,3,2]));
   1.461  (*Reveal case 1, OR3, Base*)
   1.462  by (Auto_tac());
   1.463  qed_spec_mp "analz_image_newK";
   1.464  
   1.465  
   1.466  goal thy
   1.467 - "!!evs. evs : otway ==>                               \
   1.468 -\        Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) = \
   1.469 -\        (K = newK evt | Key K : analz (sees Enemy evs))";
   1.470 + "!!evs. evs : otway lost ==>                               \
   1.471 +\        Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) = \
   1.472 +\        (K = newK evt | Key K : analz (sees lost Spy evs))";
   1.473  by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
   1.474 -				   insert_Key_singleton]) 1);
   1.475 +                                   insert_Key_singleton]) 1);
   1.476  by (Fast_tac 1);
   1.477  qed "analz_insert_Key_newK";
   1.478  
   1.479 @@ -389,13 +417,13 @@
   1.480  fun ex_strip_tac i = REPEAT (ares_tac [exI, conjI] i) THEN assume_tac (i+1);
   1.481  
   1.482  goal thy 
   1.483 - "!!evs. evs : otway ==>                      \
   1.484 + "!!evs. evs : otway lost ==>                      \
   1.485  \      EX A' B' NA' NB'. ALL A B NA NB.                    \
   1.486  \       Says Server B \
   1.487  \            {|NA, Crypt {|NA, K|} (shrK A),                      \
   1.488  \                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs --> \
   1.489  \       A=A' & B=B' & NA=NA' & NB=NB'";
   1.490 -be otway.induct 1;
   1.491 +by (etac otway.induct 1);
   1.492  by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   1.493  by (Step_tac 1);
   1.494  (*Remaining cases: OR3 and OR4*)
   1.495 @@ -406,8 +434,8 @@
   1.496  by (REPEAT (ares_tac [refl,exI,impI,conjI] 1));
   1.497  (*...we assume X is a very new message, and handle this case by contradiction*)
   1.498  by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
   1.499 -	              delrules [conjI]    (*prevent split-up into 4 subgoals*)
   1.500 -	              addss (!simpset addsimps [parts_insertI])) 1);
   1.501 +                      delrules [conjI]    (*prevent split-up into 4 subgoals*)
   1.502 +                      addss (!simpset addsimps [parts_insertI])) 1);
   1.503  val lemma = result();
   1.504  
   1.505  goal thy 
   1.506 @@ -419,9 +447,9 @@
   1.507  \              {|NA', Crypt {|NA', K|} (shrK A'),                  \
   1.508  \                     Crypt {|NB', K|} (shrK B')|}                 \
   1.509  \            : set_of_list evs;                                    \
   1.510 -\           evs : otway |]                                         \
   1.511 +\           evs : otway lost |]                                         \
   1.512  \        ==> A=A' & B=B' & NA=NA' & NB=NB'";
   1.513 -bd lemma 1;
   1.514 +by (dtac lemma 1);
   1.515  by (REPEAT (etac exE 1));
   1.516  (*Duplicate the assumption*)
   1.517  by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
   1.518 @@ -434,18 +462,18 @@
   1.519  
   1.520  (*Only OR1 can have caused such a part of a message to appear.*)
   1.521  goal thy 
   1.522 - "!!evs. [| A ~: bad;  evs : otway |]               \
   1.523 + "!!evs. [| A ~: lost;  evs : otway lost |]               \
   1.524  \        ==> Crypt {|NA, Agent A, Agent B|} (shrK A)        \
   1.525 -\             : parts (sees Enemy evs) -->                  \
   1.526 +\             : parts (sees lost Spy evs) -->                  \
   1.527  \            Says A B {|NA, Agent A, Agent B,               \
   1.528  \                       Crypt {|NA, Agent A, Agent B|} (shrK A)|}  \
   1.529  \             : set_of_list evs";
   1.530 -be otway.induct 1;
   1.531 +by (etac otway.induct 1);
   1.532  by parts_Fake_tac;
   1.533  by (ALLGOALS Asm_simp_tac);
   1.534  (*Fake*)
   1.535  by (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
   1.536 -			      impOfSubs Fake_parts_insert]) 2);
   1.537 +                              impOfSubs Fake_parts_insert]) 2);
   1.538  by (Auto_tac());
   1.539  qed_spec_mp "Crypt_imp_OR1";
   1.540  
   1.541 @@ -453,16 +481,16 @@
   1.542  (** The Nonce NA uniquely identifies A's  message. **)
   1.543  
   1.544  goal thy 
   1.545 - "!!evs. [| evs : otway; A ~: bad |]               \
   1.546 + "!!evs. [| evs : otway lost; A ~: lost |]               \
   1.547  \ ==> EX B'. ALL B.    \
   1.548 -\        Crypt {|NA, Agent A, Agent B|} (shrK A) : parts (sees Enemy evs) --> \
   1.549 +\        Crypt {|NA, Agent A, Agent B|} (shrK A) : parts (sees lost Spy evs) --> \
   1.550  \        B = B'";
   1.551 -be otway.induct 1;
   1.552 +by (etac otway.induct 1);
   1.553  by parts_Fake_tac;
   1.554  by (ALLGOALS Asm_simp_tac);
   1.555  (*Fake*)
   1.556  by (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
   1.557 -			      impOfSubs Fake_parts_insert]) 2);
   1.558 +                              impOfSubs Fake_parts_insert]) 2);
   1.559  (*Base case*)
   1.560  by (fast_tac (!claset addss (!simpset)) 1);
   1.561  by (Step_tac 1);
   1.562 @@ -471,16 +499,16 @@
   1.563  by (Asm_simp_tac 1);
   1.564  by (Fast_tac 1);
   1.565  by (best_tac (!claset addSEs partsEs
   1.566 -	              addEs  [new_nonces_not_seen RSN(2,rev_notE)]) 1);
   1.567 +                      addEs  [new_nonces_not_seen RSN(2,rev_notE)]) 1);
   1.568  val lemma = result();
   1.569  
   1.570  goal thy 
   1.571 - "!!evs.[| Crypt {|NA, Agent A, Agent B|} (shrK A) : parts (sees Enemy evs); \ 
   1.572 -\          Crypt {|NA, Agent A, Agent C|} (shrK A) : parts (sees Enemy evs); \ 
   1.573 -\          evs : otway;  A ~: bad |]                                         \
   1.574 + "!!evs.[| Crypt {|NA, Agent A, Agent B|} (shrK A) : parts (sees lost Spy evs); \ 
   1.575 +\          Crypt {|NA, Agent A, Agent C|} (shrK A) : parts (sees lost Spy evs); \ 
   1.576 +\          evs : otway lost;  A ~: lost |]                                         \
   1.577  \        ==> B = C";
   1.578 -bd lemma 1;
   1.579 -ba 1;
   1.580 +by (dtac lemma 1);
   1.581 +by (assume_tac 1);
   1.582  by (etac exE 1);
   1.583  (*Duplicate the assumption*)
   1.584  by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
   1.585 @@ -494,22 +522,22 @@
   1.586    OR2 encrypts Nonce NB.  It prevents the attack that can occur in the
   1.587    over-simplified version of this protocol: see OtwayRees_Bad.*)
   1.588  goal thy 
   1.589 - "!!evs. [| A ~: bad;  evs : otway |]                            \
   1.590 + "!!evs. [| A ~: lost;  evs : otway lost |]                            \
   1.591  \        ==> Crypt {|NA, Agent A, Agent B|} (shrK A)             \
   1.592 -\             : parts (sees Enemy evs) -->                       \
   1.593 +\             : parts (sees lost Spy evs) -->                       \
   1.594  \            Crypt {|NA', NA, Agent A', Agent A|} (shrK A)       \
   1.595 -\             ~: parts (sees Enemy evs)";
   1.596 -be otway.induct 1;
   1.597 +\             ~: parts (sees lost Spy evs)";
   1.598 +by (etac otway.induct 1);
   1.599  by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert2])));
   1.600  (*It is hard to generate this proof in a reasonable amount of time*)
   1.601  by (step_tac (!claset addSEs [MPair_parts, nonce_not_seen_now]
   1.602 -                      addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
   1.603 +                      addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
   1.604  by (REPEAT_FIRST (fast_tac (!claset (*40 seconds??*)
   1.605 -			    addSDs  [impOfSubs analz_subset_parts,
   1.606 -				     impOfSubs parts_insert_subset_Un]
   1.607 -			    addss  (!simpset))));
   1.608 +                            addSDs  [impOfSubs analz_subset_parts,
   1.609 +                                     impOfSubs parts_insert_subset_Un]
   1.610 +                            addss  (!simpset))));
   1.611  by (REPEAT_FIRST (fast_tac (!claset 
   1.612 -			      addSEs (partsEs@[nonce_not_seen_now])
   1.613 +                              addSEs (partsEs@[nonce_not_seen_now])
   1.614                                addSDs  [impOfSubs parts_insert_subset_Un]
   1.615                                addss (!simpset))));
   1.616  qed_spec_mp"no_nonce_OR1_OR2";
   1.617 @@ -519,8 +547,8 @@
   1.618  (*If the encrypted message appears, and A has used Nonce NA to start a run,
   1.619    then it originated with the Server!*)
   1.620  goal thy 
   1.621 - "!!evs. [| A ~: bad;  evs : otway |]                                        \
   1.622 -\        ==> Crypt {|Nonce NA, Key K|} (shrK A) : parts (sees Enemy evs) --> \
   1.623 + "!!evs. [| A ~: lost;  A ~= Spy;  evs : otway lost |]                     \
   1.624 +\        ==> Crypt {|Nonce NA, Key K|} (shrK A) : parts (sees lost Spy evs) --> \
   1.625  \            Says A B {|Nonce NA, Agent A, Agent B,                          \
   1.626  \                       Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|}      \
   1.627  \             : set_of_list evs -->                                          \
   1.628 @@ -529,43 +557,43 @@
   1.629  \                   Crypt {|Nonce NA, Key K|} (shrK A),                      \
   1.630  \                   Crypt {|Nonce NB, Key K|} (shrK B)|}                     \
   1.631  \                   : set_of_list evs)";
   1.632 -be otway.induct 1;
   1.633 +by (etac otway.induct 1);
   1.634  by parts_Fake_tac;
   1.635  by (ALLGOALS Asm_simp_tac);
   1.636  (*Fake*)
   1.637  by (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
   1.638 -			      impOfSubs Fake_parts_insert]) 1);
   1.639 +                              impOfSubs Fake_parts_insert]) 1);
   1.640  (*OR1: it cannot be a new Nonce, contradiction.*)
   1.641  by (fast_tac (!claset addSIs [parts_insertI]
   1.642 -		      addSEs partsEs
   1.643 -		      addEs [Says_imp_old_nonces RS less_irrefl]
   1.644 -	              addss (!simpset)) 1);
   1.645 +                      addSEs partsEs
   1.646 +                      addEs [Says_imp_old_nonces RS less_irrefl]
   1.647 +                      addss (!simpset)) 1);
   1.648  (*OR3 and OR4*)  (** LEVEL 5 **)
   1.649  (*OR4*)
   1.650  by (REPEAT (Safe_step_tac 2));
   1.651  by (REPEAT (best_tac (!claset addSDs [parts_cut]) 3));
   1.652  by (fast_tac (!claset addSIs [Crypt_imp_OR1]
   1.653 -		      addEs  partsEs
   1.654 -	              addDs [Says_imp_sees_Enemy RS parts.Inj]) 2);
   1.655 +                      addEs  partsEs
   1.656 +                      addDs [Says_imp_sees_Spy RS parts.Inj]) 2);
   1.657  (*OR3*)  (** LEVEL 8 **)
   1.658  by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
   1.659  by (step_tac (!claset delrules [disjCI, impCE]) 1);
   1.660 -by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS parts.Inj]
   1.661 +by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
   1.662                        addSEs [MPair_parts]
   1.663                        addEs  [unique_OR1_nonce]) 1);
   1.664  by (fast_tac (!claset addSEs [MPair_parts]
   1.665 -                      addSDs [Says_imp_sees_Enemy RS parts.Inj]
   1.666 +                      addSDs [Says_imp_sees_Spy RS parts.Inj]
   1.667                        addEs  [no_nonce_OR1_OR2 RSN (2, rev_notE)]
   1.668 -	              delrules [conjI] (*stop split-up into 4 subgoals*)) 1);
   1.669 +                      delrules [conjI] (*stop split-up into 4 subgoals*)) 1);
   1.670  qed_spec_mp "Crypt_imp_Server_msg";
   1.671  
   1.672  
   1.673  (*Crucial property: if A receives B's OR4 message and the nonce NA agrees
   1.674    then the key really did come from the Server!  CANNOT prove this of the
   1.675 -  bad form of this protocol, even though we can prove
   1.676 -  Enemy_not_see_encrypted_key*)
   1.677 +  lost form of this protocol, even though we can prove
   1.678 +  Spy_not_see_encrypted_key*)
   1.679  goal thy 
   1.680 - "!!evs. [| A ~: bad;  evs : otway |]                                    \
   1.681 + "!!evs. [| A ~: lost;  A ~= Spy;  evs : otway lost |]                 \
   1.682  \        ==> Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|}  \
   1.683  \             : set_of_list evs -->                                      \
   1.684  \            Says A B {|Nonce NA, Agent A, Agent B,                      \
   1.685 @@ -576,32 +604,30 @@
   1.686  \                       Crypt {|Nonce NA, Key K|} (shrK A),              \
   1.687  \                       Crypt {|Nonce NB, Key K|} (shrK B)|}             \
   1.688  \                       : set_of_list evs)";
   1.689 -be otway.induct 1;
   1.690 +by (etac otway.induct 1);
   1.691  by (ALLGOALS (asm_simp_tac (!simpset addcongs [conj_cong])));
   1.692  (*OR2*)
   1.693  by (Fast_tac 3);
   1.694  (*OR1: it cannot be a new Nonce, contradiction.*)
   1.695  by (fast_tac (!claset addSIs [parts_insertI]
   1.696 -		      addEs [Says_imp_old_nonces RS less_irrefl]
   1.697 -	              addss (!simpset)) 2);
   1.698 +                      addEs [Says_imp_old_nonces RS less_irrefl]
   1.699 +                      addss (!simpset)) 2);
   1.700  (*Fake, OR4*) (** LEVEL 4 **)
   1.701  by (step_tac (!claset delrules [impCE]) 1);
   1.702  by (ALLGOALS Asm_simp_tac);
   1.703  by (Fast_tac 4);
   1.704  by (fast_tac (!claset addSIs [Crypt_imp_OR1]
   1.705 -		      addEs  partsEs
   1.706 -	              addDs [Says_imp_sees_Enemy RS parts.Inj]) 3);
   1.707 +                      addEs  partsEs
   1.708 +                      addDs [Says_imp_sees_Spy RS parts.Inj]) 3);
   1.709  (** LEVEL 8 **)
   1.710  (*Still subcases of Fake and OR4*)
   1.711  by (fast_tac (!claset addSIs [Crypt_imp_Server_msg]
   1.712 -	              addDs  [impOfSubs analz_subset_parts]) 1);
   1.713 +                      addDs  [impOfSubs analz_subset_parts]) 1);
   1.714  by (fast_tac (!claset addSIs [Crypt_imp_Server_msg]
   1.715 -	              addEs  partsEs
   1.716 -	              addDs  [Says_imp_sees_Enemy RS parts.Inj]) 1);
   1.717 -val lemma = result();
   1.718 -
   1.719 +                      addEs  partsEs
   1.720 +                      addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
   1.721  val OR4_imp_Says_Server_A = 
   1.722 -    lemma RSN (2, rev_mp) RS mp |> standard;
   1.723 +    result() RSN (2, rev_mp) RS mp |> standard;
   1.724  
   1.725  
   1.726  
   1.727 @@ -610,48 +636,48 @@
   1.728   "!!evs. [| Says Server B \
   1.729  \            {|NA, Crypt {|NA, K|} (shrK A),                      \
   1.730  \                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs;  \
   1.731 -\           evs : otway |]                                        \
   1.732 -\        ==> (EX evt:otway. K = Key(newK evt)) &                  \
   1.733 +\           evs : otway lost |]                                        \
   1.734 +\        ==> (EX evt: otway lost. K = Key(newK evt)) &                  \
   1.735  \            (EX i. NA = Nonce i)";
   1.736 -be rev_mp 1;
   1.737 -be otway.induct 1;
   1.738 +by (etac rev_mp 1);
   1.739 +by (etac otway.induct 1);
   1.740  by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset))));
   1.741  qed "Says_Server_message_form";
   1.742  
   1.743  
   1.744 -(** Crucial secrecy property: Enemy does not see the keys sent in msg OR3 **)
   1.745 +(** Crucial secrecy property: Spy does not see the keys sent in msg OR3 **)
   1.746  
   1.747  goal thy 
   1.748 - "!!evs. [| A ~: bad;  B ~: bad;  evs : otway;  evt : otway |]         \
   1.749 + "!!evs. [| A ~: lost;  B ~: lost;  evs : otway lost;  evt : otway lost |] \
   1.750  \        ==> Says Server B                                             \
   1.751  \              {|Nonce NA, Crypt {|Nonce NA, Key(newK evt)|} (shrK A), \
   1.752  \                Crypt {|NB, Key(newK evt)|} (shrK B)|} : set_of_list evs --> \
   1.753 -\            Says A Enemy {|Nonce NA, Key(newK evt)|} ~: set_of_list evs --> \
   1.754 -\            Key(newK evt) ~: analz (sees Enemy evs)";
   1.755 -be otway.induct 1;
   1.756 -bd OR2_analz_sees_Enemy 4;
   1.757 -bd OR4_analz_sees_Enemy 6;
   1.758 +\            Says A Spy {|Nonce NA, Key(newK evt)|} ~: set_of_list evs --> \
   1.759 +\            Key(newK evt) ~: analz (sees lost Spy evs)";
   1.760 +by (etac otway.induct 1);
   1.761 +by (dtac OR2_analz_sees_Spy 4);
   1.762 +by (dtac OR4_analz_sees_Spy 6);
   1.763  by (forward_tac [Reveal_message_form] 7);
   1.764  by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, disjE] ORELSE' hyp_subst_tac));
   1.765  by (ALLGOALS
   1.766      (asm_full_simp_tac 
   1.767       (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
   1.768 -			  analz_insert_Key_newK] @ pushes)
   1.769 +                          analz_insert_Key_newK] @ pushes)
   1.770                 setloop split_tac [expand_if])));
   1.771  (** LEVEL 6 **)
   1.772  (*OR3*)
   1.773  by (fast_tac (!claset addSIs [parts_insertI]
   1.774 -		      addEs [Says_imp_old_keys RS less_irrefl]
   1.775 -	              addss (!simpset)) 3);
   1.776 +                      addEs [Says_imp_old_keys RS less_irrefl]
   1.777 +                      addss (!simpset)) 3);
   1.778  (*Reveal case 2, OR4, OR2, Fake*) 
   1.779 -by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' enemy_analz_tac));
   1.780 +by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));
   1.781  (*Reveal case 1*) (** LEVEL 8 **)
   1.782 -by (excluded_middle_tac "Aa : bad" 1);
   1.783 -(*But this contradicts Key(newK evt) ~: analz (sees Enemy evsa) *)
   1.784 -bd (Says_imp_sees_Enemy RS analz.Inj) 2;
   1.785 +by (excluded_middle_tac "Aa : lost" 1);
   1.786 +(*But this contradicts Key(newK evt) ~: analz (sees lost Spy evsa) *)
   1.787 +by (dtac (Says_imp_sees_Spy RS analz.Inj) 2);
   1.788  by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 2);
   1.789 -(*So now we have  Aa ~: bad *)
   1.790 -by (dresolve_tac [OR4_imp_Says_Server_A] 1);
   1.791 +(*So now we have  Aa ~: lost *)
   1.792 +by (dtac OR4_imp_Says_Server_A 1);
   1.793  by (REPEAT (assume_tac 1));
   1.794  by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 1);
   1.795  val lemma = result() RS mp RS mp RSN(2,rev_notE);
   1.796 @@ -660,32 +686,46 @@
   1.797   "!!evs. [| Says Server B \
   1.798  \            {|NA, Crypt {|NA, K|} (shrK A),                      \
   1.799  \                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs;  \
   1.800 -\           Says A Enemy {|NA, K|} ~: set_of_list evs;            \
   1.801 -\           A ~: bad;  B ~: bad;  evs : otway |]                  \
   1.802 -\        ==> K ~: analz (sees Enemy evs)";
   1.803 +\           Says A Spy {|NA, K|} ~: set_of_list evs;            \
   1.804 +\           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
   1.805 +\        ==> K ~: analz (sees lost Spy evs)";
   1.806  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   1.807  by (fast_tac (!claset addSEs [lemma]) 1);
   1.808 -qed "Enemy_not_see_encrypted_key";
   1.809 +qed "Spy_not_see_encrypted_key";
   1.810 +
   1.811  
   1.812 +goal thy 
   1.813 + "!!evs. [| C ~: {A,B,Server}; \
   1.814 +\           Says Server B \
   1.815 +\            {|NA, Crypt {|NA, K|} (shrK A),                      \
   1.816 +\                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs;  \
   1.817 +\           Says A Spy {|NA, K|} ~: set_of_list evs;            \
   1.818 +\           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
   1.819 +\        ==> K ~: analz (sees lost C evs)";
   1.820 +by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   1.821 +by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
   1.822 +by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
   1.823 +by (REPEAT_FIRST (fast_tac (!claset addIs [otway_mono RS subsetD])));
   1.824 +qed "Agent_not_see_encrypted_key";
   1.825  
   1.826  
   1.827  (** A session key uniquely identifies a pair of senders in the message
   1.828      encrypted by a good agent C. **)
   1.829  goal thy 
   1.830 - "!!evs. evs : otway ==>                                           \
   1.831 + "!!evs. evs : otway lost ==>                                           \
   1.832  \      EX A B. ALL C N.                                            \
   1.833 -\         C ~: bad -->                                             \
   1.834 -\         Crypt {|N, Key K|} (shrK C) : parts (sees Enemy evs) --> \
   1.835 +\         C ~: lost -->                                             \
   1.836 +\         Crypt {|N, Key K|} (shrK C) : parts (sees lost Spy evs) --> \
   1.837  \         C=A | C=B";
   1.838 -by (Simp_tac 1);	(*Miniscoping*)
   1.839 -be otway.induct 1;
   1.840 -bd OR2_analz_sees_Enemy 4;
   1.841 -bd OR4_analz_sees_Enemy 6;
   1.842 -(*enemy_analz_tac just does not work here: it is an entirely different proof!*)
   1.843 +by (Simp_tac 1);        (*Miniscoping*)
   1.844 +by (etac otway.induct 1);
   1.845 +by (dres_inst_tac [("lost","lost")] OR2_analz_sees_Spy 4);
   1.846 +by (dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6);
   1.847 +(*spy_analz_tac just does not work here: it is an entirely different proof!*)
   1.848  by (ALLGOALS 
   1.849      (asm_simp_tac (!simpset addsimps [all_conj_distrib, ex_disj_distrib,
   1.850 -				      imp_conj_distrib, parts_insert_sees,
   1.851 -				      parts_insert2])));
   1.852 +                                      imp_conj_distrib, parts_insert_sees,
   1.853 +                                      parts_insert2])));
   1.854  by (REPEAT_FIRST (etac exE));
   1.855  (*OR3: extraction of K = newK evsa to global context...*) (** LEVEL 6 **)
   1.856  by (excluded_middle_tac "K = newK evsa" 4);
   1.857 @@ -693,13 +733,16 @@
   1.858  by (REPEAT (ares_tac [exI] 4));
   1.859  (*...we prove this case by contradiction: the key is too new!*)
   1.860  by (fast_tac (!claset addSEs partsEs
   1.861 -		      addEs [Says_imp_old_keys RS less_irrefl]
   1.862 -	              addss (!simpset)) 4);
   1.863 +                      addEs [Says_imp_old_keys RS less_irrefl]
   1.864 +                      addss (!simpset)) 4);
   1.865  (*Base, Fake, OR2, OR4*)
   1.866  by (REPEAT_FIRST ex_strip_tac);
   1.867 -bd synth.Inj 4;
   1.868 -bd synth.Inj 3;
   1.869 +by (dtac synth.Inj 4);
   1.870 +by (dtac synth.Inj 3);
   1.871  (*Now in effect there are three Fake cases*)
   1.872  by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs Fake_parts_insert]
   1.873 -			            addss (!simpset))));
   1.874 +                                    delrules [disjCI, disjE]
   1.875 +                                    addss (!simpset))));
   1.876  qed "key_identifies_senders";
   1.877 +
   1.878 +