Introduction of "lost" argument
authorpaulson
Thu Sep 26 12:50:48 1996 +0200 (1996-09-26)
changeset 20321bbf1bdcaf56
parent 2031 03a843f0f447
child 2033 639de962ded4
Introduction of "lost" argument
Changed Enemy -> Spy
Ran expandshort
src/HOL/Auth/Event.ML
src/HOL/Auth/Event.thy
src/HOL/Auth/Message.ML
src/HOL/Auth/Message.thy
src/HOL/Auth/NS_Shared.ML
src/HOL/Auth/NS_Shared.thy
src/HOL/Auth/OtwayRees.ML
src/HOL/Auth/OtwayRees.thy
src/HOL/Auth/OtwayRees_Bad.ML
src/HOL/Auth/OtwayRees_Bad.thy
src/HOL/Auth/Shared.ML
src/HOL/Auth/Shared.thy
src/HOL/Auth/Yahalom.ML
src/HOL/Auth/Yahalom.thy
     1.1 --- a/src/HOL/Auth/Event.ML	Thu Sep 26 12:47:47 1996 +0200
     1.2 +++ b/src/HOL/Auth/Event.ML	Thu Sep 26 12:50:48 1996 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  Datatype of events;
     1.5  inductive relation "traces" for Needham-Schroeder (shared keys)
     1.6  
     1.7 -Rewrites should not refer to	 initState (Friend i)    -- not in normal form
     1.8 +Rewrites should not refer to     initState (Friend i)    -- not in normal form
     1.9  *)
    1.10  
    1.11  Addsimps [parts_cut_eq];
    1.12 @@ -58,7 +58,7 @@
    1.13  val newN_inject = inj_newN RS injD
    1.14  and newK_inject = inj_newK RS injD;
    1.15  AddSEs [shrK_inject, newN_inject, newK_inject,
    1.16 -	fresh_newK RS notE, fresh_newN RS notE];
    1.17 +        fresh_newK RS notE, fresh_newN RS notE];
    1.18  Addsimps [inj_shrK RS inj_eq, inj_newN RS inj_eq, inj_newK RS inj_eq];
    1.19  Addsimps [fresh_newN, fresh_newK];
    1.20  
    1.21 @@ -75,7 +75,7 @@
    1.22  (*Good for talking about Server's initial state*)
    1.23  goal thy "!!H. H <= Key``E ==> parts H = H";
    1.24  by (Auto_tac ());
    1.25 -be parts.induct 1;
    1.26 +by (etac parts.induct 1);
    1.27  by (ALLGOALS (fast_tac (!claset addss (!simpset))));
    1.28  qed "parts_image_subset";
    1.29  
    1.30 @@ -83,7 +83,7 @@
    1.31  
    1.32  goal thy "!!H. H <= Key``E ==> analz H = H";
    1.33  by (Auto_tac ());
    1.34 -be analz.induct 1;
    1.35 +by (etac analz.induct 1);
    1.36  by (ALLGOALS (fast_tac (!claset addss (!simpset))));
    1.37  qed "analz_image_subset";
    1.38  
    1.39 @@ -118,7 +118,7 @@
    1.40  qed "analz_own_shrK";
    1.41  
    1.42  bind_thm ("parts_own_shrK",
    1.43 -	  [analz_subset_parts, analz_own_shrK] MRS subsetD);
    1.44 +          [analz_subset_parts, analz_own_shrK] MRS subsetD);
    1.45  
    1.46  Addsimps [analz_own_shrK, parts_own_shrK];
    1.47  
    1.48 @@ -130,7 +130,7 @@
    1.49  
    1.50  val Says_tracesE        = mk_cases "Says A B X # evs: traces";
    1.51  val Says_Server_tracesE = mk_cases "Says Server B X # evs: traces";
    1.52 -val Says_Enemy_tracesE  = mk_cases "Says Enemy B X # evs: traces";
    1.53 +val Says_Spy_tracesE  = mk_cases "Says Spy B X # evs: traces";
    1.54  val Says_to_Server_tracesE = mk_cases "Says A Server X # evs: traces";
    1.55  val Notes_tracesE       = mk_cases "Notes A X # evs: traces";
    1.56  
    1.57 @@ -160,9 +160,9 @@
    1.58  by (Asm_simp_tac 1);
    1.59  qed "sees_Friend";
    1.60  
    1.61 -goal thy "sees Enemy (Says A B X # evs) = insert X (sees Enemy evs)";
    1.62 +goal thy "sees Spy (Says A B X # evs) = insert X (sees Spy evs)";
    1.63  by (Simp_tac 1);
    1.64 -qed "sees_Enemy";
    1.65 +qed "sees_Spy";
    1.66  
    1.67  goal thy "sees A (Says A' B X # evs) <= insert X (sees A evs)";
    1.68  by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
    1.69 @@ -178,19 +178,19 @@
    1.70  goal thy "(UN A. parts (sees A (Says B C Y # evs))) = \
    1.71  \         parts {Y} Un (UN A. parts (sees A evs))";
    1.72  by (Step_tac 1);
    1.73 -be rev_mp 1;	(*for some reason, split_tac does not work on assumptions*)
    1.74 +by (etac rev_mp 1);     (*for some reason, split_tac does not work on assumptions*)
    1.75  val ss = (!simpset addsimps [parts_Un, sees_Cons] 
    1.76 -	           setloop split_tac [expand_if]);
    1.77 +                   setloop split_tac [expand_if]);
    1.78  by (ALLGOALS (fast_tac (!claset addss ss)));
    1.79  qed "UN_parts_sees_Says";
    1.80  
    1.81 -goal thy "Says A B X : set_of_list evs --> X : sees Enemy evs";
    1.82 +goal thy "Says A B X : set_of_list evs --> X : sees Spy evs";
    1.83  by (list.induct_tac "evs" 1);
    1.84  by (Auto_tac ());
    1.85 -qed_spec_mp "Says_imp_sees_Enemy";
    1.86 +qed_spec_mp "Says_imp_sees_Spy";
    1.87  
    1.88 -Addsimps [Says_imp_sees_Enemy];
    1.89 -AddIs    [Says_imp_sees_Enemy];
    1.90 +Addsimps [Says_imp_sees_Spy];
    1.91 +AddIs    [Says_imp_sees_Spy];
    1.92  
    1.93  goal thy "initState C <= Key `` range shrK";
    1.94  by (agent.induct_tac "C" 1);
    1.95 @@ -204,7 +204,7 @@
    1.96  by (list.induct_tac "evs" 1);
    1.97  by (ALLGOALS Asm_simp_tac);
    1.98  by (fast_tac (!claset addDs [impOfSubs initState_subset]) 1);
    1.99 -br conjI 1;
   1.100 +by (rtac conjI 1);
   1.101  by (Fast_tac 2);
   1.102  by (event.induct_tac "a" 1);
   1.103  by (ALLGOALS (asm_simp_tac (!simpset addsimps [mem_if])));
   1.104 @@ -212,32 +212,32 @@
   1.105  qed_spec_mp "seesD";
   1.106  
   1.107  
   1.108 -Addsimps [UN_parts_sees_Says, sees_own, sees_Server, sees_Friend, sees_Enemy];
   1.109 -Delsimps [sees_Cons];	(**** NOTE REMOVAL -- laws above are cleaner ****)
   1.110 +Addsimps [UN_parts_sees_Says, sees_own, sees_Server, sees_Friend, sees_Spy];
   1.111 +Delsimps [sees_Cons];   (**** NOTE REMOVAL -- laws above are cleaner ****)
   1.112  
   1.113  
   1.114  (**** Inductive proofs about traces ****)
   1.115  
   1.116 -(*The Enemy can see more than anybody else, except for their initial state*)
   1.117 +(*The Spy can see more than anybody else, except for their initial state*)
   1.118  goal thy 
   1.119   "!!evs. evs : traces ==> \
   1.120 -\     sees A evs <= initState A Un sees Enemy evs";
   1.121 -be traces.induct 1;
   1.122 +\     sees A evs <= initState A Un sees Spy evs";
   1.123 +by (etac traces.induct 1);
   1.124  by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] 
   1.125 -			        addss (!simpset))));
   1.126 -qed "sees_agent_subset_sees_Enemy";
   1.127 +                                addss (!simpset))));
   1.128 +qed "sees_agent_subset_sees_Spy";
   1.129  
   1.130  
   1.131  (*Nobody sends themselves messages*)
   1.132  goal thy "!!evs. evs : traces ==> ALL A X. Says A A X ~: set_of_list evs";
   1.133 -be traces.induct 1;
   1.134 +by (etac traces.induct 1);
   1.135  by (Auto_tac());
   1.136  qed_spec_mp "not_Says_to_self";
   1.137  Addsimps [not_Says_to_self];
   1.138  AddSEs   [not_Says_to_self RSN (2, rev_notE)];
   1.139  
   1.140  goal thy "!!evs. evs : traces ==> Notes A X ~: set_of_list evs";
   1.141 -be traces.induct 1;
   1.142 +by (etac traces.induct 1);
   1.143  by (Auto_tac());
   1.144  qed "not_Notes";
   1.145  Addsimps [not_Notes];
   1.146 @@ -245,60 +245,60 @@
   1.147  
   1.148  
   1.149  goal thy "!!evs. (Says S A (Crypt {|N, B, K, X|} KA)) : set_of_list evs ==> \
   1.150 -\                X : parts (sees Enemy evs)";
   1.151 +\                X : parts (sees Spy evs)";
   1.152  by (fast_tac (!claset addSEs partsEs
   1.153 -	              addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
   1.154 -qed "NS3_msg_in_parts_sees_Enemy";
   1.155 -			      
   1.156 +                      addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
   1.157 +qed "NS3_msg_in_parts_sees_Spy";
   1.158 +                              
   1.159  
   1.160  (*** Server keys are not betrayed ***)
   1.161  
   1.162 -(*Enemy never sees another agent's server key!*)
   1.163 +(*Spy never sees another agent's server key!*)
   1.164  goal thy 
   1.165 - "!!evs. [| evs : traces; A ~= Enemy |] ==> \
   1.166 -\        Key (shrK A) ~: parts (sees Enemy evs)";
   1.167 -be traces.induct 1;
   1.168 -bd NS3_msg_in_parts_sees_Enemy 5;
   1.169 + "!!evs. [| evs : traces; A ~= Spy |] ==> \
   1.170 +\        Key (shrK A) ~: parts (sees Spy evs)";
   1.171 +by (etac traces.induct 1);
   1.172 +by (dtac NS3_msg_in_parts_sees_Spy 5);
   1.173  by (Auto_tac());
   1.174  (*Deals with Fake message*)
   1.175  by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   1.176 -			     impOfSubs synth_analz_parts_insert_subset_Un]) 1);
   1.177 -qed "Enemy_not_see_shrK";
   1.178 +                             impOfSubs synth_analz_parts_insert_subset_Un]) 1);
   1.179 +qed "Spy_not_see_shrK";
   1.180  
   1.181 -bind_thm ("Enemy_not_analz_shrK",
   1.182 -	  [analz_subset_parts, Enemy_not_see_shrK] MRS contra_subsetD);
   1.183 +bind_thm ("Spy_not_analz_shrK",
   1.184 +          [analz_subset_parts, Spy_not_see_shrK] MRS contra_subsetD);
   1.185  
   1.186 -Addsimps [Enemy_not_see_shrK, 
   1.187 -	  not_sym RSN (2, Enemy_not_see_shrK), 
   1.188 -	  Enemy_not_analz_shrK, 
   1.189 -	  not_sym RSN (2, Enemy_not_analz_shrK)];
   1.190 +Addsimps [Spy_not_see_shrK, 
   1.191 +          not_sym RSN (2, Spy_not_see_shrK), 
   1.192 +          Spy_not_analz_shrK, 
   1.193 +          not_sym RSN (2, Spy_not_analz_shrK)];
   1.194  
   1.195  (*We go to some trouble to preserve R in the 3rd subgoal*)
   1.196  val major::prems = 
   1.197 -goal thy  "[| Key (shrK A) : parts (sees Enemy evs);    \
   1.198 +goal thy  "[| Key (shrK A) : parts (sees Spy evs);    \
   1.199  \             evs : traces;                                  \
   1.200 -\             A=Enemy ==> R                                  \
   1.201 +\             A=Spy ==> R                                  \
   1.202  \           |] ==> R";
   1.203 -br ccontr 1;
   1.204 -br ([major, Enemy_not_see_shrK] MRS rev_notE) 1;
   1.205 +by (rtac ccontr 1);
   1.206 +by (rtac ([major, Spy_not_see_shrK] MRS rev_notE) 1);
   1.207  by (swap_res_tac prems 2);
   1.208  by (ALLGOALS (fast_tac (!claset addIs prems)));
   1.209 -qed "Enemy_see_shrK_E";
   1.210 +qed "Spy_see_shrK_E";
   1.211  
   1.212 -bind_thm ("Enemy_analz_shrK_E", 
   1.213 -	  analz_subset_parts RS subsetD RS Enemy_see_shrK_E);
   1.214 +bind_thm ("Spy_analz_shrK_E", 
   1.215 +          analz_subset_parts RS subsetD RS Spy_see_shrK_E);
   1.216  
   1.217  (*Classical reasoner doesn't need the not_sym versions (with swapped ~=) *)
   1.218 -AddSEs [Enemy_see_shrK_E, Enemy_analz_shrK_E];
   1.219 +AddSEs [Spy_see_shrK_E, Spy_analz_shrK_E];
   1.220  
   1.221  
   1.222  (*No Friend will ever see another agent's server key 
   1.223 -  (excluding the Enemy, who might transmit his).
   1.224 +  (excluding the Spy, who might transmit his).
   1.225    The Server, of course, knows all server keys.*)
   1.226  goal thy 
   1.227 - "!!evs. [| evs : traces; A ~= Enemy;  A ~= Friend j |] ==> \
   1.228 + "!!evs. [| evs : traces; A ~= Spy;  A ~= Friend j |] ==> \
   1.229  \        Key (shrK A) ~: parts (sees (Friend j) evs)";
   1.230 -br (sees_agent_subset_sees_Enemy RS parts_mono RS contra_subsetD) 1;
   1.231 +by (rtac (sees_agent_subset_sees_Spy RS parts_mono RS contra_subsetD) 1);
   1.232  by (ALLGOALS Asm_simp_tac);
   1.233  qed "Friend_not_see_shrK";
   1.234  
   1.235 @@ -307,11 +307,11 @@
   1.236  goal thy  
   1.237   "!!evs. evs : traces ==>                                  \
   1.238  \        (Key (shrK A) \
   1.239 -\           : analz (insert (Key (shrK B)) (sees Enemy evs))) =  \
   1.240 -\        (A=B | A=Enemy)";
   1.241 +\           : analz (insert (Key (shrK B)) (sees Spy evs))) =  \
   1.242 +\        (A=B | A=Spy)";
   1.243  by (best_tac (!claset addDs [impOfSubs analz_subset_parts]
   1.244 -		      addIs [impOfSubs (subset_insertI RS analz_mono)]
   1.245 -	              addss (!simpset)) 1);
   1.246 +                      addIs [impOfSubs (subset_insertI RS analz_mono)]
   1.247 +                      addss (!simpset)) 1);
   1.248  qed "shrK_mem_analz";
   1.249  
   1.250  
   1.251 @@ -328,14 +328,14 @@
   1.252  goal thy "!!evs. evs : traces ==> \
   1.253  \                length evs <= length evs' --> \
   1.254  \                          Key (newK evs') ~: (UN C. parts (sees C evs))";
   1.255 -be traces.induct 1;
   1.256 -bd NS3_msg_in_parts_sees_Enemy 5;
   1.257 +by (etac traces.induct 1);
   1.258 +by (dtac NS3_msg_in_parts_sees_Spy 5);
   1.259  (*auto_tac does not work here, as it performs safe_tac first*)
   1.260  by (ALLGOALS Asm_simp_tac);
   1.261  by (ALLGOALS (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   1.262 -				       impOfSubs parts_insert_subset_Un,
   1.263 -				       Suc_leD]
   1.264 -			        addss (!simpset))));
   1.265 +                                       impOfSubs parts_insert_subset_Un,
   1.266 +                                       Suc_leD]
   1.267 +                                addss (!simpset))));
   1.268  val lemma = result();
   1.269  
   1.270  (*Variant needed for the main theorem below*)
   1.271 @@ -352,14 +352,14 @@
   1.272  \           Key (newK evt) : parts {X};    \
   1.273  \           evs : traces                 \
   1.274  \        |] ==> length evt < length evs";
   1.275 -br ccontr 1;
   1.276 -by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Enemy]
   1.277 -	              addIs [impOfSubs parts_mono, leI]) 1);
   1.278 +by (rtac ccontr 1);
   1.279 +by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
   1.280 +                      addIs [impOfSubs parts_mono, leI]) 1);
   1.281  qed "Says_imp_old_keys";
   1.282  
   1.283  
   1.284  goal thy "!!K. newK evs = invKey K ==> newK evs = K";
   1.285 -br (invKey_eq RS iffD1) 1;
   1.286 +by (rtac (invKey_eq RS iffD1) 1);
   1.287  by (Simp_tac 1);
   1.288  val newK_invKey = result();
   1.289  
   1.290 @@ -371,24 +371,24 @@
   1.291  goal thy "!!evs. evs : traces ==> \
   1.292  \                length evs <= length evs' --> \
   1.293  \                newK evs' ~: keysFor (UN C. parts (sees C evs))";
   1.294 -be traces.induct 1;
   1.295 -bd NS3_msg_in_parts_sees_Enemy 5;
   1.296 +by (etac traces.induct 1);
   1.297 +by (dtac NS3_msg_in_parts_sees_Spy 5);
   1.298  by (ALLGOALS Asm_simp_tac);
   1.299  (*NS1 and NS2*)
   1.300  map (by o fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [3,2];
   1.301  (*Fake and NS3*)
   1.302  map (by o best_tac
   1.303       (!claset addSDs [newK_invKey]
   1.304 -	      addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   1.305 -		     impOfSubs (parts_insert_subset_Un RS keysFor_mono),
   1.306 -		     Suc_leD]
   1.307 -	      addEs [new_keys_not_seen RS not_parts_not_analz RSN (2,rev_notE)]
   1.308 -	      addss (!simpset)))
   1.309 +              addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   1.310 +                     impOfSubs (parts_insert_subset_Un RS keysFor_mono),
   1.311 +                     Suc_leD]
   1.312 +              addEs [new_keys_not_seen RS not_parts_not_analz RSN (2,rev_notE)]
   1.313 +              addss (!simpset)))
   1.314      [2,1];
   1.315  (*NS4 and NS5: nonce exchange*)
   1.316  by (ALLGOALS (deepen_tac (!claset addSDs [newK_invKey, Says_imp_old_keys]
   1.317 -	                          addIs  [less_SucI, impOfSubs keysFor_mono]
   1.318 -		                  addss (!simpset addsimps [le_def])) 0));
   1.319 +                                  addIs  [less_SucI, impOfSubs keysFor_mono]
   1.320 +                                  addss (!simpset addsimps [le_def])) 0));
   1.321  val lemma = result();
   1.322  
   1.323  goal thy 
   1.324 @@ -398,8 +398,8 @@
   1.325  qed "new_keys_not_used";
   1.326  
   1.327  bind_thm ("new_keys_not_analzd",
   1.328 -	  [analz_subset_parts RS keysFor_mono,
   1.329 -	   new_keys_not_used] MRS contra_subsetD);
   1.330 +          [analz_subset_parts RS keysFor_mono,
   1.331 +           new_keys_not_used] MRS contra_subsetD);
   1.332  
   1.333  Addsimps [new_keys_not_used, new_keys_not_analzd];
   1.334  
   1.335 @@ -434,14 +434,14 @@
   1.336  \                         X = (Crypt {|K, Agent A|} (shrK B)) & \
   1.337  \                         K' = shrK A & \
   1.338  \                         length evt < length evs)";
   1.339 -be rev_mp 1;
   1.340 -be traces.induct 1;
   1.341 +by (etac rev_mp 1);
   1.342 +by (etac traces.induct 1);
   1.343  by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset))));
   1.344  qed "Says_Server_message_form";
   1.345  
   1.346  (* c ~: keysFor (parts H) ==> c ~: keysFor (analz H) *)
   1.347  bind_thm ("not_parts_not_keysFor_analz", 
   1.348 -	  analz_subset_parts RS keysFor_mono RS contra_subsetD);
   1.349 +          analz_subset_parts RS keysFor_mono RS contra_subsetD);
   1.350  
   1.351  
   1.352  
   1.353 @@ -451,13 +451,13 @@
   1.354  \                 (Crypt {|N, Agent(Friend j), K, X|} K') # evs';  \
   1.355  \           evs : traces;  i~=k                                    \
   1.356  \        |] ==>                                                    \
   1.357 -\     K ~: analz (insert (Key (shrK (Friend k))) (sees Enemy evs))";
   1.358 -be rev_mp 1;
   1.359 -be traces.induct 1;
   1.360 +\     K ~: analz (insert (Key (shrK (Friend k))) (sees Spy evs))";
   1.361 +by (etac rev_mp 1);
   1.362 +by (etac traces.induct 1);
   1.363  by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes)));
   1.364  by (Step_tac 1);
   1.365  by (asm_full_simp_tac (!simpset addsimps[analz_subset_parts RS contra_subsetD]) 1);
   1.366 -val Enemy_not_see_encrypted_key_lemma = result();
   1.367 +val Spy_not_see_encrypted_key_lemma = result();
   1.368  *)
   1.369  
   1.370  
   1.371 @@ -466,44 +466,44 @@
   1.372   "!!evs. evs : traces ==>                             \
   1.373  \        ALL A NA B K X.                            \
   1.374  \            (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) \
   1.375 -\            : parts (sees Enemy evs) & A ~= Enemy  -->   \
   1.376 +\            : parts (sees Spy evs) & A ~= Spy  -->   \
   1.377  \          (EX evt:traces. K = newK evt & \
   1.378  \                          X = (Crypt {|Key K, Agent A|} (shrK B)))";
   1.379 -be traces.induct 1;
   1.380 -bd NS3_msg_in_parts_sees_Enemy 5;
   1.381 +by (etac traces.induct 1);
   1.382 +by (dtac NS3_msg_in_parts_sees_Spy 5);
   1.383  by (Step_tac 1);
   1.384  by (ALLGOALS Asm_full_simp_tac);
   1.385  (*Remaining cases are Fake and NS2*)
   1.386  by (fast_tac (!claset addSDs [spec]) 2);
   1.387  (*Now for the Fake case*)
   1.388  by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   1.389 -			     impOfSubs synth_analz_parts_insert_subset_Un]
   1.390 -	              addss (!simpset)) 1);
   1.391 +                             impOfSubs synth_analz_parts_insert_subset_Un]
   1.392 +                      addss (!simpset)) 1);
   1.393  qed_spec_mp "encrypted_form";
   1.394  
   1.395  
   1.396 -(*For eliminating the A ~= Enemy condition from the previous result*)
   1.397 +(*For eliminating the A ~= Spy condition from the previous result*)
   1.398  goal thy 
   1.399   "!!evs. evs : traces ==>                             \
   1.400  \        ALL S A NA B K X.                            \
   1.401  \            Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) \
   1.402  \            : set_of_list evs  -->   \
   1.403 -\        S = Server | S = Enemy";
   1.404 -be traces.induct 1;
   1.405 +\        S = Server | S = Spy";
   1.406 +by (etac traces.induct 1);
   1.407  by (ALLGOALS Asm_simp_tac);
   1.408  (*We are left with NS3*)
   1.409 -by (subgoal_tac "S = Server | S = Enemy" 1);
   1.410 +by (subgoal_tac "S = Server | S = Spy" 1);
   1.411  (*First justify this assumption!*)
   1.412  by (fast_tac (!claset addSEs [allE, mp] addss (!simpset)) 2);
   1.413  by (Step_tac 1);
   1.414 -bd Says_Server_message_form 1;
   1.415 +by (dtac Says_Server_message_form 1);
   1.416  by (ALLGOALS Full_simp_tac);
   1.417  (*Final case.  Clear out needless quantifiers to speed the following step*)
   1.418  by (eres_inst_tac [("V","ALL x. ?P(x)")] thin_rl 1);
   1.419 -bd encrypted_form 1;
   1.420 -br (parts.Inj RS conjI) 1;
   1.421 +by (dtac encrypted_form 1);
   1.422 +by (rtac (parts.Inj RS conjI) 1);
   1.423  auto();
   1.424 -qed_spec_mp "Server_or_Enemy";
   1.425 +qed_spec_mp "Server_or_Spy";
   1.426  
   1.427  
   1.428  (*Describes the form of X when the following message is sent;
   1.429 @@ -514,12 +514,12 @@
   1.430  \           evs : traces               \
   1.431  \        |] ==> (EX evt:traces. K = newK evt & length evt < length evs & \
   1.432  \                               X = (Crypt {|Key K, Agent A|} (shrK B)))";
   1.433 -by (forward_tac [Server_or_Enemy] 1);
   1.434 -ba 1;
   1.435 +by (forward_tac [Server_or_Spy] 1);
   1.436 +by (assume_tac 1);
   1.437  by (Step_tac 1);
   1.438  by (fast_tac (!claset addSDs [Says_Server_message_form] addss (!simpset)) 1);
   1.439  by (forward_tac [encrypted_form] 1);
   1.440 -br (parts.Inj RS conjI) 1;
   1.441 +by (rtac (parts.Inj RS conjI) 1);
   1.442  by (auto_tac (!claset addIs [Says_imp_old_keys], !simpset));
   1.443  qed "Says_S_message_form";
   1.444  
   1.445 @@ -533,7 +533,7 @@
   1.446  \                               X = (Crypt {|Key K, Agent A|} (shrK B)))";
   1.447  by (forward_tac [traces_eq_ConsE] 1);
   1.448  by (dtac (set_of_list_eqI1 RS Says_S_message_form) 2);
   1.449 -by (Auto_tac());	
   1.450 +by (Auto_tac());        
   1.451  qed "Says_S_message_form_eq";
   1.452  
   1.453  
   1.454 @@ -542,8 +542,8 @@
   1.455   The following is to prove theorems of the form
   1.456  
   1.457            Key K : analz (insert (Key (newK evt)) 
   1.458 -	                   (insert (Key (shrK C)) (sees Enemy evs))) ==>
   1.459 -          Key K : analz (insert (Key (shrK C)) (sees Enemy evs))
   1.460 +                           (insert (Key (shrK C)) (sees Spy evs))) ==>
   1.461 +          Key K : analz (insert (Key (shrK C)) (sees Spy evs))
   1.462  
   1.463   A more general formula must be proved inductively.
   1.464  
   1.465 @@ -555,14 +555,14 @@
   1.466    We require that agents should behave like this subsequently also.*)
   1.467  goal thy 
   1.468   "!!evs. evs : traces ==> \
   1.469 -\        (Crypt X (newK evt)) : parts (sees Enemy evs) & \
   1.470 -\        Key K : parts {X} --> Key K : parts (sees Enemy evs)";
   1.471 -be traces.induct 1;
   1.472 -bd NS3_msg_in_parts_sees_Enemy 5;
   1.473 +\        (Crypt X (newK evt)) : parts (sees Spy evs) & \
   1.474 +\        Key K : parts {X} --> Key K : parts (sees Spy evs)";
   1.475 +by (etac traces.induct 1);
   1.476 +by (dtac NS3_msg_in_parts_sees_Spy 5);
   1.477  by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes)));
   1.478  (*Deals with Faked messages*)
   1.479  by (best_tac (!claset addSEs partsEs
   1.480 -		      addDs [impOfSubs analz_subset_parts,
   1.481 +                      addDs [impOfSubs analz_subset_parts,
   1.482                               impOfSubs parts_insert_subset_Un]
   1.483                        addss (!simpset)) 1);
   1.484  (*NS4 and NS5*)
   1.485 @@ -591,17 +591,17 @@
   1.486  goal thy  
   1.487   "!!evs. evs : traces ==> \
   1.488  \  ALL K E. (Key K : analz (insert (Key (shrK C)) \
   1.489 -\                             (Key``(newK``E) Un (sees Enemy evs)))) = \
   1.490 +\                             (Key``(newK``E) Un (sees Spy evs)))) = \
   1.491  \           (K : newK``E |  \
   1.492  \            Key K : analz (insert (Key (shrK C)) \
   1.493 -\                             (sees Enemy evs)))";
   1.494 -be traces.induct 1;
   1.495 -by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);	
   1.496 +\                             (sees Spy evs)))";
   1.497 +by (etac traces.induct 1);
   1.498 +by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);     
   1.499  by (REPEAT ((eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac) 5));
   1.500  by (ALLGOALS 
   1.501      (asm_simp_tac 
   1.502       (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
   1.503 -			 @ pushes)
   1.504 +                         @ pushes)
   1.505                 setloop split_tac [expand_if])));
   1.506  (*Cases NS2 and NS3!!  Simple, thanks to auto case splits*)
   1.507  by (REPEAT (Fast_tac 3));
   1.508 @@ -615,7 +615,7 @@
   1.509      "Key K : analz \
   1.510  \             (synth \
   1.511  \              (analz (insert (Key (shrK C)) \
   1.512 -\                        (Key``(newK``E) Un (sees Enemy evsa)))))" 1);
   1.513 +\                        (Key``(newK``E) Un (sees Spy evsa)))))" 1);
   1.514  (*First, justify this subgoal*)
   1.515  (*Discard formulae for better speed*)
   1.516  by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2);
   1.517 @@ -631,28 +631,28 @@
   1.518   "!!evs. evs : traces ==>                                  \
   1.519  \        Key K : analz (insert (Key (newK evt))            \
   1.520  \                         (insert (Key (shrK C))      \
   1.521 -\                          (sees Enemy evs))) =            \
   1.522 +\                          (sees Spy evs))) =            \
   1.523  \             (K = newK evt |                              \
   1.524  \              Key K : analz (insert (Key (shrK C))   \
   1.525 -\                               (sees Enemy evs)))";
   1.526 +\                               (sees Spy evs)))";
   1.527  by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
   1.528 -				   insert_Key_singleton]) 1);
   1.529 +                                   insert_Key_singleton]) 1);
   1.530  by (Fast_tac 1);
   1.531  qed "analz_insert_Key_newK";
   1.532  
   1.533  
   1.534  
   1.535  (*This says that the Key, K, uniquely identifies the message.
   1.536 -    But if C=Enemy then he could send all sorts of nonsense.*)
   1.537 +    But if C=Spy then he could send all sorts of nonsense.*)
   1.538  goal thy 
   1.539   "!!evs. evs : traces ==>                      \
   1.540  \      EX X'. ALL C S A Y N B X.               \
   1.541 -\         C ~= Enemy -->                       \
   1.542 +\         C ~= Spy -->                       \
   1.543  \         Says S A Y : set_of_list evs -->     \
   1.544  \         ((Crypt {|N, Agent B, Key K, X|} (shrK C)) : parts{Y} --> \
   1.545  \       (X = X'))";
   1.546 -be traces.induct 1;
   1.547 -by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);	
   1.548 +by (etac traces.induct 1);
   1.549 +by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);     
   1.550  by (ALLGOALS 
   1.551      (asm_simp_tac (!simpset addsimps [all_conj_distrib, imp_conj_distrib])));
   1.552  (*NS2: Case split propagates some context to other subgoal...*)
   1.553 @@ -660,28 +660,28 @@
   1.554  by (Asm_simp_tac 2);
   1.555  (*...we assume X is a very new message, and handle this case by contradiction*)
   1.556  by (fast_tac (!claset addIs [impOfSubs (subset_insertI RS parts_mono)]
   1.557 -		      addSEs partsEs
   1.558 -		      addEs [Says_imp_old_keys RS less_irrefl]
   1.559 -	              addss (!simpset)) 2);
   1.560 +                      addSEs partsEs
   1.561 +                      addEs [Says_imp_old_keys RS less_irrefl]
   1.562 +                      addss (!simpset)) 2);
   1.563  (*NS3: No relevant messages*)
   1.564  by (fast_tac (!claset addSEs [exI] addss (!simpset)) 2);
   1.565  (*Fake*)
   1.566  by (Step_tac 1);
   1.567 -br exI 1;
   1.568 -br conjI 1;
   1.569 -ba 2;
   1.570 +by (rtac exI 1);
   1.571 +by (rtac conjI 1);
   1.572 +by (assume_tac 2);
   1.573  by (Step_tac 1);
   1.574  (** LEVEL 12 **)
   1.575  by (subgoal_tac "Crypt {|N, Agent Ba, Key K, Xa|} (shrK C) \
   1.576 -\                  : parts (sees Enemy evsa)" 1);
   1.577 +\                  : parts (sees Spy evsa)" 1);
   1.578  by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2);
   1.579  by (best_tac (!claset addSEs [impOfSubs analz_subset_parts]
   1.580 -	              addDs [impOfSubs parts_insert_subset_Un]
   1.581 +                      addDs [impOfSubs parts_insert_subset_Un]
   1.582                        addss (!simpset)) 2);
   1.583  by (eres_inst_tac [("V","?aa : parts {X}")] thin_rl 1);
   1.584 -bd parts_singleton 1;
   1.585 +by (dtac parts_singleton 1);
   1.586  by (Step_tac 1);
   1.587 -bd seesD 1;
   1.588 +by (dtac seesD 1);
   1.589  by (Step_tac 1);
   1.590  by (Full_simp_tac 2);
   1.591  by (fast_tac (!claset addSDs [spec]) 1);
   1.592 @@ -696,25 +696,25 @@
   1.593   \          Says S' A'                                         \
   1.594  \             (Crypt {|N', Agent B', Key K, X'|} (shrK C')) \
   1.595  \                  : set_of_list evs;                         \
   1.596 -\           evs : traces;  C ~= Enemy;  C' ~= Enemy    |] ==> X = X'";
   1.597 -bd lemma 1;
   1.598 -be exE 1;
   1.599 +\           evs : traces;  C ~= Spy;  C' ~= Spy    |] ==> X = X'";
   1.600 +by (dtac lemma 1);
   1.601 +by (etac exE 1);
   1.602  by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
   1.603  by (Fast_tac 1);
   1.604  qed "unique_session_keys";
   1.605  
   1.606  
   1.607  
   1.608 -(*Crucial security property: Enemy does not see the keys sent in msg NS2
   1.609 +(*Crucial security property: Spy does not see the keys sent in msg NS2
   1.610     -- even if another key is compromised*)
   1.611  goal thy 
   1.612   "!!evs. [| Says Server (Friend i) \
   1.613  \            (Crypt {|N, Agent(Friend j), K, X|} K') : set_of_list evs;  \
   1.614  \           evs : traces;  Friend i ~= C;  Friend j ~= C              \
   1.615  \        |] ==>                                                       \
   1.616 -\     K ~: analz (insert (Key (shrK C)) (sees Enemy evs))";
   1.617 -be rev_mp 1;
   1.618 -be traces.induct 1;
   1.619 +\     K ~: analz (insert (Key (shrK C)) (sees Spy evs))";
   1.620 +by (etac rev_mp 1);
   1.621 +by (etac traces.induct 1);
   1.622  by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes)));
   1.623  (*Next 3 steps infer that K has the form "Key (newK evs'" ... *)
   1.624  by (REPEAT_FIRST (resolve_tac [conjI, impI]));
   1.625 @@ -723,21 +723,21 @@
   1.626  by (ALLGOALS 
   1.627      (asm_full_simp_tac 
   1.628       (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
   1.629 -			  analz_insert_Key_newK] @ pushes)
   1.630 +                          analz_insert_Key_newK] @ pushes)
   1.631                 setloop split_tac [expand_if])));
   1.632  (*NS2*)
   1.633  by (fast_tac (!claset addSEs [less_irrefl]) 2);
   1.634  (** LEVEL 8 **)
   1.635  (*Now for the Fake case*)
   1.636 -br notI 1;
   1.637 +by (rtac notI 1);
   1.638  by (subgoal_tac 
   1.639      "Key (newK evt) : \
   1.640  \    analz (synth (analz (insert (Key (shrK C)) \
   1.641 -\                                  (sees Enemy evsa))))" 1);
   1.642 -be (impOfSubs analz_mono) 2;
   1.643 +\                                  (sees Spy evsa))))" 1);
   1.644 +by (etac (impOfSubs analz_mono) 2);
   1.645  by (deepen_tac (!claset addIs [analz_mono RS synth_mono RSN (2,rev_subsetD),
   1.646 -			       impOfSubs synth_increasing,
   1.647 -			       impOfSubs analz_increasing]) 0 2);
   1.648 +                               impOfSubs synth_increasing,
   1.649 +                               impOfSubs analz_increasing]) 0 2);
   1.650  (*Proves the Fake goal*)
   1.651  by (fast_tac (!claset addss (!simpset)) 1);
   1.652  
   1.653 @@ -750,12 +750,12 @@
   1.654      (!simpset addsimps (mem_if::analz_insert_Key_newK::pushes)) 1);
   1.655  by (Step_tac 1);
   1.656  (**LEVEL 18 **)
   1.657 -bd unique_session_keys 1;
   1.658 +by (dtac unique_session_keys 1);
   1.659  by (REPEAT_FIRST assume_tac);
   1.660  by (ALLGOALS Full_simp_tac);
   1.661  by (Step_tac 1);
   1.662  by (asm_full_simp_tac (!simpset addsimps [shrK_mem_analz]) 1);
   1.663 -qed "Enemy_not_see_encrypted_key";
   1.664 +qed "Spy_not_see_encrypted_key";
   1.665  
   1.666  
   1.667  
   1.668 @@ -772,8 +772,8 @@
   1.669  \             (Crypt {|N, Agent B, K|} K') : set_of_list evs;  \
   1.670  \           evs : traces;  i~=j    \
   1.671  \         |] ==> K ~: analz (sees (Friend j) evs)";
   1.672 -br (sees_agent_subset_sees_Enemy RS analz_mono RS contra_subsetD) 1;
   1.673 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [Enemy_not_see_encrypted_key])));
   1.674 +by (rtac (sees_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
   1.675 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [Spy_not_see_encrypted_key])));
   1.676  qed "Friend_not_see_encrypted_key";
   1.677  
   1.678  goal thy 
   1.679 @@ -786,8 +786,8 @@
   1.680  by (agent.induct_tac "A" 1);
   1.681  by (ALLGOALS Simp_tac);
   1.682  by (asm_simp_tac (!simpset addsimps [eq_sym_conv, 
   1.683 -				     Friend_not_see_encrypted_key]) 1);
   1.684 -br ([analz_mono, Enemy_not_see_encrypted_key] MRS contra_subsetD) 1;
   1.685 +                                     Friend_not_see_encrypted_key]) 1);
   1.686 +by (rtac ([analz_mono, Spy_not_see_encrypted_key] MRS contra_subsetD) 1);
   1.687  (*  hyp_subst_tac would deletes the equality assumption... *)
   1.688  by (ALLGOALS (rtac n_not_Suc_n ORELSE' Fast_tac));
   1.689  qed "Agent_not_see_encrypted_key";
   1.690 @@ -801,7 +801,7 @@
   1.691  \        |] ==>  knownBy evs K <= {Friend i, Server}";
   1.692  
   1.693  by (Step_tac 1);
   1.694 -br ccontr 1;
   1.695 +by (rtac ccontr 1);
   1.696  by (fast_tac (!claset addDs [Agent_not_see_encrypted_key]) 1);
   1.697  qed "knownBy_encrypted_key";
   1.698  
   1.699 @@ -817,13 +817,13 @@
   1.700  \                 (Crypt {|N, Agent(Friend j), K, X|} K') # evs';  \
   1.701  \           evs : traces;  i~=k                                    \
   1.702  \        |] ==>                                                    \
   1.703 -\     K ~: analz (insert (Key (shrK (Friend k))) (sees Enemy evs))";
   1.704 -be rev_mp 1;
   1.705 -be traces.induct 1;
   1.706 +\     K ~: analz (insert (Key (shrK (Friend k))) (sees Spy evs))";
   1.707 +by (etac rev_mp 1);
   1.708 +by (etac traces.induct 1);
   1.709  by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes)));
   1.710  by (Step_tac 1);
   1.711  by (asm_full_simp_tac (!simpset addsimps[analz_subset_parts RS contra_subsetD]) 1);
   1.712 -val Enemy_not_see_encrypted_key_lemma = result();
   1.713 +val Spy_not_see_encrypted_key_lemma = result();
   1.714  
   1.715  
   1.716  
   1.717 @@ -835,10 +835,10 @@
   1.718    with the aid of  analz_subset_parts RS contra_subsetD  might do the
   1.719    same thing.*)
   1.720  goal thy 
   1.721 - "!!evs. [| evs : traces; A ~= Enemy;  A ~= Friend j |] ==> \
   1.722 + "!!evs. [| evs : traces; A ~= Spy;  A ~= Friend j |] ==> \
   1.723  \        Key (shrK A) ~:                               \
   1.724 -\          analz (insert (Key (shrK (Friend j))) (sees Enemy evs))";
   1.725 -br (analz_subset_parts RS contra_subsetD) 1;
   1.726 +\          analz (insert (Key (shrK (Friend j))) (sees Spy evs))";
   1.727 +by (rtac (analz_subset_parts RS contra_subsetD) 1);
   1.728  by (Asm_simp_tac 1);
   1.729  qed "insert_not_analz_shrK";
   1.730  
   1.731 @@ -862,15 +862,15 @@
   1.732  \        : set_of_list evs  -->   \
   1.733  \    (EX B'. Says Server B' (Crypt X (shrK (Friend i))) : set_of_list evs | \
   1.734  \            Says (Friend i) B' (Crypt X (shrK (Friend i))) : set_of_list evs)";
   1.735 -be traces.induct 1;
   1.736 +by (etac traces.induct 1);
   1.737  by (Step_tac 1);
   1.738  by (ALLGOALS Asm_full_simp_tac);
   1.739  (*Remaining cases are Fake, NS2 and NS3*)
   1.740 -by (Fast_tac 2);	(*Proves the NS2 case*)
   1.741 +by (Fast_tac 2);        (*Proves the NS2 case*)
   1.742  
   1.743  by (REPEAT (dtac spec 2));
   1.744  fe conjE;
   1.745 -bd mp 2;
   1.746 +by (dtac mp 2);
   1.747  
   1.748  by (REPEAT (resolve_tac [refl, conjI] 2));
   1.749  by (ALLGOALS Asm_full_simp_tac);
   1.750 @@ -879,7 +879,7 @@
   1.751  
   1.752  
   1.753  by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2);
   1.754 -be conjE 2;
   1.755 +by (etac conjE 2);
   1.756  by ((dtac spec THEN' dtac spec THEN' dtac spec THEN' dtac spec)2);
   1.757  
   1.758  (*The NS3 case needs the induction hypothesis twice!
   1.759 @@ -887,18 +887,18 @@
   1.760  by (subgoal_tac "? evs'. X = Crypt {|Key (newK evs'), Agent A|} (shrK B)" 2);
   1.761  by (Fast_tac 3);
   1.762  by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2);
   1.763 -be conjE 2;
   1.764 +by (etac conjE 2);
   1.765  (*DELETE the first quantified formula: it's now useless*)
   1.766  by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2);
   1.767  by (fast_tac (!claset addss (!simpset)) 2);
   1.768  (*Now for the Fake case*)
   1.769 -be disjE 1;
   1.770 +by (etac disjE 1);
   1.771  (*The subcase of Fake, where the message in question is NOT the most recent*)
   1.772  by (Best_tac 2);
   1.773  
   1.774  by (REPEAT_FIRST (etac conjE ORELSE' hyp_subst_tac));
   1.775 -be Crypt_synth 1;
   1.776 -be Key_synth 2;
   1.777 +by (etac Crypt_synth 1);
   1.778 +by (etac Key_synth 2);
   1.779  
   1.780  (*Split up the possibilities of that message being synthd...*)
   1.781  by (Step_tac 1);
     2.1 --- a/src/HOL/Auth/Event.thy	Thu Sep 26 12:47:47 1996 +0200
     2.2 +++ b/src/HOL/Auth/Event.thy	Thu Sep 26 12:50:48 1996 +0200
     2.3 @@ -28,7 +28,7 @@
     2.4          (*Server knows all keys; other agents know only their own*)
     2.5    initState_Server  "initState Server     = Key `` range shrK"
     2.6    initState_Friend  "initState (Friend i) = {Key (shrK (Friend i))}"
     2.7 -  initState_Enemy   "initState Enemy  = {Key (shrK Enemy)}"
     2.8 +  initState_Spy   "initState Spy  = {Key (shrK Spy)}"
     2.9  
    2.10  (**
    2.11  For asymmetric keys: server knows all public and private keys,
    2.12 @@ -45,7 +45,7 @@
    2.13  primrec sees1 event
    2.14             (*First agent recalls all that it says, but NOT everything
    2.15               that is sent to it; it must note such things if/when received*)
    2.16 -  sees1_Says  "sees1 A (Says A' B X)  = (if A:{A',Enemy} then {X} else {})"
    2.17 +  sees1_Says  "sees1 A (Says A' B X)  = (if A:{A',Spy} then {X} else {})"
    2.18            (*part of A's internal state*)
    2.19    sees1_Notes "sees1 A (Notes A' X)   = (if A=A' then {X} else {})"
    2.20  
    2.21 @@ -89,11 +89,11 @@
    2.22           (*Initial trace is empty*)
    2.23      Nil  "[]: traces"
    2.24  
    2.25 -         (*The enemy MAY say anything he CAN say.  We do not expect him to
    2.26 +         (*The spy MAY say anything he CAN say.  We do not expect him to
    2.27             invent new nonces here, but he can also use NS1.  Common to
    2.28             all similar protocols.*)
    2.29 -    Fake "[| evs: traces;  B ~= Enemy;  X: synth (analz (sees Enemy evs))
    2.30 -          |] ==> (Says Enemy B X) # evs : traces"
    2.31 +    Fake "[| evs: traces;  B ~= Spy;  X: synth (analz (sees Spy evs))
    2.32 +          |] ==> (Says Spy B X) # evs : traces"
    2.33  
    2.34           (*Alice initiates a protocol run*)
    2.35      NS1  "[| evs: traces;  A ~= Server
    2.36 @@ -112,7 +112,7 @@
    2.37                     (shrK A))) # evs : traces"
    2.38  
    2.39            (*We can't assume S=Server.  Agent A "remembers" her nonce.
    2.40 -            May assume WLOG that she is NOT the Enemy: the Fake rule
    2.41 +            May assume WLOG that she is NOT the Spy: the Fake rule
    2.42              covers this case.  Can inductively show A ~= Server*)
    2.43      NS3  "[| evs: traces;  A ~= B;
    2.44               (Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))) 
     3.1 --- a/src/HOL/Auth/Message.ML	Thu Sep 26 12:47:47 1996 +0200
     3.2 +++ b/src/HOL/Auth/Message.ML	Thu Sep 26 12:50:48 1996 +0200
     3.3 @@ -14,7 +14,7 @@
     3.4  
     3.5  goal thy "!!K K'. (invKey K = invKey K') = (K=K')";
     3.6  by (Step_tac 1);
     3.7 -br box_equals 1;
     3.8 +by (rtac box_equals 1);
     3.9  by (REPEAT (rtac invKey 2));
    3.10  by (Asm_simp_tac 1);
    3.11  qed "invKey_eq";
    3.12 @@ -64,9 +64,9 @@
    3.13  qed "keysFor_insert_Crypt";
    3.14  
    3.15  Addsimps [keysFor_empty, keysFor_Un, keysFor_UN, 
    3.16 -	  keysFor_insert_Agent, keysFor_insert_Nonce,
    3.17 -	  keysFor_insert_Key, keysFor_insert_MPair,
    3.18 -	  keysFor_insert_Crypt];
    3.19 +          keysFor_insert_Agent, keysFor_insert_Nonce,
    3.20 +          keysFor_insert_Key, keysFor_insert_MPair,
    3.21 +          keysFor_insert_Crypt];
    3.22  
    3.23  
    3.24  (**** Inductive relation "parts" ****)
    3.25 @@ -76,7 +76,7 @@
    3.26  \            [| X : parts H; Y : parts H |] ==> P  \
    3.27  \         |] ==> P";
    3.28  by (cut_facts_tac [major] 1);
    3.29 -brs prems 1;
    3.30 +by (resolve_tac prems 1);
    3.31  by (REPEAT (eresolve_tac [asm_rl, parts.Fst, parts.Snd] 1));
    3.32  qed "MPair_parts";
    3.33  
    3.34 @@ -101,7 +101,7 @@
    3.35  
    3.36  goal thy "parts{} = {}";
    3.37  by (Step_tac 1);
    3.38 -be parts.induct 1;
    3.39 +by (etac parts.induct 1);
    3.40  by (ALLGOALS Fast_tac);
    3.41  qed "parts_empty";
    3.42  Addsimps [parts_empty];
    3.43 @@ -113,7 +113,7 @@
    3.44  
    3.45  (*WARNING: loops if H = {Y}, therefore must not be repeated!*)
    3.46  goal thy "!!H. X: parts H ==> EX Y:H. X: parts {Y}";
    3.47 -be parts.induct 1;
    3.48 +by (etac parts.induct 1);
    3.49  by (ALLGOALS Fast_tac);
    3.50  qed "parts_singleton";
    3.51  
    3.52 @@ -125,8 +125,8 @@
    3.53  val parts_Un_subset1 = result();
    3.54  
    3.55  goal thy "parts(G Un H) <= parts(G) Un parts(H)";
    3.56 -br subsetI 1;
    3.57 -be parts.induct 1;
    3.58 +by (rtac subsetI 1);
    3.59 +by (etac parts.induct 1);
    3.60  by (ALLGOALS Fast_tac);
    3.61  val parts_Un_subset2 = result();
    3.62  
    3.63 @@ -151,8 +151,8 @@
    3.64  val parts_UN_subset1 = result();
    3.65  
    3.66  goal thy "parts(UN x:A. H x) <= (UN x:A. parts(H x))";
    3.67 -br subsetI 1;
    3.68 -be parts.induct 1;
    3.69 +by (rtac subsetI 1);
    3.70 +by (etac parts.induct 1);
    3.71  by (ALLGOALS Fast_tac);
    3.72  val parts_UN_subset2 = result();
    3.73  
    3.74 @@ -174,7 +174,7 @@
    3.75  (** Idempotence and transitivity **)
    3.76  
    3.77  goal thy "!!H. X: parts (parts H) ==> X: parts H";
    3.78 -be parts.induct 1;
    3.79 +by (etac parts.induct 1);
    3.80  by (ALLGOALS Fast_tac);
    3.81  qed "parts_partsE";
    3.82  AddSEs [parts_partsE];
    3.83 @@ -191,7 +191,7 @@
    3.84  
    3.85  (*Cut*)
    3.86  goal thy "!!H. [| Y: parts (insert X H);  X: parts H |] ==> Y: parts H";
    3.87 -be parts_trans 1;
    3.88 +by (etac parts_trans 1);
    3.89  by (Fast_tac 1);
    3.90  qed "parts_cut";
    3.91  
    3.92 @@ -209,8 +209,8 @@
    3.93  
    3.94  goal thy "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)";
    3.95  by (rtac (parts_insert_subset RSN (2, equalityI)) 1);
    3.96 -br subsetI 1;
    3.97 -be parts.induct 1;
    3.98 +by (rtac subsetI 1);
    3.99 +by (etac parts.induct 1);
   3.100  (*Simplification breaks up equalities between messages;
   3.101    how to make it work for fast_tac??*)
   3.102  by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   3.103 @@ -218,45 +218,45 @@
   3.104  
   3.105  goal thy "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)";
   3.106  by (rtac (parts_insert_subset RSN (2, equalityI)) 1);
   3.107 -br subsetI 1;
   3.108 -be parts.induct 1;
   3.109 +by (rtac subsetI 1);
   3.110 +by (etac parts.induct 1);
   3.111  by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   3.112  qed "parts_insert_Nonce";
   3.113  
   3.114  goal thy "parts (insert (Key K) H) = insert (Key K) (parts H)";
   3.115  by (rtac (parts_insert_subset RSN (2, equalityI)) 1);
   3.116 -br subsetI 1;
   3.117 -be parts.induct 1;
   3.118 +by (rtac subsetI 1);
   3.119 +by (etac parts.induct 1);
   3.120  by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   3.121  qed "parts_insert_Key";
   3.122  
   3.123  goal thy "parts (insert (Crypt X K) H) = \
   3.124  \         insert (Crypt X K) (parts (insert X H))";
   3.125 -br equalityI 1;
   3.126 -br subsetI 1;
   3.127 -be parts.induct 1;
   3.128 +by (rtac equalityI 1);
   3.129 +by (rtac subsetI 1);
   3.130 +by (etac parts.induct 1);
   3.131  by (Auto_tac());
   3.132 -be parts.induct 1;
   3.133 +by (etac parts.induct 1);
   3.134  by (ALLGOALS (best_tac (!claset addIs [parts.Body])));
   3.135  qed "parts_insert_Crypt";
   3.136  
   3.137  goal thy "parts (insert {|X,Y|} H) = \
   3.138  \         insert {|X,Y|} (parts (insert X (insert Y H)))";
   3.139 -br equalityI 1;
   3.140 -br subsetI 1;
   3.141 -be parts.induct 1;
   3.142 +by (rtac equalityI 1);
   3.143 +by (rtac subsetI 1);
   3.144 +by (etac parts.induct 1);
   3.145  by (Auto_tac());
   3.146 -be parts.induct 1;
   3.147 +by (etac parts.induct 1);
   3.148  by (ALLGOALS (best_tac (!claset addIs [parts.Fst, parts.Snd])));
   3.149  qed "parts_insert_MPair";
   3.150  
   3.151  Addsimps [parts_insert_Agent, parts_insert_Nonce, 
   3.152 -	  parts_insert_Key, parts_insert_Crypt, parts_insert_MPair];
   3.153 +          parts_insert_Key, parts_insert_Crypt, parts_insert_MPair];
   3.154  
   3.155  
   3.156  goal thy "parts (Key``N) = Key``N";
   3.157  by (Auto_tac());
   3.158 -be parts.induct 1;
   3.159 +by (etac parts.induct 1);
   3.160  by (Auto_tac());
   3.161  qed "parts_image_Key";
   3.162  
   3.163 @@ -270,7 +270,7 @@
   3.164  \            [| X : analz H; Y : analz H |] ==> P  \
   3.165  \         |] ==> P";
   3.166  by (cut_facts_tac [major] 1);
   3.167 -brs prems 1;
   3.168 +by (resolve_tac prems 1);
   3.169  by (REPEAT (eresolve_tac [asm_rl, analz.Fst, analz.Snd] 1));
   3.170  qed "MPair_analz";
   3.171  
   3.172 @@ -286,7 +286,7 @@
   3.173  
   3.174  goal thy "analz H <= parts H";
   3.175  by (rtac subsetI 1);
   3.176 -be analz.induct 1;
   3.177 +by (etac analz.induct 1);
   3.178  by (ALLGOALS Fast_tac);
   3.179  qed "analz_subset_parts";
   3.180  
   3.181 @@ -294,8 +294,8 @@
   3.182  
   3.183  
   3.184  goal thy "parts (analz H) = parts H";
   3.185 -br equalityI 1;
   3.186 -br (analz_subset_parts RS parts_mono RS subset_trans) 1;
   3.187 +by (rtac equalityI 1);
   3.188 +by (rtac (analz_subset_parts RS parts_mono RS subset_trans) 1);
   3.189  by (Simp_tac 1);
   3.190  by (fast_tac (!claset addDs [analz_increasing RS parts_mono RS subsetD]) 1);
   3.191  qed "parts_analz";
   3.192 @@ -303,7 +303,7 @@
   3.193  
   3.194  goal thy "analz (parts H) = parts H";
   3.195  by (Auto_tac());
   3.196 -be analz.induct 1;
   3.197 +by (etac analz.induct 1);
   3.198  by (Auto_tac());
   3.199  qed "analz_parts";
   3.200  Addsimps [analz_parts];
   3.201 @@ -318,7 +318,7 @@
   3.202  
   3.203  goal thy "analz{} = {}";
   3.204  by (Step_tac 1);
   3.205 -be analz.induct 1;
   3.206 +by (etac analz.induct 1);
   3.207  by (ALLGOALS Fast_tac);
   3.208  qed "analz_empty";
   3.209  Addsimps [analz_empty];
   3.210 @@ -337,8 +337,8 @@
   3.211  
   3.212  goal thy "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)";
   3.213  by (rtac (analz_insert RSN (2, equalityI)) 1);
   3.214 -br subsetI 1;
   3.215 -be analz.induct 1;
   3.216 +by (rtac subsetI 1);
   3.217 +by (etac analz.induct 1);
   3.218  (*Simplification breaks up equalities between messages;
   3.219    how to make it work for fast_tac??*)
   3.220  by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   3.221 @@ -346,8 +346,8 @@
   3.222  
   3.223  goal thy "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)";
   3.224  by (rtac (analz_insert RSN (2, equalityI)) 1);
   3.225 -br subsetI 1;
   3.226 -be analz.induct 1;
   3.227 +by (rtac subsetI 1);
   3.228 +by (etac analz.induct 1);
   3.229  by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   3.230  qed "analz_insert_Nonce";
   3.231  
   3.232 @@ -356,18 +356,18 @@
   3.233      "!!K. K ~: keysFor (analz H) ==>  \
   3.234  \         analz (insert (Key K) H) = insert (Key K) (analz H)";
   3.235  by (rtac (analz_insert RSN (2, equalityI)) 1);
   3.236 -br subsetI 1;
   3.237 -be analz.induct 1;
   3.238 +by (rtac subsetI 1);
   3.239 +by (etac analz.induct 1);
   3.240  by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   3.241  qed "analz_insert_Key";
   3.242  
   3.243  goal thy "analz (insert {|X,Y|} H) = \
   3.244  \         insert {|X,Y|} (analz (insert X (insert Y H)))";
   3.245 -br equalityI 1;
   3.246 -br subsetI 1;
   3.247 -be analz.induct 1;
   3.248 +by (rtac equalityI 1);
   3.249 +by (rtac subsetI 1);
   3.250 +by (etac analz.induct 1);
   3.251  by (Auto_tac());
   3.252 -be analz.induct 1;
   3.253 +by (etac analz.induct 1);
   3.254  by (ALLGOALS (deepen_tac (!claset addIs [analz.Fst, analz.Snd, analz.Decrypt]) 0));
   3.255  qed "analz_insert_MPair";
   3.256  
   3.257 @@ -376,15 +376,15 @@
   3.258  \              analz (insert (Crypt X K) H) = \
   3.259  \              insert (Crypt X K) (analz H)";
   3.260  by (rtac (analz_insert RSN (2, equalityI)) 1);
   3.261 -br subsetI 1;
   3.262 -be analz.induct 1;
   3.263 +by (rtac subsetI 1);
   3.264 +by (etac analz.induct 1);
   3.265  by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   3.266  qed "analz_insert_Crypt";
   3.267  
   3.268  goal thy "!!H. Key (invKey K) : analz H ==>  \
   3.269  \              analz (insert (Crypt X K) H) <= \
   3.270  \              insert (Crypt X K) (analz (insert X H))";
   3.271 -br subsetI 1;
   3.272 +by (rtac subsetI 1);
   3.273  by (eres_inst_tac [("za","x")] analz.induct 1);
   3.274  by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   3.275  val lemma1 = result();
   3.276 @@ -396,7 +396,7 @@
   3.277  by (eres_inst_tac [("za","x")] analz.induct 1);
   3.278  by (Auto_tac());
   3.279  by (best_tac (!claset addIs [subset_insertI RS analz_mono RS subsetD,
   3.280 -			     analz.Decrypt]) 1);
   3.281 +                             analz.Decrypt]) 1);
   3.282  val lemma2 = result();
   3.283  
   3.284  goal thy "!!H. Key (invKey K) : analz H ==>  \
   3.285 @@ -415,25 +415,25 @@
   3.286  \          else insert (Crypt X' K) (analz H))";
   3.287  by (excluded_middle_tac "Key (invKey K)  : analz H " 1);
   3.288  by (ALLGOALS (asm_simp_tac (!simpset addsimps [analz_insert_Crypt, 
   3.289 -					       analz_insert_Decrypt])));
   3.290 +                                               analz_insert_Decrypt])));
   3.291  qed "analz_Crypt_if";
   3.292  
   3.293  Addsimps [analz_insert_Agent, analz_insert_Nonce, 
   3.294 -	  analz_insert_Key, analz_insert_MPair, 
   3.295 -	  analz_Crypt_if];
   3.296 +          analz_insert_Key, analz_insert_MPair, 
   3.297 +          analz_Crypt_if];
   3.298  
   3.299  (*This rule supposes "for the sake of argument" that we have the key.*)
   3.300  goal thy  "analz (insert (Crypt X K) H) <=  \
   3.301  \          insert (Crypt X K) (analz (insert X H))";
   3.302 -br subsetI 1;
   3.303 -be analz.induct 1;
   3.304 +by (rtac subsetI 1);
   3.305 +by (etac analz.induct 1);
   3.306  by (Auto_tac());
   3.307  qed "analz_insert_Crypt_subset";
   3.308  
   3.309  
   3.310  goal thy "analz (Key``N) = Key``N";
   3.311  by (Auto_tac());
   3.312 -be analz.induct 1;
   3.313 +by (etac analz.induct 1);
   3.314  by (Auto_tac());
   3.315  qed "analz_image_Key";
   3.316  
   3.317 @@ -443,7 +443,7 @@
   3.318  (** Idempotence and transitivity **)
   3.319  
   3.320  goal thy "!!H. X: analz (analz H) ==> X: analz H";
   3.321 -be analz.induct 1;
   3.322 +by (etac analz.induct 1);
   3.323  by (ALLGOALS Fast_tac);
   3.324  qed "analz_analzE";
   3.325  AddSEs [analz_analzE];
   3.326 @@ -460,7 +460,7 @@
   3.327  
   3.328  (*Cut; Lemma 2 of Lowe*)
   3.329  goal thy "!!H. [| Y: analz (insert X H);  X: analz H |] ==> Y: analz H";
   3.330 -be analz_trans 1;
   3.331 +by (etac analz_trans 1);
   3.332  by (Fast_tac 1);
   3.333  qed "analz_cut";
   3.334  
   3.335 @@ -474,39 +474,39 @@
   3.336  goal thy "!!H. [| analz G <= analz G'; analz H <= analz H' \
   3.337  \              |] ==> analz (G Un H) <= analz (G' Un H')";
   3.338  by (Step_tac 1);
   3.339 -be analz.induct 1;
   3.340 +by (etac analz.induct 1);
   3.341  by (ALLGOALS (best_tac (!claset addIs [analz_mono RS subsetD])));
   3.342  qed "analz_subset_cong";
   3.343  
   3.344  goal thy "!!H. [| analz G = analz G'; analz H = analz H' \
   3.345  \              |] ==> analz (G Un H) = analz (G' Un H')";
   3.346  by (REPEAT_FIRST (ares_tac [equalityI, analz_subset_cong]
   3.347 -	  ORELSE' etac equalityE));
   3.348 +          ORELSE' etac equalityE));
   3.349  qed "analz_cong";
   3.350  
   3.351  
   3.352  goal thy "!!H. analz H = analz H' ==> analz(insert X H) = analz(insert X H')";
   3.353  by (asm_simp_tac (!simpset addsimps [insert_def] 
   3.354 -		           setloop (rtac analz_cong)) 1);
   3.355 +                           setloop (rtac analz_cong)) 1);
   3.356  qed "analz_insert_cong";
   3.357  
   3.358  (*If there are no pairs or encryptions then analz does nothing*)
   3.359  goal thy "!!H. [| ALL X Y. {|X,Y|} ~: H;  ALL X K. Crypt X K ~: H |] ==> \
   3.360  \         analz H = H";
   3.361  by (Step_tac 1);
   3.362 -be analz.induct 1;
   3.363 +by (etac analz.induct 1);
   3.364  by (ALLGOALS Fast_tac);
   3.365  qed "analz_trivial";
   3.366  
   3.367  (*Helps to prove Fake cases*)
   3.368  goal thy "!!X. X: analz (UN i. analz (H i)) ==> X: analz (UN i. H i)";
   3.369 -be analz.induct 1;
   3.370 +by (etac analz.induct 1);
   3.371  by (ALLGOALS (fast_tac (!claset addEs [impOfSubs analz_mono])));
   3.372  val lemma = result();
   3.373  
   3.374  goal thy "analz (UN i. analz (H i)) = analz (UN i. H i)";
   3.375  by (fast_tac (!claset addIs [lemma]
   3.376 -		      addEs [impOfSubs analz_mono]) 1);
   3.377 +                      addEs [impOfSubs analz_mono]) 1);
   3.378  qed "analz_UN_analz";
   3.379  Addsimps [analz_UN_analz];
   3.380  
   3.381 @@ -552,7 +552,7 @@
   3.382  (** Idempotence and transitivity **)
   3.383  
   3.384  goal thy "!!H. X: synth (synth H) ==> X: synth H";
   3.385 -be synth.induct 1;
   3.386 +by (etac synth.induct 1);
   3.387  by (ALLGOALS Fast_tac);
   3.388  qed "synth_synthE";
   3.389  AddSEs [synth_synthE];
   3.390 @@ -568,7 +568,7 @@
   3.391  
   3.392  (*Cut; Lemma 2 of Lowe*)
   3.393  goal thy "!!H. [| Y: synth (insert X H);  X: synth H |] ==> Y: synth H";
   3.394 -be synth_trans 1;
   3.395 +by (etac synth_trans 1);
   3.396  by (Fast_tac 1);
   3.397  qed "synth_cut";
   3.398  
   3.399 @@ -601,19 +601,19 @@
   3.400  (*** Combinations of parts, analz and synth ***)
   3.401  
   3.402  goal thy "parts (synth H) = parts H Un synth H";
   3.403 -br equalityI 1;
   3.404 -br subsetI 1;
   3.405 -be parts.induct 1;
   3.406 +by (rtac equalityI 1);
   3.407 +by (rtac subsetI 1);
   3.408 +by (etac parts.induct 1);
   3.409  by (ALLGOALS
   3.410      (best_tac (!claset addIs ((synth_increasing RS parts_mono RS subsetD)
   3.411 -			     ::parts.intrs))));
   3.412 +                             ::parts.intrs))));
   3.413  qed "parts_synth";
   3.414  Addsimps [parts_synth];
   3.415  
   3.416  goal thy "analz (synth H) = analz H Un synth H";
   3.417 -br equalityI 1;
   3.418 -br subsetI 1;
   3.419 -be analz.induct 1;
   3.420 +by (rtac equalityI 1);
   3.421 +by (rtac subsetI 1);
   3.422 +by (etac analz.induct 1);
   3.423  by (best_tac
   3.424      (!claset addIs [synth_increasing RS analz_mono RS subsetD]) 5);
   3.425  (*Strange that best_tac just can't hack this one...*)
   3.426 @@ -621,20 +621,20 @@
   3.427  qed "analz_synth";
   3.428  Addsimps [analz_synth];
   3.429  
   3.430 -(*Hard to prove; still needed now that there's only one Enemy?*)
   3.431 +(*Hard to prove; still needed now that there's only one Spy?*)
   3.432  goal thy "analz (UN i. synth (H i)) = \
   3.433  \         analz (UN i. H i) Un (UN i. synth (H i))";
   3.434 -br equalityI 1;
   3.435 -br subsetI 1;
   3.436 -be analz.induct 1;
   3.437 +by (rtac equalityI 1);
   3.438 +by (rtac subsetI 1);
   3.439 +by (etac analz.induct 1);
   3.440  by (best_tac
   3.441      (!claset addEs [impOfSubs synth_increasing,
   3.442 -		    impOfSubs analz_mono]) 5);
   3.443 +                    impOfSubs analz_mono]) 5);
   3.444  by (Best_tac 1);
   3.445  by (deepen_tac (!claset addIs [analz.Fst]) 0 1);
   3.446  by (deepen_tac (!claset addIs [analz.Snd]) 0 1);
   3.447  by (deepen_tac (!claset addSEs [analz.Decrypt]
   3.448 -			addIs  [analz.Decrypt]) 0 1);
   3.449 +                        addIs  [analz.Decrypt]) 0 1);
   3.450  qed "analz_UN1_synth";
   3.451  Addsimps [analz_UN1_synth];
   3.452  
   3.453 @@ -642,21 +642,21 @@
   3.454  (** For reasoning about the Fake rule in traces **)
   3.455  
   3.456  goal thy "!!Y. X: G ==> parts(insert X H) <= parts G Un parts H";
   3.457 -br ([parts_mono, parts_Un_subset2] MRS subset_trans) 1;
   3.458 +by (rtac ([parts_mono, parts_Un_subset2] MRS subset_trans) 1);
   3.459  by (Fast_tac 1);
   3.460  qed "parts_insert_subset_Un";
   3.461  
   3.462  (*More specifically for Fake*)
   3.463  goal thy "!!H. X: synth (analz G) ==> \
   3.464  \              parts (insert X H) <= synth (analz G) Un parts G Un parts H";
   3.465 -bd parts_insert_subset_Un 1;
   3.466 +by (dtac parts_insert_subset_Un 1);
   3.467  by (Full_simp_tac 1);
   3.468  by (Deepen_tac 0 1);
   3.469  qed "Fake_parts_insert";
   3.470  
   3.471  goal thy "!!H. [| X: synth (analz G); G <= H |] ==> \
   3.472  \              analz (insert X H) <= synth (analz H) Un analz H";
   3.473 -br subsetI 1;
   3.474 +by (rtac subsetI 1);
   3.475  by (subgoal_tac "x : analz (synth (analz H))" 1);
   3.476  by (best_tac (!claset addIs [impOfSubs (analz_mono RS synth_mono)]
   3.477                        addSEs [impOfSubs analz_mono]) 2);
     4.1 --- a/src/HOL/Auth/Message.thy	Thu Sep 26 12:47:47 1996 +0200
     4.2 +++ b/src/HOL/Auth/Message.thy	Thu Sep 26 12:50:48 1996 +0200
     4.3 @@ -36,15 +36,15 @@
     4.4      inductive definition instead of a datatype.*) 
     4.5  
     4.6  datatype  (*We allow any number of friendly agents*)
     4.7 -  agent = Server | Friend nat | Enemy
     4.8 +  agent = Server | Friend nat | Spy
     4.9  
    4.10  consts  
    4.11 -  isEnemy :: agent => bool
    4.12 +  isSpy :: agent => bool
    4.13  
    4.14 -primrec isEnemy agent
    4.15 -  isEnemy_Server  "isEnemy Server  = False"
    4.16 -  isEnemy_Friend  "isEnemy (Friend i) = False"
    4.17 -  isEnemy_Enemy   "isEnemy Enemy = True"
    4.18 +primrec isSpy agent
    4.19 +  isSpy_Server  "isSpy Server  = False"
    4.20 +  isSpy_Friend  "isSpy (Friend i) = False"
    4.21 +  isSpy_Spy   "isSpy Spy = True"
    4.22  
    4.23  datatype  (*Messages are agent names, nonces, keys, pairs and encryptions*)
    4.24    msg = Agent agent
     5.1 --- a/src/HOL/Auth/NS_Shared.ML	Thu Sep 26 12:47:47 1996 +0200
     5.2 +++ b/src/HOL/Auth/NS_Shared.ML	Thu Sep 26 12:50:48 1996 +0200
     5.3 @@ -19,10 +19,10 @@
     5.4  (*Weak liveness: there are traces that reach the end*)
     5.5  goal thy 
     5.6   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
     5.7 -\        ==> EX N K. EX evs: ns_shared.          \
     5.8 +\        ==> EX N K. EX evs: ns_shared lost.          \
     5.9  \               Says A B (Crypt {|Nonce N, Nonce N|} K) : set_of_list evs";
    5.10  by (REPEAT (resolve_tac [exI,bexI] 1));
    5.11 -br (ns_shared.Nil RS ns_shared.NS1 RS ns_shared.NS2 RS ns_shared.NS3 RS ns_shared.NS4 RS ns_shared.NS5) 2;
    5.12 +by (rtac (ns_shared.Nil RS ns_shared.NS1 RS ns_shared.NS2 RS ns_shared.NS3 RS ns_shared.NS4 RS ns_shared.NS5) 2);
    5.13  by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
    5.14  by (REPEAT_FIRST (resolve_tac [refl, conjI]));
    5.15  by (ALLGOALS (fast_tac (!claset addss (!simpset setsolver safe_solver))));
    5.16 @@ -31,19 +31,38 @@
    5.17  
    5.18  (**** Inductive proofs about ns_shared ****)
    5.19  
    5.20 -(*The Enemy can see more than anybody else, except for their initial state*)
    5.21 +goal thy "!!evs. lost' <= lost ==> ns_shared lost' <= ns_shared lost";
    5.22 +by (rtac subsetI 1);
    5.23 +by (etac ns_shared.induct 1);
    5.24 +by (REPEAT_FIRST
    5.25 +    (best_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
    5.26 +                              :: ns_shared.intrs))));
    5.27 +qed "ns_shared_mono";
    5.28 +
    5.29 +
    5.30 +(*The Spy can see more than anybody else, except for their initial state*)
    5.31  goal thy 
    5.32 - "!!evs. evs : ns_shared ==> \
    5.33 -\     sees A evs <= initState A Un sees Enemy evs";
    5.34 -be ns_shared.induct 1;
    5.35 + "!!evs. evs : ns_shared lost ==> \
    5.36 +\     sees lost A evs <= initState lost A Un sees lost Spy evs";
    5.37 +by (etac ns_shared.induct 1);
    5.38  by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] 
    5.39 -			        addss (!simpset))));
    5.40 -qed "sees_agent_subset_sees_Enemy";
    5.41 +                                addss (!simpset))));
    5.42 +qed "sees_agent_subset_sees_Spy";
    5.43 +
    5.44 +
    5.45 +(*The Spy can see more than anybody else who's lost their key!*)
    5.46 +goal thy 
    5.47 + "!!evs. evs : ns_shared lost ==> \
    5.48 +\        A: lost --> A ~= Server --> sees lost A evs <= sees lost Spy evs";
    5.49 +by (etac ns_shared.induct 1);
    5.50 +by (agent.induct_tac "A" 1);
    5.51 +by (auto_tac (!claset addDs [sees_Says_subset_insert RS subsetD], (!simpset)));
    5.52 +qed_spec_mp "sees_lost_agent_subset_sees_Spy";
    5.53  
    5.54  
    5.55  (*Nobody sends themselves messages*)
    5.56 -goal thy "!!evs. evs : ns_shared ==> ALL A X. Says A A X ~: set_of_list evs";
    5.57 -be ns_shared.induct 1;
    5.58 +goal thy "!!evs. evs : ns_shared lost ==> ALL A X. Says A A X ~: set_of_list evs";
    5.59 +by (etac ns_shared.induct 1);
    5.60  by (Auto_tac());
    5.61  qed_spec_mp "not_Says_to_self";
    5.62  Addsimps [not_Says_to_self];
    5.63 @@ -51,56 +70,58 @@
    5.64  
    5.65  (*For reasoning about the encrypted portion of message NS3*)
    5.66  goal thy "!!evs. (Says S A (Crypt {|N, B, K, X|} KA)) : set_of_list evs ==> \
    5.67 -\                X : parts (sees Enemy evs)";
    5.68 +\                X : parts (sees lost Spy evs)";
    5.69  by (fast_tac (!claset addSEs partsEs
    5.70 -	              addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
    5.71 -qed "NS3_msg_in_parts_sees_Enemy";
    5.72 -			      
    5.73 +                      addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
    5.74 +qed "NS3_msg_in_parts_sees_Spy";
    5.75 +                              
    5.76 +val parts_Fake_tac = 
    5.77 +    dres_inst_tac [("lost","lost")] NS3_msg_in_parts_sees_Spy 5;
    5.78  
    5.79 -(** Theorems of the form X ~: parts (sees Enemy evs) imply that NOBODY
    5.80 +(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
    5.81      sends messages containing X! **)
    5.82  
    5.83 -(*Enemy never sees another agent's shared key!*)
    5.84 +(*Spy never sees lost another agent's shared key!*)
    5.85  goal thy 
    5.86 - "!!evs. [| evs : ns_shared; A ~: bad |]    \
    5.87 -\        ==> Key (shrK A) ~: parts (sees Enemy evs)";
    5.88 -be ns_shared.induct 1;
    5.89 -bd NS3_msg_in_parts_sees_Enemy 5;
    5.90 + "!!evs. [| evs : ns_shared lost; A ~: lost |]    \
    5.91 +\        ==> Key (shrK A) ~: parts (sees lost Spy evs)";
    5.92 +by (etac ns_shared.induct 1);
    5.93 +by parts_Fake_tac;
    5.94  by (Auto_tac());
    5.95  (*Deals with Fake message*)
    5.96  by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    5.97 -			     impOfSubs Fake_parts_insert]) 1);
    5.98 -qed "Enemy_not_see_shrK";
    5.99 +                             impOfSubs Fake_parts_insert]) 1);
   5.100 +qed "Spy_not_see_shrK";
   5.101  
   5.102 -bind_thm ("Enemy_not_analz_shrK",
   5.103 -	  [analz_subset_parts, Enemy_not_see_shrK] MRS contra_subsetD);
   5.104 +bind_thm ("Spy_not_analz_shrK",
   5.105 +          [analz_subset_parts, Spy_not_see_shrK] MRS contra_subsetD);
   5.106  
   5.107 -Addsimps [Enemy_not_see_shrK, Enemy_not_analz_shrK];
   5.108 +Addsimps [Spy_not_see_shrK, Spy_not_analz_shrK];
   5.109  
   5.110  (*We go to some trouble to preserve R in the 3rd and 4th subgoals
   5.111    As usual fast_tac cannot be used because it uses the equalities too soon*)
   5.112  val major::prems = 
   5.113 -goal thy  "[| Key (shrK A) : parts (sees Enemy evs);       \
   5.114 -\             evs : ns_shared;                             \
   5.115 -\             A:bad ==> R                                  \
   5.116 +goal thy  "[| Key (shrK A) : parts (sees lost Spy evs);       \
   5.117 +\             evs : ns_shared lost;                             \
   5.118 +\             A:lost ==> R                                  \
   5.119  \           |] ==> R";
   5.120 -br ccontr 1;
   5.121 -br ([major, Enemy_not_see_shrK] MRS rev_notE) 1;
   5.122 +by (rtac ccontr 1);
   5.123 +by (rtac ([major, Spy_not_see_shrK] MRS rev_notE) 1);
   5.124  by (swap_res_tac prems 2);
   5.125  by (ALLGOALS (fast_tac (!claset addIs prems)));
   5.126 -qed "Enemy_see_shrK_E";
   5.127 +qed "Spy_see_shrK_E";
   5.128  
   5.129 -bind_thm ("Enemy_analz_shrK_E", 
   5.130 -	  analz_subset_parts RS subsetD RS Enemy_see_shrK_E);
   5.131 +bind_thm ("Spy_analz_shrK_E", 
   5.132 +          analz_subset_parts RS subsetD RS Spy_see_shrK_E);
   5.133  
   5.134 -AddSEs [Enemy_see_shrK_E, Enemy_analz_shrK_E];
   5.135 +AddSEs [Spy_see_shrK_E, Spy_analz_shrK_E];
   5.136  
   5.137  
   5.138  goal thy  
   5.139 - "!!evs. evs : ns_shared ==>                              \
   5.140 -\        (Key (shrK A) : analz (sees Enemy evs)) = (A : bad)";
   5.141 + "!!evs. evs : ns_shared lost ==>                              \
   5.142 +\        (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
   5.143  by (best_tac (!claset addIs [impOfSubs (subset_insertI RS analz_mono)]
   5.144 -	              addss (!simpset)) 1);
   5.145 +                      addss (!simpset)) 1);
   5.146  qed "shrK_mem_analz";
   5.147  
   5.148  Addsimps [shrK_mem_analz];
   5.149 @@ -114,23 +135,23 @@
   5.150    standard Fake rule.  
   5.151        The length comparison, and Union over C, are essential for the 
   5.152    induction! *)
   5.153 -goal thy "!!evs. evs : ns_shared ==> \
   5.154 +goal thy "!!evs. evs : ns_shared lost ==> \
   5.155  \                length evs <= length evs' --> \
   5.156 -\                          Key (newK evs') ~: (UN C. parts (sees C evs))";
   5.157 -be ns_shared.induct 1;
   5.158 -bd NS3_msg_in_parts_sees_Enemy 5;
   5.159 +\                          Key (newK evs') ~: (UN C. parts (sees lost C evs))";
   5.160 +by (etac ns_shared.induct 1);
   5.161 +by parts_Fake_tac;
   5.162  (*auto_tac does not work here, as it performs safe_tac first*)
   5.163  by (ALLGOALS Asm_simp_tac);
   5.164  by (ALLGOALS (fast_tac (!claset addDs [impOfSubs analz_subset_parts,
   5.165 -				       impOfSubs parts_insert_subset_Un,
   5.166 -				       Suc_leD]
   5.167 -			        addss (!simpset))));
   5.168 +                                       impOfSubs parts_insert_subset_Un,
   5.169 +                                       Suc_leD]
   5.170 +                                addss (!simpset))));
   5.171  val lemma = result();
   5.172  
   5.173  (*Variant needed for the main theorem below*)
   5.174  goal thy 
   5.175 - "!!evs. [| evs : ns_shared;  length evs <= length evs' |]    \
   5.176 -\        ==> Key (newK evs') ~: parts (sees C evs)";
   5.177 + "!!evs. [| evs : ns_shared lost;  length evs <= length evs' |]    \
   5.178 +\        ==> Key (newK evs') ~: parts (sees lost C evs)";
   5.179  by (fast_tac (!claset addDs [lemma]) 1);
   5.180  qed "new_keys_not_seen";
   5.181  Addsimps [new_keys_not_seen];
   5.182 @@ -139,22 +160,22 @@
   5.183  goal thy 
   5.184   "!!evs. [| Says A B X : set_of_list evs;  \
   5.185  \           Key (newK evt) : parts {X};    \
   5.186 -\           evs : ns_shared                 \
   5.187 +\           evs : ns_shared lost                 \
   5.188  \        |] ==> length evt < length evs";
   5.189 -br ccontr 1;
   5.190 -bd leI 1;
   5.191 -by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Enemy]
   5.192 +by (rtac ccontr 1);
   5.193 +by (dtac leI 1);
   5.194 +by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
   5.195                        addIs  [impOfSubs parts_mono]) 1);
   5.196  qed "Says_imp_old_keys";
   5.197  
   5.198  
   5.199  (*Nobody can have USED keys that will be generated in the future.
   5.200    ...very like new_keys_not_seen*)
   5.201 -goal thy "!!evs. evs : ns_shared ==> \
   5.202 +goal thy "!!evs. evs : ns_shared lost ==> \
   5.203  \                length evs <= length evs' --> \
   5.204 -\                newK evs' ~: keysFor (UN C. parts (sees C evs))";
   5.205 -be ns_shared.induct 1;
   5.206 -bd NS3_msg_in_parts_sees_Enemy 5;
   5.207 +\                newK evs' ~: keysFor (UN C. parts (sees lost C evs))";
   5.208 +by (etac ns_shared.induct 1);
   5.209 +by parts_Fake_tac;
   5.210  by (ALLGOALS Asm_simp_tac);
   5.211  (*NS1 and NS2*)
   5.212  map (by o fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [3,2];
   5.213 @@ -162,25 +183,25 @@
   5.214  map (by o best_tac
   5.215       (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   5.216                       impOfSubs (parts_insert_subset_Un RS keysFor_mono),
   5.217 -		     Suc_leD]
   5.218 -	      addEs [new_keys_not_seen RS not_parts_not_analz RSN (2,rev_notE)]
   5.219 -	      addss (!simpset)))
   5.220 +                     Suc_leD]
   5.221 +              addEs [new_keys_not_seen RS not_parts_not_analz RSN (2,rev_notE)]
   5.222 +              addss (!simpset)))
   5.223      [2,1];
   5.224  (*NS4 and NS5: nonce exchange*)
   5.225  by (ALLGOALS (deepen_tac (!claset addSDs [Says_imp_old_keys]
   5.226 -	                          addIs  [less_SucI, impOfSubs keysFor_mono]
   5.227 -		                  addss (!simpset addsimps [le_def])) 0));
   5.228 +                                  addIs  [less_SucI, impOfSubs keysFor_mono]
   5.229 +                                  addss (!simpset addsimps [le_def])) 0));
   5.230  val lemma = result();
   5.231  
   5.232  goal thy 
   5.233 - "!!evs. [| evs : ns_shared;  length evs <= length evs' |]    \
   5.234 -\        ==> newK evs' ~: keysFor (parts (sees C evs))";
   5.235 + "!!evs. [| evs : ns_shared lost;  length evs <= length evs' |]    \
   5.236 +\        ==> newK evs' ~: keysFor (parts (sees lost C evs))";
   5.237  by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
   5.238  qed "new_keys_not_used";
   5.239  
   5.240  bind_thm ("new_keys_not_analzd",
   5.241 -	  [analz_subset_parts RS keysFor_mono,
   5.242 -	   new_keys_not_used] MRS contra_subsetD);
   5.243 +          [analz_subset_parts RS keysFor_mono,
   5.244 +           new_keys_not_used] MRS contra_subsetD);
   5.245  
   5.246  Addsimps [new_keys_not_used, new_keys_not_analzd];
   5.247  
   5.248 @@ -190,13 +211,13 @@
   5.249  (*Describes the form of K, X and K' when the Server sends this message.*)
   5.250  goal thy 
   5.251   "!!evs. [| Says Server A (Crypt {|N, Agent B, K, X|} K') : set_of_list evs; \
   5.252 -\           evs : ns_shared |]    \
   5.253 -\        ==> (EX evt:ns_shared. \
   5.254 +\           evs : ns_shared lost |]    \
   5.255 +\        ==> (EX evt: ns_shared lost. \
   5.256  \                  K = Key(newK evt) & \
   5.257  \                  X = (Crypt {|K, Agent A|} (shrK B)) & \
   5.258  \                  K' = shrK A)";
   5.259 -be rev_mp 1;
   5.260 -be ns_shared.induct 1;
   5.261 +by (etac rev_mp 1);
   5.262 +by (etac ns_shared.induct 1);
   5.263  by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   5.264  qed "Says_Server_message_form";
   5.265  
   5.266 @@ -205,24 +226,24 @@
   5.267    "parts" strengthens the induction hyp for proving the Fake case.  The
   5.268    assumptions on A are needed to prevent its being a Faked message.*)
   5.269  goal thy
   5.270 - "!!evs. evs : ns_shared ==>                                              \
   5.271 + "!!evs. evs : ns_shared lost ==>                                         \
   5.272  \            Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)               \
   5.273 -\               : parts (sees Enemy evs) &                                \
   5.274 -\            A ~: bad --> \
   5.275 -\          (EX evt:ns_shared. K = newK evt & \
   5.276 +\               : parts (sees lost Spy evs) &                           \
   5.277 +\            A ~: lost -->                                                \
   5.278 +\          (EX evt: ns_shared lost. K = newK evt & \
   5.279  \                             X = (Crypt {|Key K, Agent A|} (shrK B)))";
   5.280 -be ns_shared.induct 1;
   5.281 -bd NS3_msg_in_parts_sees_Enemy 5;
   5.282 +by (etac ns_shared.induct 1);
   5.283 +by parts_Fake_tac;
   5.284  (*Fake case*)
   5.285  by (best_tac (!claset addSDs [impOfSubs Fake_parts_insert]
   5.286 -	              addDs  [impOfSubs analz_subset_parts]
   5.287 -	              addss  (!simpset)) 2);
   5.288 +                      addDs  [impOfSubs analz_subset_parts]
   5.289 +                      addss  (!simpset)) 2);
   5.290  by (Auto_tac());
   5.291  val lemma = result() RS mp;
   5.292  
   5.293  
   5.294  (*The following theorem is proved by cases.  If the message was sent with a
   5.295 -  bad key then the Enemy reads it -- even if he didn't send it in the first
   5.296 +  bad key then the Spy reads it -- even if he didn't send it in the first
   5.297    place.*)
   5.298  
   5.299  
   5.300 @@ -231,16 +252,16 @@
   5.301    Use Says_Server_message_form if applicable.*)
   5.302  goal thy 
   5.303   "!!evs. [| Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))    \
   5.304 -\            : set_of_list evs;  evs : ns_shared |]                      \
   5.305 -\        ==> (EX evt:ns_shared. K = newK evt & length evt < length evs & \
   5.306 +\            : set_of_list evs;  evs : ns_shared lost |]                      \
   5.307 +\        ==> (EX evt: ns_shared lost. K = newK evt & length evt < length evs & \
   5.308  \                               X = (Crypt {|Key K, Agent A|} (shrK B))) | \
   5.309 -\            X : analz (sees Enemy evs)";
   5.310 -by (excluded_middle_tac "A : bad" 1);
   5.311 -by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]
   5.312 -	              addss (!simpset)) 2);
   5.313 +\            X : analz (sees lost Spy evs)";
   5.314 +by (excluded_middle_tac "A : lost" 1);
   5.315 +by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
   5.316 +                      addss (!simpset)) 2);
   5.317  by (forward_tac [lemma] 1);
   5.318  by (fast_tac (!claset addEs  partsEs
   5.319 -	              addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
   5.320 +                      addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
   5.321  by (fast_tac (!claset addIs [Says_imp_old_keys] addss (!simpset)) 1);
   5.322  qed "Says_S_message_form";
   5.323  
   5.324 @@ -249,8 +270,8 @@
   5.325  (****
   5.326   The following is to prove theorems of the form
   5.327  
   5.328 -          Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) ==>
   5.329 -          Key K : analz (sees Enemy evs)
   5.330 +          Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) ==>
   5.331 +          Key K : analz (sees lost Spy evs)
   5.332  
   5.333   A more general formula must be proved inductively.
   5.334  
   5.335 @@ -261,15 +282,15 @@
   5.336    to encrypt messages containing other keys, in the actual protocol.
   5.337    We require that agents should behave like this subsequently also.*)
   5.338  goal thy 
   5.339 - "!!evs. evs : ns_shared ==> \
   5.340 -\        (Crypt X (newK evt)) : parts (sees Enemy evs) & \
   5.341 -\        Key K : parts {X} --> Key K : parts (sees Enemy evs)";
   5.342 -be ns_shared.induct 1;
   5.343 -bd NS3_msg_in_parts_sees_Enemy 5;
   5.344 + "!!evs. evs : ns_shared lost ==> \
   5.345 +\        (Crypt X (newK evt)) : parts (sees lost Spy evs) & \
   5.346 +\        Key K : parts {X} --> Key K : parts (sees lost Spy evs)";
   5.347 +by (etac ns_shared.induct 1);
   5.348 +by parts_Fake_tac;
   5.349  by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes)));
   5.350  (*Deals with Faked messages*)
   5.351  by (best_tac (!claset addSEs partsEs
   5.352 -		      addDs [impOfSubs parts_insert_subset_Un]
   5.353 +                      addDs [impOfSubs parts_insert_subset_Un]
   5.354                        addss (!simpset)) 2);
   5.355  (*Base, NS4 and NS5*)
   5.356  by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   5.357 @@ -284,8 +305,8 @@
   5.358  Delsimps [image_Un];
   5.359  Addsimps [image_Un RS sym];
   5.360  
   5.361 -goal thy "insert (Key (newK x)) (sees A evs) = \
   5.362 -\         Key `` (newK``{x}) Un (sees A evs)";
   5.363 +goal thy "insert (Key (newK x)) (sees lost A evs) = \
   5.364 +\         Key `` (newK``{x}) Un (sees lost A evs)";
   5.365  by (Fast_tac 1);
   5.366  val insert_Key_singleton = result();
   5.367  
   5.368 @@ -307,36 +328,36 @@
   5.369  
   5.370  (*The equality makes the induction hypothesis easier to apply*)
   5.371  goal thy  
   5.372 - "!!evs. evs : ns_shared ==> \
   5.373 -\  ALL K E. (Key K : analz (Key``(newK``E) Un (sees Enemy evs))) = \
   5.374 -\           (K : newK``E | Key K : analz (sees Enemy evs))";
   5.375 -be ns_shared.induct 1;
   5.376 -by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);	
   5.377 + "!!evs. evs : ns_shared lost ==> \
   5.378 +\  ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \
   5.379 +\           (K : newK``E | Key K : analz (sees lost Spy evs))";
   5.380 +by (etac ns_shared.induct 1);
   5.381 +by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);     
   5.382  by (REPEAT ((eresolve_tac [bexE, conjE, disjE] ORELSE' hyp_subst_tac) 5));
   5.383  by (REPEAT_FIRST (resolve_tac [allI, lemma]));
   5.384  by (ALLGOALS 
   5.385      (asm_simp_tac 
   5.386       (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
   5.387 -			 @ pushes)
   5.388 +                         @ pushes)
   5.389                 setloop split_tac [expand_if])));
   5.390  (** LEVEL 5 **)
   5.391  (*NS3, Fake subcase*)
   5.392 -by (enemy_analz_tac 5);
   5.393 +by (spy_analz_tac 5);
   5.394  (*Cases NS2 and NS3!!  Simple, thanks to auto case splits*)
   5.395  by (REPEAT (Fast_tac 3));
   5.396  (*Fake case*) (** LEVEL 7 **)
   5.397 -by (enemy_analz_tac 2);
   5.398 +by (spy_analz_tac 2);
   5.399  (*Base case*)
   5.400  by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
   5.401  qed_spec_mp "analz_image_newK";
   5.402  
   5.403  
   5.404  goal thy
   5.405 - "!!evs. evs : ns_shared ==>                               \
   5.406 -\        Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) = \
   5.407 -\        (K = newK evt | Key K : analz (sees Enemy evs))";
   5.408 + "!!evs. evs : ns_shared lost ==>                               \
   5.409 +\        Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) = \
   5.410 +\        (K = newK evt | Key K : analz (sees lost Spy evs))";
   5.411  by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
   5.412 -				   insert_Key_singleton]) 1);
   5.413 +                                   insert_Key_singleton]) 1);
   5.414  by (Fast_tac 1);
   5.415  qed "analz_insert_Key_newK";
   5.416  
   5.417 @@ -347,32 +368,32 @@
   5.418  fun ex_strip_tac i = REPEAT (ares_tac [exI, conjI] i) THEN assume_tac (i+1);
   5.419  
   5.420  goal thy 
   5.421 - "!!evs. evs : ns_shared ==>                             \
   5.422 + "!!evs. evs : ns_shared lost ==>                             \
   5.423  \      EX X'. ALL A X N B.                               \
   5.424 -\       A ~: bad -->                                     \
   5.425 -\       Crypt {|N, Agent B, Key K, X|} (shrK A) : parts (sees Enemy evs) --> \
   5.426 +\       A ~: lost -->                                     \
   5.427 +\       Crypt {|N, Agent B, Key K, X|} (shrK A) : parts (sees lost Spy evs) --> \
   5.428  \       X=X'";
   5.429 -by (Simp_tac 1);	(*Miniscoping*)
   5.430 -be ns_shared.induct 1;
   5.431 -by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);	
   5.432 +by (Simp_tac 1);        (*Miniscoping*)
   5.433 +by (etac ns_shared.induct 1);
   5.434 +by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);     
   5.435  by (ALLGOALS 
   5.436      (asm_simp_tac (!simpset addsimps [all_conj_distrib, ex_disj_distrib,
   5.437 -				      imp_conj_distrib, parts_insert_sees])));
   5.438 +                                      imp_conj_distrib, parts_insert_sees])));
   5.439  by (REPEAT_FIRST (eresolve_tac [exE,disjE]));
   5.440  (*NS2: Cextraction of K = newK evsa to global context...*) 
   5.441  (** LEVEL 5 **)
   5.442  by (excluded_middle_tac "K = newK evsa" 3);
   5.443  by (Asm_simp_tac 3);
   5.444 -be exI 3;
   5.445 +by (etac exI 3);
   5.446  (*...we assume X is a very new message, and handle this case by contradiction*)
   5.447  by (fast_tac (!claset addSEs partsEs
   5.448 -		      addEs [Says_imp_old_keys RS less_irrefl]
   5.449 -	              addss (!simpset)) 3);
   5.450 +                      addEs [Says_imp_old_keys RS less_irrefl]
   5.451 +                      addss (!simpset)) 3);
   5.452  (*Base, Fake, NS3*) (** LEVEL 9 **)
   5.453  by (REPEAT_FIRST ex_strip_tac);
   5.454 -bd synth.Inj 4;
   5.455 +by (dtac synth.Inj 4);
   5.456  by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs Fake_parts_insert]
   5.457 -			            addss (!simpset))));
   5.458 +                                    addss (!simpset))));
   5.459  val lemma = result();
   5.460  
   5.461  (*In messages of this form, the session key uniquely identifies the rest*)
   5.462 @@ -383,52 +404,54 @@
   5.463  \           Says S' A'                                         \
   5.464  \             (Crypt {|N', Agent B', Key K, X'|} (shrK C')) \
   5.465  \                  : set_of_list evs;                         \
   5.466 -\           evs : ns_shared;  C ~= Enemy;  C ~: bad;  C' ~: bad |] ==> X = X'";
   5.467 -bd lemma 1;
   5.468 -be exE 1;
   5.469 +\           evs : ns_shared lost;  C ~: lost;  C' ~: lost |] ==> X = X'";
   5.470 +by (dtac lemma 1);
   5.471 +by (etac exE 1);
   5.472  (*Duplicate the assumption*)
   5.473  by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
   5.474 -by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
   5.475 +by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
   5.476  qed "unique_session_keys";
   5.477  
   5.478  
   5.479  
   5.480 -(** Crucial secrecy property: Enemy does not see the keys sent in msg NS2 **)
   5.481 +(** Crucial secrecy property: Spy does not see the keys sent in msg NS2 **)
   5.482  
   5.483  goal thy 
   5.484 - "!!evs. [| A ~: bad;  B ~: bad;  evs : ns_shared;  evt: ns_shared |]  \
   5.485 + "!!evs. [| A ~: lost;  B ~: lost;  \
   5.486 +\           evs : ns_shared lost;  evt: ns_shared lost |]  \
   5.487  \        ==> Says Server A                                             \
   5.488  \              (Crypt {|N, Agent B, Key(newK evt),                     \
   5.489  \                       Crypt {|Key(newK evt), Agent A|} (shrK B)|} (shrK A)) \
   5.490  \             : set_of_list evs --> \
   5.491 -\        Key(newK evt) ~: analz (sees Enemy evs)";
   5.492 -be ns_shared.induct 1;
   5.493 +\        Key(newK evt) ~: analz (sees lost Spy evs)";
   5.494 +by (etac ns_shared.induct 1);
   5.495  by (ALLGOALS 
   5.496      (asm_simp_tac 
   5.497       (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
   5.498 -			  analz_insert_Key_newK] @ pushes)
   5.499 +                          analz_insert_Key_newK] @ pushes)
   5.500                 setloop split_tac [expand_if])));
   5.501  (*NS2*)
   5.502  by (fast_tac (!claset addIs [parts_insertI]
   5.503 -		      addEs [Says_imp_old_keys RS less_irrefl]
   5.504 -	              addss (!simpset)) 2);
   5.505 +                      addEs [Says_imp_old_keys RS less_irrefl]
   5.506 +                      addss (!simpset)) 2);
   5.507  (*Fake case*)
   5.508 -by (enemy_analz_tac 1);
   5.509 +by (spy_analz_tac 1);
   5.510  (*NS3: that message from the Server was sent earlier*)
   5.511  by (forward_tac [Says_S_message_form] 1 THEN assume_tac 1);
   5.512  by (Step_tac 1);
   5.513 -by (enemy_analz_tac 2);		(*Prove the Fake subcase*)
   5.514 +by (REPEAT_FIRST assume_tac);
   5.515 +by (spy_analz_tac 2);           (*Prove the Fake subcase*)
   5.516  by (asm_full_simp_tac
   5.517      (!simpset addsimps (mem_if::analz_insert_Key_newK::pushes)) 1);
   5.518  by (Step_tac 1);
   5.519 -(**LEVEL 9 **)
   5.520 -by (excluded_middle_tac "Aa : bad" 1);
   5.521 -(*But this contradicts Key(newK evt) ~: analz (sees Enemy evsa) *)
   5.522 -bd (Says_imp_sees_Enemy RS analz.Inj) 2;
   5.523 +(**LEVEL 10 **)
   5.524 +by (excluded_middle_tac "Aa : lost" 1);
   5.525 +(*But this contradicts Key(newK evt) ~: analz (sees lost Spy evsa) *)
   5.526 +by (dtac (Says_imp_sees_Spy RS analz.Inj) 2);
   5.527  by (fast_tac (!claset addSDs [analz.Decrypt]
   5.528 -	              addss (!simpset)) 2);
   5.529 -(*So now we have  Aa ~: bad *)
   5.530 -bd unique_session_keys 1;
   5.531 +                      addss (!simpset)) 2);
   5.532 +(*So now we have  Aa ~: lost *)
   5.533 +by (dtac unique_session_keys 1);
   5.534  by (Auto_tac ());
   5.535  val lemma = result() RS mp RSN(2,rev_notE);
   5.536  
   5.537 @@ -437,9 +460,22 @@
   5.538  goal thy 
   5.539   "!!evs. [| Says Server A                                                \
   5.540  \            (Crypt {|N, Agent B, K, X|} K') : set_of_list evs;          \
   5.541 -\           A ~: bad;  B ~: bad;  evs : ns_shared                        \
   5.542 +\           A ~: lost;  B ~: lost;  evs : ns_shared lost                        \
   5.543  \        |] ==>                                                          \
   5.544 -\     K ~: analz (sees Enemy evs)";
   5.545 +\     K ~: analz (sees lost Spy evs)";
   5.546  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   5.547  by (fast_tac (!claset addSEs [lemma]) 1);
   5.548 -qed "Enemy_not_see_encrypted_key";
   5.549 +qed "Spy_not_see_encrypted_key";
   5.550 +
   5.551 +
   5.552 +goal thy 
   5.553 + "!!evs. [| C ~: {A,B,Server}; \
   5.554 +\           Says Server A                                                \
   5.555 +\            (Crypt {|N, Agent B, K, X|} K') : set_of_list evs;          \
   5.556 +\           A ~: lost;  B ~: lost;  evs : ns_shared lost |]                  \
   5.557 +\        ==> K ~: analz (sees lost C evs)";
   5.558 +by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   5.559 +by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
   5.560 +by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
   5.561 +by (REPEAT_FIRST (fast_tac (!claset addIs [ns_shared_mono RS subsetD])));
   5.562 +qed "Agent_not_see_encrypted_key";
     6.1 --- a/src/HOL/Auth/NS_Shared.thy	Thu Sep 26 12:47:47 1996 +0200
     6.2 +++ b/src/HOL/Auth/NS_Shared.thy	Thu Sep 26 12:50:48 1996 +0200
     6.3 @@ -12,57 +12,58 @@
     6.4  
     6.5  NS_Shared = Shared + 
     6.6  
     6.7 -consts  ns_shared   :: "event list set"
     6.8 -inductive ns_shared
     6.9 +consts  ns_shared   :: "agent set => event list set"
    6.10 +inductive "ns_shared lost"
    6.11    intrs 
    6.12           (*Initial trace is empty*)
    6.13 -    Nil  "[]: ns_shared"
    6.14 +    Nil  "[]: ns_shared lost"
    6.15  
    6.16 -         (*The enemy MAY say anything he CAN say.  We do not expect him to
    6.17 +         (*The spy MAY say anything he CAN say.  We do not expect him to
    6.18             invent new nonces here, but he can also use NS1.  Common to
    6.19             all similar protocols.*)
    6.20 -    Fake "[| evs: ns_shared;  B ~= Enemy;  X: synth (analz (sees Enemy evs)) |]
    6.21 -          ==> Says Enemy B X # evs : ns_shared"
    6.22 +    Fake "[| evs: ns_shared lost;  B ~= Spy;  
    6.23 +             X: synth (analz (sees lost Spy evs)) |]
    6.24 +          ==> Says Spy B X # evs : ns_shared lost"
    6.25  
    6.26           (*Alice initiates a protocol run, requesting to talk to any B*)
    6.27 -    NS1  "[| evs: ns_shared;  A ~= Server |]
    6.28 +    NS1  "[| evs: ns_shared lost;  A ~= Server |]
    6.29            ==> Says A Server {|Agent A, Agent B, Nonce (newN evs)|} # evs
    6.30 -                 : ns_shared"
    6.31 +                 : ns_shared lost"
    6.32  
    6.33           (*Server's response to Alice's message.
    6.34             !! It may respond more than once to A's request !!
    6.35  	   Server doesn't know who the true sender is, hence the A' in
    6.36                 the sender field.*)
    6.37 -    NS2  "[| evs: ns_shared;  A ~= B;  A ~= Server;
    6.38 +    NS2  "[| evs: ns_shared lost;  A ~= B;  A ~= Server;
    6.39               Says A' Server {|Agent A, Agent B, Nonce NA|} : set_of_list evs |]
    6.40            ==> Says Server A 
    6.41                    (Crypt {|Nonce NA, Agent B, Key (newK evs),   
    6.42                             (Crypt {|Key (newK evs), Agent A|} (shrK B))|}
    6.43 -                   (shrK A)) # evs : ns_shared"
    6.44 +                   (shrK A)) # evs : ns_shared lost"
    6.45  
    6.46            (*We can't assume S=Server.  Agent A "remembers" her nonce.
    6.47              Can inductively show A ~= Server*)
    6.48 -    NS3  "[| evs: ns_shared;  A ~= B;
    6.49 +    NS3  "[| evs: ns_shared lost;  A ~= B;
    6.50               Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) 
    6.51                 : set_of_list evs;
    6.52               Says A Server {|Agent A, Agent B, Nonce NA|} : set_of_list evs |]
    6.53 -          ==> Says A B X # evs : ns_shared"
    6.54 +          ==> Says A B X # evs : ns_shared lost"
    6.55  
    6.56           (*Bob's nonce exchange.  He does not know who the message came
    6.57             from, but responds to A because she is mentioned inside.*)
    6.58 -    NS4  "[| evs: ns_shared;  A ~= B;  
    6.59 +    NS4  "[| evs: ns_shared lost;  A ~= B;  
    6.60               Says A' B (Crypt {|Key K, Agent A|} (shrK B)) : set_of_list evs |]
    6.61 -          ==> Says B A (Crypt (Nonce (newN evs)) K) # evs : ns_shared"
    6.62 +          ==> Says B A (Crypt (Nonce (newN evs)) K) # evs : ns_shared lost"
    6.63  
    6.64           (*Alice responds with the Nonce, if she has seen the key before.
    6.65 -           We do NOT use N-1 or similar as the Enemy cannot spoof such things.
    6.66 -           Allowing the Enemy to add or subtract 1 allows him to send ALL
    6.67 +           We do NOT use N-1 or similar as the Spy cannot spoof such things.
    6.68 +           Allowing the Spy to add or subtract 1 allows him to send ALL
    6.69                 nonces.  Instead we distinguish the messages by sending the
    6.70                 nonce twice.*)
    6.71 -    NS5  "[| evs: ns_shared;  A ~= B;  
    6.72 +    NS5  "[| evs: ns_shared lost;  A ~= B;  
    6.73               Says B' A (Crypt (Nonce N) K) : set_of_list evs;
    6.74               Says S  A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))
    6.75                 : set_of_list evs |]
    6.76 -          ==> Says A B (Crypt {|Nonce N, Nonce N|} K) # evs : ns_shared"
    6.77 +          ==> Says A B (Crypt {|Nonce N, Nonce N|} K) # evs : ns_shared lost"
    6.78  
    6.79  end
     7.1 --- a/src/HOL/Auth/OtwayRees.ML	Thu Sep 26 12:47:47 1996 +0200
     7.2 +++ b/src/HOL/Auth/OtwayRees.ML	Thu Sep 26 12:50:48 1996 +0200
     7.3 @@ -22,11 +22,11 @@
     7.4  (*Weak liveness: there are traces that reach the end*)
     7.5  goal thy 
     7.6   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
     7.7 -\        ==> EX K. EX NA. EX evs: otway.          \
     7.8 +\        ==> EX K. EX NA. EX evs: otway lost.          \
     7.9  \               Says B A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|} \
    7.10  \                 : set_of_list evs";
    7.11  by (REPEAT (resolve_tac [exI,bexI] 1));
    7.12 -br (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2;
    7.13 +by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
    7.14  by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
    7.15  by (REPEAT_FIRST (resolve_tac [refl, conjI]));
    7.16  by (ALLGOALS (fast_tac (!claset addss (!simpset setsolver safe_solver))));
    7.17 @@ -35,19 +35,37 @@
    7.18  
    7.19  (**** Inductive proofs about otway ****)
    7.20  
    7.21 -(*The Enemy can see more than anybody else, except for their initial state*)
    7.22 +goal thy "!!evs. lost' <= lost ==> otway lost' <= otway lost";
    7.23 +by (rtac subsetI 1);
    7.24 +by (etac otway.induct 1);
    7.25 +by (REPEAT_FIRST
    7.26 +    (best_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
    7.27 +                              :: otway.intrs))));
    7.28 +qed "otway_mono";
    7.29 +
    7.30 +
    7.31 +(*The Spy can see more than anybody else, except for their initial state*)
    7.32  goal thy 
    7.33 - "!!evs. evs : otway ==> \
    7.34 -\     sees A evs <= initState A Un sees Enemy evs";
    7.35 -be otway.induct 1;
    7.36 + "!!evs. evs : otway lost ==> \
    7.37 +\     sees lost A evs <= initState lost A Un sees lost Spy evs";
    7.38 +by (etac otway.induct 1);
    7.39  by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] 
    7.40 -			        addss (!simpset))));
    7.41 -qed "sees_agent_subset_sees_Enemy";
    7.42 +                                addss (!simpset))));
    7.43 +qed "sees_agent_subset_sees_Spy";
    7.44 +
    7.45 +(*The Spy can see more than anybody else who's lost their key!*)
    7.46 +goal thy 
    7.47 + "!!evs. evs : otway lost ==> \
    7.48 +\        A: lost --> A ~= Server --> sees lost A evs <= sees lost Spy evs";
    7.49 +by (etac otway.induct 1);
    7.50 +by (agent.induct_tac "A" 1);
    7.51 +by (auto_tac (!claset addDs [sees_Says_subset_insert RS subsetD], (!simpset)));
    7.52 +qed_spec_mp "sees_lost_agent_subset_sees_Spy";
    7.53  
    7.54  
    7.55  (*Nobody sends themselves messages*)
    7.56 -goal thy "!!evs. evs : otway ==> ALL A X. Says A A X ~: set_of_list evs";
    7.57 -be otway.induct 1;
    7.58 +goal thy "!!evs. evs : otway lost ==> ALL A X. Says A A X ~: set_of_list evs";
    7.59 +by (etac otway.induct 1);
    7.60  by (Auto_tac());
    7.61  qed_spec_mp "not_Says_to_self";
    7.62  Addsimps [not_Says_to_self];
    7.63 @@ -57,69 +75,78 @@
    7.64  (** For reasoning about the encrypted portion of messages **)
    7.65  
    7.66  goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set_of_list evs ==> \
    7.67 -\                X : analz (sees Enemy evs)";
    7.68 -by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]) 1);
    7.69 -qed "OR2_analz_sees_Enemy";
    7.70 +\                X : analz (sees lost Spy evs)";
    7.71 +by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    7.72 +qed "OR2_analz_sees_Spy";
    7.73  
    7.74  goal thy "!!evs. Says S B {|N, X, X'|} : set_of_list evs ==> \
    7.75 -\                X : analz (sees Enemy evs)";
    7.76 -by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]) 1);
    7.77 -qed "OR4_analz_sees_Enemy";
    7.78 +\                X : analz (sees lost Spy evs)";
    7.79 +by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    7.80 +qed "OR4_analz_sees_Spy";
    7.81  
    7.82  goal thy "!!evs. Says B' A {|N, Crypt {|N,K|} K'|} : set_of_list evs ==> \
    7.83 -\                K : parts (sees Enemy evs)";
    7.84 +\                K : parts (sees lost Spy evs)";
    7.85  by (fast_tac (!claset addSEs partsEs
    7.86 -	              addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
    7.87 -qed "Reveal_parts_sees_Enemy";
    7.88 +                      addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
    7.89 +qed "Reveal_parts_sees_Spy";
    7.90  
    7.91  (*OR2_analz... and OR4_analz... let us treat those cases using the same 
    7.92    argument as for the Fake case.  This is possible for most, but not all,
    7.93    proofs: Fake does not invent new nonces (as in OR2), and of course Fake
    7.94 -  messages originate from the Enemy. *)
    7.95 +  messages originate from the Spy. *)
    7.96  
    7.97 +bind_thm ("OR2_parts_sees_Spy",
    7.98 +          OR2_analz_sees_Spy RS (impOfSubs analz_subset_parts));
    7.99 +bind_thm ("OR4_parts_sees_Spy",
   7.100 +          OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
   7.101 +
   7.102 +(*We instantiate the variable to "lost".  Leaving it as a Var makes proofs
   7.103 +  harder to complete, since simplification does less for us.*)
   7.104  val parts_Fake_tac = 
   7.105 -    forward_tac [OR2_analz_sees_Enemy RS (impOfSubs analz_subset_parts)] 4 THEN
   7.106 -    forward_tac [OR4_analz_sees_Enemy RS (impOfSubs analz_subset_parts)] 6 THEN
   7.107 -    forward_tac [Reveal_parts_sees_Enemy] 7;
   7.108 +    let val tac = forw_inst_tac [("lost","lost")] 
   7.109 +    in  tac OR2_parts_sees_Spy 4 THEN 
   7.110 +        tac OR4_parts_sees_Spy 6 THEN
   7.111 +        tac Reveal_parts_sees_Spy 7
   7.112 +    end;
   7.113  
   7.114  
   7.115 -(** Theorems of the form X ~: parts (sees Enemy evs) imply that NOBODY
   7.116 +(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
   7.117      sends messages containing X! **)
   7.118  
   7.119 -(*Enemy never sees another agent's shared key! (unless it is leaked at start)*)
   7.120 +(*Spy never sees lost another agent's shared key! (unless it is leaked at start)*)
   7.121  goal thy 
   7.122 - "!!evs. [| evs : otway;  A ~: bad |]    \
   7.123 -\        ==> Key (shrK A) ~: parts (sees Enemy evs)";
   7.124 -be otway.induct 1;
   7.125 + "!!evs. [| evs : otway lost;  A ~: lost |]    \
   7.126 +\        ==> Key (shrK A) ~: parts (sees lost Spy evs)";
   7.127 +by (etac otway.induct 1);
   7.128  by parts_Fake_tac;
   7.129  by (Auto_tac());
   7.130  (*Deals with Fake message*)
   7.131  by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   7.132 -			     impOfSubs Fake_parts_insert]) 1);
   7.133 -qed "Enemy_not_see_shrK";
   7.134 +                             impOfSubs Fake_parts_insert]) 1);
   7.135 +qed "Spy_not_see_shrK";
   7.136  
   7.137 -bind_thm ("Enemy_not_analz_shrK",
   7.138 -	  [analz_subset_parts, Enemy_not_see_shrK] MRS contra_subsetD);
   7.139 +bind_thm ("Spy_not_analz_shrK",
   7.140 +          [analz_subset_parts, Spy_not_see_shrK] MRS contra_subsetD);
   7.141  
   7.142 -Addsimps [Enemy_not_see_shrK, Enemy_not_analz_shrK];
   7.143 +Addsimps [Spy_not_see_shrK, Spy_not_analz_shrK];
   7.144  
   7.145  (*We go to some trouble to preserve R in the 3rd and 4th subgoals
   7.146    As usual fast_tac cannot be used because it uses the equalities too soon*)
   7.147  val major::prems = 
   7.148 -goal thy  "[| Key (shrK A) : parts (sees Enemy evs);       \
   7.149 -\             evs : otway;                                 \
   7.150 -\             A:bad ==> R                                  \
   7.151 +goal thy  "[| Key (shrK A) : parts (sees lost Spy evs);       \
   7.152 +\             evs : otway lost;                                 \
   7.153 +\             A:lost ==> R                                  \
   7.154  \           |] ==> R";
   7.155 -br ccontr 1;
   7.156 -br ([major, Enemy_not_see_shrK] MRS rev_notE) 1;
   7.157 +by (rtac ccontr 1);
   7.158 +by (rtac ([major, Spy_not_see_shrK] MRS rev_notE) 1);
   7.159  by (swap_res_tac prems 2);
   7.160  by (ALLGOALS (fast_tac (!claset addIs prems)));
   7.161 -qed "Enemy_see_shrK_E";
   7.162 +qed "Spy_see_shrK_E";
   7.163  
   7.164 -bind_thm ("Enemy_analz_shrK_E", 
   7.165 -	  analz_subset_parts RS subsetD RS Enemy_see_shrK_E);
   7.166 +bind_thm ("Spy_analz_shrK_E", 
   7.167 +          analz_subset_parts RS subsetD RS Spy_see_shrK_E);
   7.168  
   7.169 -AddSEs [Enemy_see_shrK_E, Enemy_analz_shrK_E];
   7.170 +AddSEs [Spy_see_shrK_E, Spy_analz_shrK_E];
   7.171  
   7.172  
   7.173  (*** Future keys can't be seen or used! ***)
   7.174 @@ -129,23 +156,23 @@
   7.175    but should go by similar reasoning every time.  Hardest case is the
   7.176    standard Fake rule.  
   7.177        The Union over C is essential for the induction! *)
   7.178 -goal thy "!!evs. evs : otway ==> \
   7.179 +goal thy "!!evs. evs : otway lost ==> \
   7.180  \                length evs <= length evs' --> \
   7.181 -\                          Key (newK evs') ~: (UN C. parts (sees C evs))";
   7.182 -be otway.induct 1;
   7.183 +\                          Key (newK evs') ~: (UN C. parts (sees lost C evs))";
   7.184 +by (etac otway.induct 1);
   7.185  by parts_Fake_tac;
   7.186  (*auto_tac does not work here, as it performs safe_tac first*)
   7.187  by (ALLGOALS Asm_simp_tac);
   7.188  by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   7.189 -					   impOfSubs parts_insert_subset_Un,
   7.190 -					   Suc_leD]
   7.191 -			            addss (!simpset))));
   7.192 +                                           impOfSubs parts_insert_subset_Un,
   7.193 +                                           Suc_leD]
   7.194 +                                    addss (!simpset))));
   7.195  val lemma = result();
   7.196  
   7.197  (*Variant needed for the main theorem below*)
   7.198  goal thy 
   7.199 - "!!evs. [| evs : otway;  length evs <= length evs' |]    \
   7.200 -\        ==> Key (newK evs') ~: parts (sees C evs)";
   7.201 + "!!evs. [| evs : otway lost;  length evs <= length evs' |]    \
   7.202 +\        ==> Key (newK evs') ~: parts (sees lost C evs)";
   7.203  by (fast_tac (!claset addDs [lemma]) 1);
   7.204  qed "new_keys_not_seen";
   7.205  Addsimps [new_keys_not_seen];
   7.206 @@ -154,37 +181,37 @@
   7.207  goal thy 
   7.208   "!!evs. [| Says A B X : set_of_list evs;  \
   7.209  \           Key (newK evt) : parts {X};    \
   7.210 -\           evs : otway                 \
   7.211 +\           evs : otway lost                 \
   7.212  \        |] ==> length evt < length evs";
   7.213 -br ccontr 1;
   7.214 -bd leI 1;
   7.215 -by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Enemy]
   7.216 +by (rtac ccontr 1);
   7.217 +by (dtac leI 1);
   7.218 +by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
   7.219                        addIs  [impOfSubs parts_mono]) 1);
   7.220  qed "Says_imp_old_keys";
   7.221  
   7.222  
   7.223  (*** Future nonces can't be seen or used! [proofs resemble those above] ***)
   7.224  
   7.225 -goal thy "!!evs. evs : otway ==> \
   7.226 +goal thy "!!evs. evs : otway lost ==> \
   7.227  \                length evs <= length evt --> \
   7.228 -\                          Nonce (newN evt) ~: (UN C. parts (sees C evs))";
   7.229 -be otway.induct 1;
   7.230 +\                Nonce (newN evt) ~: (UN C. parts (sees lost C evs))";
   7.231 +by (etac otway.induct 1);
   7.232  (*auto_tac does not work here, as it performs safe_tac first*)
   7.233 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [ parts_insert2]
   7.234 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert2]
   7.235                                       addcongs [disj_cong])));
   7.236  by (REPEAT_FIRST (fast_tac (!claset 
   7.237 -			      addSEs partsEs
   7.238 -			      addSDs  [Says_imp_sees_Enemy RS parts.Inj]
   7.239 -			      addDs  [impOfSubs analz_subset_parts,
   7.240 -				      impOfSubs parts_insert_subset_Un,
   7.241 -				      Suc_leD]
   7.242 -			      addss (!simpset))));
   7.243 +                              addSEs partsEs
   7.244 +                              addSDs  [Says_imp_sees_Spy RS parts.Inj]
   7.245 +                              addDs  [impOfSubs analz_subset_parts,
   7.246 +                                      impOfSubs parts_insert_subset_Un,
   7.247 +                                      Suc_leD]
   7.248 +                              addss (!simpset))));
   7.249  val lemma = result();
   7.250  
   7.251  (*Variant needed for the main theorem below*)
   7.252  goal thy 
   7.253 - "!!evs. [| evs : otway;  length evs <= length evs' |]    \
   7.254 -\        ==> Nonce (newN evs') ~: parts (sees C evs)";
   7.255 + "!!evs. [| evs : otway lost;  length evs <= length evs' |]    \
   7.256 +\        ==> Nonce (newN evs') ~: parts (sees lost C evs)";
   7.257  by (fast_tac (!claset addDs [lemma]) 1);
   7.258  qed "new_nonces_not_seen";
   7.259  Addsimps [new_nonces_not_seen];
   7.260 @@ -193,21 +220,21 @@
   7.261  goal thy 
   7.262   "!!evs. [| Says A B X : set_of_list evs;  \
   7.263  \           Nonce (newN evt) : parts {X};    \
   7.264 -\           evs : otway                 \
   7.265 +\           evs : otway lost                 \
   7.266  \        |] ==> length evt < length evs";
   7.267 -br ccontr 1;
   7.268 -bd leI 1;
   7.269 -by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Enemy]
   7.270 -	              addIs  [impOfSubs parts_mono]) 1);
   7.271 +by (rtac ccontr 1);
   7.272 +by (dtac leI 1);
   7.273 +by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Spy]
   7.274 +                      addIs  [impOfSubs parts_mono]) 1);
   7.275  qed "Says_imp_old_nonces";
   7.276  
   7.277  
   7.278  (*Nobody can have USED keys that will be generated in the future.
   7.279    ...very like new_keys_not_seen*)
   7.280 -goal thy "!!evs. evs : otway ==> \
   7.281 +goal thy "!!evs. evs : otway lost ==> \
   7.282  \                length evs <= length evs' --> \
   7.283 -\                newK evs' ~: keysFor (UN C. parts (sees C evs))";
   7.284 -be otway.induct 1;
   7.285 +\                newK evs' ~: keysFor (UN C. parts (sees lost C evs))";
   7.286 +by (etac otway.induct 1);
   7.287  by parts_Fake_tac;
   7.288  by (ALLGOALS Asm_simp_tac);
   7.289  (*OR1 and OR3*)
   7.290 @@ -217,26 +244,26 @@
   7.291      (map
   7.292       (best_tac
   7.293        (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   7.294 -		      impOfSubs (parts_insert_subset_Un RS keysFor_mono),
   7.295 -		      Suc_leD]
   7.296 -	       addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
   7.297 -	       addss (!simpset)))
   7.298 +                      impOfSubs (parts_insert_subset_Un RS keysFor_mono),
   7.299 +                      Suc_leD]
   7.300 +               addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
   7.301 +               addss (!simpset)))
   7.302       [3,2,1]));
   7.303  (*Reveal: dummy message*)
   7.304  by (best_tac (!claset addEs  [new_keys_not_seen RSN(2,rev_notE)]
   7.305 -		      addIs  [less_SucI, impOfSubs keysFor_mono]
   7.306 -		      addss (!simpset addsimps [le_def])) 1);
   7.307 +                      addIs  [less_SucI, impOfSubs keysFor_mono]
   7.308 +                      addss (!simpset addsimps [le_def])) 1);
   7.309  val lemma = result();
   7.310  
   7.311  goal thy 
   7.312 - "!!evs. [| evs : otway;  length evs <= length evs' |]    \
   7.313 -\        ==> newK evs' ~: keysFor (parts (sees C evs))";
   7.314 + "!!evs. [| evs : otway lost;  length evs <= length evs' |]    \
   7.315 +\        ==> newK evs' ~: keysFor (parts (sees lost C evs))";
   7.316  by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
   7.317  qed "new_keys_not_used";
   7.318  
   7.319  bind_thm ("new_keys_not_analzd",
   7.320 -	  [analz_subset_parts RS keysFor_mono,
   7.321 -	   new_keys_not_used] MRS contra_subsetD);
   7.322 +          [analz_subset_parts RS keysFor_mono,
   7.323 +           new_keys_not_used] MRS contra_subsetD);
   7.324  
   7.325  Addsimps [new_keys_not_used, new_keys_not_analzd];
   7.326  
   7.327 @@ -247,8 +274,8 @@
   7.328  (****
   7.329   The following is to prove theorems of the form
   7.330  
   7.331 -          Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) ==>
   7.332 -          Key K : analz (sees Enemy evs)
   7.333 +          Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) ==>
   7.334 +          Key K : analz (sees lost Spy evs)
   7.335  
   7.336   A more general formula must be proved inductively.
   7.337  
   7.338 @@ -259,15 +286,15 @@
   7.339    to encrypt messages containing other keys, in the actual protocol.
   7.340    We require that agents should behave like this subsequently also.*)
   7.341  goal thy 
   7.342 - "!!evs. evs : otway ==> \
   7.343 -\        (Crypt X (newK evt)) : parts (sees Enemy evs) & \
   7.344 -\        Key K : parts {X} --> Key K : parts (sees Enemy evs)";
   7.345 -be otway.induct 1;
   7.346 + "!!evs. evs : otway lost ==> \
   7.347 +\        (Crypt X (newK evt)) : parts (sees lost Spy evs) & \
   7.348 +\        Key K : parts {X} --> Key K : parts (sees lost Spy evs)";
   7.349 +by (etac otway.induct 1);
   7.350  by parts_Fake_tac;
   7.351 -by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes)));
   7.352 +by (ALLGOALS Asm_simp_tac);
   7.353  (*Deals with Faked messages*)
   7.354  by (best_tac (!claset addSEs partsEs
   7.355 -		      addDs [impOfSubs parts_insert_subset_Un]
   7.356 +                      addDs [impOfSubs parts_insert_subset_Un]
   7.357                        addss (!simpset)) 2);
   7.358  (*Base case and Reveal*)
   7.359  by (Auto_tac());
   7.360 @@ -282,8 +309,8 @@
   7.361  Delsimps [image_Un];
   7.362  Addsimps [image_Un RS sym];
   7.363  
   7.364 -goal thy "insert (Key (newK x)) (sees A evs) = \
   7.365 -\         Key `` (newK``{x}) Un (sees A evs)";
   7.366 +goal thy "insert (Key (newK x)) (sees lost A evs) = \
   7.367 +\         Key `` (newK``{x}) Un (sees lost A evs)";
   7.368  by (Fast_tac 1);
   7.369  val insert_Key_singleton = result();
   7.370  
   7.371 @@ -295,10 +322,10 @@
   7.372  
   7.373  (*This lets us avoid analyzing the new message -- unless we have to!*)
   7.374  (*NEEDED??*)
   7.375 -goal thy "synth (analz (sees Enemy evs)) <=   \
   7.376 -\         synth (analz (sees Enemy (Says A B X # evs)))";
   7.377 +goal thy "synth (analz (sees lost Spy evs)) <=   \
   7.378 +\         synth (analz (sees lost Spy (Says A B X # evs)))";
   7.379  by (Simp_tac 1);
   7.380 -br (subset_insertI RS analz_mono RS synth_mono) 1;
   7.381 +by (rtac (subset_insertI RS analz_mono RS synth_mono) 1);
   7.382  qed "synth_analz_thin";
   7.383  
   7.384  AddIs [impOfSubs synth_analz_thin];
   7.385 @@ -312,16 +339,17 @@
   7.386    assumptions on A are needed to prevent its being a Faked message.  (Based
   7.387    on NS_Shared/Says_S_message_form) *)
   7.388  goal thy
   7.389 - "!!evs. evs: otway ==>                                           \
   7.390 -\          Crypt {|N, Key K|} (shrK A) : parts (sees Enemy evs) & \
   7.391 -\          A ~: bad -->                                           \
   7.392 -\        (EX evt:otway. K = newK evt)";
   7.393 -be otway.induct 1;
   7.394 + "!!evs. evs: otway lost ==>                                           \
   7.395 +\          Crypt {|N, Key K|} (shrK A) : parts (sees lost Spy evs) & \
   7.396 +\          A ~: lost -->                                           \
   7.397 +\        (EX evt: otway lost. K = newK evt)";
   7.398 +by (etac otway.induct 1);
   7.399  by parts_Fake_tac;
   7.400 -by (Auto_tac());
   7.401 +by (ALLGOALS Asm_simp_tac);
   7.402  (*Deals with Fake message*)
   7.403  by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   7.404 -			     impOfSubs Fake_parts_insert]) 1);
   7.405 +                             impOfSubs Fake_parts_insert]) 2);
   7.406 +by (Auto_tac());
   7.407  val lemma = result() RS mp;
   7.408  
   7.409  
   7.410 @@ -329,14 +357,14 @@
   7.411    OR     reduces it to the Fake case.*)
   7.412  goal thy 
   7.413   "!!evs. [| Says B' A {|N, Crypt {|N, Key K|} (shrK A)|} : set_of_list evs;  \
   7.414 -\           evs : otway |]                      \
   7.415 -\        ==> (EX evt:otway. K = newK evt) | Key K : analz (sees Enemy evs)";
   7.416 -by (excluded_middle_tac "A : bad" 1);
   7.417 -by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]
   7.418 -	              addss (!simpset)) 2);
   7.419 +\           evs : otway lost |]                      \
   7.420 +\        ==> (EX evt: otway lost. K = newK evt) | Key K : analz (sees lost Spy evs)";
   7.421 +by (excluded_middle_tac "A : lost" 1);
   7.422 +by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
   7.423 +                      addss (!simpset)) 2);
   7.424  by (forward_tac [lemma] 1);
   7.425  by (fast_tac (!claset addEs  partsEs
   7.426 -	              addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
   7.427 +                      addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
   7.428  by (Fast_tac 1);
   7.429  qed "Reveal_message_form";
   7.430  
   7.431 @@ -352,34 +380,34 @@
   7.432  
   7.433  (*The equality makes the induction hypothesis easier to apply*)
   7.434  goal thy  
   7.435 - "!!evs. evs : otway ==> \
   7.436 -\  ALL K E. (Key K : analz (Key``(newK``E) Un (sees Enemy evs))) = \
   7.437 -\           (K : newK``E | Key K : analz (sees Enemy evs))";
   7.438 -be otway.induct 1;
   7.439 -bd OR2_analz_sees_Enemy 4;
   7.440 -bd OR4_analz_sees_Enemy 6;
   7.441 -bd Reveal_message_form 7;
   7.442 + "!!evs. evs : otway lost ==> \
   7.443 +\  ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \
   7.444 +\           (K : newK``E | Key K : analz (sees lost Spy evs))";
   7.445 +by (etac otway.induct 1);
   7.446 +by (dtac OR2_analz_sees_Spy 4);
   7.447 +by (dtac OR4_analz_sees_Spy 6);
   7.448 +by (dtac Reveal_message_form 7);
   7.449  by (REPEAT_FIRST (ares_tac [allI, lemma]));
   7.450  by (REPEAT ((eresolve_tac [bexE, disjE] ORELSE' hyp_subst_tac) 7));
   7.451  by (ALLGOALS (*Takes 28 secs*)
   7.452      (asm_simp_tac 
   7.453       (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
   7.454 -			 @ pushes)
   7.455 +                         @ pushes)
   7.456                 setloop split_tac [expand_if])));
   7.457  (** LEVEL 7 **)
   7.458  (*Reveal case 2, OR4, OR2, Fake*) 
   7.459 -by (EVERY (map enemy_analz_tac [7,5,3,2]));
   7.460 +by (EVERY (map spy_analz_tac [7,5,3,2]));
   7.461  (*Reveal case 1, OR3, Base*)
   7.462  by (Auto_tac());
   7.463  qed_spec_mp "analz_image_newK";
   7.464  
   7.465  
   7.466  goal thy
   7.467 - "!!evs. evs : otway ==>                               \
   7.468 -\        Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) = \
   7.469 -\        (K = newK evt | Key K : analz (sees Enemy evs))";
   7.470 + "!!evs. evs : otway lost ==>                               \
   7.471 +\        Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) = \
   7.472 +\        (K = newK evt | Key K : analz (sees lost Spy evs))";
   7.473  by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
   7.474 -				   insert_Key_singleton]) 1);
   7.475 +                                   insert_Key_singleton]) 1);
   7.476  by (Fast_tac 1);
   7.477  qed "analz_insert_Key_newK";
   7.478  
   7.479 @@ -389,13 +417,13 @@
   7.480  fun ex_strip_tac i = REPEAT (ares_tac [exI, conjI] i) THEN assume_tac (i+1);
   7.481  
   7.482  goal thy 
   7.483 - "!!evs. evs : otway ==>                      \
   7.484 + "!!evs. evs : otway lost ==>                      \
   7.485  \      EX A' B' NA' NB'. ALL A B NA NB.                    \
   7.486  \       Says Server B \
   7.487  \            {|NA, Crypt {|NA, K|} (shrK A),                      \
   7.488  \                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs --> \
   7.489  \       A=A' & B=B' & NA=NA' & NB=NB'";
   7.490 -be otway.induct 1;
   7.491 +by (etac otway.induct 1);
   7.492  by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   7.493  by (Step_tac 1);
   7.494  (*Remaining cases: OR3 and OR4*)
   7.495 @@ -406,8 +434,8 @@
   7.496  by (REPEAT (ares_tac [refl,exI,impI,conjI] 1));
   7.497  (*...we assume X is a very new message, and handle this case by contradiction*)
   7.498  by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
   7.499 -	              delrules [conjI]    (*prevent split-up into 4 subgoals*)
   7.500 -	              addss (!simpset addsimps [parts_insertI])) 1);
   7.501 +                      delrules [conjI]    (*prevent split-up into 4 subgoals*)
   7.502 +                      addss (!simpset addsimps [parts_insertI])) 1);
   7.503  val lemma = result();
   7.504  
   7.505  goal thy 
   7.506 @@ -419,9 +447,9 @@
   7.507  \              {|NA', Crypt {|NA', K|} (shrK A'),                  \
   7.508  \                     Crypt {|NB', K|} (shrK B')|}                 \
   7.509  \            : set_of_list evs;                                    \
   7.510 -\           evs : otway |]                                         \
   7.511 +\           evs : otway lost |]                                         \
   7.512  \        ==> A=A' & B=B' & NA=NA' & NB=NB'";
   7.513 -bd lemma 1;
   7.514 +by (dtac lemma 1);
   7.515  by (REPEAT (etac exE 1));
   7.516  (*Duplicate the assumption*)
   7.517  by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
   7.518 @@ -434,18 +462,18 @@
   7.519  
   7.520  (*Only OR1 can have caused such a part of a message to appear.*)
   7.521  goal thy 
   7.522 - "!!evs. [| A ~: bad;  evs : otway |]               \
   7.523 + "!!evs. [| A ~: lost;  evs : otway lost |]               \
   7.524  \        ==> Crypt {|NA, Agent A, Agent B|} (shrK A)        \
   7.525 -\             : parts (sees Enemy evs) -->                  \
   7.526 +\             : parts (sees lost Spy evs) -->                  \
   7.527  \            Says A B {|NA, Agent A, Agent B,               \
   7.528  \                       Crypt {|NA, Agent A, Agent B|} (shrK A)|}  \
   7.529  \             : set_of_list evs";
   7.530 -be otway.induct 1;
   7.531 +by (etac otway.induct 1);
   7.532  by parts_Fake_tac;
   7.533  by (ALLGOALS Asm_simp_tac);
   7.534  (*Fake*)
   7.535  by (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
   7.536 -			      impOfSubs Fake_parts_insert]) 2);
   7.537 +                              impOfSubs Fake_parts_insert]) 2);
   7.538  by (Auto_tac());
   7.539  qed_spec_mp "Crypt_imp_OR1";
   7.540  
   7.541 @@ -453,16 +481,16 @@
   7.542  (** The Nonce NA uniquely identifies A's  message. **)
   7.543  
   7.544  goal thy 
   7.545 - "!!evs. [| evs : otway; A ~: bad |]               \
   7.546 + "!!evs. [| evs : otway lost; A ~: lost |]               \
   7.547  \ ==> EX B'. ALL B.    \
   7.548 -\        Crypt {|NA, Agent A, Agent B|} (shrK A) : parts (sees Enemy evs) --> \
   7.549 +\        Crypt {|NA, Agent A, Agent B|} (shrK A) : parts (sees lost Spy evs) --> \
   7.550  \        B = B'";
   7.551 -be otway.induct 1;
   7.552 +by (etac otway.induct 1);
   7.553  by parts_Fake_tac;
   7.554  by (ALLGOALS Asm_simp_tac);
   7.555  (*Fake*)
   7.556  by (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
   7.557 -			      impOfSubs Fake_parts_insert]) 2);
   7.558 +                              impOfSubs Fake_parts_insert]) 2);
   7.559  (*Base case*)
   7.560  by (fast_tac (!claset addss (!simpset)) 1);
   7.561  by (Step_tac 1);
   7.562 @@ -471,16 +499,16 @@
   7.563  by (Asm_simp_tac 1);
   7.564  by (Fast_tac 1);
   7.565  by (best_tac (!claset addSEs partsEs
   7.566 -	              addEs  [new_nonces_not_seen RSN(2,rev_notE)]) 1);
   7.567 +                      addEs  [new_nonces_not_seen RSN(2,rev_notE)]) 1);
   7.568  val lemma = result();
   7.569  
   7.570  goal thy 
   7.571 - "!!evs.[| Crypt {|NA, Agent A, Agent B|} (shrK A) : parts (sees Enemy evs); \ 
   7.572 -\          Crypt {|NA, Agent A, Agent C|} (shrK A) : parts (sees Enemy evs); \ 
   7.573 -\          evs : otway;  A ~: bad |]                                         \
   7.574 + "!!evs.[| Crypt {|NA, Agent A, Agent B|} (shrK A) : parts (sees lost Spy evs); \ 
   7.575 +\          Crypt {|NA, Agent A, Agent C|} (shrK A) : parts (sees lost Spy evs); \ 
   7.576 +\          evs : otway lost;  A ~: lost |]                                         \
   7.577  \        ==> B = C";
   7.578 -bd lemma 1;
   7.579 -ba 1;
   7.580 +by (dtac lemma 1);
   7.581 +by (assume_tac 1);
   7.582  by (etac exE 1);
   7.583  (*Duplicate the assumption*)
   7.584  by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
   7.585 @@ -494,22 +522,22 @@
   7.586    OR2 encrypts Nonce NB.  It prevents the attack that can occur in the
   7.587    over-simplified version of this protocol: see OtwayRees_Bad.*)
   7.588  goal thy 
   7.589 - "!!evs. [| A ~: bad;  evs : otway |]                            \
   7.590 + "!!evs. [| A ~: lost;  evs : otway lost |]                            \
   7.591  \        ==> Crypt {|NA, Agent A, Agent B|} (shrK A)             \
   7.592 -\             : parts (sees Enemy evs) -->                       \
   7.593 +\             : parts (sees lost Spy evs) -->                       \
   7.594  \            Crypt {|NA', NA, Agent A', Agent A|} (shrK A)       \
   7.595 -\             ~: parts (sees Enemy evs)";
   7.596 -be otway.induct 1;
   7.597 +\             ~: parts (sees lost Spy evs)";
   7.598 +by (etac otway.induct 1);
   7.599  by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert2])));
   7.600  (*It is hard to generate this proof in a reasonable amount of time*)
   7.601  by (step_tac (!claset addSEs [MPair_parts, nonce_not_seen_now]
   7.602 -                      addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
   7.603 +                      addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
   7.604  by (REPEAT_FIRST (fast_tac (!claset (*40 seconds??*)
   7.605 -			    addSDs  [impOfSubs analz_subset_parts,
   7.606 -				     impOfSubs parts_insert_subset_Un]
   7.607 -			    addss  (!simpset))));
   7.608 +                            addSDs  [impOfSubs analz_subset_parts,
   7.609 +                                     impOfSubs parts_insert_subset_Un]
   7.610 +                            addss  (!simpset))));
   7.611  by (REPEAT_FIRST (fast_tac (!claset 
   7.612 -			      addSEs (partsEs@[nonce_not_seen_now])
   7.613 +                              addSEs (partsEs@[nonce_not_seen_now])
   7.614                                addSDs  [impOfSubs parts_insert_subset_Un]
   7.615                                addss (!simpset))));
   7.616  qed_spec_mp"no_nonce_OR1_OR2";
   7.617 @@ -519,8 +547,8 @@
   7.618  (*If the encrypted message appears, and A has used Nonce NA to start a run,
   7.619    then it originated with the Server!*)
   7.620  goal thy 
   7.621 - "!!evs. [| A ~: bad;  evs : otway |]                                        \
   7.622 -\        ==> Crypt {|Nonce NA, Key K|} (shrK A) : parts (sees Enemy evs) --> \
   7.623 + "!!evs. [| A ~: lost;  A ~= Spy;  evs : otway lost |]                     \
   7.624 +\        ==> Crypt {|Nonce NA, Key K|} (shrK A) : parts (sees lost Spy evs) --> \
   7.625  \            Says A B {|Nonce NA, Agent A, Agent B,                          \
   7.626  \                       Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|}      \
   7.627  \             : set_of_list evs -->                                          \
   7.628 @@ -529,43 +557,43 @@
   7.629  \                   Crypt {|Nonce NA, Key K|} (shrK A),                      \
   7.630  \                   Crypt {|Nonce NB, Key K|} (shrK B)|}                     \
   7.631  \                   : set_of_list evs)";
   7.632 -be otway.induct 1;
   7.633 +by (etac otway.induct 1);
   7.634  by parts_Fake_tac;
   7.635  by (ALLGOALS Asm_simp_tac);
   7.636  (*Fake*)
   7.637  by (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
   7.638 -			      impOfSubs Fake_parts_insert]) 1);
   7.639 +                              impOfSubs Fake_parts_insert]) 1);
   7.640  (*OR1: it cannot be a new Nonce, contradiction.*)
   7.641  by (fast_tac (!claset addSIs [parts_insertI]
   7.642 -		      addSEs partsEs
   7.643 -		      addEs [Says_imp_old_nonces RS less_irrefl]
   7.644 -	              addss (!simpset)) 1);
   7.645 +                      addSEs partsEs
   7.646 +                      addEs [Says_imp_old_nonces RS less_irrefl]
   7.647 +                      addss (!simpset)) 1);
   7.648  (*OR3 and OR4*)  (** LEVEL 5 **)
   7.649  (*OR4*)
   7.650  by (REPEAT (Safe_step_tac 2));
   7.651  by (REPEAT (best_tac (!claset addSDs [parts_cut]) 3));
   7.652  by (fast_tac (!claset addSIs [Crypt_imp_OR1]
   7.653 -		      addEs  partsEs
   7.654 -	              addDs [Says_imp_sees_Enemy RS parts.Inj]) 2);
   7.655 +                      addEs  partsEs
   7.656 +                      addDs [Says_imp_sees_Spy RS parts.Inj]) 2);
   7.657  (*OR3*)  (** LEVEL 8 **)
   7.658  by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
   7.659  by (step_tac (!claset delrules [disjCI, impCE]) 1);
   7.660 -by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS parts.Inj]
   7.661 +by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
   7.662                        addSEs [MPair_parts]
   7.663                        addEs  [unique_OR1_nonce]) 1);
   7.664  by (fast_tac (!claset addSEs [MPair_parts]
   7.665 -                      addSDs [Says_imp_sees_Enemy RS parts.Inj]
   7.666 +                      addSDs [Says_imp_sees_Spy RS parts.Inj]
   7.667                        addEs  [no_nonce_OR1_OR2 RSN (2, rev_notE)]
   7.668 -	              delrules [conjI] (*stop split-up into 4 subgoals*)) 1);
   7.669 +                      delrules [conjI] (*stop split-up into 4 subgoals*)) 1);
   7.670  qed_spec_mp "Crypt_imp_Server_msg";
   7.671  
   7.672  
   7.673  (*Crucial property: if A receives B's OR4 message and the nonce NA agrees
   7.674    then the key really did come from the Server!  CANNOT prove this of the
   7.675 -  bad form of this protocol, even though we can prove
   7.676 -  Enemy_not_see_encrypted_key*)
   7.677 +  lost form of this protocol, even though we can prove
   7.678 +  Spy_not_see_encrypted_key*)
   7.679  goal thy 
   7.680 - "!!evs. [| A ~: bad;  evs : otway |]                                    \
   7.681 + "!!evs. [| A ~: lost;  A ~= Spy;  evs : otway lost |]                 \
   7.682  \        ==> Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|}  \
   7.683  \             : set_of_list evs -->                                      \
   7.684  \            Says A B {|Nonce NA, Agent A, Agent B,                      \
   7.685 @@ -576,32 +604,30 @@
   7.686  \                       Crypt {|Nonce NA, Key K|} (shrK A),              \
   7.687  \                       Crypt {|Nonce NB, Key K|} (shrK B)|}             \
   7.688  \                       : set_of_list evs)";
   7.689 -be otway.induct 1;
   7.690 +by (etac otway.induct 1);
   7.691  by (ALLGOALS (asm_simp_tac (!simpset addcongs [conj_cong])));
   7.692  (*OR2*)
   7.693  by (Fast_tac 3);
   7.694  (*OR1: it cannot be a new Nonce, contradiction.*)
   7.695  by (fast_tac (!claset addSIs [parts_insertI]
   7.696 -		      addEs [Says_imp_old_nonces RS less_irrefl]
   7.697 -	              addss (!simpset)) 2);
   7.698 +                      addEs [Says_imp_old_nonces RS less_irrefl]
   7.699 +                      addss (!simpset)) 2);
   7.700  (*Fake, OR4*) (** LEVEL 4 **)
   7.701  by (step_tac (!claset delrules [impCE]) 1);
   7.702  by (ALLGOALS Asm_simp_tac);
   7.703  by (Fast_tac 4);
   7.704  by (fast_tac (!claset addSIs [Crypt_imp_OR1]
   7.705 -		      addEs  partsEs
   7.706 -	              addDs [Says_imp_sees_Enemy RS parts.Inj]) 3);
   7.707 +                      addEs  partsEs
   7.708 +                      addDs [Says_imp_sees_Spy RS parts.Inj]) 3);
   7.709  (** LEVEL 8 **)
   7.710  (*Still subcases of Fake and OR4*)
   7.711  by (fast_tac (!claset addSIs [Crypt_imp_Server_msg]
   7.712 -	              addDs  [impOfSubs analz_subset_parts]) 1);
   7.713 +                      addDs  [impOfSubs analz_subset_parts]) 1);
   7.714  by (fast_tac (!claset addSIs [Crypt_imp_Server_msg]
   7.715 -	              addEs  partsEs
   7.716 -	              addDs  [Says_imp_sees_Enemy RS parts.Inj]) 1);
   7.717 -val lemma = result();
   7.718 -
   7.719 +                      addEs  partsEs
   7.720 +                      addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
   7.721  val OR4_imp_Says_Server_A = 
   7.722 -    lemma RSN (2, rev_mp) RS mp |> standard;
   7.723 +    result() RSN (2, rev_mp) RS mp |> standard;
   7.724  
   7.725  
   7.726  
   7.727 @@ -610,48 +636,48 @@
   7.728   "!!evs. [| Says Server B \
   7.729  \            {|NA, Crypt {|NA, K|} (shrK A),                      \
   7.730  \                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs;  \
   7.731 -\           evs : otway |]                                        \
   7.732 -\        ==> (EX evt:otway. K = Key(newK evt)) &                  \
   7.733 +\           evs : otway lost |]                                        \
   7.734 +\        ==> (EX evt: otway lost. K = Key(newK evt)) &                  \
   7.735  \            (EX i. NA = Nonce i)";
   7.736 -be rev_mp 1;
   7.737 -be otway.induct 1;
   7.738 +by (etac rev_mp 1);
   7.739 +by (etac otway.induct 1);
   7.740  by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset))));
   7.741  qed "Says_Server_message_form";
   7.742  
   7.743  
   7.744 -(** Crucial secrecy property: Enemy does not see the keys sent in msg OR3 **)
   7.745 +(** Crucial secrecy property: Spy does not see the keys sent in msg OR3 **)
   7.746  
   7.747  goal thy 
   7.748 - "!!evs. [| A ~: bad;  B ~: bad;  evs : otway;  evt : otway |]         \
   7.749 + "!!evs. [| A ~: lost;  B ~: lost;  evs : otway lost;  evt : otway lost |] \
   7.750  \        ==> Says Server B                                             \
   7.751  \              {|Nonce NA, Crypt {|Nonce NA, Key(newK evt)|} (shrK A), \
   7.752  \                Crypt {|NB, Key(newK evt)|} (shrK B)|} : set_of_list evs --> \
   7.753 -\            Says A Enemy {|Nonce NA, Key(newK evt)|} ~: set_of_list evs --> \
   7.754 -\            Key(newK evt) ~: analz (sees Enemy evs)";
   7.755 -be otway.induct 1;
   7.756 -bd OR2_analz_sees_Enemy 4;
   7.757 -bd OR4_analz_sees_Enemy 6;
   7.758 +\            Says A Spy {|Nonce NA, Key(newK evt)|} ~: set_of_list evs --> \
   7.759 +\            Key(newK evt) ~: analz (sees lost Spy evs)";
   7.760 +by (etac otway.induct 1);
   7.761 +by (dtac OR2_analz_sees_Spy 4);
   7.762 +by (dtac OR4_analz_sees_Spy 6);
   7.763  by (forward_tac [Reveal_message_form] 7);
   7.764  by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, disjE] ORELSE' hyp_subst_tac));
   7.765  by (ALLGOALS
   7.766      (asm_full_simp_tac 
   7.767       (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
   7.768 -			  analz_insert_Key_newK] @ pushes)
   7.769 +                          analz_insert_Key_newK] @ pushes)
   7.770                 setloop split_tac [expand_if])));
   7.771  (** LEVEL 6 **)
   7.772  (*OR3*)
   7.773  by (fast_tac (!claset addSIs [parts_insertI]
   7.774 -		      addEs [Says_imp_old_keys RS less_irrefl]
   7.775 -	              addss (!simpset)) 3);
   7.776 +                      addEs [Says_imp_old_keys RS less_irrefl]
   7.777 +                      addss (!simpset)) 3);
   7.778  (*Reveal case 2, OR4, OR2, Fake*) 
   7.779 -by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' enemy_analz_tac));
   7.780 +by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));
   7.781  (*Reveal case 1*) (** LEVEL 8 **)
   7.782 -by (excluded_middle_tac "Aa : bad" 1);
   7.783 -(*But this contradicts Key(newK evt) ~: analz (sees Enemy evsa) *)
   7.784 -bd (Says_imp_sees_Enemy RS analz.Inj) 2;
   7.785 +by (excluded_middle_tac "Aa : lost" 1);
   7.786 +(*But this contradicts Key(newK evt) ~: analz (sees lost Spy evsa) *)
   7.787 +by (dtac (Says_imp_sees_Spy RS analz.Inj) 2);
   7.788  by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 2);
   7.789 -(*So now we have  Aa ~: bad *)
   7.790 -by (dresolve_tac [OR4_imp_Says_Server_A] 1);
   7.791 +(*So now we have  Aa ~: lost *)
   7.792 +by (dtac OR4_imp_Says_Server_A 1);
   7.793  by (REPEAT (assume_tac 1));
   7.794  by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 1);
   7.795  val lemma = result() RS mp RS mp RSN(2,rev_notE);
   7.796 @@ -660,32 +686,46 @@
   7.797   "!!evs. [| Says Server B \
   7.798  \            {|NA, Crypt {|NA, K|} (shrK A),                      \
   7.799  \                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs;  \
   7.800 -\           Says A Enemy {|NA, K|} ~: set_of_list evs;            \
   7.801 -\           A ~: bad;  B ~: bad;  evs : otway |]                  \
   7.802 -\        ==> K ~: analz (sees Enemy evs)";
   7.803 +\           Says A Spy {|NA, K|} ~: set_of_list evs;            \
   7.804 +\           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
   7.805 +\        ==> K ~: analz (sees lost Spy evs)";
   7.806  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   7.807  by (fast_tac (!claset addSEs [lemma]) 1);
   7.808 -qed "Enemy_not_see_encrypted_key";
   7.809 +qed "Spy_not_see_encrypted_key";
   7.810 +
   7.811  
   7.812 +goal thy 
   7.813 + "!!evs. [| C ~: {A,B,Server}; \
   7.814 +\           Says Server B \
   7.815 +\            {|NA, Crypt {|NA, K|} (shrK A),                      \
   7.816 +\                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs;  \
   7.817 +\           Says A Spy {|NA, K|} ~: set_of_list evs;            \
   7.818 +\           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
   7.819 +\        ==> K ~: analz (sees lost C evs)";
   7.820 +by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   7.821 +by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
   7.822 +by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
   7.823 +by (REPEAT_FIRST (fast_tac (!claset addIs [otway_mono RS subsetD])));
   7.824 +qed "Agent_not_see_encrypted_key";
   7.825  
   7.826  
   7.827  (** A session key uniquely identifies a pair of senders in the message
   7.828      encrypted by a good agent C. **)
   7.829  goal thy 
   7.830 - "!!evs. evs : otway ==>                                           \
   7.831 + "!!evs. evs : otway lost ==>                                           \
   7.832  \      EX A B. ALL C N.                                            \
   7.833 -\         C ~: bad -->                                             \
   7.834 -\         Crypt {|N, Key K|} (shrK C) : parts (sees Enemy evs) --> \
   7.835 +\         C ~: lost -->                                             \
   7.836 +\         Crypt {|N, Key K|} (shrK C) : parts (sees lost Spy evs) --> \
   7.837  \         C=A | C=B";
   7.838 -by (Simp_tac 1);	(*Miniscoping*)
   7.839 -be otway.induct 1;
   7.840 -bd OR2_analz_sees_Enemy 4;
   7.841 -bd OR4_analz_sees_Enemy 6;
   7.842 -(*enemy_analz_tac just does not work here: it is an entirely different proof!*)
   7.843 +by (Simp_tac 1);        (*Miniscoping*)
   7.844 +by (etac otway.induct 1);
   7.845 +by (dres_inst_tac [("lost","lost")] OR2_analz_sees_Spy 4);
   7.846 +by (dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6);
   7.847 +(*spy_analz_tac just does not work here: it is an entirely different proof!*)
   7.848  by (ALLGOALS 
   7.849      (asm_simp_tac (!simpset addsimps [all_conj_distrib, ex_disj_distrib,
   7.850 -				      imp_conj_distrib, parts_insert_sees,
   7.851 -				      parts_insert2])));
   7.852 +                                      imp_conj_distrib, parts_insert_sees,
   7.853 +                                      parts_insert2])));
   7.854  by (REPEAT_FIRST (etac exE));
   7.855  (*OR3: extraction of K = newK evsa to global context...*) (** LEVEL 6 **)
   7.856  by (excluded_middle_tac "K = newK evsa" 4);
   7.857 @@ -693,13 +733,16 @@
   7.858  by (REPEAT (ares_tac [exI] 4));
   7.859  (*...we prove this case by contradiction: the key is too new!*)
   7.860  by (fast_tac (!claset addSEs partsEs
   7.861 -		      addEs [Says_imp_old_keys RS less_irrefl]
   7.862 -	              addss (!simpset)) 4);
   7.863 +                      addEs [Says_imp_old_keys RS less_irrefl]
   7.864 +                      addss (!simpset)) 4);
   7.865  (*Base, Fake, OR2, OR4*)
   7.866  by (REPEAT_FIRST ex_strip_tac);
   7.867 -bd synth.Inj 4;
   7.868 -bd synth.Inj 3;
   7.869 +by (dtac synth.Inj 4);
   7.870 +by (dtac synth.Inj 3);
   7.871  (*Now in effect there are three Fake cases*)
   7.872  by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs Fake_parts_insert]
   7.873 -			            addss (!simpset))));
   7.874 +                                    delrules [disjCI, disjE]
   7.875 +                                    addss (!simpset))));
   7.876  qed "key_identifies_senders";
   7.877 +
   7.878 +
     8.1 --- a/src/HOL/Auth/OtwayRees.thy	Thu Sep 26 12:47:47 1996 +0200
     8.2 +++ b/src/HOL/Auth/OtwayRees.thy	Thu Sep 26 12:50:48 1996 +0200
     8.3 @@ -14,40 +14,41 @@
     8.4  
     8.5  OtwayRees = Shared + 
     8.6  
     8.7 -consts  otway   :: "event list set"
     8.8 -inductive otway
     8.9 +consts  otway   :: "agent set => event list set"
    8.10 +inductive "otway lost"
    8.11    intrs 
    8.12           (*Initial trace is empty*)
    8.13 -    Nil  "[]: otway"
    8.14 +    Nil  "[]: otway lost"
    8.15  
    8.16 -         (*The enemy MAY say anything he CAN say.  We do not expect him to
    8.17 +         (*The spy MAY say anything he CAN say.  We do not expect him to
    8.18             invent new nonces here, but he can also use NS1.  Common to
    8.19             all similar protocols.*)
    8.20 -    Fake "[| evs: otway;  B ~= Enemy;  X: synth (analz (sees Enemy evs)) |]
    8.21 -          ==> Says Enemy B X  # evs : otway"
    8.22 +    Fake "[| evs: otway lost;  B ~= Spy;  
    8.23 +             X: synth (analz (sees lost Spy evs)) |]
    8.24 +          ==> Says Spy B X  # evs : otway lost"
    8.25  
    8.26           (*Alice initiates a protocol run*)
    8.27 -    OR1  "[| evs: otway;  A ~= B;  B ~= Server |]
    8.28 +    OR1  "[| evs: otway lost;  A ~= B;  B ~= Server |]
    8.29            ==> Says A B {|Nonce (newN evs), Agent A, Agent B, 
    8.30                           Crypt {|Nonce (newN evs), Agent A, Agent B|} 
    8.31                                 (shrK A) |} 
    8.32 -                 # evs : otway"
    8.33 +                 # evs : otway lost"
    8.34  
    8.35           (*Bob's response to Alice's message.  Bob doesn't know who 
    8.36  	   the sender is, hence the A' in the sender field.
    8.37             We modify the published protocol by NOT encrypting NB.*)
    8.38 -    OR2  "[| evs: otway;  B ~= Server;
    8.39 +    OR2  "[| evs: otway lost;  B ~= Server;
    8.40               Says A' B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |]
    8.41            ==> Says B Server 
    8.42                    {|Nonce NA, Agent A, Agent B, X, 
    8.43                      Crypt {|Nonce NA, Nonce (newN evs), 
    8.44                              Agent A, Agent B|} (shrK B)|}
    8.45 -                 # evs : otway"
    8.46 +                 # evs : otway lost"
    8.47  
    8.48           (*The Server receives Bob's message and checks that the three NAs
    8.49             match.  Then he sends a new session key to Bob with a packet for
    8.50             forwarding to Alice.*)
    8.51 -    OR3  "[| evs: otway;  B ~= Server;
    8.52 +    OR3  "[| evs: otway lost;  B ~= Server;
    8.53               Says B' Server 
    8.54                    {|Nonce NA, Agent A, Agent B, 
    8.55                      Crypt {|Nonce NA, Agent A, Agent B|} (shrK A), 
    8.56 @@ -57,27 +58,27 @@
    8.57                    {|Nonce NA, 
    8.58                      Crypt {|Nonce NA, Key (newK evs)|} (shrK A),
    8.59                      Crypt {|Nonce NB, Key (newK evs)|} (shrK B)|}
    8.60 -                 # evs : otway"
    8.61 +                 # evs : otway lost"
    8.62  
    8.63           (*Bob receives the Server's (?) message and compares the Nonces with
    8.64  	   those in the message he previously sent the Server.*)
    8.65 -    OR4  "[| evs: otway;  A ~= B;  B ~= Server;
    8.66 +    OR4  "[| evs: otway lost;  A ~= B;  B ~= Server;
    8.67               Says S B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|}
    8.68                 : set_of_list evs;
    8.69               Says B Server {|Nonce NA, Agent A, Agent B, X', 
    8.70                               Crypt {|Nonce NA, Nonce NB, Agent A, Agent B|} 
    8.71                                     (shrK B)|}
    8.72                 : set_of_list evs |]
    8.73 -          ==> Says B A {|Nonce NA, X|} # evs : otway"
    8.74 +          ==> Says B A {|Nonce NA, X|} # evs : otway lost"
    8.75  
    8.76           (*This message models possible leaks of session keys.  Alice's Nonce
    8.77             identifies the protocol run.*)
    8.78 -    Reveal "[| evs: otway;  A ~= Enemy;
    8.79 +    Reveal "[| evs: otway lost;  A ~= Spy;
    8.80                 Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|}
    8.81                   : set_of_list evs;
    8.82                 Says A  B {|Nonce NA, Agent A, Agent B, 
    8.83                             Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|}
    8.84                   : set_of_list evs |]
    8.85 -            ==> Says A Enemy {|Nonce NA, Key K|} # evs : otway"
    8.86 +            ==> Says A Spy {|Nonce NA, Key K|} # evs : otway lost"
    8.87  
    8.88  end
     9.1 --- a/src/HOL/Auth/OtwayRees_Bad.ML	Thu Sep 26 12:47:47 1996 +0200
     9.2 +++ b/src/HOL/Auth/OtwayRees_Bad.ML	Thu Sep 26 12:50:48 1996 +0200
     9.3 @@ -10,7 +10,7 @@
     9.4    Proc. Royal Soc. 426 (1989)
     9.5  
     9.6  This file illustrates the consequences of such errors.  We can still prove
     9.7 -impressive-looking properties such as Enemy_not_see_encrypted_key, yet the
     9.8 +impressive-looking properties such as Spy_not_see_encrypted_key, yet the
     9.9  protocol is open to a middleperson attack.  Attempting to prove some key lemmas
    9.10  indicates the possibility of this attack.
    9.11  *)
    9.12 @@ -28,7 +28,7 @@
    9.13  \               Says B A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|} \
    9.14  \                 : set_of_list evs";
    9.15  by (REPEAT (resolve_tac [exI,bexI] 1));
    9.16 -br (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2;
    9.17 +by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
    9.18  by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
    9.19  by (REPEAT_FIRST (resolve_tac [refl, conjI]));
    9.20  by (ALLGOALS (fast_tac (!claset addss (!simpset setsolver safe_solver))));
    9.21 @@ -37,19 +37,19 @@
    9.22  
    9.23  (**** Inductive proofs about otway ****)
    9.24  
    9.25 -(*The Enemy can see more than anybody else, except for their initial state*)
    9.26 +(*The Spy can see more than anybody else, except for their initial state*)
    9.27  goal thy 
    9.28   "!!evs. evs : otway ==> \
    9.29 -\     sees A evs <= initState A Un sees Enemy evs";
    9.30 -be otway.induct 1;
    9.31 +\     sees A evs <= initState A Un sees Spy evs";
    9.32 +by (etac otway.induct 1);
    9.33  by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] 
    9.34 -			        addss (!simpset))));
    9.35 -qed "sees_agent_subset_sees_Enemy";
    9.36 +                                addss (!simpset))));
    9.37 +qed "sees_agent_subset_sees_Spy";
    9.38  
    9.39  
    9.40  (*Nobody sends themselves messages*)
    9.41  goal thy "!!evs. evs : otway ==> ALL A X. Says A A X ~: set_of_list evs";
    9.42 -be otway.induct 1;
    9.43 +by (etac otway.induct 1);
    9.44  by (Auto_tac());
    9.45  qed_spec_mp "not_Says_to_self";
    9.46  Addsimps [not_Says_to_self];
    9.47 @@ -59,69 +59,69 @@
    9.48  (** For reasoning about the encrypted portion of messages **)
    9.49  
    9.50  goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set_of_list evs ==> \
    9.51 -\                X : analz (sees Enemy evs)";
    9.52 -by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]) 1);
    9.53 -qed "OR2_analz_sees_Enemy";
    9.54 +\                X : analz (sees Spy evs)";
    9.55 +by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    9.56 +qed "OR2_analz_sees_Spy";
    9.57  
    9.58  goal thy "!!evs. Says S B {|N, X, X'|} : set_of_list evs ==> \
    9.59 -\                X : analz (sees Enemy evs)";
    9.60 -by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]) 1);
    9.61 -qed "OR4_analz_sees_Enemy";
    9.62 +\                X : analz (sees Spy evs)";
    9.63 +by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    9.64 +qed "OR4_analz_sees_Spy";
    9.65  
    9.66  goal thy "!!evs. Says B' A {|N, Crypt {|N,K|} K'|} : set_of_list evs ==> \
    9.67 -\                K : parts (sees Enemy evs)";
    9.68 +\                K : parts (sees Spy evs)";
    9.69  by (fast_tac (!claset addSEs partsEs
    9.70 -	              addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
    9.71 -qed "Reveal_parts_sees_Enemy";
    9.72 +                      addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
    9.73 +qed "Reveal_parts_sees_Spy";
    9.74  
    9.75  (*OR2_analz... and OR4_analz... let us treat those cases using the same 
    9.76    argument as for the Fake case.  This is possible for most, but not all,
    9.77    proofs: Fake does not invent new nonces (as in OR2), and of course Fake
    9.78 -  messages originate from the Enemy. *)
    9.79 +  messages originate from the Spy. *)
    9.80  
    9.81  val parts_Fake_tac = 
    9.82 -    dtac (OR2_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 4 THEN
    9.83 -    dtac (OR4_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 6 THEN
    9.84 -    dtac Reveal_parts_sees_Enemy 7;
    9.85 +    dtac (OR2_analz_sees_Spy RS (impOfSubs analz_subset_parts)) 4 THEN
    9.86 +    dtac (OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts)) 6 THEN
    9.87 +    dtac Reveal_parts_sees_Spy 7;
    9.88  
    9.89  
    9.90 -(** Theorems of the form X ~: parts (sees Enemy evs) imply that NOBODY
    9.91 +(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
    9.92      sends messages containing X! **)
    9.93  
    9.94 -(*Enemy never sees another agent's shared key! (unless it is leaked at start)*)
    9.95 +(*Spy never sees another agent's shared key! (unless it is leaked at start)*)
    9.96  goal thy 
    9.97   "!!evs. [| evs : otway;  A ~: bad |]    \
    9.98 -\        ==> Key (shrK A) ~: parts (sees Enemy evs)";
    9.99 -be otway.induct 1;
   9.100 +\        ==> Key (shrK A) ~: parts (sees Spy evs)";
   9.101 +by (etac otway.induct 1);
   9.102  by parts_Fake_tac;
   9.103  by (Auto_tac());
   9.104  (*Deals with Fake message*)
   9.105  by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   9.106 -			     impOfSubs Fake_parts_insert]) 1);
   9.107 -qed "Enemy_not_see_shrK";
   9.108 +                             impOfSubs Fake_parts_insert]) 1);
   9.109 +qed "Spy_not_see_shrK";
   9.110  
   9.111 -bind_thm ("Enemy_not_analz_shrK",
   9.112 -	  [analz_subset_parts, Enemy_not_see_shrK] MRS contra_subsetD);
   9.113 +bind_thm ("Spy_not_analz_shrK",
   9.114 +          [analz_subset_parts, Spy_not_see_shrK] MRS contra_subsetD);
   9.115  
   9.116 -Addsimps [Enemy_not_see_shrK, Enemy_not_analz_shrK];
   9.117 +Addsimps [Spy_not_see_shrK, Spy_not_analz_shrK];
   9.118  
   9.119  (*We go to some trouble to preserve R in the 3rd and 4th subgoals
   9.120    As usual fast_tac cannot be used because it uses the equalities too soon*)
   9.121  val major::prems = 
   9.122 -goal thy  "[| Key (shrK A) : parts (sees Enemy evs);       \
   9.123 +goal thy  "[| Key (shrK A) : parts (sees Spy evs);       \
   9.124  \             evs : otway;                                 \
   9.125  \             A:bad ==> R                                  \
   9.126  \           |] ==> R";
   9.127 -br ccontr 1;
   9.128 -br ([major, Enemy_not_see_shrK] MRS rev_notE) 1;
   9.129 +by (rtac ccontr 1);
   9.130 +by (rtac ([major, Spy_not_see_shrK] MRS rev_notE) 1);
   9.131  by (swap_res_tac prems 2);
   9.132  by (ALLGOALS (fast_tac (!claset addIs prems)));
   9.133 -qed "Enemy_see_shrK_E";
   9.134 +qed "Spy_see_shrK_E";
   9.135  
   9.136 -bind_thm ("Enemy_analz_shrK_E", 
   9.137 -	  analz_subset_parts RS subsetD RS Enemy_see_shrK_E);
   9.138 +bind_thm ("Spy_analz_shrK_E", 
   9.139 +          analz_subset_parts RS subsetD RS Spy_see_shrK_E);
   9.140  
   9.141 -AddSEs [Enemy_see_shrK_E, Enemy_analz_shrK_E];
   9.142 +AddSEs [Spy_see_shrK_E, Spy_analz_shrK_E];
   9.143  
   9.144  
   9.145  (*** Future keys can't be seen or used! ***)
   9.146 @@ -134,14 +134,14 @@
   9.147  goal thy "!!evs. evs : otway ==> \
   9.148  \                length evs <= length evs' --> \
   9.149  \                          Key (newK evs') ~: (UN C. parts (sees C evs))";
   9.150 -be otway.induct 1;
   9.151 +by (etac otway.induct 1);
   9.152  by parts_Fake_tac;
   9.153  (*auto_tac does not work here, as it performs safe_tac first*)
   9.154  by (ALLGOALS Asm_simp_tac);
   9.155  by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   9.156 -				       impOfSubs parts_insert_subset_Un,
   9.157 -				       Suc_leD]
   9.158 -			        addss (!simpset))));
   9.159 +                                       impOfSubs parts_insert_subset_Un,
   9.160 +                                       Suc_leD]
   9.161 +                                addss (!simpset))));
   9.162  val lemma = result();
   9.163  
   9.164  (*Variant needed for the main theorem below*)
   9.165 @@ -158,9 +158,9 @@
   9.166  \           Key (newK evt) : parts {X};    \
   9.167  \           evs : otway                 \
   9.168  \        |] ==> length evt < length evs";
   9.169 -br ccontr 1;
   9.170 -by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Enemy]
   9.171 -	              addIs  [impOfSubs parts_mono, leI]) 1);
   9.172 +by (rtac ccontr 1);
   9.173 +by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
   9.174 +                      addIs  [impOfSubs parts_mono, leI]) 1);
   9.175  qed "Says_imp_old_keys";
   9.176  
   9.177  
   9.178 @@ -169,17 +169,17 @@
   9.179  goal thy "!!evs. evs : otway ==> \
   9.180  \                length evs <= length evs' --> \
   9.181  \                          Nonce (newN evs') ~: (UN C. parts (sees C evs))";
   9.182 -be otway.induct 1;
   9.183 +by (etac otway.induct 1);
   9.184  (*auto_tac does not work here, as it performs safe_tac first*)
   9.185  by (ALLGOALS (asm_simp_tac (!simpset addsimps [de_Morgan_disj]
   9.186                                       addcongs [conj_cong])));
   9.187  by (REPEAT_FIRST (fast_tac (!claset (*60 seconds???*)
   9.188 -			      addSEs [MPair_parts]
   9.189 -			      addDs  [Says_imp_sees_Enemy RS parts.Inj,
   9.190 -				      impOfSubs analz_subset_parts,
   9.191 -				      impOfSubs parts_insert_subset_Un,
   9.192 -				      Suc_leD]
   9.193 -			      addss (!simpset))));
   9.194 +                              addSEs [MPair_parts]
   9.195 +                              addDs  [Says_imp_sees_Spy RS parts.Inj,
   9.196 +                                      impOfSubs analz_subset_parts,
   9.197 +                                      impOfSubs parts_insert_subset_Un,
   9.198 +                                      Suc_leD]
   9.199 +                              addss (!simpset))));
   9.200  val lemma = result();
   9.201  
   9.202  (*Variant needed for the main theorem below*)
   9.203 @@ -196,9 +196,9 @@
   9.204  \           Nonce (newN evt) : parts {X};    \
   9.205  \           evs : otway                 \
   9.206  \        |] ==> length evt < length evs";
   9.207 -br ccontr 1;
   9.208 -by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Enemy]
   9.209 -	              addIs  [impOfSubs parts_mono, leI]) 1);
   9.210 +by (rtac ccontr 1);
   9.211 +by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Spy]
   9.212 +                      addIs  [impOfSubs parts_mono, leI]) 1);
   9.213  qed "Says_imp_old_nonces";
   9.214  
   9.215  
   9.216 @@ -207,7 +207,7 @@
   9.217  goal thy "!!evs. evs : otway ==> \
   9.218  \                length evs <= length evs' --> \
   9.219  \                newK evs' ~: keysFor (UN C. parts (sees C evs))";
   9.220 -be otway.induct 1;
   9.221 +by (etac otway.induct 1);
   9.222  by parts_Fake_tac;
   9.223  by (ALLGOALS Asm_simp_tac);
   9.224  (*OR1 and OR3*)
   9.225 @@ -217,15 +217,15 @@
   9.226      (map
   9.227       (best_tac
   9.228        (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   9.229 -		      impOfSubs (parts_insert_subset_Un RS keysFor_mono),
   9.230 -		      Suc_leD]
   9.231 -	       addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
   9.232 -	       addss (!simpset)))
   9.233 +                      impOfSubs (parts_insert_subset_Un RS keysFor_mono),
   9.234 +                      Suc_leD]
   9.235 +               addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
   9.236 +               addss (!simpset)))
   9.237       [3,2,1]));
   9.238  (*Reveal: dummy message*)
   9.239  by (best_tac (!claset addEs  [new_keys_not_seen RSN(2,rev_notE)]
   9.240 -		      addIs  [less_SucI, impOfSubs keysFor_mono]
   9.241 -		      addss (!simpset addsimps [le_def])) 1);
   9.242 +                      addIs  [less_SucI, impOfSubs keysFor_mono]
   9.243 +                      addss (!simpset addsimps [le_def])) 1);
   9.244  val lemma = result();
   9.245  
   9.246  goal thy 
   9.247 @@ -235,8 +235,8 @@
   9.248  qed "new_keys_not_used";
   9.249  
   9.250  bind_thm ("new_keys_not_analzd",
   9.251 -	  [analz_subset_parts RS keysFor_mono,
   9.252 -	   new_keys_not_used] MRS contra_subsetD);
   9.253 +          [analz_subset_parts RS keysFor_mono,
   9.254 +           new_keys_not_used] MRS contra_subsetD);
   9.255  
   9.256  Addsimps [new_keys_not_used, new_keys_not_analzd];
   9.257  
   9.258 @@ -247,8 +247,8 @@
   9.259  (****
   9.260   The following is to prove theorems of the form
   9.261  
   9.262 -          Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) ==>
   9.263 -          Key K : analz (sees Enemy evs)
   9.264 +          Key K : analz (insert (Key (newK evt)) (sees Spy evs)) ==>
   9.265 +          Key K : analz (sees Spy evs)
   9.266  
   9.267   A more general formula must be proved inductively.
   9.268  
   9.269 @@ -260,14 +260,14 @@
   9.270    We require that agents should behave like this subsequently also.*)
   9.271  goal thy 
   9.272   "!!evs. evs : otway ==> \
   9.273 -\        (Crypt X (newK evt)) : parts (sees Enemy evs) & \
   9.274 -\        Key K : parts {X} --> Key K : parts (sees Enemy evs)";
   9.275 -be otway.induct 1;
   9.276 +\        (Crypt X (newK evt)) : parts (sees Spy evs) & \
   9.277 +\        Key K : parts {X} --> Key K : parts (sees Spy evs)";
   9.278 +by (etac otway.induct 1);
   9.279  by parts_Fake_tac;
   9.280  by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes)));
   9.281  (*Deals with Faked messages*)
   9.282  by (best_tac (!claset addSEs partsEs
   9.283 -		      addDs [impOfSubs analz_subset_parts,
   9.284 +                      addDs [impOfSubs analz_subset_parts,
   9.285                               impOfSubs parts_insert_subset_Un]
   9.286                        addss (!simpset)) 2);
   9.287  (*Base case and Reveal*)
   9.288 @@ -296,10 +296,10 @@
   9.289  
   9.290  (*This lets us avoid analyzing the new message -- unless we have to!*)
   9.291  (*NEEDED??*)
   9.292 -goal thy "synth (analz (sees Enemy evs)) <=   \
   9.293 -\         synth (analz (sees Enemy (Says A B X # evs)))";
   9.294 +goal thy "synth (analz (sees Spy evs)) <=   \
   9.295 +\         synth (analz (sees Spy (Says A B X # evs)))";
   9.296  by (Simp_tac 1);
   9.297 -br (subset_insertI RS analz_mono RS synth_mono) 1;
   9.298 +by (rtac (subset_insertI RS analz_mono RS synth_mono) 1);
   9.299  qed "synth_analz_thin";
   9.300  
   9.301  AddIs [impOfSubs synth_analz_thin];
   9.302 @@ -314,15 +314,15 @@
   9.303    on NS_Shared/Says_S_message_form) *)
   9.304  goal thy
   9.305   "!!evs. evs: otway ==>  \
   9.306 -\          Crypt {|N, Key K|} (shrK A) : parts (sees Enemy evs) & \
   9.307 +\          Crypt {|N, Key K|} (shrK A) : parts (sees Spy evs) & \
   9.308  \          A ~: bad --> \
   9.309  \        (EX evt:otway. K = newK evt)";
   9.310 -be otway.induct 1;
   9.311 +by (etac otway.induct 1);
   9.312  by parts_Fake_tac;
   9.313  by (Auto_tac());
   9.314  (*Deals with Fake message*)
   9.315  by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   9.316 -			     impOfSubs Fake_parts_insert]) 1);
   9.317 +                             impOfSubs Fake_parts_insert]) 1);
   9.318  val lemma = result() RS mp;
   9.319  
   9.320  
   9.321 @@ -331,13 +331,13 @@
   9.322  goal thy 
   9.323   "!!evs. [| Says B' A {|N, Crypt {|N, Key K|} (shrK A)|} : set_of_list evs;  \
   9.324  \           evs : otway |]                      \
   9.325 -\        ==> (EX evt:otway. K = newK evt) | Key K : analz (sees Enemy evs)";
   9.326 +\        ==> (EX evt:otway. K = newK evt) | Key K : analz (sees Spy evs)";
   9.327  by (excluded_middle_tac "A : bad" 1);
   9.328 -by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]
   9.329 -	              addss (!simpset)) 2);
   9.330 +by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
   9.331 +                      addss (!simpset)) 2);
   9.332  by (forward_tac [lemma] 1);
   9.333  by (fast_tac (!claset addEs  partsEs
   9.334 -	              addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
   9.335 +                      addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
   9.336  by (Fast_tac 1);
   9.337  qed "Reveal_message_form";
   9.338  
   9.339 @@ -354,22 +354,22 @@
   9.340  (*The equality makes the induction hypothesis easier to apply*)
   9.341  goal thy  
   9.342   "!!evs. evs : otway ==> \
   9.343 -\  ALL K E. (Key K : analz (Key``(newK``E) Un (sees Enemy evs))) = \
   9.344 -\           (K : newK``E | Key K : analz (sees Enemy evs))";
   9.345 -be otway.induct 1;
   9.346 -bd OR2_analz_sees_Enemy 4;
   9.347 -bd OR4_analz_sees_Enemy 6;
   9.348 -bd Reveal_message_form 7;
   9.349 +\  ALL K E. (Key K : analz (Key``(newK``E) Un (sees Spy evs))) = \
   9.350 +\           (K : newK``E | Key K : analz (sees Spy evs))";
   9.351 +by (etac otway.induct 1);
   9.352 +by (dtac OR2_analz_sees_Spy 4);
   9.353 +by (dtac OR4_analz_sees_Spy 6);
   9.354 +by (dtac Reveal_message_form 7);
   9.355  by (REPEAT_FIRST (ares_tac [allI, lemma]));
   9.356  by (REPEAT ((eresolve_tac [bexE, disjE] ORELSE' hyp_subst_tac) 7));
   9.357  by (ALLGOALS (*Takes 28 secs*)
   9.358      (asm_simp_tac 
   9.359       (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
   9.360 -			 @ pushes)
   9.361 +                         @ pushes)
   9.362                 setloop split_tac [expand_if])));
   9.363  (** LEVEL 7 **)
   9.364  (*Reveal case 2, OR4, OR2, Fake*) 
   9.365 -by (EVERY (map enemy_analz_tac [7,5,3,2]));
   9.366 +by (EVERY (map spy_analz_tac [7,5,3,2]));
   9.367  (*Reveal case 1, OR3, Base*)
   9.368  by (Auto_tac());
   9.369  qed_spec_mp "analz_image_newK";
   9.370 @@ -377,10 +377,10 @@
   9.371  
   9.372  goal thy
   9.373   "!!evs. evs : otway ==>                               \
   9.374 -\        Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) = \
   9.375 -\        (K = newK evt | Key K : analz (sees Enemy evs))";
   9.376 +\        Key K : analz (insert (Key (newK evt)) (sees Spy evs)) = \
   9.377 +\        (K = newK evt | Key K : analz (sees Spy evs))";
   9.378  by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
   9.379 -				   insert_Key_singleton]) 1);
   9.380 +                                   insert_Key_singleton]) 1);
   9.381  by (Fast_tac 1);
   9.382  qed "analz_insert_Key_newK";
   9.383  
   9.384 @@ -393,8 +393,8 @@
   9.385  \           evs : otway |]                                        \
   9.386  \        ==> (EX evt:otway. K = Key(newK evt)) &            \
   9.387  \            (EX i. NA = Nonce i)";
   9.388 -be rev_mp 1;
   9.389 -be otway.induct 1;
   9.390 +by (etac rev_mp 1);
   9.391 +by (etac otway.induct 1);
   9.392  by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset))));
   9.393  qed "Says_Server_message_form";
   9.394  
   9.395 @@ -402,34 +402,34 @@
   9.396  (*Crucial security property, but not itself enough to guarantee correctness!
   9.397    The need for quantification over N, C seems to indicate the problem.
   9.398    Omitting the Reveal message from the description deprives us of even 
   9.399 -	this clue. *)
   9.400 +        this clue. *)
   9.401  goal thy 
   9.402   "!!evs. [| A ~: bad;  B ~: bad;  evs : otway;  evt : otway |]        \
   9.403  \    ==> Says Server B \
   9.404  \          {|Nonce NA, Crypt {|Nonce NA, Key(newK evt)|} (shrK A), \
   9.405  \            Crypt {|NB, Key(newK evt)|} (shrK B)|} : set_of_list evs --> \
   9.406 -\        (ALL N C. Says C Enemy {|N, Key(newK evt)|} ~: set_of_list evs) --> \
   9.407 -\        Key(newK evt) ~: analz (sees Enemy evs)";
   9.408 -be otway.induct 1;
   9.409 -bd OR2_analz_sees_Enemy 4;
   9.410 -bd OR4_analz_sees_Enemy 6;
   9.411 -bd Reveal_message_form 7;
   9.412 +\        (ALL N C. Says C Spy {|N, Key(newK evt)|} ~: set_of_list evs) --> \
   9.413 +\        Key(newK evt) ~: analz (sees Spy evs)";
   9.414 +by (etac otway.induct 1);
   9.415 +by (dtac OR2_analz_sees_Spy 4);
   9.416 +by (dtac OR4_analz_sees_Spy 6);
   9.417 +by (dtac Reveal_message_form 7);
   9.418  by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, disjE] ORELSE' hyp_subst_tac));
   9.419  by (ALLGOALS
   9.420      (asm_full_simp_tac 
   9.421       (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
   9.422 -			  analz_insert_Key_newK] @ pushes)
   9.423 +                          analz_insert_Key_newK] @ pushes)
   9.424                 setloop split_tac [expand_if])));
   9.425  (** LEVEL 6 **)
   9.426  (*Reveal case 1*)
   9.427  by (Fast_tac 5);
   9.428  (*OR3*)
   9.429  by (fast_tac (!claset addSIs [parts_insertI]
   9.430 -		      addEs [Says_imp_old_keys RS less_irrefl]
   9.431 -	              addss (!simpset)) 3);
   9.432 +                      addEs [Says_imp_old_keys RS less_irrefl]
   9.433 +                      addss (!simpset)) 3);
   9.434  (*Reveal case 2, OR4, OR2, Fake*) 
   9.435 -br conjI 3;
   9.436 -by (REPEAT (enemy_analz_tac 1));
   9.437 +by (rtac conjI 3);
   9.438 +by (REPEAT (spy_analz_tac 1));
   9.439  val lemma = result() RS mp RS mp RSN(2,rev_notE);
   9.440  
   9.441  
   9.442 @@ -439,12 +439,12 @@
   9.443   "!!evs. [| Says Server B \
   9.444  \            {|NA, Crypt {|NA, K|} (shrK A),                      \
   9.445  \                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs;  \
   9.446 -\           (ALL N C. Says C Enemy {|N, K|} ~: set_of_list evs);  \
   9.447 +\           (ALL N C. Says C Spy {|N, K|} ~: set_of_list evs);  \
   9.448  \           A ~: bad;  B ~: bad;  evs : otway |]                  \
   9.449 -\        ==> K ~: analz (sees Enemy evs)";
   9.450 +\        ==> K ~: analz (sees Spy evs)";
   9.451  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   9.452  by (fast_tac (!claset addSEs [lemma]) 1);
   9.453 -qed "Enemy_not_see_encrypted_key";
   9.454 +qed "Spy_not_see_encrypted_key";
   9.455  
   9.456  
   9.457  (*** Attempting to prove stronger properties ***)
   9.458 @@ -460,7 +460,7 @@
   9.459  \            {|NA, Crypt {|NA, K|} (shrK A),                      \
   9.460  \                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs --> \
   9.461  \       A=A' & B=B' & NA=NA' & NB=NB'";
   9.462 -be otway.induct 1;
   9.463 +by (etac otway.induct 1);
   9.464  by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   9.465  by (Step_tac 1);
   9.466  (*Remaining cases: OR3 and OR4*)
   9.467 @@ -471,8 +471,8 @@
   9.468  by (REPEAT (ares_tac [refl,exI,impI,conjI] 1));
   9.469  (*...we assume X is a very new message, and handle this case by contradiction*)
   9.470  by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
   9.471 -	              delrules [conjI]    (*prevent split-up into 4 subgoals*)
   9.472 -	              addss (!simpset addsimps [parts_insertI])) 1);
   9.473 +                      delrules [conjI]    (*prevent split-up into 4 subgoals*)
   9.474 +                      addss (!simpset addsimps [parts_insertI])) 1);
   9.475  val lemma = result();
   9.476  
   9.477  
   9.478 @@ -487,7 +487,7 @@
   9.479  \            : set_of_list evs;                                    \
   9.480  \           evs : otway |]                                         \
   9.481  \        ==> A=A' & B=B' & NA=NA' & NB=NB'";
   9.482 -bd lemma 1;
   9.483 +by (dtac lemma 1);
   9.484  by (REPEAT (etac exE 1));
   9.485  (*Duplicate the assumption*)
   9.486  by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
   9.487 @@ -499,16 +499,16 @@
   9.488  goal thy 
   9.489   "!!evs. [| A ~: bad;  A ~= B; evs : otway |]               \
   9.490  \        ==> Crypt {|NA, Agent A, Agent B|} (shrK A)        \
   9.491 -\             : parts (sees Enemy evs) -->                  \
   9.492 +\             : parts (sees Spy evs) -->                  \
   9.493  \            Says A B {|NA, Agent A, Agent B,               \
   9.494  \                       Crypt {|NA, Agent A, Agent B|} (shrK A)|}  \
   9.495  \             : set_of_list evs";
   9.496 -be otway.induct 1;
   9.497 +by (etac otway.induct 1);
   9.498  by parts_Fake_tac;
   9.499  by (ALLGOALS Asm_simp_tac);
   9.500  (*Fake*)
   9.501  by (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
   9.502 -			      impOfSubs Fake_parts_insert]) 2);
   9.503 +                              impOfSubs Fake_parts_insert]) 2);
   9.504  by (Auto_tac());
   9.505  qed_spec_mp "Crypt_imp_OR1";
   9.506  
   9.507 @@ -517,7 +517,7 @@
   9.508            substituting some other nonce NA' for NB.*)
   9.509  goal thy 
   9.510   "!!evs. [| A ~: bad;  evs : otway |]                                 \
   9.511 -\        ==> Crypt {|Nonce NA, Key K|} (shrK A) : parts (sees Enemy evs) --> \
   9.512 +\        ==> Crypt {|Nonce NA, Key K|} (shrK A) : parts (sees Spy evs) --> \
   9.513  \            Says A B {|Nonce NA, Agent A, Agent B,  \
   9.514  \                       Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|}  \
   9.515  \             : set_of_list evs --> \
   9.516 @@ -526,23 +526,23 @@
   9.517  \                   Crypt {|Nonce NA, Key K|} (shrK A),              \
   9.518  \                   Crypt {|Nonce NB, Key K|} (shrK B)|}             \
   9.519  \                   : set_of_list evs)";
   9.520 -be otway.induct 1;
   9.521 +by (etac otway.induct 1);
   9.522  fun ftac rl = forward_tac [rl];
   9.523  by (
   9.524 -    ftac (OR2_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 4 THEN
   9.525 -    ftac (OR4_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 6 THEN
   9.526 -    ftac Reveal_parts_sees_Enemy 7);
   9.527 +    ftac (OR2_analz_sees_Spy RS (impOfSubs analz_subset_parts)) 4 THEN
   9.528 +    ftac (OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts)) 6 THEN
   9.529 +    ftac Reveal_parts_sees_Spy 7);
   9.530  
   9.531  (*  by parts_Fake_tac;  ?*)
   9.532  by (ALLGOALS Asm_simp_tac);
   9.533  (*Fake*)
   9.534  by (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
   9.535 -			      impOfSubs Fake_parts_insert]) 1);
   9.536 +                              impOfSubs Fake_parts_insert]) 1);
   9.537  (*OR1: it cannot be a new Nonce, contradiction.*)
   9.538  by (fast_tac (!claset addSIs [parts_insertI]
   9.539 -		      addSEs partsEs
   9.540 -		      addEs [Says_imp_old_nonces RS less_irrefl]
   9.541 -	              addss (!simpset)) 1);
   9.542 +                      addSEs partsEs
   9.543 +                      addEs [Says_imp_old_nonces RS less_irrefl]
   9.544 +                      addss (!simpset)) 1);
   9.545  (*OR3 and OR4*)  (** LEVEL 5 **)
   9.546  (*OR4*)
   9.547  by (REPEAT (Safe_step_tac 2));
   9.548 @@ -550,7 +550,7 @@
   9.549  by (best_tac (!claset addSDs [parts_cut]) 3);
   9.550  by (forward_tac [Crypt_imp_OR1] 2);
   9.551  by (fast_tac (!claset addEs  partsEs
   9.552 -	              addSDs [Says_imp_sees_Enemy RS parts.Inj]) 4);
   9.553 +                      addSDs [Says_imp_sees_Spy RS parts.Inj]) 4);
   9.554  by (REPEAT (Fast_tac 2));
   9.555  (*OR3*)  (** LEVEL 11 **)
   9.556  by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
   9.557 @@ -577,14 +577,14 @@
   9.558  \                       Crypt {|Nonce NA, Key K|} (shrK A),              \
   9.559  \                       Crypt {|Nonce NB, Key K|} (shrK B)|}             \
   9.560  \                       : set_of_list evs)";
   9.561 -be otway.induct 1;
   9.562 +by (etac otway.induct 1);
   9.563  by (ALLGOALS (asm_simp_tac (!simpset addcongs [conj_cong])));
   9.564  (*OR2*)
   9.565  by (Fast_tac 3);
   9.566  (*OR1: it cannot be a new Nonce, contradiction.*)
   9.567  by (fast_tac (!claset addSIs [parts_insertI]
   9.568 -		      addEs [Says_imp_old_nonces RS less_irrefl]
   9.569 -	              addss (!simpset)) 2);
   9.570 +                      addEs [Says_imp_old_nonces RS less_irrefl]
   9.571 +                      addss (!simpset)) 2);
   9.572  by (ALLGOALS 
   9.573      (asm_simp_tac (!simpset addsimps [all_conj_distrib, de_Morgan_disj, de_Morgan_conj])));
   9.574  (*Fake, OR4*) (** LEVEL 5 **)
   9.575 @@ -593,7 +593,7 @@
   9.576  by (fast_tac (!claset addSDs [spec]) 4);
   9.577  by (forward_tac [Crypt_imp_OR1] 3);
   9.578  by (fast_tac (!claset addEs  partsEs
   9.579 -	              addSDs [Says_imp_sees_Enemy RS parts.Inj]) 5);
   9.580 +                      addSDs [Says_imp_sees_Spy RS parts.Inj]) 5);
   9.581  by (REPEAT (Fast_tac 3));
   9.582  (** LEVEL 11 **)
   9.583  (*Fake (??) and OR4*)
   9.584 @@ -607,12 +607,12 @@
   9.585  (** First, two lemmas for the Fake, OR2 and OR4 cases **)
   9.586  
   9.587  goal thy 
   9.588 - "!!evs. [| X : synth (analz (sees Enemy evs));                \
   9.589 + "!!evs. [| X : synth (analz (sees Spy evs));                \
   9.590  \           Crypt X' (shrK C) : parts{X};                      \
   9.591  \           C ~: bad;  evs : otway |]  \
   9.592 -\        ==> Crypt X' (shrK C) : parts (sees Enemy evs)";
   9.593 +\        ==> Crypt X' (shrK C) : parts (sees Spy evs)";
   9.594  by (best_tac (!claset addSEs [impOfSubs analz_subset_parts]
   9.595 -	              addDs [impOfSubs parts_insert_subset_Un]
   9.596 +                      addDs [impOfSubs parts_insert_subset_Un]
   9.597                        addss (!simpset)) 1);
   9.598  qed "Crypt_Fake_parts";
   9.599  
   9.600 @@ -620,12 +620,12 @@
   9.601   "!!evs. [| Crypt X' K : parts (sees A evs);  evs : otway |]  \
   9.602  \        ==> EX S S' Y. Says S S' Y : set_of_list evs &       \
   9.603  \            Crypt X' K : parts {Y}";
   9.604 -bd parts_singleton 1;
   9.605 +by (dtac parts_singleton 1);
   9.606  by (fast_tac (!claset addSDs [seesD] addss (!simpset)) 1);
   9.607  qed "Crypt_parts_singleton";
   9.608  
   9.609  (*The Key K uniquely identifies a pair of senders in the message encrypted by
   9.610 -  C, but if C=Enemy then he could send all sorts of nonsense.*)
   9.611 +  C, but if C=Spy then he could send all sorts of nonsense.*)
   9.612  goal thy 
   9.613   "!!evs. evs : otway ==>                                     \
   9.614  \      EX A B. ALL C.                                        \
   9.615 @@ -633,33 +633,33 @@
   9.616  \         (ALL S S' X. Says S S' X : set_of_list evs -->     \
   9.617  \           (EX NA. Crypt {|NA, Key K|} (shrK C) : parts{X}) --> C=A | C=B)";
   9.618  by (Simp_tac 1);
   9.619 -be otway.induct 1;
   9.620 -bd OR2_analz_sees_Enemy 4;
   9.621 -bd OR4_analz_sees_Enemy 6;
   9.622 +by (etac otway.induct 1);
   9.623 +by (dtac OR2_analz_sees_Spy 4);
   9.624 +by (dtac OR4_analz_sees_Spy 6);
   9.625  by (ALLGOALS 
   9.626      (asm_simp_tac (!simpset addsimps [all_conj_distrib, imp_conj_distrib])));
   9.627  by (REPEAT_FIRST (etac exE));
   9.628  (*OR4*)
   9.629  by (ex_strip_tac 4);
   9.630  by (fast_tac (!claset addSDs [synth.Inj RS Crypt_Fake_parts, 
   9.631 -			      Crypt_parts_singleton]) 4);
   9.632 +                              Crypt_parts_singleton]) 4);
   9.633  (*OR3: Case split propagates some context to other subgoal...*)
   9.634 -	(** LEVEL 8 **)
   9.635 +        (** LEVEL 8 **)
   9.636  by (excluded_middle_tac "K = newK evsa" 3);
   9.637  by (Asm_simp_tac 3);
   9.638  by (REPEAT (ares_tac [exI] 3));
   9.639  (*...we prove this case by contradiction: the key is too new!*)
   9.640  by (fast_tac (!claset addIs [parts_insertI]
   9.641 -		      addSEs partsEs
   9.642 -		      addEs [Says_imp_old_keys RS less_irrefl]
   9.643 -	              addss (!simpset)) 3);
   9.644 +                      addSEs partsEs
   9.645 +                      addEs [Says_imp_old_keys RS less_irrefl]
   9.646 +                      addss (!simpset)) 3);
   9.647  (*OR2*) (** LEVEL 12 **)
   9.648 -(*enemy_analz_tac just does not work here: it is an entirely different proof!*)
   9.649 +(*spy_analz_tac just does not work here: it is an entirely different proof!*)
   9.650  by (ex_strip_tac 2);
   9.651  by (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 2);
   9.652  by (Simp_tac 2);
   9.653  by (fast_tac (!claset addSDs [synth.Inj RS Crypt_Fake_parts, 
   9.654 -			      Crypt_parts_singleton]) 2);
   9.655 +                              Crypt_parts_singleton]) 2);
   9.656  (*Fake*) (** LEVEL 16 **)
   9.657  by (ex_strip_tac 1);
   9.658  by (fast_tac (!claset addSDs [Crypt_Fake_parts, Crypt_parts_singleton]) 1);
    10.1 --- a/src/HOL/Auth/OtwayRees_Bad.thy	Thu Sep 26 12:47:47 1996 +0200
    10.2 +++ b/src/HOL/Auth/OtwayRees_Bad.thy	Thu Sep 26 12:50:48 1996 +0200
    10.3 @@ -18,11 +18,11 @@
    10.4           (*Initial trace is empty*)
    10.5      Nil  "[]: otway"
    10.6  
    10.7 -         (*The enemy MAY say anything he CAN say.  We do not expect him to
    10.8 +         (*The spy MAY say anything he CAN say.  We do not expect him to
    10.9             invent new nonces here, but he can also use NS1.  Common to
   10.10             all similar protocols.*)
   10.11 -    Fake "[| evs: otway;  B ~= Enemy;  X: synth (analz (sees Enemy evs)) |]
   10.12 -          ==> Says Enemy B X  # evs : otway"
   10.13 +    Fake "[| evs: otway;  B ~= Spy;  X: synth (analz (sees Spy evs)) |]
   10.14 +          ==> Says Spy B X  # evs : otway"
   10.15  
   10.16           (*Alice initiates a protocol run*)
   10.17      OR1  "[| evs: otway;  A ~= B;  B ~= Server |]
   10.18 @@ -68,12 +68,12 @@
   10.19  
   10.20           (*This message models possible leaks of session keys.  Alice's Nonce
   10.21             identifies the protocol run.*)
   10.22 -    Reveal "[| evs: otway;  A ~= Enemy;
   10.23 +    Reveal "[| evs: otway;  A ~= Spy;
   10.24                 Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|}
   10.25                   : set_of_list evs;
   10.26                 Says A  B {|Nonce NA, Agent A, Agent B, 
   10.27                             Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|}
   10.28                   : set_of_list evs |]
   10.29 -            ==> Says A Enemy {|Nonce NA, Key K|} # evs : otway"
   10.30 +            ==> Says A Spy {|Nonce NA, Key K|} # evs : otway"
   10.31  
   10.32  end
    11.1 --- a/src/HOL/Auth/Shared.ML	Thu Sep 26 12:47:47 1996 +0200
    11.2 +++ b/src/HOL/Auth/Shared.ML	Thu Sep 26 12:50:48 1996 +0200
    11.3 @@ -6,11 +6,41 @@
    11.4  Theory of Shared Keys (common to all symmetric-key protocols)
    11.5  
    11.6  Server keys; initial states of agents; new nonces and keys; function "sees" 
    11.7 +*)
    11.8 +
    11.9  
   11.10  
   11.11 -*)
   11.12 +(****************DELETE****************)
   11.13  
   11.14 -Addsimps [parts_cut_eq];
   11.15 +local
   11.16 +    fun string_of (a,0) = a
   11.17 +      | string_of (a,i) = a ^ "_" ^ string_of_int i;
   11.18 +in
   11.19 +  fun freeze_thaw th =
   11.20 +    let val fth = freezeT th
   11.21 +        val {prop,sign,...} = rep_thm fth
   11.22 +        fun mk_inst (Var(v,T)) = 
   11.23 +            (cterm_of sign (Var(v,T)),
   11.24 +             cterm_of sign (Free(string_of v, T)))
   11.25 +        val insts = map mk_inst (term_vars prop)
   11.26 +        fun thaw th' = 
   11.27 +            th' |> forall_intr_list (map #2 insts)
   11.28 +                |> forall_elim_list (map #1 insts)
   11.29 +    in  (instantiate ([],insts) fth, thaw)  end;
   11.30 +end;
   11.31 +fun defer_tac i state = 
   11.32 +    let val (state',thaw) = freeze_thaw state
   11.33 +        val hyps = Drule.strip_imp_prems (adjust_maxidx (cprop_of state'))
   11.34 +        val hyp::hyps' = drop(i-1,hyps)
   11.35 +    in  implies_intr hyp (implies_elim_list state' (map assume hyps)) 
   11.36 +        |> implies_intr_list (take(i-1,hyps) @ hyps')
   11.37 +        |> thaw
   11.38 +        |> Sequence.single
   11.39 +    end
   11.40 +    handle Bind => Sequence.null;
   11.41 +
   11.42 +
   11.43 +
   11.44  
   11.45  (*GOALS.ML??*)
   11.46  fun prlim n = (goals_limit:=n; pr());
   11.47 @@ -47,42 +77,26 @@
   11.48  
   11.49  
   11.50  (*Injectiveness and freshness of new keys and nonces*)
   11.51 -AddIffs [inj_shrK RS inj_eq, inj_newN RS inj_eq, inj_newK RS inj_eq,
   11.52 -	 fresh_newN, fresh_newK];
   11.53 +AddIffs [inj_shrK RS inj_eq, inj_newN RS inj_eq, inj_newK RS inj_eq];
   11.54  
   11.55  (** Rewrites should not refer to  initState(Friend i) 
   11.56      -- not in normal form! **)
   11.57  
   11.58 -goal thy "newK evs ~= shrK B";
   11.59 -by (subgoal_tac "newK evs = shrK B --> \
   11.60 -\                Key (newK evs) : parts (initState B)" 1);
   11.61 -by (Fast_tac 1);
   11.62 -by (agent.induct_tac "B" 1);
   11.63 -by (auto_tac (!claset addIs [range_eqI], !simpset addsimps [bad_def]));
   11.64 -qed "newK_neq_shrK";
   11.65 -
   11.66  Addsimps [newK_neq_shrK, newK_neq_shrK RS not_sym];
   11.67  
   11.68 -(*Good for talking about Server's initial state*)
   11.69 -goal thy "!!H. H <= Key``E ==> parts H = H";
   11.70 +goal thy "Key (newK evs) ~: parts (initState lost B)";
   11.71 +by (agent.induct_tac "B" 1);
   11.72  by (Auto_tac ());
   11.73 -be parts.induct 1;
   11.74 -by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   11.75 -qed "parts_image_subset";
   11.76 -
   11.77 -bind_thm ("parts_image_Key", subset_refl RS parts_image_subset);
   11.78 +qed "newK_notin_initState";
   11.79  
   11.80 -goal thy "!!H. H <= Key``E ==> analz H = H";
   11.81 +goal thy "Nonce (newN evs) ~: parts (initState lost B)";
   11.82 +by (agent.induct_tac "B" 1);
   11.83  by (Auto_tac ());
   11.84 -be analz.induct 1;
   11.85 -by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   11.86 -qed "analz_image_subset";
   11.87 +qed "newN_notin_initState";
   11.88  
   11.89 -bind_thm ("analz_image_Key", subset_refl RS analz_image_subset);
   11.90 +AddIffs [newK_notin_initState, newN_notin_initState];
   11.91  
   11.92 -Addsimps [parts_image_Key, analz_image_Key];
   11.93 -
   11.94 -goalw thy [keysFor_def] "keysFor (parts (initState C)) = {}";
   11.95 +goalw thy [keysFor_def] "keysFor (parts (initState lost C)) = {}";
   11.96  by (agent.induct_tac "C" 1);
   11.97  by (auto_tac (!claset addIs [range_eqI], !simpset));
   11.98  qed "keysFor_parts_initState";
   11.99 @@ -99,106 +113,105 @@
  11.100  qed "shrK_notin_image_newK";
  11.101  Addsimps [shrK_notin_image_newK];
  11.102  
  11.103 +
  11.104 +(*** Function "sees" ***)
  11.105 +
  11.106 +goal thy
  11.107 +    "!!evs. lost' <= lost ==> sees lost' A evs <= sees lost A evs";
  11.108 +by (list.induct_tac "evs" 1);
  11.109 +by (agent.induct_tac "A" 1);
  11.110 +by (event.induct_tac "a" 2);
  11.111 +by (Auto_tac ());
  11.112 +qed "sees_mono";
  11.113 +
  11.114  (*Agents see their own shared keys!*)
  11.115 -goal thy "Key (shrK A) : sees A evs";
  11.116 +goal thy "A ~= Spy --> Key (shrK A) : sees lost A evs";
  11.117  by (list.induct_tac "evs" 1);
  11.118  by (agent.induct_tac "A" 1);
  11.119 -by (auto_tac (!claset, !simpset addsimps [bad_def]));
  11.120 -qed "sees_own_shrK";
  11.121 -
  11.122 -(*Enemy sees shared keys of bad agents!*)
  11.123 -goal thy "!!i. A: bad ==> Key (shrK A) : sees Enemy evs";
  11.124 -by (list.induct_tac "evs" 1);
  11.125 -by (auto_tac (!claset, !simpset addsimps [bad_def]));
  11.126 -qed "Enemy_sees_bad";
  11.127 -
  11.128 -AddSIs [sees_own_shrK, Enemy_sees_bad];
  11.129 +by (Auto_tac ());
  11.130 +qed_spec_mp "sees_own_shrK";
  11.131  
  11.132 -goal thy "Enemy: bad";
  11.133 -by (simp_tac (!simpset addsimps [bad_def]) 1);
  11.134 -qed "Enemy_in_bad";
  11.135 -
  11.136 -AddIffs [Enemy_in_bad];
  11.137 +(*Spy sees shared keys of lost agents!*)
  11.138 +goal thy "!!i. A: lost ==> Key (shrK A) : sees lost Spy evs";
  11.139 +by (list.induct_tac "evs" 1);
  11.140 +by (Auto_tac());
  11.141 +qed "Spy_sees_bad";
  11.142  
  11.143 -goal thy "!!A. A ~: bad ==> A ~= Enemy";
  11.144 -by (Fast_tac 1);
  11.145 -qed "not_bad_imp_not_Enemy";
  11.146 +AddSIs [sees_own_shrK, Spy_sees_bad];
  11.147 +
  11.148  
  11.149 -AddIffs [Enemy_in_bad];
  11.150 +(** Specialized rewrite rules for (sees lost A (Says...#evs)) **)
  11.151  
  11.152 -(** Specialized rewrite rules for (sees A (Says...#evs)) **)
  11.153 -
  11.154 -goal thy "sees A (Says A B X # evs) = insert X (sees A evs)";
  11.155 +goal thy "sees lost A (Says A B X # evs) = insert X (sees lost A evs)";
  11.156  by (Simp_tac 1);
  11.157  qed "sees_own";
  11.158  
  11.159  goal thy "!!A. Server ~= A ==> \
  11.160 -\              sees Server (Says A B X # evs) = sees Server evs";
  11.161 +\              sees lost Server (Says A B X # evs) = sees lost Server evs";
  11.162  by (Asm_simp_tac 1);
  11.163  qed "sees_Server";
  11.164  
  11.165  goal thy "!!A. Friend i ~= A ==> \
  11.166 -\              sees (Friend i) (Says A B X # evs) = sees (Friend i) evs";
  11.167 +\              sees lost (Friend i) (Says A B X # evs) = sees lost (Friend i) evs";
  11.168  by (Asm_simp_tac 1);
  11.169  qed "sees_Friend";
  11.170  
  11.171 -goal thy "sees Enemy (Says A B X # evs) = insert X (sees Enemy evs)";
  11.172 +goal thy "sees lost Spy (Says A B X # evs) = insert X (sees lost Spy evs)";
  11.173  by (Simp_tac 1);
  11.174 -qed "sees_Enemy";
  11.175 +qed "sees_Spy";
  11.176  
  11.177 -goal thy "sees A (Says A' B X # evs) <= insert X (sees A evs)";
  11.178 +goal thy "sees lost A (Says A' B X # evs) <= insert X (sees lost A evs)";
  11.179  by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
  11.180  by (Fast_tac 1);
  11.181  qed "sees_Says_subset_insert";
  11.182  
  11.183 -goal thy "sees A evs <= sees A (Says A' B X # evs)";
  11.184 +goal thy "sees lost A evs <= sees lost A (Says A' B X # evs)";
  11.185  by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
  11.186  by (Fast_tac 1);
  11.187  qed "sees_subset_sees_Says";
  11.188  
  11.189 -(*Pushing Unions into parts; one of the A's equals B, and thus sees Y*)
  11.190 -goal thy "(UN A. parts (sees A (Says B C Y # evs))) = \
  11.191 -\         parts {Y} Un (UN A. parts (sees A evs))";
  11.192 +(*Pushing Unions into parts; one of the A's equals B, and thus sees lost Y*)
  11.193 +goal thy "(UN A. parts (sees lost A (Says B C Y # evs))) = \
  11.194 +\         parts {Y} Un (UN A. parts (sees lost A evs))";
  11.195  by (Step_tac 1);
  11.196 -be rev_mp 1;	(*for some reason, split_tac does not work on assumptions*)
  11.197 +by (etac rev_mp 1);     (*for some reason, split_tac does not work on assumptions*)
  11.198  val ss = (!simpset addsimps [parts_Un, sees_Cons] 
  11.199 -	           setloop split_tac [expand_if]);
  11.200 +                   setloop split_tac [expand_if]);
  11.201  by (ALLGOALS (fast_tac (!claset addss ss)));
  11.202  qed "UN_parts_sees_Says";
  11.203  
  11.204 -goal thy "Says A B X : set_of_list evs --> X : sees Enemy evs";
  11.205 +goal thy "Says A B X : set_of_list evs --> X : sees lost Spy evs";
  11.206  by (list.induct_tac "evs" 1);
  11.207  by (Auto_tac ());
  11.208 -qed_spec_mp "Says_imp_sees_Enemy";
  11.209 +qed_spec_mp "Says_imp_sees_Spy";
  11.210  
  11.211 -Addsimps [Says_imp_sees_Enemy];
  11.212 -AddIs    [Says_imp_sees_Enemy];
  11.213 +Addsimps [Says_imp_sees_Spy];
  11.214 +AddIs    [Says_imp_sees_Spy];
  11.215  
  11.216 -goal thy "initState C <= Key `` range shrK";
  11.217 +goal thy "initState lost C <= Key `` range shrK";
  11.218  by (agent.induct_tac "C" 1);
  11.219  by (Auto_tac ());
  11.220  qed "initState_subset";
  11.221  
  11.222 -goal thy "X : sees C evs --> \
  11.223 +goal thy "X : sees lost C evs --> \
  11.224  \          (EX A B. Says A B X : set_of_list evs) | \
  11.225  \          (EX A. X = Key (shrK A))";
  11.226  by (list.induct_tac "evs" 1);
  11.227  by (ALLGOALS Asm_simp_tac);
  11.228  by (fast_tac (!claset addDs [impOfSubs initState_subset]) 1);
  11.229 -br conjI 1;
  11.230 +by (rtac conjI 1);
  11.231  by (Fast_tac 2);
  11.232  by (event.induct_tac "a" 1);
  11.233  by (ALLGOALS (asm_simp_tac (!simpset addsimps [mem_if])));
  11.234  by (ALLGOALS Fast_tac);
  11.235  qed_spec_mp "seesD";
  11.236  
  11.237 -
  11.238 -Addsimps [UN_parts_sees_Says, sees_own, sees_Server, sees_Friend, sees_Enemy];
  11.239 -Delsimps [sees_Cons];	(**** NOTE REMOVAL -- laws above are cleaner ****)
  11.240 +Addsimps [UN_parts_sees_Says, sees_own, sees_Server, sees_Friend, sees_Spy];
  11.241 +Delsimps [sees_Cons];   (**** NOTE REMOVAL -- laws above are cleaner ****)
  11.242  
  11.243  
  11.244  goal thy "!!K. newK evs = invKey K ==> newK evs = K";
  11.245 -br (invKey_eq RS iffD1) 1;
  11.246 +by (rtac (invKey_eq RS iffD1) 1);
  11.247  by (Simp_tac 1);
  11.248  val newK_invKey = result();
  11.249  
  11.250 @@ -229,26 +242,25 @@
  11.251  
  11.252  (*Analysis of Fake cases and of messages that forward unknown parts
  11.253    Abstraction over i is ESSENTIAL: it delays the dereferencing of claset*)
  11.254 -fun enemy_analz_tac i =
  11.255 +fun spy_analz_tac i =
  11.256    SELECT_GOAL 
  11.257     (EVERY [  (*push in occurrences of X...*)
  11.258 -	   (REPEAT o CHANGED)
  11.259 -	     (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1),
  11.260 -	     (*...allowing further simplifications*)
  11.261 -	   simp_tac (!simpset setloop split_tac [expand_if]) 1,
  11.262 -	   REPEAT (resolve_tac [impI,notI] 1),
  11.263 -	   dtac (impOfSubs Fake_analz_insert) 1,
  11.264 -	   eresolve_tac [asm_rl, synth.Inj] 1,
  11.265 -	   Fast_tac 1,
  11.266 -	   Asm_full_simp_tac 1,
  11.267 -	   IF_UNSOLVED (deepen_tac (!claset addIs [impOfSubs analz_mono]) 0 1)
  11.268 -	   ]) i;
  11.269 +           (REPEAT o CHANGED)
  11.270 +             (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1),
  11.271 +             (*...allowing further simplifications*)
  11.272 +           simp_tac (!simpset setloop split_tac [expand_if]) 1,
  11.273 +           REPEAT (resolve_tac [impI,notI] 1),
  11.274 +           dtac (impOfSubs Fake_analz_insert) 1,
  11.275 +           eresolve_tac [asm_rl, synth.Inj] 1,
  11.276 +           Fast_tac 1,
  11.277 +           Asm_full_simp_tac 1,
  11.278 +           IF_UNSOLVED (deepen_tac (!claset addIs [impOfSubs analz_mono]) 0 1)
  11.279 +           ]) i;
  11.280  
  11.281  
  11.282 -(** Simplifying   parts (insert X (sees A evs))
  11.283 -                = parts {X} Un parts (sees A evs) -- since general case loops*)
  11.284 +(** Simplifying   parts (insert X (sees lost A evs))
  11.285 +                = parts {X} Un parts (sees lost A evs) -- since general case loops*)
  11.286  
  11.287  val parts_insert_sees = 
  11.288 -    parts_insert |> read_instantiate_sg (sign_of thy) [("H", "sees A evs")]
  11.289 +    parts_insert |> read_instantiate_sg (sign_of thy) [("H", "sees lost A evs")]
  11.290                   |> standard;
  11.291 -
    12.1 --- a/src/HOL/Auth/Shared.thy	Thu Sep 26 12:47:47 1996 +0200
    12.2 +++ b/src/HOL/Auth/Shared.thy	Thu Sep 26 12:50:48 1996 +0200
    12.3 @@ -12,22 +12,19 @@
    12.4  
    12.5  consts
    12.6    shrK    :: agent => key  (*symmetric keys*)
    12.7 -  leaked  :: nat set       (*Friendly agents whose keys have leaked to Enemy*)
    12.8 -
    12.9 -constdefs     (*Enemy and compromised agents*)
   12.10 -  bad     :: agent set     "bad == insert Enemy (Friend``leaked)"
   12.11  
   12.12  rules
   12.13    isSym_shrK "isSymKey (shrK A)"
   12.14  
   12.15  consts  (*Initial states of agents -- parameter of the construction*)
   12.16 -  initState :: agent => msg set
   12.17 +  initState :: [agent set, agent] => msg set
   12.18  
   12.19  primrec initState agent
   12.20          (*Server knows all keys; other agents know only their own*)
   12.21 -  initState_Server  "initState Server     = Key `` range shrK"
   12.22 -  initState_Friend  "initState (Friend i) = {Key (shrK (Friend i))}"
   12.23 -  initState_Enemy   "initState Enemy      = Key``shrK``bad"
   12.24 +  initState_Server  "initState lost Server     = Key `` range shrK"
   12.25 +  initState_Friend  "initState lost (Friend i) = {Key (shrK (Friend i))}"
   12.26 +  initState_Spy   "initState lost Spy      = Key``shrK``lost"
   12.27 +
   12.28  
   12.29  datatype  (*Messages, and components of agent stores*)
   12.30    event = Says agent agent msg
   12.31 @@ -38,16 +35,16 @@
   12.32  primrec sees1 event
   12.33             (*First agent recalls all that it says, but NOT everything
   12.34               that is sent to it; it must note such things if/when received*)
   12.35 -  sees1_Says  "sees1 A (Says A' B X)  = (if A:{A',Enemy} then {X} else {})"
   12.36 +  sees1_Says  "sees1 A (Says A' B X)  = (if A:{A',Spy} then {X} else {})"
   12.37            (*part of A's internal state*)
   12.38  
   12.39  consts  
   12.40 -  sees :: [agent, event list] => msg set
   12.41 +  sees :: [agent set, agent, event list] => msg set
   12.42  
   12.43  primrec sees list
   12.44          (*Initial knowledge includes all public keys and own private key*)
   12.45 -  sees_Nil  "sees A []       = initState A"
   12.46 -  sees_Cons "sees A (ev#evs) = sees1 A ev Un sees A evs"
   12.47 +  sees_Nil  "sees lost A []       = initState lost A"
   12.48 +  sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs"
   12.49  
   12.50  
   12.51  (*Agents generate "random" nonces.  Different traces always yield
   12.52 @@ -57,13 +54,12 @@
   12.53    newK :: "event list => key"
   12.54  
   12.55  rules
   12.56 -  inj_shrK "inj shrK"
   12.57 +  inj_shrK      "inj shrK"
   12.58 +
   12.59 +  inj_newN      "inj newN"
   12.60  
   12.61 -  inj_newN   "inj newN"
   12.62 -  fresh_newN "Nonce (newN evs) ~: parts (initState B)" 
   12.63 -
   12.64 -  inj_newK   "inj newK"
   12.65 -  fresh_newK "Key (newK evs) ~: parts (initState B)" 
   12.66 -  isSym_newK "isSymKey (newK evs)"
   12.67 +  inj_newK      "inj newK"
   12.68 +  newK_neq_shrK "newK evs ~= shrK A" 
   12.69 +  isSym_newK    "isSymKey (newK evs)"
   12.70  
   12.71  end
    13.1 --- a/src/HOL/Auth/Yahalom.ML	Thu Sep 26 12:47:47 1996 +0200
    13.2 +++ b/src/HOL/Auth/Yahalom.ML	Thu Sep 26 12:50:48 1996 +0200
    13.3 @@ -20,10 +20,10 @@
    13.4  
    13.5  goal thy 
    13.6   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
    13.7 -\        ==> EX X NB K. EX evs: yahalom.          \
    13.8 +\        ==> EX X NB K. EX evs: yahalom lost.          \
    13.9  \               Says A B {|X, Crypt (Nonce NB) K|} : set_of_list evs";
   13.10  by (REPEAT (resolve_tac [exI,bexI] 1));
   13.11 -br (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS yahalom.YM4) 2;
   13.12 +by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS yahalom.YM4) 2);
   13.13  by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
   13.14  by (ALLGOALS Fast_tac);
   13.15  result();
   13.16 @@ -31,19 +31,19 @@
   13.17  
   13.18  (**** Inductive proofs about yahalom ****)
   13.19  
   13.20 -(*The Enemy can see more than anybody else, except for their initial state*)
   13.21 +(*The Spy can see more than anybody else, except for their initial state*)
   13.22  goal thy 
   13.23 - "!!evs. evs : yahalom ==> \
   13.24 -\     sees A evs <= initState A Un sees Enemy evs";
   13.25 -be yahalom.induct 1;
   13.26 + "!!evs. evs : yahalom lost ==> \
   13.27 +\     sees lost A evs <= initState lost A Un sees lost Spy evs";
   13.28 +by (etac yahalom.induct 1);
   13.29  by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] 
   13.30 -			        addss (!simpset))));
   13.31 -qed "sees_agent_subset_sees_Enemy";
   13.32 +                                addss (!simpset))));
   13.33 +qed "sees_agent_subset_sees_Spy";
   13.34  
   13.35  
   13.36  (*Nobody sends themselves messages*)
   13.37 -goal thy "!!evs. evs : yahalom ==> ALL A X. Says A A X ~: set_of_list evs";
   13.38 -be yahalom.induct 1;
   13.39 +goal thy "!!evs. evs : yahalom lost ==> ALL A X. Says A A X ~: set_of_list evs";
   13.40 +by (etac yahalom.induct 1);
   13.41  by (Auto_tac());
   13.42  qed_spec_mp "not_Says_to_self";
   13.43  Addsimps [not_Says_to_self];
   13.44 @@ -54,58 +54,58 @@
   13.45  
   13.46  (*Lets us treat YM4 using a similar argument as for the Fake case.*)
   13.47  goal thy "!!evs. Says S A {|Crypt Y (shrK A), X|} : set_of_list evs ==> \
   13.48 -\                X : analz (sees Enemy evs)";
   13.49 -by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]) 1);
   13.50 -qed "YM4_analz_sees_Enemy";
   13.51 +\                X : analz (sees lost Spy evs)";
   13.52 +by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
   13.53 +qed "YM4_analz_sees_Spy";
   13.54  
   13.55  goal thy "!!evs. Says S A {|Crypt {|B, K, NA, NB|} (shrK A), X|} \
   13.56  \                  : set_of_list evs ==> \
   13.57 -\                K : parts (sees Enemy evs)";
   13.58 +\                K : parts (sees lost Spy evs)";
   13.59  by (fast_tac (!claset addSEs partsEs
   13.60 -	              addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
   13.61 -qed "YM4_parts_sees_Enemy";
   13.62 +                      addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
   13.63 +qed "YM4_parts_sees_Spy";
   13.64  
   13.65  
   13.66  
   13.67 -(** Theorems of the form X ~: parts (sees Enemy evs) imply that NOBODY
   13.68 +(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
   13.69      sends messages containing X! **)
   13.70  
   13.71 -(*Enemy never sees another agent's shared key! (unless it is leaked at start)*)
   13.72 +(*Spy never sees lost another agent's shared key! (unless it is leaked at start)*)
   13.73  goal thy 
   13.74 - "!!evs. [| evs : yahalom;  A ~: bad |]    \
   13.75 -\        ==> Key (shrK A) ~: parts (sees Enemy evs)";
   13.76 -be yahalom.induct 1;
   13.77 -bd (YM4_analz_sees_Enemy RS synth.Inj) 6;
   13.78 + "!!evs. [| evs : yahalom lost;  A ~: lost |]    \
   13.79 +\        ==> Key (shrK A) ~: parts (sees lost Spy evs)";
   13.80 +by (etac yahalom.induct 1);
   13.81 +by (dtac (YM4_analz_sees_Spy RS synth.Inj) 6);
   13.82  by (ALLGOALS Asm_simp_tac);
   13.83  by (stac insert_commute 3);
   13.84  by (Auto_tac());
   13.85  (*Fake and YM4 are similar*)
   13.86  by (ALLGOALS (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
   13.87 -					impOfSubs Fake_parts_insert])));
   13.88 -qed "Enemy_not_see_shrK";
   13.89 +                                        impOfSubs Fake_parts_insert])));
   13.90 +qed "Spy_not_see_shrK";
   13.91  
   13.92 -bind_thm ("Enemy_not_analz_shrK",
   13.93 -	  [analz_subset_parts, Enemy_not_see_shrK] MRS contra_subsetD);
   13.94 +bind_thm ("Spy_not_analz_shrK",
   13.95 +          [analz_subset_parts, Spy_not_see_shrK] MRS contra_subsetD);
   13.96  
   13.97 -Addsimps [Enemy_not_see_shrK, Enemy_not_analz_shrK];
   13.98 +Addsimps [Spy_not_see_shrK, Spy_not_analz_shrK];
   13.99  
  13.100  (*We go to some trouble to preserve R in the 3rd and 4th subgoals
  13.101    As usual fast_tac cannot be used because it uses the equalities too soon*)
  13.102  val major::prems = 
  13.103 -goal thy  "[| Key (shrK A) : parts (sees Enemy evs);       \
  13.104 -\             evs : yahalom;                               \
  13.105 -\             A:bad ==> R                                  \
  13.106 +goal thy  "[| Key (shrK A) : parts (sees lost Spy evs);       \
  13.107 +\             evs : yahalom lost;                               \
  13.108 +\             A:lost ==> R                                  \
  13.109  \           |] ==> R";
  13.110 -br ccontr 1;
  13.111 -br ([major, Enemy_not_see_shrK] MRS rev_notE) 1;
  13.112 +by (rtac ccontr 1);
  13.113 +by (rtac ([major, Spy_not_see_shrK] MRS rev_notE) 1);
  13.114  by (swap_res_tac prems 2);
  13.115  by (ALLGOALS (fast_tac (!claset addIs prems)));
  13.116 -qed "Enemy_see_shrK_E";
  13.117 +qed "Spy_see_shrK_E";
  13.118  
  13.119 -bind_thm ("Enemy_analz_shrK_E", 
  13.120 -	  analz_subset_parts RS subsetD RS Enemy_see_shrK_E);
  13.121 +bind_thm ("Spy_analz_shrK_E", 
  13.122 +          analz_subset_parts RS subsetD RS Spy_see_shrK_E);
  13.123  
  13.124 -AddSEs [Enemy_see_shrK_E, Enemy_analz_shrK_E];
  13.125 +AddSEs [Spy_see_shrK_E, Spy_analz_shrK_E];
  13.126  
  13.127  
  13.128  (*** Future keys can't be seen or used! ***)
  13.129 @@ -116,21 +116,21 @@
  13.130    standard Fake rule.  
  13.131        The length comparison, and Union over C, are essential for the 
  13.132    induction! *)
  13.133 -goal thy "!!evs. evs : yahalom ==> \
  13.134 +goal thy "!!evs. evs : yahalom lost ==> \
  13.135  \                length evs <= length evs' --> \
  13.136 -\                          Key (newK evs') ~: (UN C. parts (sees C evs))";
  13.137 -be yahalom.induct 1;
  13.138 -bd (YM4_analz_sees_Enemy RS synth.Inj) 6;
  13.139 +\                          Key (newK evs') ~: (UN C. parts (sees lost C evs))";
  13.140 +by (etac yahalom.induct 1);
  13.141 +by (dtac (YM4_analz_sees_Spy RS synth.Inj) 6);
  13.142  by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
  13.143 -					   impOfSubs parts_insert_subset_Un,
  13.144 -					   Suc_leD]
  13.145 -			            addss (!simpset))));
  13.146 +                                           impOfSubs parts_insert_subset_Un,
  13.147 +                                           Suc_leD]
  13.148 +                                    addss (!simpset))));
  13.149  val lemma = result();
  13.150  
  13.151  (*Variant needed for the main theorem below*)
  13.152  goal thy 
  13.153 - "!!evs. [| evs : yahalom;  length evs <= length evs' |]    \
  13.154 -\        ==> Key (newK evs') ~: parts (sees C evs)";
  13.155 + "!!evs. [| evs : yahalom lost;  length evs <= length evs' |]    \
  13.156 +\        ==> Key (newK evs') ~: parts (sees lost C evs)";
  13.157  by (fast_tac (!claset addDs [lemma]) 1);
  13.158  qed "new_keys_not_seen";
  13.159  Addsimps [new_keys_not_seen];
  13.160 @@ -139,23 +139,23 @@
  13.161  goal thy 
  13.162   "!!evs. [| Says A B X : set_of_list evs;  \
  13.163  \           Key (newK evt) : parts {X};    \
  13.164 -\           evs : yahalom                 \
  13.165 +\           evs : yahalom lost                 \
  13.166  \        |] ==> length evt < length evs";
  13.167 -br ccontr 1;
  13.168 -bd leI 1;
  13.169 -by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Enemy]
  13.170 +by (rtac ccontr 1);
  13.171 +by (dtac leI 1);
  13.172 +by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
  13.173                        addIs  [impOfSubs parts_mono]) 1);
  13.174  qed "Says_imp_old_keys";
  13.175  
  13.176  
  13.177  (*Nobody can have USED keys that will be generated in the future.
  13.178    ...very like new_keys_not_seen*)
  13.179 -goal thy "!!evs. evs : yahalom ==> \
  13.180 +goal thy "!!evs. evs : yahalom lost ==> \
  13.181  \                length evs <= length evs' --> \
  13.182 -\                newK evs' ~: keysFor (UN C. parts (sees C evs))";
  13.183 -be yahalom.induct 1;
  13.184 -by (forward_tac [YM4_parts_sees_Enemy] 6);
  13.185 -bd (YM4_analz_sees_Enemy RS synth.Inj) 6;
  13.186 +\                newK evs' ~: keysFor (UN C. parts (sees lost C evs))";
  13.187 +by (etac yahalom.induct 1);
  13.188 +by (forward_tac [YM4_parts_sees_Spy] 6);
  13.189 +by (dtac (YM4_analz_sees_Spy RS synth.Inj) 6);
  13.190  by (ALLGOALS Asm_full_simp_tac);
  13.191  (*YM1, YM2 and YM3*)
  13.192  by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,3,2]));
  13.193 @@ -167,22 +167,22 @@
  13.194  by (ALLGOALS
  13.195       (best_tac
  13.196        (!claset addDs [impOfSubs analz_subset_parts,
  13.197 -		      impOfSubs (analz_subset_parts RS keysFor_mono),
  13.198 -		      impOfSubs (parts_insert_subset_Un RS keysFor_mono),
  13.199 -		      Suc_leD]
  13.200 -	       addEs [new_keys_not_seen RSN(2,rev_notE)]
  13.201 -	       addss (!simpset))));
  13.202 +                      impOfSubs (analz_subset_parts RS keysFor_mono),
  13.203 +                      impOfSubs (parts_insert_subset_Un RS keysFor_mono),
  13.204 +                      Suc_leD]
  13.205 +               addEs [new_keys_not_seen RSN(2,rev_notE)]
  13.206 +               addss (!simpset))));
  13.207  val lemma = result();
  13.208  
  13.209  goal thy 
  13.210 - "!!evs. [| evs : yahalom;  length evs <= length evs' |]    \
  13.211 -\        ==> newK evs' ~: keysFor (parts (sees C evs))";
  13.212 + "!!evs. [| evs : yahalom lost;  length evs <= length evs' |]    \
  13.213 +\        ==> newK evs' ~: keysFor (parts (sees lost C evs))";
  13.214  by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
  13.215  qed "new_keys_not_used";
  13.216  
  13.217  bind_thm ("new_keys_not_analzd",
  13.218 -	  [analz_subset_parts RS keysFor_mono,
  13.219 -	   new_keys_not_used] MRS contra_subsetD);
  13.220 +          [analz_subset_parts RS keysFor_mono,
  13.221 +           new_keys_not_used] MRS contra_subsetD);
  13.222  
  13.223  Addsimps [new_keys_not_used, new_keys_not_analzd];
  13.224  
  13.225 @@ -193,8 +193,8 @@
  13.226  (****
  13.227   The following is to prove theorems of the form
  13.228  
  13.229 -          Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) ==>
  13.230 -          Key K : analz (sees Enemy evs)
  13.231 +          Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) ==>
  13.232 +          Key K : analz (sees lost Spy evs)
  13.233  
  13.234   A more general formula must be proved inductively.
  13.235  
  13.236 @@ -205,17 +205,17 @@
  13.237    to encrypt messages containing other keys, in the actual protocol.
  13.238    We require that agents should behave like this subsequently also.*)
  13.239  goal thy 
  13.240 - "!!evs. evs : yahalom ==> \
  13.241 -\        (Crypt X (newK evt)) : parts (sees Enemy evs) & \
  13.242 -\        Key K : parts {X} --> Key K : parts (sees Enemy evs)";
  13.243 -be yahalom.induct 1;
  13.244 -bd (YM4_analz_sees_Enemy RS synth.Inj) 6;
  13.245 + "!!evs. evs : yahalom lost ==> \
  13.246 +\        (Crypt X (newK evt)) : parts (sees lost Spy evs) & \
  13.247 +\        Key K : parts {X} --> Key K : parts (sees lost Spy evs)";
  13.248 +by (etac yahalom.induct 1);
  13.249 +by (dtac (YM4_analz_sees_Spy RS synth.Inj) 6);
  13.250  by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes)));
  13.251  (*Deals with Faked messages*)
  13.252  by (EVERY 
  13.253      (map (best_tac (!claset addSEs partsEs
  13.254 -			    addDs [impOfSubs parts_insert_subset_Un]
  13.255 -			    addss (!simpset)))
  13.256 +                            addDs [impOfSubs parts_insert_subset_Un]
  13.257 +                            addss (!simpset)))
  13.258       [3,2]));
  13.259  (*Base case*)
  13.260  by (Auto_tac());
  13.261 @@ -230,8 +230,8 @@
  13.262  Delsimps [image_Un];
  13.263  Addsimps [image_Un RS sym];
  13.264  
  13.265 -goal thy "insert (Key (newK x)) (sees A evs) = \
  13.266 -\         Key `` (newK``{x}) Un (sees A evs)";
  13.267 +goal thy "insert (Key (newK x)) (sees lost A evs) = \
  13.268 +\         Key `` (newK``{x}) Un (sees lost A evs)";
  13.269  by (Fast_tac 1);
  13.270  val insert_Key_singleton = result();
  13.271  
  13.272 @@ -243,10 +243,10 @@
  13.273  
  13.274  (*This lets us avoid analyzing the new message -- unless we have to!*)
  13.275  (*NEEDED??*)
  13.276 -goal thy "synth (analz (sees Enemy evs)) <=   \
  13.277 -\         synth (analz (sees Enemy (Says A B X # evs)))";
  13.278 +goal thy "synth (analz (sees lost Spy evs)) <=   \
  13.279 +\         synth (analz (sees lost Spy (Says A B X # evs)))";
  13.280  by (Simp_tac 1);
  13.281 -br (subset_insertI RS analz_mono RS synth_mono) 1;
  13.282 +by (rtac (subset_insertI RS analz_mono RS synth_mono) 1);
  13.283  qed "synth_analz_thin";
  13.284  
  13.285  AddIs [impOfSubs synth_analz_thin];
  13.286 @@ -265,33 +265,33 @@
  13.287  
  13.288  
  13.289  goal thy  
  13.290 - "!!evs. evs : yahalom ==> \
  13.291 -\  ALL K E. (Key K : analz (Key``(newK``E) Un (sees Enemy evs))) = \
  13.292 -\           (K : newK``E | Key K : analz (sees Enemy evs))";
  13.293 -be yahalom.induct 1;
  13.294 -bd YM4_analz_sees_Enemy 6;
  13.295 + "!!evs. evs : yahalom lost ==> \
  13.296 +\  ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \
  13.297 +\           (K : newK``E | Key K : analz (sees lost Spy evs))";
  13.298 +by (etac yahalom.induct 1);
  13.299 +by (dtac YM4_analz_sees_Spy 6);
  13.300  by (REPEAT_FIRST (resolve_tac [allI, lemma]));
  13.301  by (ALLGOALS 
  13.302      (asm_simp_tac 
  13.303       (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
  13.304 -			 @ pushes)
  13.305 +                         @ pushes)
  13.306                 setloop split_tac [expand_if])));
  13.307  (*YM4*) 
  13.308 -by (enemy_analz_tac 4);
  13.309 +by (spy_analz_tac 4);
  13.310  (*YM3*)
  13.311  by (Fast_tac 3);
  13.312  (*Fake case*)
  13.313 -by (enemy_analz_tac 2);
  13.314 +by (spy_analz_tac 2);
  13.315  (*Base case*)
  13.316  by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
  13.317  qed_spec_mp "analz_image_newK";
  13.318  
  13.319  goal thy
  13.320 - "!!evs. evs : yahalom ==>                               \
  13.321 -\        Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) = \
  13.322 -\        (K = newK evt | Key K : analz (sees Enemy evs))";
  13.323 + "!!evs. evs : yahalom lost ==>                               \
  13.324 +\        Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) = \
  13.325 +\        (K = newK evt | Key K : analz (sees lost Spy evs))";
  13.326  by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
  13.327 -				   insert_Key_singleton]) 1);
  13.328 +                                   insert_Key_singleton]) 1);
  13.329  by (Fast_tac 1);
  13.330  qed "analz_insert_Key_newK";
  13.331  
  13.332 @@ -301,39 +301,39 @@
  13.333   "!!evs. [| Says Server A                                           \
  13.334  \            {|Crypt {|Agent B, K, NA, NB|} (shrK A),               \
  13.335  \              Crypt {|Agent A, K|} (shrK B)|} : set_of_list evs;   \
  13.336 -\           evs : yahalom |]                                        \
  13.337 -\        ==> (EX evt:yahalom. K = Key(newK evt))";
  13.338 -be rev_mp 1;
  13.339 -be yahalom.induct 1;
  13.340 +\           evs : yahalom lost |]                                        \
  13.341 +\        ==> (EX evt: yahalom lost. K = Key(newK evt))";
  13.342 +by (etac rev_mp 1);
  13.343 +by (etac yahalom.induct 1);
  13.344  by (ALLGOALS (fast_tac (!claset addss (!simpset))));
  13.345  qed "Says_Server_message_form";
  13.346  
  13.347  
  13.348 -(** Crucial secrecy property: Enemy does not see the keys sent in msg YM3
  13.349 +(** Crucial secrecy property: Spy does not see the keys sent in msg YM3
  13.350      As with Otway-Rees, proof does not need uniqueness of session keys. **)
  13.351  
  13.352  goal thy 
  13.353 - "!!evs. [| A ~: bad;  B ~: bad;  evs : yahalom;  evt : yahalom |]        \
  13.354 + "!!evs. [| A ~: lost;  B ~: lost;  evs : yahalom lost;  evt : yahalom lost |]        \
  13.355  \        ==> Says Server A                                                \
  13.356  \              {|Crypt {|Agent B, Key(newK evt), NA, NB|} (shrK A),       \
  13.357  \                Crypt {|Agent A, Key(newK evt)|} (shrK B)|}              \
  13.358  \             : set_of_list evs -->    \
  13.359 -\            Key(newK evt) ~: analz (sees Enemy evs)";
  13.360 -be yahalom.induct 1;
  13.361 -bd YM4_analz_sees_Enemy 6;
  13.362 +\            Key(newK evt) ~: analz (sees lost Spy evs)";
  13.363 +by (etac yahalom.induct 1);
  13.364 +by (dtac YM4_analz_sees_Spy 6);
  13.365  by (ALLGOALS
  13.366      (asm_simp_tac 
  13.367       (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
  13.368 -			  analz_insert_Key_newK] @ pushes)
  13.369 +                          analz_insert_Key_newK] @ pushes)
  13.370                 setloop split_tac [expand_if])));
  13.371  (*YM4*)
  13.372 -by (enemy_analz_tac 3);
  13.373 +by (spy_analz_tac 3);
  13.374  (*YM3*)
  13.375  by (fast_tac (!claset addIs [parts_insertI]
  13.376 -		      addEs [Says_imp_old_keys RS less_irrefl]
  13.377 -	              addss (!simpset)) 2);
  13.378 +                      addEs [Says_imp_old_keys RS less_irrefl]
  13.379 +                      addss (!simpset)) 2);
  13.380  (*Fake*) (** LEVEL 10 **)
  13.381 -by (enemy_analz_tac 1);
  13.382 +by (spy_analz_tac 1);
  13.383  val lemma = result() RS mp RSN(2,rev_notE);
  13.384  
  13.385  
  13.386 @@ -342,26 +342,26 @@
  13.387   "!!evs. [| Says Server A \
  13.388  \            {|Crypt {|Agent B, K, NA, NB|} (shrK A),                   \
  13.389  \              Crypt {|Agent A, K|} (shrK B)|} : set_of_list evs;       \
  13.390 -\           A ~: bad;  B ~: bad;  evs : yahalom |] ==>                  \
  13.391 -\     K ~: analz (sees Enemy evs)";
  13.392 +\           A ~: lost;  B ~: lost;  evs : yahalom lost |] ==>                  \
  13.393 +\     K ~: analz (sees lost Spy evs)";
  13.394  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
  13.395  by (fast_tac (!claset addSEs [lemma]) 1);
  13.396 -qed "Enemy_not_see_encrypted_key";
  13.397 +qed "Spy_not_see_encrypted_key";
  13.398  
  13.399  
  13.400  (** Towards proofs of stronger authenticity properties **)
  13.401  
  13.402  goal thy 
  13.403 - "!!evs. [| Crypt {|Agent A, Key K|} (shrK B) : parts (sees Enemy evs); \
  13.404 -\           B ~: bad;  evs : yahalom |]                                 \
  13.405 + "!!evs. [| Crypt {|Agent A, Key K|} (shrK B) : parts (sees lost Spy evs); \
  13.406 +\           B ~: lost;  evs : yahalom lost |]                                 \
  13.407  \        ==> EX NA NB. Says Server A                                    \
  13.408  \                        {|Crypt {|Agent B, Key K,                      \
  13.409  \                                  Nonce NA, Nonce NB|} (shrK A),       \
  13.410  \                          Crypt {|Agent A, Key K|} (shrK B)|}          \
  13.411  \                       : set_of_list evs";
  13.412 -be rev_mp 1;
  13.413 -be yahalom.induct 1;
  13.414 -bd (YM4_analz_sees_Enemy RS synth.Inj) 6;
  13.415 +by (etac rev_mp 1);
  13.416 +by (etac yahalom.induct 1);
  13.417 +by (dtac (YM4_analz_sees_Spy RS synth.Inj) 6);
  13.418  by (ALLGOALS Asm_simp_tac);
  13.419  (*YM3*)
  13.420  by (Fast_tac 3);
  13.421 @@ -371,28 +371,28 @@
  13.422  by (stac insert_commute 2 THEN Simp_tac 2);
  13.423  (*Fake and YM4 are similar*)
  13.424  by (ALLGOALS (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
  13.425 -					impOfSubs Fake_parts_insert])));
  13.426 +                                        impOfSubs Fake_parts_insert])));
  13.427  qed "Crypt_imp_Server_msg";
  13.428  
  13.429  
  13.430  (*What can B deduce from receipt of YM4?  
  13.431    NOT THAT THE NONCES AGREE (in this version).  But what does the Nonce
  13.432 -	give us??*)
  13.433 +        give us??*)
  13.434  goal thy 
  13.435   "!!evs. [| Says A' B {|Crypt {|Agent A, Key K|} (shrK B),              \
  13.436  \                       Crypt (Nonce NB) K|} : set_of_list evs;         \
  13.437 -\           B ~: bad;  evs : yahalom |]                                 \
  13.438 +\           B ~: lost;  evs : yahalom lost |]                                 \
  13.439  \        ==> EX NA NB. Says Server A                                    \
  13.440  \                     {|Crypt {|Agent B, Key K,                         \
  13.441  \                               Nonce NA, Nonce NB|} (shrK A),          \
  13.442  \                       Crypt {|Agent A, Key K|} (shrK B)|}             \
  13.443  \                   : set_of_list evs";
  13.444 -be rev_mp 1;
  13.445 -be yahalom.induct 1;
  13.446 -by (dresolve_tac [YM4_analz_sees_Enemy] 6);
  13.447 +by (etac rev_mp 1);
  13.448 +by (etac yahalom.induct 1);
  13.449 +by (dtac YM4_analz_sees_Spy 6);
  13.450  by (ALLGOALS Asm_simp_tac);
  13.451  by (ALLGOALS (fast_tac (!claset addSDs [impOfSubs analz_subset_parts RS
  13.452 -					Crypt_imp_Server_msg])));
  13.453 +                                        Crypt_imp_Server_msg])));
  13.454  qed "YM4_imp_Says_Server_A";
  13.455  
  13.456  
  13.457 @@ -400,8 +400,8 @@
  13.458  goal thy 
  13.459   "!!evs. [| Says A' B {|Crypt {|Agent A, Key K|} (shrK B),              \
  13.460  \                       Crypt (Nonce NB) K|} : set_of_list evs;         \
  13.461 -\           A ~: bad;  B ~: bad;  evs : yahalom |]                      \
  13.462 -\        ==> Key K ~: analz (sees Enemy evs)";
  13.463 +\           A ~: lost;  B ~: lost;  evs : yahalom lost |]                      \
  13.464 +\        ==> Key K ~: analz (sees lost Spy evs)";
  13.465  by (fast_tac (!claset addSDs [YM4_imp_Says_Server_A,
  13.466 -			      Enemy_not_see_encrypted_key]) 1);
  13.467 +                              Spy_not_see_encrypted_key]) 1);
  13.468  qed "B_gets_secure_key";
    14.1 --- a/src/HOL/Auth/Yahalom.thy	Thu Sep 26 12:47:47 1996 +0200
    14.2 +++ b/src/HOL/Auth/Yahalom.thy	Thu Sep 26 12:50:48 1996 +0200
    14.3 @@ -12,34 +12,35 @@
    14.4  
    14.5  Yahalom = Shared + 
    14.6  
    14.7 -consts  yahalom   :: "event list set"
    14.8 -inductive yahalom
    14.9 +consts  yahalom   :: "agent set => event list set"
   14.10 +inductive "yahalom lost"
   14.11    intrs 
   14.12           (*Initial trace is empty*)
   14.13 -    Nil  "[]: yahalom"
   14.14 +    Nil  "[]: yahalom lost"
   14.15  
   14.16 -         (*The enemy MAY say anything he CAN say.  We do not expect him to
   14.17 +         (*The spy MAY say anything he CAN say.  We do not expect him to
   14.18             invent new nonces here, but he can also use NS1.  Common to
   14.19             all similar protocols.*)
   14.20 -    Fake "[| evs: yahalom;  B ~= Enemy;  X: synth (analz (sees Enemy evs)) |]
   14.21 -          ==> Says Enemy B X  # evs : yahalom"
   14.22 +    Fake "[| evs: yahalom lost;  B ~= Spy;  
   14.23 +             X: synth (analz (sees lost Spy evs)) |]
   14.24 +          ==> Says Spy B X  # evs : yahalom lost"
   14.25  
   14.26           (*Alice initiates a protocol run*)
   14.27 -    YM1  "[| evs: yahalom;  A ~= B |]
   14.28 -          ==> Says A B {|Agent A, Nonce (newN evs)|} # evs : yahalom"
   14.29 +    YM1  "[| evs: yahalom lost;  A ~= B |]
   14.30 +          ==> Says A B {|Agent A, Nonce (newN evs)|} # evs : yahalom lost"
   14.31  
   14.32           (*Bob's response to Alice's message.  Bob doesn't know who 
   14.33  	   the sender is, hence the A' in the sender field.*)
   14.34 -    YM2  "[| evs: yahalom;  B ~= Server;
   14.35 +    YM2  "[| evs: yahalom lost;  B ~= Server;
   14.36               Says A' B {|Agent A, Nonce NA|} : set_of_list evs |]
   14.37            ==> Says B Server 
   14.38                    {|Agent B, 
   14.39                      Crypt {|Agent A, Nonce NA, Nonce (newN evs)|} (shrK B)|}
   14.40 -                 # evs : yahalom"
   14.41 +                 # evs : yahalom lost"
   14.42  
   14.43           (*The Server receives Bob's message.  He responds by sending a
   14.44              new session key to Alice, with a packet for forwarding to Bob.*)
   14.45 -    YM3  "[| evs: yahalom;  A ~= Server;
   14.46 +    YM3  "[| evs: yahalom lost;  A ~= Server;
   14.47               Says B' Server 
   14.48                    {|Agent B, Crypt {|Agent A, Nonce NA, Nonce NB|} (shrK B)|}
   14.49                 : set_of_list evs |]
   14.50 @@ -47,15 +48,15 @@
   14.51                    {|Crypt {|Agent B, Key (newK evs), 
   14.52                              Nonce NA, Nonce NB|} (shrK A),
   14.53                      Crypt {|Agent A, Key (newK evs)|} (shrK B)|}
   14.54 -                 # evs : yahalom"
   14.55 +                 # evs : yahalom lost"
   14.56  
   14.57           (*Alice receives the Server's (?) message, checks her Nonce, and
   14.58             uses the new session key to send Bob his Nonce.*)
   14.59 -    YM4  "[| evs: yahalom;  A ~= B;  
   14.60 +    YM4  "[| evs: yahalom lost;  A ~= B;  
   14.61               Says S A {|Crypt {|Agent B, Key K, Nonce NA, Nonce NB|} (shrK A),
   14.62                          X|}
   14.63                 : set_of_list evs;
   14.64               Says A B {|Agent A, Nonce NA|} : set_of_list evs |]
   14.65 -          ==> Says A B {|X, Crypt (Nonce NB) K|} # evs : yahalom"
   14.66 +          ==> Says A B {|X, Crypt (Nonce NB) K|} # evs : yahalom lost"
   14.67  
   14.68  end