Global change: lost->bad and sees Spy->spies
authorpaulson
Thu Sep 18 13:24:04 1997 +0200 (1997-09-18)
changeset 3683aafe719dff14
parent 3682 597efdb7decb
child 3684 f677f0bc1cdf
Global change: lost->bad and sees Spy->spies
First change just gives a more sensible name.
Second change eliminates the agent parameter of "sees" to simplify
definitions and theorems
src/HOL/Auth/Event.ML
src/HOL/Auth/Event.thy
src/HOL/Auth/Message.ML
src/HOL/Auth/NS_Public.ML
src/HOL/Auth/NS_Public.thy
src/HOL/Auth/NS_Public_Bad.ML
src/HOL/Auth/NS_Public_Bad.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_AN.ML
src/HOL/Auth/OtwayRees_AN.thy
src/HOL/Auth/OtwayRees_Bad.ML
src/HOL/Auth/OtwayRees_Bad.thy
src/HOL/Auth/Public.ML
src/HOL/Auth/Public.thy
src/HOL/Auth/Recur.ML
src/HOL/Auth/Recur.thy
src/HOL/Auth/Shared.ML
src/HOL/Auth/Shared.thy
src/HOL/Auth/TLS.ML
src/HOL/Auth/TLS.thy
src/HOL/Auth/WooLam.ML
src/HOL/Auth/WooLam.thy
src/HOL/Auth/Yahalom.ML
src/HOL/Auth/Yahalom.thy
src/HOL/Auth/Yahalom2.ML
src/HOL/Auth/Yahalom2.thy
     1.1 --- a/src/HOL/Auth/Event.ML	Wed Sep 17 16:40:52 1997 +0200
     1.2 +++ b/src/HOL/Auth/Event.ML	Thu Sep 18 13:24:04 1997 +0200
     1.3 @@ -10,147 +10,111 @@
     1.4  
     1.5  open Event;
     1.6  
     1.7 -AddIffs [Spy_in_lost, Server_not_lost];
     1.8 -
     1.9 -(**** Function "sees" ****)
    1.10 -
    1.11 -(** Specialized rewrite rules for (sees A' (Says A B X #evs)) **)
    1.12 +AddIffs [Spy_in_bad, Server_not_bad];
    1.13  
    1.14 -goal thy "sees B (Says A B X # evs) = insert X (sees B evs)";
    1.15 -by (Simp_tac 1);
    1.16 -qed "sees_own_Says";
    1.17 -
    1.18 -(** Three special-case rules for rewriting of sees A **)
    1.19 +(**** Function "spies" ****)
    1.20  
    1.21 -goal thy "!!A. Server ~= B ==> \
    1.22 -\              sees Server (Says A B X # evs) = sees Server evs";
    1.23 -by (Asm_simp_tac 1);
    1.24 -qed "sees_Server_Says";
    1.25 +(** Simplifying   parts (insert X (spies evs))
    1.26 +      = parts {X} Un parts (spies evs) -- since general case loops*)
    1.27  
    1.28 -goal thy "!!A. Friend i ~= B ==> \
    1.29 -\              sees (Friend i) (Says A B X # evs) = sees (Friend i) evs";
    1.30 -by (Asm_simp_tac 1);
    1.31 -qed "sees_Friend_Says";
    1.32 -
    1.33 -goal thy "sees Spy (Says A B X # evs) = insert X (sees Spy evs)";
    1.34 -by (Simp_tac 1);
    1.35 -qed "sees_Spy_Says";
    1.36 +bind_thm ("parts_insert_spies",
    1.37 +	  parts_insert |> 
    1.38 +	  read_instantiate_sg (sign_of thy) [("H", "spies evs")]);
    1.39  
    1.40  
    1.41 -(** Specialized rewrite rules for (sees A' (Notes A X evs)) **)
    1.42 -
    1.43 -goal thy "sees A (Notes A X # evs) = insert X (sees A evs)";
    1.44 -by (Simp_tac 1);
    1.45 -qed "sees_own_Notes";
    1.46 -
    1.47 -(** Three special-case rules for rewriting of sees A **)
    1.48 +goal thy
    1.49 +    "P(event_case sf nf ev) = \
    1.50 +\      ((ALL A B X. ev = Says A B X --> P(sf A B X)) & \
    1.51 +\       (ALL A X. ev = Notes A X --> P(nf A X)))";
    1.52 +by (induct_tac "ev" 1);
    1.53 +by (Auto_tac());
    1.54 +qed "expand_event_case";
    1.55  
    1.56 -goal thy "!!A. Server ~= A ==> \
    1.57 -\              sees Server (Notes A X # evs) = sees Server evs";
    1.58 -by (Asm_simp_tac 1);
    1.59 -qed "sees_Server_Notes";
    1.60 -
    1.61 -goal thy "!!A. Friend i ~= A ==> \
    1.62 -\              sees (Friend i) (Notes A X # evs) = sees (Friend i) evs";
    1.63 -by (Asm_simp_tac 1);
    1.64 -qed "sees_Friend_Notes";
    1.65 +goal thy "spies (Says A B X # evs) = insert X (spies evs)";
    1.66 +by (Simp_tac 1);
    1.67 +qed "spies_Says";
    1.68  
    1.69 -(*The point of letting the Spy see "lost" agents' notes is to prevent
    1.70 -  redundant case-splits on whether A=Spy and whether A:lost*)
    1.71 -goal thy "sees Spy (Notes A X # evs) = \
    1.72 -\         (if A:lost then insert X (sees Spy evs) else sees Spy evs)";
    1.73 -by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
    1.74 -by (Blast_tac 1);
    1.75 -qed "sees_Spy_Notes";
    1.76 -
    1.77 +(*The point of letting the Spy see "bad" agents' notes is to prevent
    1.78 +  redundant case-splits on whether A=Spy and whether A:bad*)
    1.79 +goal thy "spies (Notes A X # evs) = \
    1.80 +\         (if A:bad then insert X (spies evs) else spies evs)";
    1.81 +by (Simp_tac 1);
    1.82 +qed "spies_Notes";
    1.83  
    1.84 -(** Other "sees" lemmas **)
    1.85 +goal thy "spies evs <= spies (Says A B X # evs)";
    1.86 +by (simp_tac (!simpset addsimps [subset_insertI]) 1);
    1.87 +qed "spies_subset_spies_Says";
    1.88  
    1.89 -goal thy "sees A (Says A' B X # evs) <= insert X (sees A evs)";
    1.90 -by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
    1.91 -by (Fast_tac 1);
    1.92 -qed "sees_Says_subset_insert";
    1.93 -
    1.94 -goal thy "sees A evs <= sees A (Says A' B X # evs)";
    1.95 +goal thy "spies evs <= spies (Notes A X # evs)";
    1.96  by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
    1.97  by (Fast_tac 1);
    1.98 -qed "sees_subset_sees_Says";
    1.99 -
   1.100 -goal thy "sees A evs <= sees A (Notes A' X # evs)";
   1.101 -by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
   1.102 -by (Fast_tac 1);
   1.103 -qed "sees_subset_sees_Notes";
   1.104 -
   1.105 -(*Pushing Unions into parts.  One of the agents A is B, and thus sees Y.*)
   1.106 -goal thy "(UN A. parts (sees A (Says B C Y # evs))) = \
   1.107 -\         parts {Y} Un (UN A. parts (sees A evs))";
   1.108 -by (Step_tac 1);
   1.109 -by (etac rev_mp 1);     (*split_tac does not work on assumptions*)
   1.110 -by (ALLGOALS
   1.111 -    (fast_tac (!claset addss (!simpset addsimps [parts_Un] 
   1.112 -				       setloop split_tac [expand_if]))));
   1.113 -qed "UN_parts_sees_Says";
   1.114 -
   1.115 -goal thy "(UN A. parts (sees A (Notes B Y # evs))) = \
   1.116 -\         parts {Y} Un (UN A. parts (sees A evs))";
   1.117 -by (Step_tac 1);
   1.118 -by (etac rev_mp 1);     (*split_tac does not work on assumptions*)
   1.119 -by (ALLGOALS
   1.120 -    (fast_tac (!claset addss (!simpset addsimps [parts_Un] 
   1.121 -				       setloop split_tac [expand_if]))));
   1.122 -qed "UN_parts_sees_Notes";
   1.123 +qed "spies_subset_spies_Notes";
   1.124  
   1.125  (*Spy sees all traffic*)
   1.126 -goal thy "Says A B X : set evs --> X : sees Spy evs";
   1.127 +goal thy "Says A B X : set evs --> X : spies evs";
   1.128  by (induct_tac "evs" 1);
   1.129 -by (Auto_tac ());
   1.130 -qed_spec_mp "Says_imp_sees_Spy";
   1.131 +by (ALLGOALS (asm_simp_tac
   1.132 +	      (!simpset setloop split_tac [expand_event_case, expand_if])));
   1.133 +qed_spec_mp "Says_imp_spies";
   1.134  
   1.135 -(*Spy sees Notes of lost agents*)
   1.136 -goal thy "Notes A X : set evs --> A: lost --> X : sees Spy evs";
   1.137 +(*Spy sees Notes of bad agents*)
   1.138 +goal thy "Notes A X : set evs --> A: bad --> X : spies evs";
   1.139  by (induct_tac "evs" 1);
   1.140 -by (Auto_tac ());
   1.141 -qed_spec_mp "Notes_imp_sees_Spy";
   1.142 +by (ALLGOALS (asm_simp_tac
   1.143 +	      (!simpset setloop split_tac [expand_event_case, expand_if])));
   1.144 +qed_spec_mp "Notes_imp_spies";
   1.145  
   1.146  (*Use with addSEs to derive contradictions from old Says events containing
   1.147    items known to be fresh*)
   1.148 -val sees_Spy_partsEs = make_elim (Says_imp_sees_Spy RS parts.Inj) :: partsEs;
   1.149 +val spies_partsEs = make_elim (Says_imp_spies RS parts.Inj) :: partsEs;
   1.150  
   1.151 -Addsimps [sees_own_Says, sees_Server_Says, sees_Friend_Says, sees_Spy_Says,
   1.152 -      sees_own_Notes, sees_Server_Notes, sees_Friend_Notes, sees_Spy_Notes];
   1.153 +Addsimps [spies_Says, spies_Notes];
   1.154  
   1.155 -(**** NOTE REMOVAL--laws above are cleaner--def of sees1 is messy ****)
   1.156 -Delsimps [sees_Cons];   
   1.157 +(**** NOTE REMOVAL--laws above are cleaner, as they don't involve "case" ****)
   1.158 +Delsimps [spies_Cons];   
   1.159  
   1.160  
   1.161  (*** Fresh nonces ***)
   1.162  
   1.163 -goalw thy [used_def] "!!X. X: parts (sees B evs) ==> X: used evs";
   1.164 -by (etac (impOfSubs parts_mono) 1);
   1.165 -by (Fast_tac 1);
   1.166 -qed "usedI";
   1.167 +goal thy "parts (spies evs) <= used evs";
   1.168 +by (induct_tac "evs" 1);
   1.169 +by (ALLGOALS (asm_simp_tac
   1.170 +	      (!simpset addsimps [parts_insert_spies]
   1.171 +	                setloop split_tac [expand_event_case, expand_if])));
   1.172 +by (ALLGOALS Blast_tac);
   1.173 +bind_thm ("usedI", impOfSubs (result()));
   1.174  AddIs [usedI];
   1.175  
   1.176 +goal thy "parts (initState B) <= used evs";
   1.177 +by (induct_tac "evs" 1);
   1.178 +by (ALLGOALS (asm_simp_tac
   1.179 +	      (!simpset addsimps [parts_insert_spies]
   1.180 +	                setloop split_tac [expand_event_case, expand_if])));
   1.181 +by (ALLGOALS Blast_tac);
   1.182 +bind_thm ("initState_into_used", impOfSubs (result()));
   1.183 +
   1.184  goal thy "used (Says A B X # evs) = parts{X} Un used evs";
   1.185 -by (simp_tac (!simpset addsimps [used_def, UN_parts_sees_Says]) 1);
   1.186 +by (Simp_tac 1);
   1.187  qed "used_Says";
   1.188  Addsimps [used_Says];
   1.189  
   1.190  goal thy "used (Notes A X # evs) = parts{X} Un used evs";
   1.191 -by (simp_tac (!simpset addsimps [used_def, UN_parts_sees_Notes]) 1);
   1.192 +by (Simp_tac 1);
   1.193  qed "used_Notes";
   1.194  Addsimps [used_Notes];
   1.195  
   1.196 -(*These two facts about "used" are unused.*)
   1.197 -goal thy "used [] <= used l";
   1.198 -by (induct_tac "l" 1);
   1.199 -by (induct_tac "a" 2);
   1.200 -by (ALLGOALS Asm_simp_tac);
   1.201 -by (ALLGOALS Blast_tac);
   1.202 +goal thy "used [] <= used evs";
   1.203 +by (Simp_tac 1);
   1.204 +by (blast_tac (!claset addIs [initState_into_used]) 1);
   1.205  qed "used_nil_subset";
   1.206  
   1.207 -goal thy "used l <= used (l@l')";
   1.208 -by (induct_tac "l" 1);
   1.209 +(**** NOTE REMOVAL--laws above are cleaner, as they don't involve "case" ****)
   1.210 +Delsimps [used_Nil, used_Cons];   
   1.211 +
   1.212 +
   1.213 +(*currently unused*)
   1.214 +goal thy "used evs <= used (evs@evs')";
   1.215 +by (induct_tac "evs" 1);
   1.216  by (simp_tac (!simpset addsimps [used_nil_subset]) 1);
   1.217  by (induct_tac "a" 1);
   1.218  by (ALLGOALS Asm_simp_tac);
   1.219 @@ -158,17 +122,7 @@
   1.220  qed "used_subset_append";
   1.221  
   1.222  
   1.223 -(** Simplifying   parts (insert X (sees A evs))
   1.224 -      = parts {X} Un parts (sees A evs) -- since general case loops*)
   1.225 -
   1.226 -val parts_insert_sees = 
   1.227 -    parts_insert |> read_instantiate_sg (sign_of thy)
   1.228 -                                        [("H", "sees A evs")]
   1.229 -                 |> standard;
   1.230 -
   1.231 -
   1.232 -
   1.233 -(*For proving theorems of the form X ~: analz (sees Spy evs) --> P
   1.234 +(*For proving theorems of the form X ~: analz (spies evs) --> P
   1.235    New events added by induction to "evs" are discarded.  Provided 
   1.236    this information isn't needed, the proof will be much shorter, since
   1.237    it will omit complicated reasoning about analz.*)
   1.238 @@ -179,8 +133,8 @@
   1.239      rtac impI THEN' 
   1.240      REPEAT1 o 
   1.241        (dresolve_tac 
   1.242 -       [sees_subset_sees_Says  RS analz_mono RS contra_subsetD,
   1.243 -	sees_subset_sees_Notes RS analz_mono RS contra_subsetD])
   1.244 +       [spies_subset_spies_Says  RS analz_mono RS contra_subsetD,
   1.245 +	spies_subset_spies_Notes RS analz_mono RS contra_subsetD])
   1.246      THEN'
   1.247      mp_tac
   1.248    end;
     2.1 --- a/src/HOL/Auth/Event.thy	Wed Sep 17 16:40:52 1997 +0200
     2.2 +++ b/src/HOL/Auth/Event.thy	Thu Sep 18 13:24:04 1997 +0200
     2.3 @@ -5,9 +5,9 @@
     2.4  
     2.5  Theory of events for security protocols
     2.6  
     2.7 -Datatype of events; function "sees"; freshness
     2.8 +Datatype of events; function "spies"; freshness
     2.9  
    2.10 -"lost" agents have been broken by the Spy; their private keys and internal
    2.11 +"bad" agents have been broken by the Spy; their private keys and internal
    2.12      stores are visible to him
    2.13  *)
    2.14  
    2.15 @@ -21,31 +21,33 @@
    2.16          | Notes agent       msg
    2.17  
    2.18  consts  
    2.19 -  lost :: agent set        (*compromised agents*)
    2.20 -  sees :: [agent, event list] => msg set
    2.21 +  bad    :: agent set        (*compromised agents*)
    2.22 +  spies  :: event list => msg set
    2.23  
    2.24  rules
    2.25    (*Spy has access to his own key for spoof messages, but Server is secure*)
    2.26 -  Spy_in_lost     "Spy: lost"
    2.27 -  Server_not_lost "Server ~: lost"
    2.28 +  Spy_in_bad     "Spy: bad"
    2.29 +  Server_not_bad "Server ~: bad"
    2.30  
    2.31 -consts  
    2.32 -  sees1 :: [agent, event] => msg set
    2.33 -
    2.34 -primrec sees1 event
    2.35 +primrec spies list
    2.36             (*Spy reads all traffic whether addressed to him or not*)
    2.37 -  sees1_Says  "sees1 A (Says A' B X)  = (if A:{B,Spy} then {X} else {})"
    2.38 -  sees1_Notes "sees1 A (Notes A' X)   = (if A=A' | A=Spy & A':lost then {X}
    2.39 -					 else {})"
    2.40 +  spies_Nil   "spies []       = initState Spy"
    2.41 +  spies_Cons  "spies (ev # evs) =
    2.42 +	         (case ev of
    2.43 +		    Says A B X => insert X (spies evs)
    2.44 +		  | Notes A X  => 
    2.45 +	              if A:bad then insert X (spies evs) else spies evs)"
    2.46  
    2.47 -primrec sees list
    2.48 -  sees_Nil  "sees A []       = initState A"
    2.49 -  sees_Cons "sees A (ev#evs) = sees1 A ev Un sees A evs"
    2.50 +consts
    2.51 +  (*Set of items that might be visible to somebody:
    2.52 +    complement of the set of fresh items*)
    2.53 +  used :: event list => msg set
    2.54  
    2.55 -constdefs
    2.56 -  (*Set of items that might be visible to somebody: complement of the set
    2.57 -        of fresh items*)
    2.58 -  used :: event list => msg set
    2.59 -    "used evs == parts (UN B. sees B evs)"
    2.60 +primrec used list
    2.61 +  used_Nil   "used []         = (UN B. parts (initState B))"
    2.62 +  used_Cons  "used (ev # evs) =
    2.63 +	         (case ev of
    2.64 +		    Says A B X => parts {X} Un (used evs)
    2.65 +		  | Notes A X  => parts {X} Un (used evs))"
    2.66  
    2.67  end
     3.1 --- a/src/HOL/Auth/Message.ML	Wed Sep 17 16:40:52 1997 +0200
     3.2 +++ b/src/HOL/Auth/Message.ML	Thu Sep 18 13:24:04 1997 +0200
     3.3 @@ -875,7 +875,7 @@
     3.4  (*** Tactics useful for many protocol proofs ***)
     3.5  
     3.6  (*Prove base case (subgoal i) and simplify others.  A typical base case
     3.7 -  concerns  Crypt K X ~: Key``shrK``lost  and cannot be proved by rewriting
     3.8 +  concerns  Crypt K X ~: Key``shrK``bad  and cannot be proved by rewriting
     3.9    alone.*)
    3.10  fun prove_simple_subgoals_tac i = 
    3.11      fast_tac (!claset addss (!simpset)) i THEN
     4.1 --- a/src/HOL/Auth/NS_Public.ML	Wed Sep 17 16:40:52 1997 +0200
     4.2 +++ b/src/HOL/Auth/NS_Public.ML	Thu Sep 18 13:24:04 1997 +0200
     4.3 @@ -12,7 +12,7 @@
     4.4  proof_timing:=true;
     4.5  HOL_quantifiers := false;
     4.6  
     4.7 -AddIffs [Spy_in_lost];
     4.8 +AddIffs [Spy_in_bad];
     4.9  
    4.10  (*A "possibility property": there are traces that reach the end*)
    4.11  goal thy 
    4.12 @@ -36,8 +36,8 @@
    4.13  
    4.14  
    4.15  (*Induction for regularity theorems.  If induction formula has the form
    4.16 -   X ~: analz (sees Spy evs) --> ... then it shortens the proof by discarding
    4.17 -   needless information about analz (insert X (sees Spy evs))  *)
    4.18 +   X ~: analz (spies evs) --> ... then it shortens the proof by discarding
    4.19 +   needless information about analz (insert X (spies evs))  *)
    4.20  fun parts_induct_tac i = 
    4.21      etac ns_public.induct i
    4.22      THEN 
    4.23 @@ -46,25 +46,25 @@
    4.24      prove_simple_subgoals_tac i;
    4.25  
    4.26  
    4.27 -(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
    4.28 +(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
    4.29      sends messages containing X! **)
    4.30  
    4.31 -(*Spy never sees another agent's private key! (unless it's lost at start)*)
    4.32 +(*Spy never sees another agent's private key! (unless it's bad at start)*)
    4.33  goal thy 
    4.34 - "!!A. evs: ns_public ==> (Key (priK A) : parts (sees Spy evs)) = (A : lost)";
    4.35 + "!!A. evs: ns_public ==> (Key (priK A) : parts (spies evs)) = (A : bad)";
    4.36  by (parts_induct_tac 1);
    4.37  by (Fake_parts_insert_tac 1);
    4.38  qed "Spy_see_priK";
    4.39  Addsimps [Spy_see_priK];
    4.40  
    4.41  goal thy 
    4.42 - "!!A. evs: ns_public ==> (Key (priK A) : analz (sees Spy evs)) = (A : lost)";
    4.43 + "!!A. evs: ns_public ==> (Key (priK A) : analz (spies evs)) = (A : bad)";
    4.44  by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
    4.45  qed "Spy_analz_priK";
    4.46  Addsimps [Spy_analz_priK];
    4.47  
    4.48 -goal thy  "!!A. [| Key (priK A) : parts (sees Spy evs);       \
    4.49 -\                  evs : ns_public |] ==> A:lost";
    4.50 +goal thy  "!!A. [| Key (priK A) : parts (spies evs);       \
    4.51 +\                  evs : ns_public |] ==> A:bad";
    4.52  by (blast_tac (!claset addDs [Spy_see_priK]) 1);
    4.53  qed "Spy_see_priK_D";
    4.54  
    4.55 @@ -77,10 +77,10 @@
    4.56  (*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce
    4.57    is secret.  (Honest users generate fresh nonces.)*)
    4.58  goal thy 
    4.59 - "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees Spy evs); \
    4.60 -\           Nonce NA ~: analz (sees Spy evs);       \
    4.61 + "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \
    4.62 +\           Nonce NA ~: analz (spies evs);       \
    4.63  \           evs : ns_public |]                      \
    4.64 -\ ==> Crypt (pubK C) {|NA', Nonce NA, Agent D|} ~: parts (sees Spy evs)";
    4.65 +\ ==> Crypt (pubK C) {|NA', Nonce NA, Agent D|} ~: parts (spies evs)";
    4.66  by (etac rev_mp 1);
    4.67  by (etac rev_mp 1);
    4.68  by (parts_induct_tac 1);
    4.69 @@ -94,14 +94,14 @@
    4.70  
    4.71  (*Unicity for NS1: nonce NA identifies agents A and B*)
    4.72  goal thy 
    4.73 - "!!evs. [| Nonce NA ~: analz (sees Spy evs);  evs : ns_public |]      \
    4.74 + "!!evs. [| Nonce NA ~: analz (spies evs);  evs : ns_public |]      \
    4.75  \ ==> EX A' B'. ALL A B.                                               \
    4.76 -\      Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees Spy evs) --> \
    4.77 +\      Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs) --> \
    4.78  \      A=A' & B=B'";
    4.79  by (etac rev_mp 1);
    4.80  by (parts_induct_tac 1);
    4.81  by (ALLGOALS
    4.82 -    (asm_simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees])));
    4.83 +    (asm_simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_spies])));
    4.84  (*NS1*)
    4.85  by (expand_case_tac "NA = ?y" 2 THEN blast_tac (!claset addSEs partsEs) 2);
    4.86  (*Fake*)
    4.87 @@ -111,10 +111,10 @@
    4.88  val lemma = result();
    4.89  
    4.90  goal thy 
    4.91 - "!!evs. [| Crypt(pubK B)  {|Nonce NA, Agent A|}  : parts(sees Spy evs); \
    4.92 -\           Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(sees Spy evs); \
    4.93 -\           Nonce NA ~: analz (sees Spy evs);                            \
    4.94 -\           evs : ns_public |]                                                \
    4.95 + "!!evs. [| Crypt(pubK B)  {|Nonce NA, Agent A|}  : parts(spies evs); \
    4.96 +\           Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(spies evs); \
    4.97 +\           Nonce NA ~: analz (spies evs);                            \
    4.98 +\           evs : ns_public |]                                        \
    4.99  \        ==> A=A' & B=B'";
   4.100  by (prove_unique_tac lemma 1);
   4.101  qed "unique_NA";
   4.102 @@ -130,19 +130,19 @@
   4.103  (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
   4.104  goal thy 
   4.105   "!!evs. [| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs;         \
   4.106 -\           A ~: lost;  B ~: lost;  evs : ns_public |]                        \
   4.107 -\        ==>  Nonce NA ~: analz (sees Spy evs)";
   4.108 +\           A ~: bad;  B ~: bad;  evs : ns_public |]                        \
   4.109 +\        ==>  Nonce NA ~: analz (spies evs)";
   4.110  by (etac rev_mp 1);
   4.111  by (analz_induct_tac 1);
   4.112  (*NS3*)
   4.113 -by (blast_tac (!claset addDs  [Says_imp_sees_Spy RS parts.Inj]
   4.114 +by (blast_tac (!claset addDs  [Says_imp_spies RS parts.Inj]
   4.115                         addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4);
   4.116  (*NS2*)
   4.117  by (blast_tac (!claset addSEs [MPair_parts]
   4.118 -		       addDs  [Says_imp_sees_Spy RS parts.Inj,
   4.119 +		       addDs  [Says_imp_spies RS parts.Inj,
   4.120  			       parts.Body, unique_NA]) 3);
   4.121  (*NS1*)
   4.122 -by (blast_tac (!claset addSEs sees_Spy_partsEs
   4.123 +by (blast_tac (!claset addSEs spies_partsEs
   4.124                         addIs  [impOfSubs analz_subset_parts]) 2);
   4.125  (*Fake*)
   4.126  by (spy_analz_tac 1);
   4.127 @@ -155,16 +155,16 @@
   4.128   "!!evs. [| Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs;  \
   4.129  \           Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|})   \
   4.130  \             : set evs;                                                \
   4.131 -\           A ~: lost;  B ~: lost;  evs : ns_public |]                  \
   4.132 +\           A ~: bad;  B ~: bad;  evs : ns_public |]                  \
   4.133  \        ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|})   \
   4.134  \              : set evs";
   4.135  by (etac rev_mp 1);
   4.136  (*prepare induction over Crypt (pubK A) {|NA,NB,B|} : parts H*)
   4.137 -by (etac (Says_imp_sees_Spy RS parts.Inj RS rev_mp) 1);
   4.138 +by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1);
   4.139  by (etac ns_public.induct 1);
   4.140  by (ALLGOALS Asm_simp_tac);
   4.141  (*NS1*)
   4.142 -by (blast_tac (!claset addSEs sees_Spy_partsEs) 2);
   4.143 +by (blast_tac (!claset addSEs spies_partsEs) 2);
   4.144  (*Fake*)
   4.145  by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert]
   4.146                         addDs  [Spy_not_see_NA, 
   4.147 @@ -173,9 +173,9 @@
   4.148  
   4.149  (*If the encrypted message appears then it originated with Alice in NS1*)
   4.150  goal thy 
   4.151 - "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees Spy evs); \
   4.152 -\           Nonce NA ~: analz (sees Spy evs);                 \
   4.153 -\           evs : ns_public |]                                     \
   4.154 + "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \
   4.155 +\           Nonce NA ~: analz (spies evs);                 \
   4.156 +\           evs : ns_public |]                             \
   4.157  \   ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs";
   4.158  by (etac rev_mp 1);
   4.159  by (etac rev_mp 1);
   4.160 @@ -191,14 +191,14 @@
   4.161    [unicity of B makes Lowe's fix work]
   4.162    [proof closely follows that for unique_NA] *)
   4.163  goal thy 
   4.164 - "!!evs. [| Nonce NB ~: analz (sees Spy evs);  evs : ns_public |]      \
   4.165 + "!!evs. [| Nonce NB ~: analz (spies evs);  evs : ns_public |]      \
   4.166  \ ==> EX A' NA' B'. ALL A NA B.                                             \
   4.167 -\      Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}                       \
   4.168 -\        : parts (sees Spy evs)  -->  A=A' & NA=NA' & B=B'";
   4.169 +\      Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|} : parts (spies evs) \
   4.170 +\         -->  A=A' & NA=NA' & B=B'";
   4.171  by (etac rev_mp 1);
   4.172  by (parts_induct_tac 1);
   4.173  by (ALLGOALS
   4.174 -    (asm_simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees])));
   4.175 +    (asm_simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_spies])));
   4.176  (*NS2*)
   4.177  by (expand_case_tac "NB = ?y" 2 THEN blast_tac (!claset addSEs partsEs) 2);
   4.178  (*Fake*)
   4.179 @@ -209,10 +209,10 @@
   4.180  
   4.181  goal thy 
   4.182   "!!evs. [| Crypt(pubK A)  {|Nonce NA, Nonce NB, Agent B|}   \
   4.183 -\             : parts(sees Spy evs);                         \
   4.184 +\             : parts(spies evs);                         \
   4.185  \           Crypt(pubK A') {|Nonce NA', Nonce NB, Agent B'|} \
   4.186 -\             : parts(sees Spy evs);                         \
   4.187 -\           Nonce NB ~: analz (sees Spy evs);                \
   4.188 +\             : parts(spies evs);                         \
   4.189 +\           Nonce NB ~: analz (spies evs);                \
   4.190  \           evs : ns_public |]                               \
   4.191  \        ==> A=A' & NA=NA' & B=B'";
   4.192  by (prove_unique_tac lemma 1);
   4.193 @@ -223,20 +223,20 @@
   4.194  goal thy 
   4.195   "!!evs. [| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
   4.196  \             : set evs;                                              \
   4.197 -\           A ~: lost;  B ~: lost;  evs : ns_public |]                \
   4.198 -\ ==> Nonce NB ~: analz (sees Spy evs)";
   4.199 +\           A ~: bad;  B ~: bad;  evs : ns_public |]                \
   4.200 +\ ==> Nonce NB ~: analz (spies evs)";
   4.201  by (etac rev_mp 1);
   4.202  by (analz_induct_tac 1);
   4.203  (*NS3*)
   4.204 -by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj, unique_NB]) 4);
   4.205 +by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj, unique_NB]) 4);
   4.206  (*NS1*)
   4.207 -by (blast_tac (!claset addSEs sees_Spy_partsEs) 2);
   4.208 +by (blast_tac (!claset addSEs spies_partsEs) 2);
   4.209  (*Fake*)
   4.210  by (spy_analz_tac 1);
   4.211  (*NS2*)
   4.212  by (Step_tac 1);
   4.213 -by (blast_tac (!claset addSEs sees_Spy_partsEs) 3);
   4.214 -by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
   4.215 +by (blast_tac (!claset addSEs spies_partsEs) 3);
   4.216 +by (blast_tac (!claset addSDs [Says_imp_spies RS parts.Inj]
   4.217                         addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 2);
   4.218  by (blast_tac (!claset addSIs [impOfSubs analz_subset_parts]) 1);
   4.219  qed "Spy_not_see_NB";
   4.220 @@ -248,21 +248,21 @@
   4.221   "!!evs. [| Says B A  (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
   4.222  \             : set evs;                                               \
   4.223  \           Says A' B (Crypt (pubK B) (Nonce NB)): set evs;            \
   4.224 -\           A ~: lost;  B ~: lost;  evs : ns_public |]                 \
   4.225 +\           A ~: bad;  B ~: bad;  evs : ns_public |]                 \
   4.226  \        ==> Says A B (Crypt (pubK B) (Nonce NB)) : set evs";
   4.227  by (etac rev_mp 1);
   4.228  (*prepare induction over Crypt (pubK B) NB : parts H*)
   4.229 -by (etac (Says_imp_sees_Spy RS parts.Inj RS rev_mp) 1);
   4.230 +by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1);
   4.231  by (parts_induct_tac 1);
   4.232  (*NS1*)
   4.233 -by (blast_tac (!claset addSEs sees_Spy_partsEs) 2);
   4.234 +by (blast_tac (!claset addSEs spies_partsEs) 2);
   4.235  (*Fake*)
   4.236  by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert]
   4.237                         addDs  [Spy_not_see_NB, 
   4.238  			       impOfSubs analz_subset_parts]) 1);
   4.239  (*NS3; not clear why blast_tac needs to be preceeded by Step_tac*)
   4.240  by (Step_tac 1);
   4.241 -by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj,
   4.242 +by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj,
   4.243  			      Spy_not_see_NB, unique_NB]) 1);
   4.244  qed "B_trusts_NS3";
   4.245  
   4.246 @@ -270,8 +270,8 @@
   4.247  (**** Overall guarantee for B*)
   4.248  
   4.249  (*Matches only NS2, not NS1 (or NS3)*)
   4.250 -val Says_imp_sees_Spy' = 
   4.251 -    read_instantiate [("X","Crypt ?K {|?XX,?YY,?ZZ|}")] Says_imp_sees_Spy;
   4.252 +val Says_imp_spies' = 
   4.253 +    read_instantiate [("X","Crypt ?K {|?XX,?YY,?ZZ|}")] Says_imp_spies;
   4.254  
   4.255  
   4.256  (*If B receives NS3 and the nonce NB agrees with the nonce he joined with
   4.257 @@ -280,16 +280,16 @@
   4.258   "!!evs. [| Says B A  (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
   4.259  \             : set evs;                                               \
   4.260  \           Says A' B (Crypt (pubK B) (Nonce NB)): set evs;            \
   4.261 -\           A ~: lost;  B ~: lost;  evs : ns_public |]                 \
   4.262 +\           A ~: bad;  B ~: bad;  evs : ns_public |]                 \
   4.263  \    ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs";
   4.264  by (etac rev_mp 1);
   4.265  (*prepare induction over Crypt (pubK B) {|NB|} : parts H*)
   4.266 -by (etac (Says_imp_sees_Spy RS parts.Inj RS rev_mp) 1);
   4.267 +by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1);
   4.268  by (etac ns_public.induct 1);
   4.269  by (ALLGOALS Asm_simp_tac);
   4.270  (*Fake, NS2, NS3*)
   4.271  (*NS1*)
   4.272 -by (blast_tac (!claset addSEs sees_Spy_partsEs) 2);
   4.273 +by (blast_tac (!claset addSEs spies_partsEs) 2);
   4.274  (*Fake*)
   4.275  by (REPEAT_FIRST (resolve_tac [impI, conjI]));
   4.276  by (Blast_tac 1);
   4.277 @@ -300,7 +300,7 @@
   4.278  (*NS3*)
   4.279  by (Step_tac 1);
   4.280  by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
   4.281 -by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   4.282 +by (blast_tac (!claset addSDs [Says_imp_spies' RS parts.Inj]
   4.283                         addDs  [unique_NB]) 1);
   4.284  qed "B_trusts_protocol";
   4.285  
     5.1 --- a/src/HOL/Auth/NS_Public.thy	Wed Sep 17 16:40:52 1997 +0200
     5.2 +++ b/src/HOL/Auth/NS_Public.thy	Thu Sep 18 13:24:04 1997 +0200
     5.3 @@ -20,7 +20,7 @@
     5.4             invent new nonces here, but he can also use NS1.  Common to
     5.5             all similar protocols.*)
     5.6      Fake "[| evs: ns_public;  B ~= Spy;  
     5.7 -             X: synth (analz (sees Spy evs)) |]
     5.8 +             X: synth (analz (spies evs)) |]
     5.9            ==> Says Spy B X  # evs : ns_public"
    5.10  
    5.11           (*Alice initiates a protocol run, sending a nonce to Bob*)
     6.1 --- a/src/HOL/Auth/NS_Public_Bad.ML	Wed Sep 17 16:40:52 1997 +0200
     6.2 +++ b/src/HOL/Auth/NS_Public_Bad.ML	Thu Sep 18 13:24:04 1997 +0200
     6.3 @@ -16,7 +16,7 @@
     6.4  proof_timing:=true;
     6.5  HOL_quantifiers := false;
     6.6  
     6.7 -AddIffs [Spy_in_lost];
     6.8 +AddIffs [Spy_in_bad];
     6.9  
    6.10  (*A "possibility property": there are traces that reach the end*)
    6.11  goal thy 
    6.12 @@ -40,8 +40,8 @@
    6.13  
    6.14  
    6.15  (*Induction for regularity theorems.  If induction formula has the form
    6.16 -   X ~: analz (sees Spy evs) --> ... then it shortens the proof by discarding
    6.17 -   needless information about analz (insert X (sees Spy evs))  *)
    6.18 +   X ~: analz (spies evs) --> ... then it shortens the proof by discarding
    6.19 +   needless information about analz (insert X (spies evs))  *)
    6.20  fun parts_induct_tac i = 
    6.21      etac ns_public.induct i
    6.22      THEN 
    6.23 @@ -50,25 +50,25 @@
    6.24      prove_simple_subgoals_tac i;
    6.25  
    6.26  
    6.27 -(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
    6.28 +(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
    6.29      sends messages containing X! **)
    6.30  
    6.31 -(*Spy never sees another agent's private key! (unless it's lost at start)*)
    6.32 +(*Spy never sees another agent's private key! (unless it's bad at start)*)
    6.33  goal thy 
    6.34 - "!!A. evs: ns_public ==> (Key (priK A) : parts (sees Spy evs)) = (A : lost)";
    6.35 + "!!A. evs: ns_public ==> (Key (priK A) : parts (spies evs)) = (A : bad)";
    6.36  by (parts_induct_tac 1);
    6.37  by (Fake_parts_insert_tac 1);
    6.38  qed "Spy_see_priK";
    6.39  Addsimps [Spy_see_priK];
    6.40  
    6.41  goal thy 
    6.42 - "!!A. evs: ns_public ==> (Key (priK A) : analz (sees Spy evs)) = (A : lost)";
    6.43 + "!!A. evs: ns_public ==> (Key (priK A) : analz (spies evs)) = (A : bad)";
    6.44  by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
    6.45  qed "Spy_analz_priK";
    6.46  Addsimps [Spy_analz_priK];
    6.47  
    6.48 -goal thy  "!!A. [| Key (priK A) : parts (sees Spy evs);       \
    6.49 -\                  evs : ns_public |] ==> A:lost";
    6.50 +goal thy  "!!A. [| Key (priK A) : parts (spies evs);       \
    6.51 +\                  evs : ns_public |] ==> A:bad";
    6.52  by (blast_tac (!claset addDs [Spy_see_priK]) 1);
    6.53  qed "Spy_see_priK_D";
    6.54  
    6.55 @@ -81,9 +81,9 @@
    6.56  (*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce
    6.57    is secret.  (Honest users generate fresh nonces.)*)
    6.58  goal thy 
    6.59 - "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees Spy evs); \
    6.60 -\           Nonce NA ~: analz (sees Spy evs);   evs : ns_public |]       \
    6.61 -\ ==> Crypt (pubK C) {|NA', Nonce NA|} ~: parts (sees Spy evs)";
    6.62 + "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \
    6.63 +\           Nonce NA ~: analz (spies evs);   evs : ns_public |]       \
    6.64 +\ ==> Crypt (pubK C) {|NA', Nonce NA|} ~: parts (spies evs)";
    6.65  by (etac rev_mp 1);
    6.66  by (etac rev_mp 1);
    6.67  by (parts_induct_tac 1);
    6.68 @@ -97,14 +97,14 @@
    6.69  
    6.70  (*Unicity for NS1: nonce NA identifies agents A and B*)
    6.71  goal thy 
    6.72 - "!!evs. [| Nonce NA ~: analz (sees Spy evs);  evs : ns_public |]      \
    6.73 + "!!evs. [| Nonce NA ~: analz (spies evs);  evs : ns_public |]      \
    6.74  \ ==> EX A' B'. ALL A B.                                               \
    6.75 -\      Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees Spy evs) --> \
    6.76 +\      Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs) --> \
    6.77  \      A=A' & B=B'";
    6.78  by (etac rev_mp 1);
    6.79  by (parts_induct_tac 1);
    6.80  by (ALLGOALS
    6.81 -    (asm_simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees])));
    6.82 +    (asm_simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_spies])));
    6.83  (*NS1*)
    6.84  by (expand_case_tac "NA = ?y" 2 THEN blast_tac (!claset addSEs partsEs) 2);
    6.85  (*Fake*)
    6.86 @@ -114,9 +114,9 @@
    6.87  val lemma = result();
    6.88  
    6.89  goal thy 
    6.90 - "!!evs. [| Crypt(pubK B)  {|Nonce NA, Agent A|}  : parts(sees Spy evs); \
    6.91 -\           Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(sees Spy evs); \
    6.92 -\           Nonce NA ~: analz (sees Spy evs);                            \
    6.93 + "!!evs. [| Crypt(pubK B)  {|Nonce NA, Agent A|}  : parts(spies evs); \
    6.94 +\           Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(spies evs); \
    6.95 +\           Nonce NA ~: analz (spies evs);                            \
    6.96  \           evs : ns_public |]                                           \
    6.97  \        ==> A=A' & B=B'";
    6.98  by (prove_unique_tac lemma 1);
    6.99 @@ -133,19 +133,19 @@
   6.100  (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
   6.101  goal thy 
   6.102   "!!evs. [| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs;     \
   6.103 -\           A ~: lost;  B ~: lost;  evs : ns_public |]                    \
   6.104 -\        ==>  Nonce NA ~: analz (sees Spy evs)";
   6.105 +\           A ~: bad;  B ~: bad;  evs : ns_public |]                    \
   6.106 +\        ==>  Nonce NA ~: analz (spies evs)";
   6.107  by (etac rev_mp 1);
   6.108  by (analz_induct_tac 1);
   6.109  (*NS3*)
   6.110 -by (blast_tac (!claset addDs  [Says_imp_sees_Spy RS parts.Inj]
   6.111 +by (blast_tac (!claset addDs  [Says_imp_spies RS parts.Inj]
   6.112                         addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4);
   6.113  (*NS2*)
   6.114  by (blast_tac (!claset addSEs [MPair_parts]
   6.115 -		       addDs  [Says_imp_sees_Spy RS parts.Inj,
   6.116 +		       addDs  [Says_imp_spies RS parts.Inj,
   6.117  			       parts.Body, unique_NA]) 3);
   6.118  (*NS1*)
   6.119 -by (blast_tac (!claset addSEs sees_Spy_partsEs
   6.120 +by (blast_tac (!claset addSEs spies_partsEs
   6.121                         addIs  [impOfSubs analz_subset_parts]) 2);
   6.122  (*Fake*)
   6.123  by (spy_analz_tac 1);
   6.124 @@ -157,29 +157,29 @@
   6.125  goal thy 
   6.126   "!!evs. [| Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs;  \
   6.127  \           Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set evs;  \
   6.128 -\           A ~: lost;  B ~: lost;  evs : ns_public |]                  \
   6.129 +\           A ~: bad;  B ~: bad;  evs : ns_public |]                  \
   6.130  \        ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set evs";
   6.131  by (etac rev_mp 1);
   6.132  (*prepare induction over Crypt (pubK A) {|NA,NB|} : parts H*)
   6.133 -by (etac (Says_imp_sees_Spy RS parts.Inj RS rev_mp) 1);
   6.134 +by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1);
   6.135  by (etac ns_public.induct 1);
   6.136  by (ALLGOALS Asm_simp_tac);
   6.137  (*NS1*)
   6.138 -by (blast_tac (!claset addSEs sees_Spy_partsEs) 2);
   6.139 +by (blast_tac (!claset addSEs spies_partsEs) 2);
   6.140  (*Fake*)
   6.141  by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert]
   6.142                         addDs  [Spy_not_see_NA, 
   6.143  			       impOfSubs analz_subset_parts]) 1);
   6.144  (*NS2; not clear why blast_tac needs to be preceeded by Step_tac*)
   6.145  by (Step_tac 1);
   6.146 -by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj,
   6.147 +by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj,
   6.148  			      Spy_not_see_NA, unique_NA]) 1);
   6.149  qed "A_trusts_NS2";
   6.150  
   6.151  (*If the encrypted message appears then it originated with Alice in NS1*)
   6.152  goal thy 
   6.153 - "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees Spy evs); \
   6.154 -\           Nonce NA ~: analz (sees Spy evs);                            \
   6.155 + "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \
   6.156 +\           Nonce NA ~: analz (spies evs);                            \
   6.157  \           evs : ns_public |]                                           \
   6.158  \   ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs";
   6.159  by (etac rev_mp 1);
   6.160 @@ -195,14 +195,14 @@
   6.161  (*Unicity for NS2: nonce NB identifies agent A and nonce NA
   6.162    [proof closely follows that for unique_NA] *)
   6.163  goal thy 
   6.164 - "!!evs. [| Nonce NB ~: analz (sees Spy evs);  evs : ns_public |]  \
   6.165 + "!!evs. [| Nonce NB ~: analz (spies evs);  evs : ns_public |]  \
   6.166  \ ==> EX A' NA'. ALL A NA.                                         \
   6.167  \      Crypt (pubK A) {|Nonce NA, Nonce NB|}                       \
   6.168 -\        : parts (sees Spy evs)  -->  A=A' & NA=NA'";
   6.169 +\        : parts (spies evs)  -->  A=A' & NA=NA'";
   6.170  by (etac rev_mp 1);
   6.171  by (parts_induct_tac 1);
   6.172  by (ALLGOALS
   6.173 -    (asm_simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees])));
   6.174 +    (asm_simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_spies])));
   6.175  (*NS2*)
   6.176  by (expand_case_tac "NB = ?y" 2 THEN blast_tac (!claset addSEs partsEs) 2);
   6.177  (*Fake*)
   6.178 @@ -212,9 +212,9 @@
   6.179  val lemma = result();
   6.180  
   6.181  goal thy 
   6.182 - "!!evs. [| Crypt(pubK A) {|Nonce NA, Nonce NB|}  : parts(sees Spy evs); \
   6.183 -\           Crypt(pubK A'){|Nonce NA', Nonce NB|} : parts(sees Spy evs); \
   6.184 -\           Nonce NB ~: analz (sees Spy evs);                            \
   6.185 + "!!evs. [| Crypt(pubK A) {|Nonce NA, Nonce NB|}  : parts(spies evs); \
   6.186 +\           Crypt(pubK A'){|Nonce NA', Nonce NB|} : parts(spies evs); \
   6.187 +\           Nonce NB ~: analz (spies evs);                            \
   6.188  \           evs : ns_public |]                                           \
   6.189  \        ==> A=A' & NA=NA'";
   6.190  by (prove_unique_tac lemma 1);
   6.191 @@ -225,13 +225,13 @@
   6.192  goal thy 
   6.193   "!!evs.[| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs;  \
   6.194  \          (ALL C. Says A C (Crypt (pubK C) (Nonce NB)) ~: set evs);    \
   6.195 -\          A ~: lost;  B ~: lost;  evs : ns_public |]                   \
   6.196 -\       ==> Nonce NB ~: analz (sees Spy evs)";
   6.197 +\          A ~: bad;  B ~: bad;  evs : ns_public |]                   \
   6.198 +\       ==> Nonce NB ~: analz (spies evs)";
   6.199  by (etac rev_mp 1);
   6.200  by (etac rev_mp 1);
   6.201  by (analz_induct_tac 1);
   6.202  (*NS1*)
   6.203 -by (blast_tac (!claset addSEs sees_Spy_partsEs) 2);
   6.204 +by (blast_tac (!claset addSEs spies_partsEs) 2);
   6.205  (*Fake*)
   6.206  by (spy_analz_tac 1);
   6.207  (*NS2 and NS3*)
   6.208 @@ -239,10 +239,10 @@
   6.209  by (step_tac (!claset delrules [allI]) 1);
   6.210  by (Blast_tac 5);
   6.211  (*NS3*)
   6.212 -by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj, unique_NB]) 4);
   6.213 +by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj, unique_NB]) 4);
   6.214  (*NS2*)
   6.215 -by (blast_tac (!claset addSEs sees_Spy_partsEs) 3);
   6.216 -by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
   6.217 +by (blast_tac (!claset addSEs spies_partsEs) 3);
   6.218 +by (blast_tac (!claset addSDs [Says_imp_spies RS parts.Inj]
   6.219                         addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 2);
   6.220  by (blast_tac (!claset addSIs [impOfSubs analz_subset_parts]) 1);
   6.221  qed "Spy_not_see_NB";
   6.222 @@ -254,35 +254,35 @@
   6.223  goal thy 
   6.224   "!!evs. [| Says B A  (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs; \
   6.225  \           Says A' B (Crypt (pubK B) (Nonce NB)): set evs;              \
   6.226 -\           A ~: lost;  B ~: lost;  evs : ns_public |]                   \
   6.227 +\           A ~: bad;  B ~: bad;  evs : ns_public |]                   \
   6.228  \        ==> EX C. Says A C (Crypt (pubK C) (Nonce NB)) : set evs";
   6.229  by (etac rev_mp 1);
   6.230  (*prepare induction over Crypt (pubK B) NB : parts H*)
   6.231 -by (etac (Says_imp_sees_Spy RS parts.Inj RS rev_mp) 1);
   6.232 +by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1);
   6.233  by (parts_induct_tac 1);
   6.234  by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
   6.235  (*NS1*)
   6.236 -by (blast_tac (!claset addSEs sees_Spy_partsEs) 2);
   6.237 +by (blast_tac (!claset addSEs spies_partsEs) 2);
   6.238  (*Fake*)
   6.239  by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert]
   6.240                         addDs  [Spy_not_see_NB, 
   6.241  			       impOfSubs analz_subset_parts]) 1);
   6.242  (*NS3; not clear why blast_tac needs to be preceeded by Step_tac*)
   6.243  by (Step_tac 1);
   6.244 -by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj,
   6.245 +by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj,
   6.246  			      Spy_not_see_NB, unique_NB]) 1);
   6.247  qed "B_trusts_NS3";
   6.248  
   6.249  
   6.250  (*Can we strengthen the secrecy theorem?  NO*)
   6.251  goal thy 
   6.252 - "!!evs. [| A ~: lost;  B ~: lost;  evs : ns_public |]           \
   6.253 + "!!evs. [| A ~: bad;  B ~: bad;  evs : ns_public |]           \
   6.254  \ ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs \
   6.255 -\     --> Nonce NB ~: analz (sees Spy evs)";
   6.256 +\     --> Nonce NB ~: analz (spies evs)";
   6.257  by (analz_induct_tac 1);
   6.258  (*NS1*)
   6.259  by (blast_tac (!claset addSEs partsEs
   6.260 -                       addSDs [Says_imp_sees_Spy RS parts.Inj]) 2);
   6.261 +                       addSDs [Says_imp_spies RS parts.Inj]) 2);
   6.262  (*Fake*)
   6.263  by (spy_analz_tac 1);
   6.264  (*NS2 and NS3*)
   6.265 @@ -290,27 +290,27 @@
   6.266  by (blast_tac (!claset addSIs [impOfSubs analz_subset_parts, usedI]) 1);
   6.267  (*NS2*)
   6.268  by (blast_tac (!claset addSEs partsEs
   6.269 -                       addSDs [Says_imp_sees_Spy RS parts.Inj]) 2);
   6.270 -by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
   6.271 +                       addSDs [Says_imp_spies RS parts.Inj]) 2);
   6.272 +by (blast_tac (!claset addSDs [Says_imp_spies RS parts.Inj]
   6.273                         addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 1);
   6.274  (*NS3*)
   6.275 -by (forw_inst_tac [("A'","A")] (Says_imp_sees_Spy RS parts.Inj RS unique_NB) 1
   6.276 -    THEN REPEAT (eresolve_tac [asm_rl, Says_imp_sees_Spy RS parts.Inj] 1));
   6.277 +by (forw_inst_tac [("A'","A")] (Says_imp_spies RS parts.Inj RS unique_NB) 1
   6.278 +    THEN REPEAT (eresolve_tac [asm_rl, Says_imp_spies RS parts.Inj] 1));
   6.279  by (Step_tac 1);
   6.280  
   6.281  (*
   6.282  THIS IS THE ATTACK!
   6.283  Level 9
   6.284 -!!evs. [| A ~: lost; B ~: lost; evs : ns_public |]
   6.285 +!!evs. [| A ~: bad; B ~: bad; evs : ns_public |]
   6.286         ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|})
   6.287             : set evs -->
   6.288 -           Nonce NB ~: analz (sees Spy evs)
   6.289 +           Nonce NB ~: analz (spies evs)
   6.290   1. !!evs Aa Ba B' NAa NBa evsa.
   6.291 -       [| A ~: lost; B ~: lost; evsa : ns_public; A ~= Ba;
   6.292 +       [| A ~: bad; B ~: bad; evsa : ns_public; A ~= Ba;
   6.293            Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evsa;
   6.294            Says A Ba (Crypt (pubK Ba) {|Nonce NA, Agent A|}) : set evsa;
   6.295 -          Ba : lost;
   6.296 +          Ba : bad;
   6.297            Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evsa;
   6.298 -          Nonce NB ~: analz (sees Spy evsa) |]
   6.299 +          Nonce NB ~: analz (spies evsa) |]
   6.300         ==> False
   6.301  *)
     7.1 --- a/src/HOL/Auth/NS_Public_Bad.thy	Wed Sep 17 16:40:52 1997 +0200
     7.2 +++ b/src/HOL/Auth/NS_Public_Bad.thy	Thu Sep 18 13:24:04 1997 +0200
     7.3 @@ -24,7 +24,7 @@
     7.4             invent new nonces here, but he can also use NS1.  Common to
     7.5             all similar protocols.*)
     7.6      Fake "[| evs: ns_public;  B ~= Spy;  
     7.7 -             X: synth (analz (sees Spy evs)) |]
     7.8 +             X: synth (analz (spies evs)) |]
     7.9            ==> Says Spy B X  # evs : ns_public"
    7.10  
    7.11           (*Alice initiates a protocol run, sending a nonce to Bob*)
     8.1 --- a/src/HOL/Auth/NS_Shared.ML	Wed Sep 17 16:40:52 1997 +0200
     8.2 +++ b/src/HOL/Auth/NS_Shared.ML	Thu Sep 18 13:24:04 1997 +0200
     8.3 @@ -48,31 +48,30 @@
     8.4  
     8.5  (*For reasoning about the encrypted portion of message NS3*)
     8.6  goal thy "!!evs. Says S A (Crypt KA {|N, B, K, X|}) : set evs \
     8.7 -\                ==> X : parts (sees Spy evs)";
     8.8 -by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
     8.9 -qed "NS3_msg_in_parts_sees_Spy";
    8.10 +\                ==> X : parts (spies evs)";
    8.11 +by (blast_tac (!claset addSEs spies_partsEs) 1);
    8.12 +qed "NS3_msg_in_parts_spies";
    8.13                                
    8.14  goal thy
    8.15      "!!evs. Says Server A (Crypt (shrK A) {|NA, B, K, X|}) : set evs \
    8.16 -\           ==> K : parts (sees Spy evs)";
    8.17 -by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
    8.18 -qed "Oops_parts_sees_Spy";
    8.19 +\           ==> K : parts (spies evs)";
    8.20 +by (blast_tac (!claset addSEs spies_partsEs) 1);
    8.21 +qed "Oops_parts_spies";
    8.22  
    8.23 -(*For proving the easier theorems about X ~: parts (sees Spy evs).*)
    8.24 +(*For proving the easier theorems about X ~: parts (spies evs).*)
    8.25  fun parts_induct_tac i = 
    8.26      etac ns_shared.induct i  THEN 
    8.27 -    forward_tac [Oops_parts_sees_Spy] (i+7)  THEN
    8.28 -    dtac NS3_msg_in_parts_sees_Spy (i+4)     THEN
    8.29 +    forward_tac [Oops_parts_spies] (i+7)  THEN
    8.30 +    dtac NS3_msg_in_parts_spies (i+4)     THEN
    8.31      prove_simple_subgoals_tac i;
    8.32  
    8.33  
    8.34 -(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
    8.35 +(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
    8.36      sends messages containing X! **)
    8.37  
    8.38 -(*Spy never sees another agent's shared key! (unless it's lost at start)*)
    8.39 +(*Spy never sees another agent's shared key! (unless it's bad at start)*)
    8.40  goal thy 
    8.41 - "!!evs. evs : ns_shared \
    8.42 -\        ==> (Key (shrK A) : parts (sees Spy evs)) = (A : lost)";
    8.43 + "!!evs. evs : ns_shared ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
    8.44  by (parts_induct_tac 1);
    8.45  by (Fake_parts_insert_tac 1);
    8.46  by (Blast_tac 1);
    8.47 @@ -80,14 +79,13 @@
    8.48  Addsimps [Spy_see_shrK];
    8.49  
    8.50  goal thy 
    8.51 - "!!evs. evs : ns_shared \
    8.52 -\        ==> (Key (shrK A) : analz (sees Spy evs)) = (A : lost)";
    8.53 + "!!evs. evs : ns_shared ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
    8.54  by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
    8.55  qed "Spy_analz_shrK";
    8.56  Addsimps [Spy_analz_shrK];
    8.57  
    8.58 -goal thy  "!!A. [| Key (shrK A) : parts (sees Spy evs);       \
    8.59 -\                  evs : ns_shared |] ==> A:lost";
    8.60 +goal thy  "!!A. [| Key (shrK A) : parts (spies evs);       \
    8.61 +\                  evs : ns_shared |] ==> A:bad";
    8.62  by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
    8.63  qed "Spy_see_shrK_D";
    8.64  
    8.65 @@ -97,7 +95,7 @@
    8.66  
    8.67  (*Nobody can have used non-existent keys!*)
    8.68  goal thy "!!evs. evs : ns_shared ==>      \
    8.69 -\         Key K ~: used evs --> K ~: keysFor (parts (sees Spy evs))";
    8.70 +\         Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
    8.71  by (parts_induct_tac 1);
    8.72  (*Fake*)
    8.73  by (best_tac
    8.74 @@ -106,7 +104,7 @@
    8.75                        impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
    8.76                 addss (!simpset)) 1);
    8.77  (*NS2, NS4, NS5*)
    8.78 -by (ALLGOALS (blast_tac (!claset addSEs sees_Spy_partsEs)));
    8.79 +by (ALLGOALS (blast_tac (!claset addSEs spies_partsEs)));
    8.80  qed_spec_mp "new_keys_not_used";
    8.81  
    8.82  bind_thm ("new_keys_not_analzd",
    8.83 @@ -120,8 +118,7 @@
    8.84  
    8.85  (*Describes the form of K, X and K' when the Server sends this message.*)
    8.86  goal thy 
    8.87 - "!!evs. [| Says Server A (Crypt K' {|N, Agent B, Key K, X|}) \
    8.88 -\             : set evs;                                      \
    8.89 + "!!evs. [| Says Server A (Crypt K' {|N, Agent B, Key K, X|}) : set evs; \
    8.90  \           evs : ns_shared |]                           \
    8.91  \        ==> K ~: range shrK &                                \
    8.92  \            X = (Crypt (shrK B) {|Key K, Agent A|}) &        \
    8.93 @@ -134,9 +131,8 @@
    8.94  
    8.95  (*If the encrypted message appears then it originated with the Server*)
    8.96  goal thy
    8.97 - "!!evs. [| Crypt (shrK A) {|NA, Agent B, Key K, X|}                    \
    8.98 -\            : parts (sees Spy evs);                                    \
    8.99 -\           A ~: lost;  evs : ns_shared |]                              \
   8.100 + "!!evs. [| Crypt (shrK A) {|NA, Agent B, Key K, X|} : parts (spies evs); \
   8.101 +\           A ~: bad;  evs : ns_shared |]                              \
   8.102  \         ==> Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})  \
   8.103  \               : set evs";
   8.104  by (etac rev_mp 1);
   8.105 @@ -153,17 +149,17 @@
   8.106  \              : set evs;                                                  \
   8.107  \           evs : ns_shared |]                                             \
   8.108  \        ==> (K ~: range shrK & X = (Crypt (shrK B) {|Key K, Agent A|}))   \
   8.109 -\            | X : analz (sees Spy evs)";
   8.110 -by (case_tac "A : lost" 1);
   8.111 -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
   8.112 +\            | X : analz (spies evs)";
   8.113 +by (case_tac "A : bad" 1);
   8.114 +by (fast_tac (!claset addSDs [Says_imp_spies RS analz.Inj]
   8.115                        addss (!simpset)) 1);
   8.116 -by (forward_tac [Says_imp_sees_Spy RS parts.Inj] 1);
   8.117 +by (forward_tac [Says_imp_spies RS parts.Inj] 1);
   8.118  by (blast_tac (!claset addSDs [A_trusts_NS2, Says_Server_message_form]) 1);
   8.119  qed "Says_S_message_form";
   8.120  
   8.121  
   8.122  (*For proofs involving analz.*)
   8.123 -val analz_sees_tac = 
   8.124 +val analz_spies_tac = 
   8.125      forward_tac [Says_Server_message_form] 8 THEN
   8.126      forward_tac [Says_S_message_form] 5 THEN 
   8.127      REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] ORELSE' hyp_subst_tac);
   8.128 @@ -172,8 +168,8 @@
   8.129  (****
   8.130   The following is to prove theorems of the form
   8.131  
   8.132 -  Key K : analz (insert (Key KAB) (sees Spy evs)) ==>
   8.133 -  Key K : analz (sees Spy evs)
   8.134 +  Key K : analz (insert (Key KAB) (spies evs)) ==>
   8.135 +  Key K : analz (spies evs)
   8.136  
   8.137   A more general formula must be proved inductively.
   8.138  
   8.139 @@ -185,8 +181,8 @@
   8.140    We require that agents should behave like this subsequently also.*)
   8.141  goal thy 
   8.142   "!!evs. [| evs : ns_shared;  Kab ~: range shrK |] ==>  \
   8.143 -\           (Crypt KAB X) : parts (sees Spy evs) &      \
   8.144 -\           Key K : parts {X} --> Key K : parts (sees Spy evs)";
   8.145 +\           (Crypt KAB X) : parts (spies evs) &      \
   8.146 +\           Key K : parts {X} --> Key K : parts (spies evs)";
   8.147  by (parts_induct_tac 1);
   8.148  (*Deals with Faked messages*)
   8.149  by (blast_tac (!claset addSEs partsEs
   8.150 @@ -202,10 +198,10 @@
   8.151  goal thy  
   8.152   "!!evs. evs : ns_shared ==>                                \
   8.153  \  ALL K KK. KK <= Compl (range shrK) -->                        \
   8.154 -\            (Key K : analz (Key``KK Un (sees Spy evs))) =  \
   8.155 -\            (K : KK | Key K : analz (sees Spy evs))";
   8.156 +\            (Key K : analz (Key``KK Un (spies evs))) =  \
   8.157 +\            (K : KK | Key K : analz (spies evs))";
   8.158  by (etac ns_shared.induct 1);
   8.159 -by analz_sees_tac;
   8.160 +by analz_spies_tac;
   8.161  by (REPEAT_FIRST (resolve_tac [allI, impI]));
   8.162  by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
   8.163  (*Takes 24 secs*)
   8.164 @@ -219,8 +215,8 @@
   8.165  
   8.166  goal thy
   8.167   "!!evs. [| evs : ns_shared;  KAB ~: range shrK |] ==>     \
   8.168 -\        Key K : analz (insert (Key KAB) (sees Spy evs)) = \
   8.169 -\        (K = KAB | Key K : analz (sees Spy evs))";
   8.170 +\        Key K : analz (insert (Key KAB) (spies evs)) = \
   8.171 +\        (K = KAB | Key K : analz (spies evs))";
   8.172  by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
   8.173  qed "analz_insert_freshK";
   8.174  
   8.175 @@ -230,8 +226,8 @@
   8.176  goal thy 
   8.177   "!!evs. evs : ns_shared ==>                                        \
   8.178  \      EX A' NA' B' X'. ALL A NA B X.                                    \
   8.179 -\       Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})         \
   8.180 -\       : set evs -->         A=A' & NA=NA' & B=B' & X=X'";
   8.181 +\       Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) : set evs \
   8.182 +\       -->         A=A' & NA=NA' & B=B' & X=X'";
   8.183  by (etac ns_shared.induct 1);
   8.184  by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   8.185  by (Step_tac 1);
   8.186 @@ -242,17 +238,15 @@
   8.187  by (expand_case_tac "K = ?y" 1);
   8.188  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   8.189  by (blast_tac (!claset delrules [conjI]    (*prevent split-up into 4 subgoals*)
   8.190 -                      addSEs sees_Spy_partsEs) 1);
   8.191 +                      addSEs spies_partsEs) 1);
   8.192  val lemma = result();
   8.193  
   8.194  (*In messages of this form, the session key uniquely identifies the rest*)
   8.195  goal thy 
   8.196   "!!evs. [| Says Server A                                    \
   8.197 -\             (Crypt (shrK A) {|NA, Agent B, Key K, X|})     \
   8.198 -\                  : set evs;                                \ 
   8.199 +\             (Crypt (shrK A) {|NA, Agent B, Key K, X|}) : set evs; \ 
   8.200  \           Says Server A'                                   \
   8.201 -\             (Crypt (shrK A') {|NA', Agent B', Key K, X'|}) \
   8.202 -\                  : set evs;                                \
   8.203 +\             (Crypt (shrK A') {|NA', Agent B', Key K, X'|}) : set evs; \
   8.204  \           evs : ns_shared |] ==> A=A' & NA=NA' & B=B' & X = X'";
   8.205  by (prove_unique_tac lemma 1);
   8.206  qed "unique_session_keys";
   8.207 @@ -261,15 +255,15 @@
   8.208  (** Crucial secrecy property: Spy does not see the keys sent in msg NS2 **)
   8.209  
   8.210  goal thy 
   8.211 - "!!evs. [| A ~: lost;  B ~: lost;  evs : ns_shared |]            \
   8.212 + "!!evs. [| A ~: bad;  B ~: bad;  evs : ns_shared |]            \
   8.213  \        ==> Says Server A                                             \
   8.214  \              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
   8.215  \                                Crypt (shrK B) {|Key K, Agent A|}|})  \
   8.216  \             : set evs -->                                            \
   8.217  \        (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs) -->         \
   8.218 -\        Key K ~: analz (sees Spy evs)";
   8.219 +\        Key K ~: analz (spies evs)";
   8.220  by (etac ns_shared.induct 1);
   8.221 -by analz_sees_tac;
   8.222 +by analz_spies_tac;
   8.223  by (ALLGOALS 
   8.224      (asm_simp_tac 
   8.225       (!simpset addsimps ([analz_insert_eq, analz_insert_freshK] @ pushes)
   8.226 @@ -279,16 +273,16 @@
   8.227  (*NS3, replay sub-case*) 
   8.228  by (Blast_tac 4);
   8.229  (*NS2*)
   8.230 -by (blast_tac (!claset addSEs sees_Spy_partsEs
   8.231 +by (blast_tac (!claset addSEs spies_partsEs
   8.232                         addIs [parts_insertI, impOfSubs analz_subset_parts]) 2);
   8.233  (*Fake*) 
   8.234  by (spy_analz_tac 1);
   8.235  (*NS3, Server sub-case*) (**LEVEL 6 **)
   8.236  by (step_tac (!claset delrules [impCE]) 1);
   8.237 -by (forward_tac [Says_imp_sees_Spy RS parts.Inj RS A_trusts_NS2] 1);
   8.238 +by (forward_tac [Says_imp_spies RS parts.Inj RS A_trusts_NS2] 1);
   8.239  by (assume_tac 2);
   8.240 -by (blast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj RS
   8.241 -			      Crypt_Spy_analz_lost]) 1);
   8.242 +by (blast_tac (!claset addDs [Says_imp_spies RS analz.Inj RS
   8.243 +			      Crypt_Spy_analz_bad]) 1);
   8.244  by (blast_tac (!claset addDs [unique_session_keys]) 1);
   8.245  val lemma = result() RS mp RS mp RSN(2,rev_notE);
   8.246  
   8.247 @@ -298,8 +292,8 @@
   8.248   "!!evs. [| Says Server A                                               \
   8.249  \            (Crypt K' {|NA, Agent B, Key K, X|}) : set evs;            \
   8.250  \           (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs);          \
   8.251 -\           A ~: lost;  B ~: lost;  evs : ns_shared                \
   8.252 -\        |] ==> Key K ~: analz (sees Spy evs)";
   8.253 +\           A ~: bad;  B ~: bad;  evs : ns_shared                \
   8.254 +\        |] ==> Key K ~: analz (spies evs)";
   8.255  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   8.256  by (blast_tac (!claset addSDs [lemma]) 1);
   8.257  qed "Spy_not_see_encrypted_key";
   8.258 @@ -312,8 +306,8 @@
   8.259  
   8.260  (*If the encrypted message appears then it originated with the Server*)
   8.261  goal thy
   8.262 - "!!evs. [| Crypt (shrK B) {|Key K, Agent A|} : parts (sees Spy evs); \
   8.263 -\           B ~: lost;  evs : ns_shared |]                        \
   8.264 + "!!evs. [| Crypt (shrK B) {|Key K, Agent A|} : parts (spies evs); \
   8.265 +\           B ~: bad;  evs : ns_shared |]                        \
   8.266  \         ==> EX NA. Says Server A                                     \
   8.267  \              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
   8.268  \                                Crypt (shrK B) {|Key K, Agent A|}|})  \
   8.269 @@ -327,19 +321,19 @@
   8.270  
   8.271  
   8.272  goal thy
   8.273 - "!!evs. [| B ~: lost;  evs : ns_shared |]                        \
   8.274 -\        ==> Key K ~: analz (sees Spy evs) -->                    \
   8.275 + "!!evs. [| B ~: bad;  evs : ns_shared |]                        \
   8.276 +\        ==> Key K ~: analz (spies evs) -->                    \
   8.277  \            Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})  \
   8.278  \            : set evs -->                                             \
   8.279 -\            Crypt K (Nonce NB) : parts (sees Spy evs) -->        \
   8.280 +\            Crypt K (Nonce NB) : parts (spies evs) -->        \
   8.281  \            Says B A (Crypt K (Nonce NB)) : set evs";
   8.282  by (etac ns_shared.induct 1);
   8.283  by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);     
   8.284 -by (dtac NS3_msg_in_parts_sees_Spy 5);
   8.285 -by (forward_tac [Oops_parts_sees_Spy] 8);
   8.286 +by (dtac NS3_msg_in_parts_spies 5);
   8.287 +by (forward_tac [Oops_parts_spies] 8);
   8.288  by (TRYALL (rtac impI));
   8.289  by (REPEAT_FIRST
   8.290 -    (dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD)));
   8.291 +    (dtac (spies_subset_spies_Says RS analz_mono RS contra_subsetD)));
   8.292  by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   8.293  (**LEVEL 7**)
   8.294  by (blast_tac (!claset addSDs [Crypt_Fake_parts_insert]
   8.295 @@ -347,25 +341,25 @@
   8.296  by (Blast_tac 2);
   8.297  by (REPEAT_FIRST (rtac impI ORELSE' etac conjE ORELSE' hyp_subst_tac));
   8.298  (*Subgoal 1: contradiction from the assumptions  
   8.299 -  Key K ~: used evsa  and Crypt K (Nonce NB) : parts (sees Spy evsa) *)
   8.300 +  Key K ~: used evsa  and Crypt K (Nonce NB) : parts (spies evsa) *)
   8.301  by (dtac Crypt_imp_invKey_keysFor 1);
   8.302  (**LEVEL 11**)
   8.303  by (Asm_full_simp_tac 1);
   8.304  by (rtac disjI1 1);
   8.305  by (thin_tac "?PP-->?QQ" 1);
   8.306 -by (case_tac "Ba : lost" 1);
   8.307 -by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj RS B_trusts_NS3, 
   8.308 +by (case_tac "Ba : bad" 1);
   8.309 +by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj RS B_trusts_NS3, 
   8.310  			      unique_session_keys]) 2);
   8.311 -by (blast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj RS
   8.312 -			      Crypt_Spy_analz_lost]) 1);
   8.313 +by (blast_tac (!claset addDs [Says_imp_spies RS analz.Inj RS
   8.314 +			      Crypt_Spy_analz_bad]) 1);
   8.315  val lemma = result();
   8.316  
   8.317  goal thy
   8.318 - "!!evs. [| Crypt K (Nonce NB) : parts (sees Spy evs);           \
   8.319 + "!!evs. [| Crypt K (Nonce NB) : parts (spies evs);           \
   8.320  \           Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})  \
   8.321  \           : set evs;                                                \
   8.322  \           ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs;          \
   8.323 -\           A ~: lost;  B ~: lost;  evs : ns_shared |]           \
   8.324 +\           A ~: bad;  B ~: bad;  evs : ns_shared |]           \
   8.325  \        ==> Says B A (Crypt K (Nonce NB)) : set evs";
   8.326  by (blast_tac (!claset addSIs [lemma RS mp RS mp RS mp]
   8.327                         addSEs [Spy_not_see_encrypted_key RSN (2,rev_notE)]) 1);
     9.1 --- a/src/HOL/Auth/NS_Shared.thy	Wed Sep 17 16:40:52 1997 +0200
     9.2 +++ b/src/HOL/Auth/NS_Shared.thy	Thu Sep 18 13:24:04 1997 +0200
     9.3 @@ -22,7 +22,7 @@
     9.4             invent new nonces here, but he can also use NS1.  Common to
     9.5             all similar protocols.*)
     9.6      Fake "[| evs: ns_shared;  B ~= Spy;  
     9.7 -             X: synth (analz (sees Spy evs)) |]
     9.8 +             X: synth (analz (spies evs)) |]
     9.9            ==> Says Spy B X # evs : ns_shared"
    9.10  
    9.11           (*Alice initiates a protocol run, requesting to talk to any B*)
    10.1 --- a/src/HOL/Auth/OtwayRees.ML	Wed Sep 17 16:40:52 1997 +0200
    10.2 +++ b/src/HOL/Auth/OtwayRees.ML	Thu Sep 18 13:24:04 1997 +0200
    10.3 @@ -44,46 +44,46 @@
    10.4  (** For reasoning about the encrypted portion of messages **)
    10.5  
    10.6  goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set evs \
    10.7 -\                ==> X : analz (sees Spy evs)";
    10.8 -by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    10.9 -qed "OR2_analz_sees_Spy";
   10.10 +\                ==> X : analz (spies evs)";
   10.11 +by (blast_tac (!claset addSDs [Says_imp_spies RS analz.Inj]) 1);
   10.12 +qed "OR2_analz_spies";
   10.13  
   10.14  goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set evs \
   10.15 -\                ==> X : analz (sees Spy evs)";
   10.16 -by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
   10.17 -qed "OR4_analz_sees_Spy";
   10.18 +\                ==> X : analz (spies evs)";
   10.19 +by (blast_tac (!claset addSDs [Says_imp_spies RS analz.Inj]) 1);
   10.20 +qed "OR4_analz_spies";
   10.21  
   10.22  goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \
   10.23 -\                 ==> K : parts (sees Spy evs)";
   10.24 -by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
   10.25 -qed "Oops_parts_sees_Spy";
   10.26 +\                 ==> K : parts (spies evs)";
   10.27 +by (blast_tac (!claset addSEs spies_partsEs) 1);
   10.28 +qed "Oops_parts_spies";
   10.29  
   10.30  (*OR2_analz... and OR4_analz... let us treat those cases using the same 
   10.31    argument as for the Fake case.  This is possible for most, but not all,
   10.32    proofs: Fake does not invent new nonces (as in OR2), and of course Fake
   10.33    messages originate from the Spy. *)
   10.34  
   10.35 -bind_thm ("OR2_parts_sees_Spy",
   10.36 -          OR2_analz_sees_Spy RS (impOfSubs analz_subset_parts));
   10.37 -bind_thm ("OR4_parts_sees_Spy",
   10.38 -          OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
   10.39 +bind_thm ("OR2_parts_spies",
   10.40 +          OR2_analz_spies RS (impOfSubs analz_subset_parts));
   10.41 +bind_thm ("OR4_parts_spies",
   10.42 +          OR4_analz_spies RS (impOfSubs analz_subset_parts));
   10.43  
   10.44 -(*For proving the easier theorems about X ~: parts (sees Spy evs).*)
   10.45 +(*For proving the easier theorems about X ~: parts (spies evs).*)
   10.46  fun parts_induct_tac i = 
   10.47      etac otway.induct i			THEN 
   10.48 -    forward_tac [Oops_parts_sees_Spy] (i+6) THEN
   10.49 -    forward_tac [OR4_parts_sees_Spy]  (i+5) THEN
   10.50 -    forward_tac [OR2_parts_sees_Spy]  (i+3) THEN 
   10.51 +    forward_tac [Oops_parts_spies] (i+6) THEN
   10.52 +    forward_tac [OR4_parts_spies]  (i+5) THEN
   10.53 +    forward_tac [OR2_parts_spies]  (i+3) THEN 
   10.54      prove_simple_subgoals_tac  i;
   10.55  
   10.56  
   10.57 -(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
   10.58 +(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
   10.59      sends messages containing X! **)
   10.60  
   10.61  
   10.62 -(*Spy never sees another agent's shared key! (unless it's lost at start)*)
   10.63 +(*Spy never sees another agent's shared key! (unless it's bad at start)*)
   10.64  goal thy 
   10.65 - "!!evs. evs : otway ==> (Key (shrK A) : parts (sees Spy evs)) = (A : lost)";
   10.66 + "!!evs. evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
   10.67  by (parts_induct_tac 1);
   10.68  by (Fake_parts_insert_tac 1);
   10.69  by (Blast_tac 1);
   10.70 @@ -91,13 +91,12 @@
   10.71  Addsimps [Spy_see_shrK];
   10.72  
   10.73  goal thy 
   10.74 - "!!evs. evs : otway ==> (Key (shrK A) : analz (sees Spy evs)) = (A : lost)";
   10.75 + "!!evs. evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
   10.76  by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
   10.77  qed "Spy_analz_shrK";
   10.78  Addsimps [Spy_analz_shrK];
   10.79  
   10.80 -goal thy  "!!A. [| Key (shrK A) : parts (sees Spy evs);       \
   10.81 -\                  evs : otway |] ==> A:lost";
   10.82 +goal thy  "!!A. [| Key (shrK A) : parts (spies evs); evs : otway |] ==> A:bad";
   10.83  by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
   10.84  qed "Spy_see_shrK_D";
   10.85  
   10.86 @@ -107,7 +106,7 @@
   10.87  
   10.88  (*Nobody can have used non-existent keys!*)
   10.89  goal thy "!!evs. evs : otway ==>          \
   10.90 -\         Key K ~: used evs --> K ~: keysFor (parts (sees Spy evs))";
   10.91 +\         Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
   10.92  by (parts_induct_tac 1);
   10.93  (*Fake*)
   10.94  by (best_tac
   10.95 @@ -142,9 +141,9 @@
   10.96  
   10.97  
   10.98  (*For proofs involving analz.*)
   10.99 -val analz_sees_tac = 
  10.100 -    dtac OR2_analz_sees_Spy 4 THEN 
  10.101 -    dtac OR4_analz_sees_Spy 6 THEN
  10.102 +val analz_spies_tac = 
  10.103 +    dtac OR2_analz_spies 4 THEN 
  10.104 +    dtac OR4_analz_spies 6 THEN
  10.105      forward_tac [Says_Server_message_form] 7 THEN
  10.106      assume_tac 7 THEN
  10.107      REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
  10.108 @@ -153,8 +152,8 @@
  10.109  (****
  10.110   The following is to prove theorems of the form
  10.111  
  10.112 -  Key K : analz (insert (Key KAB) (sees Spy evs)) ==>
  10.113 -  Key K : analz (sees Spy evs)
  10.114 +  Key K : analz (insert (Key KAB) (spies evs)) ==>
  10.115 +  Key K : analz (spies evs)
  10.116  
  10.117   A more general formula must be proved inductively.
  10.118  ****)
  10.119 @@ -166,10 +165,10 @@
  10.120  goal thy  
  10.121   "!!evs. evs : otway ==>                                    \
  10.122  \  ALL K KK. KK <= Compl (range shrK) -->                   \
  10.123 -\            (Key K : analz (Key``KK Un (sees Spy evs))) =  \
  10.124 -\            (K : KK | Key K : analz (sees Spy evs))";
  10.125 +\            (Key K : analz (Key``KK Un (spies evs))) =  \
  10.126 +\            (K : KK | Key K : analz (spies evs))";
  10.127  by (etac otway.induct 1);
  10.128 -by analz_sees_tac;
  10.129 +by analz_spies_tac;
  10.130  by (REPEAT_FIRST (resolve_tac [allI, impI]));
  10.131  by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
  10.132  by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
  10.133 @@ -182,8 +181,8 @@
  10.134  
  10.135  goal thy
  10.136   "!!evs. [| evs : otway;  KAB ~: range shrK |] ==>          \
  10.137 -\        Key K : analz (insert (Key KAB) (sees Spy evs)) =  \
  10.138 -\        (K = KAB | Key K : analz (sees Spy evs))";
  10.139 +\        Key K : analz (insert (Key KAB) (spies evs)) =  \
  10.140 +\        (K = KAB | Key K : analz (spies evs))";
  10.141  by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
  10.142  qed "analz_insert_freshK";
  10.143  
  10.144 @@ -204,7 +203,7 @@
  10.145  by (expand_case_tac "K = ?y" 1);
  10.146  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
  10.147  (*...we assume X is a recent message, and handle this case by contradiction*)
  10.148 -by (blast_tac (!claset addSEs sees_Spy_partsEs
  10.149 +by (blast_tac (!claset addSEs spies_partsEs
  10.150                         delrules [conjI] (*no split-up into 4 subgoals*)) 1);
  10.151  val lemma = result();
  10.152  
  10.153 @@ -221,9 +220,8 @@
  10.154  
  10.155  (*Only OR1 can have caused such a part of a message to appear.*)
  10.156  goal thy 
  10.157 - "!!evs. [| A ~: lost;  evs : otway |]                             \
  10.158 -\        ==> Crypt (shrK A) {|NA, Agent A, Agent B|}               \
  10.159 -\             : parts (sees Spy evs) -->                           \
  10.160 + "!!evs. [| A ~: bad;  evs : otway |]                             \
  10.161 +\        ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) --> \
  10.162  \            Says A B {|NA, Agent A, Agent B,                      \
  10.163  \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \
  10.164  \             : set evs";
  10.165 @@ -235,22 +233,22 @@
  10.166  (** The Nonce NA uniquely identifies A's message. **)
  10.167  
  10.168  goal thy 
  10.169 - "!!evs. [| evs : otway; A ~: lost |]               \
  10.170 + "!!evs. [| evs : otway; A ~: bad |]               \
  10.171  \ ==> EX B'. ALL B.                                 \
  10.172 -\        Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (sees Spy evs) \
  10.173 +\        Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) \
  10.174  \        --> B = B'";
  10.175  by (parts_induct_tac 1);
  10.176  by (Fake_parts_insert_tac 1);
  10.177  by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
  10.178  (*OR1: creation of new Nonce.  Move assertion into global context*)
  10.179  by (expand_case_tac "NA = ?y" 1);
  10.180 -by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
  10.181 +by (blast_tac (!claset addSEs spies_partsEs) 1);
  10.182  val lemma = result();
  10.183  
  10.184  goal thy 
  10.185 - "!!evs.[| Crypt (shrK A) {|NA, Agent A, Agent B|}: parts (sees Spy evs); \
  10.186 -\          Crypt (shrK A) {|NA, Agent A, Agent C|}: parts (sees Spy evs); \
  10.187 -\          evs : otway;  A ~: lost |]                                     \
  10.188 + "!!evs.[| Crypt (shrK A) {|NA, Agent A, Agent B|}: parts (spies evs); \
  10.189 +\          Crypt (shrK A) {|NA, Agent A, Agent C|}: parts (spies evs); \
  10.190 +\          evs : otway;  A ~: bad |]                                   \
  10.191  \        ==> B = C";
  10.192  by (prove_unique_tac lemma 1);
  10.193  qed "unique_NA";
  10.194 @@ -260,14 +258,13 @@
  10.195    OR2 encrypts Nonce NB.  It prevents the attack that can occur in the
  10.196    over-simplified version of this protocol: see OtwayRees_Bad.*)
  10.197  goal thy 
  10.198 - "!!evs. [| A ~: lost;  evs : otway |]                      \
  10.199 -\        ==> Crypt (shrK A) {|NA, Agent A, Agent B|}        \
  10.200 -\             : parts (sees Spy evs) -->                    \
  10.201 + "!!evs. [| A ~: bad;  evs : otway |]                      \
  10.202 +\        ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) --> \
  10.203  \            Crypt (shrK A) {|NA', NA, Agent A', Agent A|}  \
  10.204 -\             ~: parts (sees Spy evs)";
  10.205 +\             ~: parts (spies evs)";
  10.206  by (parts_induct_tac 1);
  10.207  by (Fake_parts_insert_tac 1);
  10.208 -by (REPEAT (blast_tac (!claset addSEs sees_Spy_partsEs
  10.209 +by (REPEAT (blast_tac (!claset addSEs spies_partsEs
  10.210                                 addSDs  [impOfSubs parts_insert_subset_Un]) 1));
  10.211  qed_spec_mp"no_nonce_OR1_OR2";
  10.212  
  10.213 @@ -275,8 +272,8 @@
  10.214  (*Crucial property: If the encrypted message appears, and A has used NA
  10.215    to start a run, then it originated with the Server!*)
  10.216  goal thy 
  10.217 - "!!evs. [| A ~: lost;  A ~= Spy;  evs : otway |]                      \
  10.218 -\    ==> Crypt (shrK A) {|NA, Key K|} : parts (sees Spy evs)           \
  10.219 + "!!evs. [| A ~: bad;  A ~= Spy;  evs : otway |]                      \
  10.220 +\    ==> Crypt (shrK A) {|NA, Key K|} : parts (spies evs)              \
  10.221  \        --> Says A B {|NA, Agent A, Agent B,                          \
  10.222  \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}      \
  10.223  \             : set evs -->                                            \
  10.224 @@ -288,21 +285,21 @@
  10.225  by (parts_induct_tac 1);
  10.226  by (Fake_parts_insert_tac 1);
  10.227  (*OR1: it cannot be a new Nonce, contradiction.*)
  10.228 -by (blast_tac (!claset addSIs [parts_insertI] addSEs sees_Spy_partsEs) 1);
  10.229 +by (blast_tac (!claset addSIs [parts_insertI] addSEs spies_partsEs) 1);
  10.230  (*OR3 and OR4*) 
  10.231  (*OR4*)
  10.232  by (REPEAT (Safe_step_tac 2));
  10.233  by (REPEAT (blast_tac (!claset addSDs [parts_cut]) 3));
  10.234  by (blast_tac (!claset addSIs [Crypt_imp_OR1]
  10.235 -                       addEs  sees_Spy_partsEs) 2);
  10.236 +                       addEs  spies_partsEs) 2);
  10.237  (*OR3*)  (** LEVEL 5 **)
  10.238  by (asm_simp_tac (!simpset addsimps [ex_disj_distrib]) 1);
  10.239  by (step_tac (!claset delrules [disjCI, impCE]) 1);
  10.240  by (blast_tac (!claset addSEs [MPair_parts]
  10.241 -                      addSDs [Says_imp_sees_Spy RS parts.Inj]
  10.242 +                      addSDs [Says_imp_spies RS parts.Inj]
  10.243                        addEs  [no_nonce_OR1_OR2 RSN (2, rev_notE)]
  10.244                        delrules [conjI] (*stop split-up into 4 subgoals*)) 2);
  10.245 -by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
  10.246 +by (blast_tac (!claset addSDs [Says_imp_spies RS parts.Inj]
  10.247                        addSEs [MPair_parts]
  10.248                        addIs  [unique_NA]) 1);
  10.249  qed_spec_mp "NA_Crypt_imp_Server_msg";
  10.250 @@ -313,19 +310,17 @@
  10.251    bad form of this protocol, even though we can prove
  10.252    Spy_not_see_encrypted_key*)
  10.253  goal thy 
  10.254 - "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|}         \
  10.255 -\            : set evs;                                            \
  10.256 -\           Says A B {|NA, Agent A, Agent B,                       \
  10.257 -\                      Crypt (shrK A) {|NA, Agent A, Agent B|}|}   \
  10.258 -\            : set evs;                                            \
  10.259 -\           A ~: lost;  A ~= Spy;  evs : otway |]                  \
  10.260 + "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \
  10.261 +\           Says A  B {|NA, Agent A, Agent B,                       \
  10.262 +\                       Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
  10.263 +\           A ~: bad;  A ~= Spy;  evs : otway |]                  \
  10.264  \        ==> EX NB. Says Server B                                  \
  10.265  \                     {|NA,                                        \
  10.266  \                       Crypt (shrK A) {|NA, Key K|},              \
  10.267  \                       Crypt (shrK B) {|NB, Key K|}|}             \
  10.268  \                       : set evs";
  10.269  by (blast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
  10.270 -                       addEs  sees_Spy_partsEs) 1);
  10.271 +                       addEs  spies_partsEs) 1);
  10.272  qed "A_trusts_OR4";
  10.273  
  10.274  
  10.275 @@ -334,14 +329,14 @@
  10.276      the premises, e.g. by having A=Spy **)
  10.277  
  10.278  goal thy 
  10.279 - "!!evs. [| A ~: lost;  B ~: lost;  evs : otway |]                    \
  10.280 + "!!evs. [| A ~: bad;  B ~: bad;  evs : otway |]                    \
  10.281  \        ==> Says Server B                                            \
  10.282  \              {|NA, Crypt (shrK A) {|NA, Key K|},                    \
  10.283  \                Crypt (shrK B) {|NB, Key K|}|} : set evs -->         \
  10.284  \            Says B Spy {|NA, NB, Key K|} ~: set evs -->              \
  10.285 -\            Key K ~: analz (sees Spy evs)";
  10.286 +\            Key K ~: analz (spies evs)";
  10.287  by (etac otway.induct 1);
  10.288 -by analz_sees_tac;
  10.289 +by analz_spies_tac;
  10.290  by (ALLGOALS
  10.291      (asm_simp_tac (!simpset addcongs [conj_cong] 
  10.292                              addsimps [analz_insert_eq, analz_insert_freshK]
  10.293 @@ -351,7 +346,7 @@
  10.294  (*OR4*) 
  10.295  by (Blast_tac 3);
  10.296  (*OR3*)
  10.297 -by (blast_tac (!claset addSEs sees_Spy_partsEs
  10.298 +by (blast_tac (!claset addSEs spies_partsEs
  10.299                         addIs [impOfSubs analz_subset_parts]) 2);
  10.300  (*Fake*) 
  10.301  by (spy_analz_tac 1);
  10.302 @@ -362,8 +357,8 @@
  10.303  \            {|NA, Crypt (shrK A) {|NA, Key K|},                    \
  10.304  \                  Crypt (shrK B) {|NB, Key K|}|} : set evs;        \
  10.305  \           Says B Spy {|NA, NB, Key K|} ~: set evs;                \
  10.306 -\           A ~: lost;  B ~: lost;  evs : otway |]                  \
  10.307 -\        ==> Key K ~: analz (sees Spy evs)";
  10.308 +\           A ~: bad;  B ~: bad;  evs : otway |]                  \
  10.309 +\        ==> Key K ~: analz (spies evs)";
  10.310  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
  10.311  by (blast_tac (!claset addSEs [lemma]) 1);
  10.312  qed "Spy_not_see_encrypted_key";
  10.313 @@ -374,9 +369,9 @@
  10.314  (*Only OR2 can have caused such a part of a message to appear.  We do not
  10.315    know anything about X: it does NOT have to have the right form.*)
  10.316  goal thy 
  10.317 - "!!evs. [| B ~: lost;  evs : otway |]                         \
  10.318 + "!!evs. [| B ~: bad;  evs : otway |]                         \
  10.319  \        ==> Crypt (shrK B) {|NA, NB, Agent A, Agent B|}       \
  10.320 -\             : parts (sees Spy evs) -->                       \
  10.321 +\             : parts (spies evs) -->                       \
  10.322  \            (EX X. Says B Server                              \
  10.323  \             {|NA, Agent A, Agent B, X,                       \
  10.324  \               Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}  \
  10.325 @@ -390,24 +385,22 @@
  10.326  (** The Nonce NB uniquely identifies B's  message. **)
  10.327  
  10.328  goal thy 
  10.329 - "!!evs. [| evs : otway; B ~: lost |]                    \
  10.330 + "!!evs. [| evs : otway; B ~: bad |]                    \
  10.331  \ ==> EX NA' A'. ALL NA A.                               \
  10.332 -\      Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(sees Spy evs) \
  10.333 +\      Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(spies evs) \
  10.334  \      --> NA = NA' & A = A'";
  10.335  by (parts_induct_tac 1);
  10.336  by (Fake_parts_insert_tac 1);
  10.337  by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
  10.338  (*OR2: creation of new Nonce.  Move assertion into global context*)
  10.339  by (expand_case_tac "NB = ?y" 1);
  10.340 -by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
  10.341 +by (blast_tac (!claset addSEs spies_partsEs) 1);
  10.342  val lemma = result();
  10.343  
  10.344  goal thy 
  10.345 - "!!evs.[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \
  10.346 -\                  : parts(sees Spy evs);         \
  10.347 -\          Crypt (shrK B) {|NC, NB, Agent C, Agent B|} \
  10.348 -\                  : parts(sees Spy evs);         \
  10.349 -\          evs : otway;  B ~: lost |]             \
  10.350 + "!!evs.[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(spies evs); \
  10.351 +\          Crypt (shrK B) {|NC, NB, Agent C, Agent B|} : parts(spies evs); \
  10.352 +\          evs : otway;  B ~: bad |]             \
  10.353  \        ==> NC = NA & C = A";
  10.354  by (prove_unique_tac lemma 1);
  10.355  qed "unique_NB";
  10.356 @@ -416,8 +409,8 @@
  10.357  (*If the encrypted message appears, and B has used Nonce NB,
  10.358    then it originated with the Server!*)
  10.359  goal thy 
  10.360 - "!!evs. [| B ~: lost;  B ~= Spy;  evs : otway |]                        \
  10.361 -\    ==> Crypt (shrK B) {|NB, Key K|} : parts (sees Spy evs)             \
  10.362 + "!!evs. [| B ~: bad;  B ~= Spy;  evs : otway |]                        \
  10.363 +\    ==> Crypt (shrK B) {|NB, Key K|} : parts (spies evs)             \
  10.364  \        --> (ALL X'. Says B Server                                      \
  10.365  \                       {|NA, Agent A, Agent B, X',                      \
  10.366  \                         Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}  \
  10.367 @@ -429,17 +422,17 @@
  10.368  by (parts_induct_tac 1);
  10.369  by (Fake_parts_insert_tac 1);
  10.370  (*OR1: it cannot be a new Nonce, contradiction.*)
  10.371 -by (blast_tac (!claset addSIs [parts_insertI] addSEs sees_Spy_partsEs) 1);
  10.372 +by (blast_tac (!claset addSIs [parts_insertI] addSEs spies_partsEs) 1);
  10.373  (*OR4*)
  10.374  by (blast_tac (!claset addSEs [MPair_parts, Crypt_imp_OR2]) 2);
  10.375  (*OR3*)
  10.376  by (step_tac (!claset delrules [disjCI, impCE]) 1);
  10.377  by (blast_tac (!claset delrules [conjI] (*stop split-up*)) 3); 
  10.378 -by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
  10.379 +by (blast_tac (!claset addSDs [Says_imp_spies RS parts.Inj]
  10.380                         addSEs [MPair_parts]
  10.381                         addDs  [unique_NB]) 2);
  10.382  by (blast_tac (!claset addSEs [MPair_parts, no_nonce_OR1_OR2 RSN (2, rev_notE)]
  10.383 -                       addSDs [Says_imp_sees_Spy RS parts.Inj]
  10.384 +                       addSDs [Says_imp_spies RS parts.Inj]
  10.385                         delrules [conjI, impCE] (*stop split-up*)) 1);
  10.386  qed_spec_mp "NB_Crypt_imp_Server_msg";
  10.387  
  10.388 @@ -447,9 +440,8 @@
  10.389  (*Guarantee for B: if it gets a message with matching NB then the Server
  10.390    has sent the correct message.*)
  10.391  goal thy 
  10.392 - "!!evs. [| B ~: lost;  B ~= Spy;  evs : otway;                    \
  10.393 -\           Says S' B {|NA, X, Crypt (shrK B) {|NB, Key K|}|}      \
  10.394 -\            : set evs;                                            \
  10.395 + "!!evs. [| B ~: bad;  B ~= Spy;  evs : otway;                    \
  10.396 +\           Says S' B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \
  10.397  \           Says B Server {|NA, Agent A, Agent B, X',              \
  10.398  \                           Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
  10.399  \            : set evs |]                                          \
  10.400 @@ -459,7 +451,7 @@
  10.401  \                   Crypt (shrK B) {|NB, Key K|}|}                 \
  10.402  \                   : set evs";
  10.403  by (blast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
  10.404 -                       addSEs sees_Spy_partsEs) 1);
  10.405 +                       addSEs spies_partsEs) 1);
  10.406  qed "B_trusts_OR3";
  10.407  
  10.408  
  10.409 @@ -467,7 +459,7 @@
  10.410  
  10.411  
  10.412  goal thy 
  10.413 - "!!evs. [| B ~: lost;  evs : otway |]                           \
  10.414 + "!!evs. [| B ~: bad;  evs : otway |]                           \
  10.415  \        ==> Says Server B                                       \
  10.416  \              {|NA, Crypt (shrK A) {|NA, Key K|},               \
  10.417  \                Crypt (shrK B) {|NB, Key K|}|} : set evs -->    \
  10.418 @@ -476,7 +468,7 @@
  10.419  \            : set evs)";
  10.420  by (etac otway.induct 1);
  10.421  by (ALLGOALS Asm_simp_tac);
  10.422 -by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj]
  10.423 +by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj]
  10.424  		       addSEs [MPair_parts, Crypt_imp_OR2]) 3);
  10.425  by (ALLGOALS Blast_tac);
  10.426  bind_thm ("OR3_imp_OR2", result() RSN (2,rev_mp) RS exE);
  10.427 @@ -489,7 +481,7 @@
  10.428   "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs;       \
  10.429  \           Says A B {|NA, Agent A, Agent B,                                \
  10.430  \                      Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
  10.431 -\           A ~: lost;  A ~= Spy;  B ~: lost;  evs : otway |]               \
  10.432 +\           A ~: bad;  A ~= Spy;  B ~: bad;  evs : otway |]               \
  10.433  \        ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X,              \
  10.434  \                              Crypt (shrK B)  {|NA, NB, Agent A, Agent B|} |}\
  10.435  \            : set evs";
    11.1 --- a/src/HOL/Auth/OtwayRees.thy	Wed Sep 17 16:40:52 1997 +0200
    11.2 +++ b/src/HOL/Auth/OtwayRees.thy	Thu Sep 18 13:24:04 1997 +0200
    11.3 @@ -24,7 +24,7 @@
    11.4             invent new nonces here, but he can also use NS1.  Common to
    11.5             all similar protocols.*)
    11.6      Fake "[| evs: otway;  B ~= Spy;  
    11.7 -             X: synth (analz (sees Spy evs)) |]
    11.8 +             X: synth (analz (spies evs)) |]
    11.9            ==> Says Spy B X  # evs : otway"
   11.10  
   11.11           (*Alice initiates a protocol run*)
    12.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Wed Sep 17 16:40:52 1997 +0200
    12.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Thu Sep 18 13:24:04 1997 +0200
    12.3 @@ -44,36 +44,36 @@
    12.4  (** For reasoning about the encrypted portion of messages **)
    12.5  
    12.6  goal thy "!!evs. Says S' B {|X, Crypt(shrK B) X'|} : set evs ==> \
    12.7 -\                X : analz (sees Spy evs)";
    12.8 -by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    12.9 -qed "OR4_analz_sees_Spy";
   12.10 +\                X : analz (spies evs)";
   12.11 +by (blast_tac (!claset addSDs [Says_imp_spies RS analz.Inj]) 1);
   12.12 +qed "OR4_analz_spies";
   12.13  
   12.14  goal thy "!!evs. Says Server B {|X, Crypt K' {|NB, a, Agent B, K|}|} \
   12.15 -\                  : set evs ==> K : parts (sees Spy evs)";
   12.16 -by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
   12.17 -qed "Oops_parts_sees_Spy";
   12.18 +\                  : set evs ==> K : parts (spies evs)";
   12.19 +by (blast_tac (!claset addSEs spies_partsEs) 1);
   12.20 +qed "Oops_parts_spies";
   12.21  
   12.22 -(*OR4_analz_sees_Spy lets us treat those cases using the same 
   12.23 +(*OR4_analz_spies lets us treat those cases using the same 
   12.24    argument as for the Fake case.  This is possible for most, but not all,
   12.25    proofs, since Fake messages originate from the Spy. *)
   12.26  
   12.27 -bind_thm ("OR4_parts_sees_Spy",
   12.28 -          OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
   12.29 +bind_thm ("OR4_parts_spies",
   12.30 +          OR4_analz_spies RS (impOfSubs analz_subset_parts));
   12.31  
   12.32 -(*For proving the easier theorems about X ~: parts (sees Spy evs).*)
   12.33 +(*For proving the easier theorems about X ~: parts (spies evs).*)
   12.34  fun parts_induct_tac i = 
   12.35      etac otway.induct i			THEN 
   12.36 -    forward_tac [Oops_parts_sees_Spy] (i+6) THEN
   12.37 -    forward_tac [OR4_parts_sees_Spy]  (i+5) THEN
   12.38 +    forward_tac [Oops_parts_spies] (i+6) THEN
   12.39 +    forward_tac [OR4_parts_spies]  (i+5) THEN
   12.40      prove_simple_subgoals_tac  i;
   12.41  
   12.42  
   12.43 -(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
   12.44 +(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
   12.45      sends messages containing X! **)
   12.46  
   12.47 -(*Spy never sees another agent's shared key! (unless it's lost at start)*)
   12.48 +(*Spy never sees another agent's shared key! (unless it's bad at start)*)
   12.49  goal thy 
   12.50 - "!!evs. evs : otway ==> (Key (shrK A) : parts (sees Spy evs)) = (A : lost)";
   12.51 + "!!evs. evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
   12.52  by (parts_induct_tac 1);
   12.53  by (Fake_parts_insert_tac 1);
   12.54  by (Blast_tac 1);
   12.55 @@ -81,13 +81,12 @@
   12.56  Addsimps [Spy_see_shrK];
   12.57  
   12.58  goal thy 
   12.59 - "!!evs. evs : otway ==> (Key (shrK A) : analz (sees Spy evs)) = (A : lost)";
   12.60 + "!!evs. evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
   12.61  by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
   12.62  qed "Spy_analz_shrK";
   12.63  Addsimps [Spy_analz_shrK];
   12.64  
   12.65 -goal thy  "!!A. [| Key (shrK A) : parts (sees Spy evs);       \
   12.66 -\                  evs : otway |] ==> A:lost";
   12.67 +goal thy  "!!A. [| Key (shrK A) : parts (spies evs); evs : otway |] ==> A:bad";
   12.68  by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
   12.69  qed "Spy_see_shrK_D";
   12.70  
   12.71 @@ -97,7 +96,7 @@
   12.72  
   12.73  (*Nobody can have used non-existent keys!*)
   12.74  goal thy "!!evs. evs : otway ==>          \
   12.75 -\         Key K ~: used evs --> K ~: keysFor (parts (sees Spy evs))";
   12.76 +\         Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
   12.77  by (parts_induct_tac 1);
   12.78  (*Fake*)
   12.79  by (best_tac
   12.80 @@ -135,8 +134,8 @@
   12.81  
   12.82  
   12.83  (*For proofs involving analz.*)
   12.84 -val analz_sees_tac = 
   12.85 -    dtac OR4_analz_sees_Spy 6 THEN
   12.86 +val analz_spies_tac = 
   12.87 +    dtac OR4_analz_spies 6 THEN
   12.88      forward_tac [Says_Server_message_form] 7 THEN
   12.89      assume_tac 7 THEN
   12.90      REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
   12.91 @@ -145,8 +144,8 @@
   12.92  (****
   12.93   The following is to prove theorems of the form
   12.94  
   12.95 -  Key K : analz (insert (Key KAB) (sees Spy evs)) ==>
   12.96 -  Key K : analz (sees Spy evs)
   12.97 +  Key K : analz (insert (Key KAB) (spies evs)) ==>
   12.98 +  Key K : analz (spies evs)
   12.99  
  12.100   A more general formula must be proved inductively.
  12.101  ****)
  12.102 @@ -158,10 +157,10 @@
  12.103  goal thy  
  12.104   "!!evs. evs : otway ==>                                    \
  12.105  \  ALL K KK. KK <= Compl (range shrK) -->                   \
  12.106 -\            (Key K : analz (Key``KK Un (sees Spy evs))) =  \
  12.107 -\            (K : KK | Key K : analz (sees Spy evs))";
  12.108 +\            (Key K : analz (Key``KK Un (spies evs))) =  \
  12.109 +\            (K : KK | Key K : analz (spies evs))";
  12.110  by (etac otway.induct 1);
  12.111 -by analz_sees_tac;
  12.112 +by analz_spies_tac;
  12.113  by (REPEAT_FIRST (resolve_tac [allI, impI]));
  12.114  by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
  12.115  by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
  12.116 @@ -174,8 +173,8 @@
  12.117  
  12.118  goal thy
  12.119   "!!evs. [| evs : otway;  KAB ~: range shrK |] ==>          \
  12.120 -\        Key K : analz (insert (Key KAB) (sees Spy evs)) =  \
  12.121 -\        (K = KAB | Key K : analz (sees Spy evs))";
  12.122 +\        Key K : analz (insert (Key KAB) (spies evs)) =  \
  12.123 +\        (K = KAB | Key K : analz (spies evs))";
  12.124  by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
  12.125  qed "analz_insert_freshK";
  12.126  
  12.127 @@ -198,7 +197,7 @@
  12.128  by (expand_case_tac "K = ?y" 1);
  12.129  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
  12.130  (*...we assume X is a recent message and handle this case by contradiction*)
  12.131 -by (blast_tac (!claset addSEs sees_Spy_partsEs
  12.132 +by (blast_tac (!claset addSEs spies_partsEs
  12.133                         delrules[conjI] (*prevent splitup into 4 subgoals*)) 1);
  12.134  val lemma = result();
  12.135  
  12.136 @@ -223,9 +222,8 @@
  12.137  
  12.138  (*If the encrypted message appears then it originated with the Server!*)
  12.139  goal thy 
  12.140 - "!!evs. [| A ~: lost;  evs : otway |]                 \
  12.141 -\ ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}   \
  12.142 -\      : parts (sees Spy evs)                          \
  12.143 + "!!evs. [| A ~: bad;  evs : otway |]                 \
  12.144 +\ ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|} : parts (spies evs) \
  12.145  \     --> (EX NB. Says Server B                                          \
  12.146  \                  {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
  12.147  \                    Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
  12.148 @@ -243,13 +241,13 @@
  12.149  goal thy 
  12.150   "!!evs. [| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|})  \
  12.151  \            : set evs;                                                 \
  12.152 -\           A ~: lost;  evs : otway |]                                  \
  12.153 +\           A ~: bad;  evs : otway |]                                  \
  12.154  \        ==> EX NB. Says Server B                                       \
  12.155  \                    {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},  \
  12.156  \                      Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
  12.157  \                   : set evs";
  12.158  by (blast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
  12.159 -                      addEs  sees_Spy_partsEs) 1);
  12.160 +                      addEs  spies_partsEs) 1);
  12.161  qed "A_trusts_OR4";
  12.162  
  12.163  
  12.164 @@ -258,15 +256,15 @@
  12.165      the premises, e.g. by having A=Spy **)
  12.166  
  12.167  goal thy 
  12.168 - "!!evs. [| A ~: lost;  B ~: lost;  evs : otway |]                 \
  12.169 + "!!evs. [| A ~: bad;  B ~: bad;  evs : otway |]                 \
  12.170  \        ==> Says Server B                                         \
  12.171  \             {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
  12.172  \               Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
  12.173  \            : set evs -->                                         \
  12.174  \            Says B Spy {|NA, NB, Key K|} ~: set evs -->           \
  12.175 -\            Key K ~: analz (sees Spy evs)";
  12.176 +\            Key K ~: analz (spies evs)";
  12.177  by (etac otway.induct 1);
  12.178 -by analz_sees_tac;
  12.179 +by analz_spies_tac;
  12.180  by (ALLGOALS
  12.181      (asm_simp_tac (!simpset addcongs [conj_cong, if_weak_cong] 
  12.182                              addsimps [analz_insert_eq, analz_insert_freshK]
  12.183 @@ -276,7 +274,7 @@
  12.184  (*OR4*) 
  12.185  by (Blast_tac 3);
  12.186  (*OR3*)
  12.187 -by (blast_tac (!claset addSEs sees_Spy_partsEs
  12.188 +by (blast_tac (!claset addSEs spies_partsEs
  12.189                         addIs [impOfSubs analz_subset_parts]) 2);
  12.190  (*Fake*) 
  12.191  by (spy_analz_tac 1);
  12.192 @@ -288,8 +286,8 @@
  12.193  \                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
  12.194  \             : set evs;                                            \
  12.195  \           Says B Spy {|NA, NB, Key K|} ~: set evs;                \
  12.196 -\           A ~: lost;  B ~: lost;  evs : otway |]                  \
  12.197 -\        ==> Key K ~: analz (sees Spy evs)";
  12.198 +\           A ~: bad;  B ~: bad;  evs : otway |]                  \
  12.199 +\        ==> Key K ~: analz (spies evs)";
  12.200  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
  12.201  by (blast_tac (!claset addSEs [lemma]) 1);
  12.202  qed "Spy_not_see_encrypted_key";
  12.203 @@ -299,9 +297,8 @@
  12.204  
  12.205  (*If the encrypted message appears then it originated with the Server!*)
  12.206  goal thy 
  12.207 - "!!evs. [| B ~: lost;  evs : otway |]                                 \
  12.208 -\    ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}                \
  12.209 -\         : parts (sees Spy evs)                                       \
  12.210 + "!!evs. [| B ~: bad;  evs : otway |]                                 \
  12.211 +\    ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|} : parts (spies evs) \
  12.212  \        --> (EX NA. Says Server B                                          \
  12.213  \                     {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
  12.214  \                       Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
  12.215 @@ -317,7 +314,7 @@
  12.216  (*Guarantee for B: if it gets a well-formed certificate then the Server
  12.217    has sent the correct message in round 3.*)
  12.218  goal thy 
  12.219 - "!!evs. [| B ~: lost;  evs : otway;                                        \
  12.220 + "!!evs. [| B ~: bad;  evs : otway;                                        \
  12.221  \           Says S' B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
  12.222  \            : set evs |]                                                   \
  12.223  \        ==> EX NA. Says Server B                                           \
  12.224 @@ -325,5 +322,5 @@
  12.225  \                       Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
  12.226  \                     : set evs";
  12.227  by (blast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
  12.228 -                       addEs  sees_Spy_partsEs) 1);
  12.229 +                       addEs  spies_partsEs) 1);
  12.230  qed "B_trusts_OR3";
    13.1 --- a/src/HOL/Auth/OtwayRees_AN.thy	Wed Sep 17 16:40:52 1997 +0200
    13.2 +++ b/src/HOL/Auth/OtwayRees_AN.thy	Thu Sep 18 13:24:04 1997 +0200
    13.3 @@ -29,7 +29,7 @@
    13.4             invent new nonces here, but he can also use NS1.  Common to
    13.5             all similar protocols.*)
    13.6      Fake "[| evs: otway;  B ~= Spy;  
    13.7 -             X: synth (analz (sees Spy evs)) |]
    13.8 +             X: synth (analz (spies evs)) |]
    13.9            ==> Says Spy B X  # evs : otway"
   13.10  
   13.11           (*Alice initiates a protocol run*)
    14.1 --- a/src/HOL/Auth/OtwayRees_Bad.ML	Wed Sep 17 16:40:52 1997 +0200
    14.2 +++ b/src/HOL/Auth/OtwayRees_Bad.ML	Thu Sep 18 13:24:04 1997 +0200
    14.3 @@ -47,45 +47,45 @@
    14.4  (** For reasoning about the encrypted portion of messages **)
    14.5  
    14.6  goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set evs ==> \
    14.7 -\                X : analz (sees Spy evs)";
    14.8 -by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    14.9 -qed "OR2_analz_sees_Spy";
   14.10 +\                X : analz (spies evs)";
   14.11 +by (blast_tac (!claset addSDs [Says_imp_spies RS analz.Inj]) 1);
   14.12 +qed "OR2_analz_spies";
   14.13  
   14.14  goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set evs ==> \
   14.15 -\                X : analz (sees Spy evs)";
   14.16 -by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
   14.17 -qed "OR4_analz_sees_Spy";
   14.18 +\                X : analz (spies evs)";
   14.19 +by (blast_tac (!claset addSDs [Says_imp_spies RS analz.Inj]) 1);
   14.20 +qed "OR4_analz_spies";
   14.21  
   14.22  goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \
   14.23 -\                 ==> K : parts (sees Spy evs)";
   14.24 -by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
   14.25 -qed "Oops_parts_sees_Spy";
   14.26 +\                 ==> K : parts (spies evs)";
   14.27 +by (blast_tac (!claset addSEs spies_partsEs) 1);
   14.28 +qed "Oops_parts_spies";
   14.29  
   14.30  (*OR2_analz... and OR4_analz... let us treat those cases using the same 
   14.31    argument as for the Fake case.  This is possible for most, but not all,
   14.32    proofs: Fake does not invent new nonces (as in OR2), and of course Fake
   14.33    messages originate from the Spy. *)
   14.34  
   14.35 -bind_thm ("OR2_parts_sees_Spy",
   14.36 -          OR2_analz_sees_Spy RS (impOfSubs analz_subset_parts));
   14.37 -bind_thm ("OR4_parts_sees_Spy",
   14.38 -          OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
   14.39 +bind_thm ("OR2_parts_spies",
   14.40 +          OR2_analz_spies RS (impOfSubs analz_subset_parts));
   14.41 +bind_thm ("OR4_parts_spies",
   14.42 +          OR4_analz_spies RS (impOfSubs analz_subset_parts));
   14.43  
   14.44 -(*For proving the easier theorems about X ~: parts (sees Spy evs).*)
   14.45 +(*For proving the easier theorems about X ~: parts (spies evs).*)
   14.46  fun parts_induct_tac i = 
   14.47      etac otway.induct i			THEN 
   14.48 -    forward_tac [Oops_parts_sees_Spy] (i+6) THEN
   14.49 -    forward_tac [OR4_parts_sees_Spy]  (i+5) THEN
   14.50 -    forward_tac [OR2_parts_sees_Spy]  (i+3) THEN 
   14.51 +    forward_tac [Oops_parts_spies] (i+6) THEN
   14.52 +    forward_tac [OR4_parts_spies]  (i+5) THEN
   14.53 +    forward_tac [OR2_parts_spies]  (i+3) THEN 
   14.54      prove_simple_subgoals_tac  i;
   14.55  
   14.56  
   14.57 -(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
   14.58 +(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
   14.59      sends messages containing X! **)
   14.60  
   14.61 -(*Spy never sees another agent's shared key! (unless it's lost at start)*)
   14.62 +(*Spy never sees another agent's shared key! (unless it's bad at start)*)
   14.63  goal thy 
   14.64 - "!!evs. evs : otway ==> (Key (shrK A) : parts (sees Spy evs)) = (A : lost)";
   14.65 + "!!evs. evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
   14.66  by (parts_induct_tac 1);
   14.67  by (Fake_parts_insert_tac 1);
   14.68  by (Blast_tac 1);
   14.69 @@ -93,13 +93,12 @@
   14.70  Addsimps [Spy_see_shrK];
   14.71  
   14.72  goal thy 
   14.73 - "!!evs. evs : otway ==> (Key (shrK A) : analz (sees Spy evs)) = (A : lost)";
   14.74 + "!!evs. evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
   14.75  by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
   14.76  qed "Spy_analz_shrK";
   14.77  Addsimps [Spy_analz_shrK];
   14.78  
   14.79 -goal thy  "!!A. [| Key (shrK A) : parts (sees Spy evs);       \
   14.80 -\                  evs : otway |] ==> A:lost";
   14.81 +goal thy  "!!A. [| Key (shrK A) : parts (spies evs); evs : otway |] ==> A:bad";
   14.82  by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
   14.83  qed "Spy_see_shrK_D";
   14.84  
   14.85 @@ -109,7 +108,7 @@
   14.86  
   14.87  (*Nobody can have used non-existent keys!*)
   14.88  goal thy "!!evs. evs : otway ==>          \
   14.89 -\         Key K ~: used evs --> K ~: keysFor (parts (sees Spy evs))";
   14.90 +\         Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
   14.91  by (parts_induct_tac 1);
   14.92  (*Fake*)
   14.93  by (best_tac
   14.94 @@ -146,9 +145,9 @@
   14.95  
   14.96  
   14.97  (*For proofs involving analz.*)
   14.98 -val analz_sees_tac = 
   14.99 -    dtac OR2_analz_sees_Spy 4 THEN 
  14.100 -    dtac OR4_analz_sees_Spy 6 THEN
  14.101 +val analz_spies_tac = 
  14.102 +    dtac OR2_analz_spies 4 THEN 
  14.103 +    dtac OR4_analz_spies 6 THEN
  14.104      forward_tac [Says_Server_message_form] 7 THEN assume_tac 7 THEN 
  14.105      REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
  14.106  
  14.107 @@ -156,8 +155,8 @@
  14.108  (****
  14.109   The following is to prove theorems of the form
  14.110  
  14.111 -  Key K : analz (insert (Key KAB) (sees Spy evs)) ==>
  14.112 -  Key K : analz (sees Spy evs)
  14.113 +  Key K : analz (insert (Key KAB) (spies evs)) ==>
  14.114 +  Key K : analz (spies evs)
  14.115  
  14.116   A more general formula must be proved inductively.
  14.117  ****)
  14.118 @@ -169,10 +168,10 @@
  14.119  goal thy  
  14.120   "!!evs. evs : otway ==>                                    \
  14.121  \  ALL K KK. KK <= Compl (range shrK) -->                   \
  14.122 -\            (Key K : analz (Key``KK Un (sees Spy evs))) =  \
  14.123 -\            (K : KK | Key K : analz (sees Spy evs))";
  14.124 +\            (Key K : analz (Key``KK Un (spies evs))) =  \
  14.125 +\            (K : KK | Key K : analz (spies evs))";
  14.126  by (etac otway.induct 1);
  14.127 -by analz_sees_tac;
  14.128 +by analz_spies_tac;
  14.129  by (REPEAT_FIRST (resolve_tac [allI, impI]));
  14.130  by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
  14.131  by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
  14.132 @@ -185,8 +184,8 @@
  14.133  
  14.134  goal thy
  14.135   "!!evs. [| evs : otway;  KAB ~: range shrK |] ==>          \
  14.136 -\        Key K : analz (insert (Key KAB) (sees Spy evs)) =  \
  14.137 -\        (K = KAB | Key K : analz (sees Spy evs))";
  14.138 +\        Key K : analz (insert (Key KAB) (spies evs)) =  \
  14.139 +\        (K = KAB | Key K : analz (spies evs))";
  14.140  by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
  14.141  qed "analz_insert_freshK";
  14.142  
  14.143 @@ -207,7 +206,7 @@
  14.144  by (expand_case_tac "K = ?y" 1);
  14.145  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
  14.146  (*...we assume X is a recent message, and handle this case by contradiction*)
  14.147 -by (blast_tac (!claset addSEs sees_Spy_partsEs
  14.148 +by (blast_tac (!claset addSEs spies_partsEs
  14.149                        delrules [conjI]    (*no split-up to 4 subgoals*)) 1);
  14.150  val lemma = result();
  14.151  
  14.152 @@ -221,14 +220,14 @@
  14.153  
  14.154  (*Crucial security property, but not itself enough to guarantee correctness!*)
  14.155  goal thy 
  14.156 - "!!evs. [| A ~: lost;  B ~: lost;  evs : otway |]                    \
  14.157 + "!!evs. [| A ~: bad;  B ~: bad;  evs : otway |]                    \
  14.158  \        ==> Says Server B                                            \
  14.159  \              {|NA, Crypt (shrK A) {|NA, Key K|},                    \
  14.160  \                Crypt (shrK B) {|NB, Key K|}|} : set evs -->         \
  14.161  \            Says B Spy {|NA, NB, Key K|} ~: set evs -->              \
  14.162 -\            Key K ~: analz (sees Spy evs)";
  14.163 +\            Key K ~: analz (spies evs)";
  14.164  by (etac otway.induct 1);
  14.165 -by analz_sees_tac;
  14.166 +by analz_spies_tac;
  14.167  by (ALLGOALS
  14.168      (asm_simp_tac (!simpset addcongs [conj_cong] 
  14.169                              addsimps [analz_insert_eq, analz_insert_freshK]
  14.170 @@ -238,7 +237,7 @@
  14.171  (*OR4*) 
  14.172  by (Blast_tac 3);
  14.173  (*OR3*)
  14.174 -by (blast_tac (!claset addSEs sees_Spy_partsEs
  14.175 +by (blast_tac (!claset addSEs spies_partsEs
  14.176                         addIs [impOfSubs analz_subset_parts]) 2);
  14.177  (*Fake*) 
  14.178  by (spy_analz_tac 1);
  14.179 @@ -249,8 +248,8 @@
  14.180  \            {|NA, Crypt (shrK A) {|NA, Key K|},                  \
  14.181  \                  Crypt (shrK B) {|NB, Key K|}|} : set evs;      \
  14.182  \           Says B Spy {|NA, NB, Key K|} ~: set evs;              \
  14.183 -\           A ~: lost;  B ~: lost;  evs : otway |]                \
  14.184 -\        ==> Key K ~: analz (sees Spy evs)";
  14.185 +\           A ~: bad;  B ~: bad;  evs : otway |]                \
  14.186 +\        ==> Key K ~: analz (spies evs)";
  14.187  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
  14.188  by (blast_tac (!claset addSEs [lemma]) 1);
  14.189  qed "Spy_not_see_encrypted_key";
  14.190 @@ -263,9 +262,8 @@
  14.191    Perhaps it's because OR2 has two similar-looking encrypted messages in
  14.192          this version.*)
  14.193  goal thy 
  14.194 - "!!evs. [| A ~: lost;  A ~= B;  evs : otway |]                \
  14.195 -\        ==> Crypt (shrK A) {|NA, Agent A, Agent B|}           \
  14.196 -\             : parts (sees Spy evs) -->                       \
  14.197 + "!!evs. [| A ~: bad;  A ~= B;  evs : otway |]                \
  14.198 +\        ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) --> \
  14.199  \            Says A B {|NA, Agent A, Agent B,                  \
  14.200  \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}  : set evs";
  14.201  by (parts_induct_tac 1);
  14.202 @@ -279,8 +277,8 @@
  14.203  (*Only it is FALSE.  Somebody could make a fake message to Server
  14.204            substituting some other nonce NA' for NB.*)
  14.205  goal thy 
  14.206 - "!!evs. [| A ~: lost;  A ~= Spy;  evs : otway |]                    \
  14.207 -\        ==> Crypt (shrK A) {|NA, Key K|} : parts (sees Spy evs) --> \
  14.208 + "!!evs. [| A ~: bad;  A ~= Spy;  evs : otway |]                    \
  14.209 +\        ==> Crypt (shrK A) {|NA, Key K|} : parts (spies evs) --> \
  14.210  \            Says A B {|NA, Agent A, Agent B,                        \
  14.211  \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}    \
  14.212  \             : set evs -->                                          \
  14.213 @@ -292,12 +290,12 @@
  14.214  by (Fake_parts_insert_tac 1);
  14.215  (*OR1: it cannot be a new Nonce, contradiction.*)
  14.216  by (blast_tac (!claset addSIs [parts_insertI]
  14.217 -                      addSEs sees_Spy_partsEs) 1);
  14.218 +                      addSEs spies_partsEs) 1);
  14.219  (*OR4*)
  14.220  by (REPEAT (Safe_step_tac 2));
  14.221  by (REPEAT (blast_tac (!claset addSDs [parts_cut]) 3));
  14.222  by (blast_tac (!claset addSIs [Crypt_imp_OR1]
  14.223 -                       addEs  sees_Spy_partsEs) 2);
  14.224 +                       addEs  spies_partsEs) 2);
  14.225  (*OR3*)  (** LEVEL 5 **)
  14.226  by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
  14.227  by (step_tac (!claset delrules [disjCI, impCE]) 1);
    15.1 --- a/src/HOL/Auth/OtwayRees_Bad.thy	Wed Sep 17 16:40:52 1997 +0200
    15.2 +++ b/src/HOL/Auth/OtwayRees_Bad.thy	Thu Sep 18 13:24:04 1997 +0200
    15.3 @@ -22,7 +22,7 @@
    15.4           (*The spy MAY say anything he CAN say.  We do not expect him to
    15.5             invent new nonces here, but he can also use NS1.  Common to
    15.6             all similar protocols.*)
    15.7 -    Fake "[| evs: otway;  B ~= Spy;  X: synth (analz (sees Spy evs)) |]
    15.8 +    Fake "[| evs: otway;  B ~= Spy;  X: synth (analz (spies evs)) |]
    15.9            ==> Says Spy B X  # evs : otway"
   15.10  
   15.11           (*Alice initiates a protocol run*)
    16.1 --- a/src/HOL/Auth/Public.ML	Wed Sep 17 16:40:52 1997 +0200
    16.2 +++ b/src/HOL/Auth/Public.ML	Thu Sep 18 13:24:04 1997 +0200
    16.3 @@ -44,49 +44,50 @@
    16.4  Addsimps [keysFor_parts_initState];
    16.5  
    16.6  
    16.7 -(*** Function "sees" ***)
    16.8 +(*** Function "spies" ***)
    16.9  
   16.10  (*Agents see their own private keys!*)
   16.11 -goal thy "A ~= Spy --> Key (priK A) : sees A evs";
   16.12 -by (induct_tac "evs" 1);
   16.13 +goal thy "Key (priK A) : initState A";
   16.14  by (induct_tac "A" 1);
   16.15 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [sees_Cons])));
   16.16 -qed_spec_mp "sees_own_priK";
   16.17 +by (Auto_tac());
   16.18 +qed "priK_in_initState";
   16.19 +AddIffs [priK_in_initState];
   16.20  
   16.21 -(*All public keys are visible to all*)
   16.22 -goal thy "Key (pubK A) : sees B evs";
   16.23 +(*All public keys are visible*)
   16.24 +goal thy "Key (pubK A) : spies evs";
   16.25  by (induct_tac "evs" 1);
   16.26 -by (induct_tac "B" 1);
   16.27 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [sees_Cons])));
   16.28 -by (Auto_tac ());
   16.29 -qed_spec_mp "sees_pubK";
   16.30 +by (ALLGOALS (asm_simp_tac
   16.31 +	      (!simpset addsimps [imageI, spies_Cons]
   16.32 +	                setloop split_tac [expand_event_case, expand_if])));
   16.33 +qed_spec_mp "spies_pubK";
   16.34  
   16.35 -(*Spy sees private keys of agents!*)
   16.36 -goal thy "!!A. A: lost ==> Key (priK A) : sees Spy evs";
   16.37 +(*Spy sees private keys of bad agents!*)
   16.38 +goal thy "!!A. A: bad ==> Key (priK A) : spies evs";
   16.39  by (induct_tac "evs" 1);
   16.40 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [sees_Cons])));
   16.41 -by (Blast_tac 1);
   16.42 -qed "Spy_sees_lost";
   16.43 +by (ALLGOALS (asm_simp_tac
   16.44 +	      (!simpset addsimps [imageI, spies_Cons]
   16.45 +	                setloop split_tac [expand_event_case, expand_if])));
   16.46 +qed "Spy_spies_bad";
   16.47  
   16.48 -AddIffs [sees_pubK, sees_pubK RS analz.Inj];
   16.49 -AddSIs  [sees_own_priK, Spy_sees_lost];
   16.50 +AddIffs [spies_pubK, spies_pubK RS analz.Inj];
   16.51 +AddSIs  [Spy_spies_bad];
   16.52  
   16.53  
   16.54 -(*For not_lost_tac*)
   16.55 -goal thy "!!A. [| Crypt (pubK A) X : analz (sees Spy evs);  A: lost |] \
   16.56 -\              ==> X : analz (sees Spy evs)";
   16.57 +(*For not_bad_tac*)
   16.58 +goal thy "!!A. [| Crypt (pubK A) X : analz (spies evs);  A: bad |] \
   16.59 +\              ==> X : analz (spies evs)";
   16.60  by (blast_tac (!claset addSDs [analz.Decrypt]) 1);
   16.61 -qed "Crypt_Spy_analz_lost";
   16.62 +qed "Crypt_Spy_analz_bad";
   16.63  
   16.64  (*Prove that the agent is uncompromised by the confidentiality of 
   16.65    a component of a message she's said.*)
   16.66 -fun not_lost_tac s =
   16.67 -    case_tac ("(" ^ s ^ ") : lost") THEN'
   16.68 +fun not_bad_tac s =
   16.69 +    case_tac ("(" ^ s ^ ") : bad") THEN'
   16.70      SELECT_GOAL 
   16.71 -      (REPEAT_DETERM (dtac (Says_imp_sees_Spy RS analz.Inj) 1) THEN
   16.72 +      (REPEAT_DETERM (dtac (Says_imp_spies RS analz.Inj) 1) THEN
   16.73         REPEAT_DETERM (etac MPair_analz 1) THEN
   16.74         THEN_BEST_FIRST 
   16.75 -         (dres_inst_tac [("A", s)] Crypt_Spy_analz_lost 1 THEN assume_tac 1)
   16.76 +         (dres_inst_tac [("A", s)] Crypt_Spy_analz_bad 1 THEN assume_tac 1)
   16.77           (has_fewer_prems 1, size_of_thm)
   16.78           (Step_tac 1));
   16.79  
   16.80 @@ -100,27 +101,30 @@
   16.81  AddIffs [Nonce_notin_initState];
   16.82  
   16.83  goal thy "Nonce N ~: used []";
   16.84 -by (simp_tac (!simpset addsimps [used_def]) 1);
   16.85 +by (simp_tac (!simpset addsimps [used_Nil]) 1);
   16.86  qed "Nonce_notin_used_empty";
   16.87  Addsimps [Nonce_notin_used_empty];
   16.88  
   16.89  
   16.90  (*** Supply fresh nonces for possibility theorems. ***)
   16.91  
   16.92 -goalw thy [used_def] "EX N. ALL n. N<=n --> Nonce n ~: used evs";
   16.93 +(*In any trace, there is an upper bound N on the greatest nonce in use.*)
   16.94 +goal thy "EX N. ALL n. N<=n --> Nonce n ~: used evs";
   16.95  by (induct_tac "evs" 1);
   16.96  by (res_inst_tac [("x","0")] exI 1);
   16.97 +by (ALLGOALS (asm_simp_tac
   16.98 +	      (!simpset addsimps [used_Cons]
   16.99 +			setloop split_tac [expand_event_case, expand_if])));
  16.100  by (Step_tac 1);
  16.101 -by (Full_simp_tac 1);
  16.102 -(*Inductive step*)
  16.103 -by (induct_tac "a" 1);
  16.104 -by (ALLGOALS (full_simp_tac 
  16.105 -	      (!simpset addsimps [UN_parts_sees_Says,
  16.106 -				  UN_parts_sees_Notes])));
  16.107  by (ALLGOALS (rtac (msg_Nonce_supply RS exE)));
  16.108  by (ALLGOALS (blast_tac (!claset addSEs [add_leE])));
  16.109  val lemma = result();
  16.110  
  16.111 +goal thy "EX N. Nonce N ~: used evs";
  16.112 +by (rtac (lemma RS exE) 1);
  16.113 +by (Blast_tac 1);
  16.114 +qed "Nonce_supply1";
  16.115 +
  16.116  goal thy "Nonce (@ N. Nonce N ~: used evs) ~: used evs";
  16.117  by (rtac (lemma RS exE) 1);
  16.118  by (rtac selectI 1);
    17.1 --- a/src/HOL/Auth/Public.thy	Wed Sep 17 16:40:52 1997 +0200
    17.2 +++ b/src/HOL/Auth/Public.thy	Thu Sep 18 13:24:04 1997 +0200
    17.3 @@ -26,7 +26,7 @@
    17.4    initState_Friend  "initState (Friend i) =    
    17.5   		         insert (Key (priK (Friend i))) (Key `` range pubK)"
    17.6    initState_Spy     "initState Spy        =    
    17.7 - 		         (Key``invKey``pubK``lost) Un (Key `` range pubK)"
    17.8 + 		         (Key``invKey``pubK``bad) Un (Key `` range pubK)"
    17.9  
   17.10  
   17.11  rules
    18.1 --- a/src/HOL/Auth/Recur.ML	Wed Sep 17 16:40:52 1997 +0200
    18.2 +++ b/src/HOL/Auth/Recur.ML	Thu Sep 18 13:24:04 1997 +0200
    18.3 @@ -112,45 +112,45 @@
    18.4  
    18.5  (** For reasoning about the encrypted portion of messages **)
    18.6  
    18.7 -val RA2_analz_sees_Spy = Says_imp_sees_Spy RS analz.Inj |> standard;
    18.8 +val RA2_analz_spies = Says_imp_spies RS analz.Inj |> standard;
    18.9  
   18.10  goal thy "!!evs. Says C' B {|Crypt K X, X', RA|} : set evs \
   18.11 -\                ==> RA : analz (sees Spy evs)";
   18.12 -by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
   18.13 -qed "RA4_analz_sees_Spy";
   18.14 +\                ==> RA : analz (spies evs)";
   18.15 +by (blast_tac (!claset addSDs [Says_imp_spies RS analz.Inj]) 1);
   18.16 +qed "RA4_analz_spies";
   18.17  
   18.18  (*RA2_analz... and RA4_analz... let us treat those cases using the same 
   18.19    argument as for the Fake case.  This is possible for most, but not all,
   18.20    proofs: Fake does not invent new nonces (as in RA2), and of course Fake
   18.21    messages originate from the Spy. *)
   18.22  
   18.23 -bind_thm ("RA2_parts_sees_Spy",
   18.24 -          RA2_analz_sees_Spy RS (impOfSubs analz_subset_parts));
   18.25 -bind_thm ("RA4_parts_sees_Spy",
   18.26 -          RA4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
   18.27 +bind_thm ("RA2_parts_spies",
   18.28 +          RA2_analz_spies RS (impOfSubs analz_subset_parts));
   18.29 +bind_thm ("RA4_parts_spies",
   18.30 +          RA4_analz_spies RS (impOfSubs analz_subset_parts));
   18.31  
   18.32 -(*For proving the easier theorems about X ~: parts (sees Spy evs).*)
   18.33 +(*For proving the easier theorems about X ~: parts (spies evs).*)
   18.34  fun parts_induct_tac i = 
   18.35      etac recur.induct i				THEN
   18.36 -    forward_tac [RA2_parts_sees_Spy] (i+3)	THEN
   18.37 +    forward_tac [RA2_parts_spies] (i+3)	THEN
   18.38      etac subst (i+3) (*RA2: DELETE needless definition of PA!*)  THEN
   18.39      forward_tac [respond_imp_responses] (i+4)	THEN
   18.40 -    forward_tac [RA4_parts_sees_Spy] (i+5)	THEN
   18.41 +    forward_tac [RA4_parts_spies] (i+5)	THEN
   18.42      prove_simple_subgoals_tac i;
   18.43  
   18.44  
   18.45 -(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
   18.46 +(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
   18.47      sends messages containing X! **)
   18.48  
   18.49  
   18.50 -(** Spy never sees another agent's shared key! (unless it's lost at start) **)
   18.51 +(** Spy never sees another agent's shared key! (unless it's bad at start) **)
   18.52  
   18.53  goal thy 
   18.54 - "!!evs. evs : recur ==> (Key (shrK A) : parts (sees Spy evs)) = (A : lost)";
   18.55 + "!!evs. evs : recur ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
   18.56  by (parts_induct_tac 1);
   18.57  by (Fake_parts_insert_tac 1);
   18.58  by (ALLGOALS 
   18.59 -    (asm_simp_tac (!simpset addsimps [parts_insert2, parts_insert_sees])));
   18.60 +    (asm_simp_tac (!simpset addsimps [parts_insert2, parts_insert_spies])));
   18.61  (*RA3*)
   18.62  by (blast_tac (!claset addDs [Key_in_parts_respond]) 2);
   18.63  (*RA2*)
   18.64 @@ -159,13 +159,12 @@
   18.65  Addsimps [Spy_see_shrK];
   18.66  
   18.67  goal thy 
   18.68 - "!!evs. evs : recur ==> (Key (shrK A) : analz (sees Spy evs)) = (A : lost)";
   18.69 + "!!evs. evs : recur ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
   18.70  by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
   18.71  qed "Spy_analz_shrK";
   18.72  Addsimps [Spy_analz_shrK];
   18.73  
   18.74 -goal thy  "!!A. [| Key (shrK A) : parts (sees Spy evs);       \
   18.75 -\                  evs : recur |] ==> A:lost";
   18.76 +goal thy  "!!A. [| Key (shrK A) : parts (spies evs); evs : recur |] ==> A:bad";
   18.77  by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
   18.78  qed "Spy_see_shrK_D";
   18.79  
   18.80 @@ -186,11 +185,11 @@
   18.81  
   18.82  
   18.83  goal thy "!!evs. evs : recur ==>          \
   18.84 -\                Key K ~: used evs --> K ~: keysFor (parts (sees Spy evs))";
   18.85 +\                Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
   18.86  by (parts_induct_tac 1);
   18.87  (*RA3*)
   18.88  by (best_tac (!claset addDs  [Key_in_keysFor_parts]
   18.89 -	      addss  (!simpset addsimps [parts_insert_sees])) 2);
   18.90 +	      addss  (!simpset addsimps [parts_insert_spies])) 2);
   18.91  (*Fake*)
   18.92  by (best_tac
   18.93        (!claset addIs [impOfSubs analz_subset_parts]
   18.94 @@ -211,17 +210,17 @@
   18.95  (*** Proofs involving analz ***)
   18.96  
   18.97  (*For proofs involving analz.*)
   18.98 -val analz_sees_tac = 
   18.99 +val analz_spies_tac = 
  18.100      etac subst 4 (*RA2: DELETE needless definition of PA!*)  THEN
  18.101 -    dtac RA2_analz_sees_Spy 4 THEN 
  18.102 +    dtac RA2_analz_spies 4 THEN 
  18.103      forward_tac [respond_imp_responses] 5                THEN
  18.104 -    dtac RA4_analz_sees_Spy 6;
  18.105 +    dtac RA4_analz_spies 6;
  18.106  
  18.107  
  18.108  (** Session keys are not used to encrypt other session keys **)
  18.109  
  18.110  (*Version for "responses" relation.  Handles case RA3 in the theorem below.  
  18.111 -  Note that it holds for *any* set H (not just "sees Spy evs")
  18.112 +  Note that it holds for *any* set H (not just "spies evs")
  18.113    satisfying the inductive hypothesis.*)
  18.114  goal thy  
  18.115   "!!evs. [| RB : responses evs;                             \
  18.116 @@ -239,10 +238,10 @@
  18.117  goal thy  
  18.118   "!!evs. evs : recur ==>                                    \
  18.119  \  ALL K KK. KK <= Compl (range shrK) -->                   \
  18.120 -\            (Key K : analz (Key``KK Un (sees Spy evs))) =  \
  18.121 -\            (K : KK | Key K : analz (sees Spy evs))";
  18.122 +\            (Key K : analz (Key``KK Un (spies evs))) =  \
  18.123 +\            (K : KK | Key K : analz (spies evs))";
  18.124  by (etac recur.induct 1);
  18.125 -by analz_sees_tac;
  18.126 +by analz_spies_tac;
  18.127  by (REPEAT_FIRST (resolve_tac [allI, impI]));
  18.128  by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
  18.129  by (ALLGOALS 
  18.130 @@ -256,11 +255,11 @@
  18.131  qed_spec_mp "analz_image_freshK";
  18.132  
  18.133  
  18.134 -(*Instance of the lemma with H replaced by (sees Spy evs):
  18.135 +(*Instance of the lemma with H replaced by (spies evs):
  18.136     [| RB : responses evs;  evs : recur; |]
  18.137     ==> KK <= Compl (range shrK) --> 
  18.138 -       Key K : analz (insert RB (Key``KK Un sees Spy evs)) =
  18.139 -       (K : KK | Key K : analz (insert RB (sees Spy evs))) 
  18.140 +       Key K : analz (insert RB (Key``KK Un spies evs)) =
  18.141 +       (K : KK | Key K : analz (insert RB (spies evs))) 
  18.142  *)
  18.143  bind_thm ("resp_analz_image_freshK",
  18.144            raw_analz_image_freshK RSN
  18.145 @@ -268,23 +267,23 @@
  18.146  
  18.147  goal thy
  18.148   "!!evs. [| evs : recur;  KAB ~: range shrK |] ==>              \
  18.149 -\        Key K : analz (insert (Key KAB) (sees Spy evs)) =      \
  18.150 -\        (K = KAB | Key K : analz (sees Spy evs))";
  18.151 +\        Key K : analz (insert (Key KAB) (spies evs)) =      \
  18.152 +\        (K = KAB | Key K : analz (spies evs))";
  18.153  by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
  18.154  qed "analz_insert_freshK";
  18.155  
  18.156  
  18.157  (*Everything that's hashed is already in past traffic. *)
  18.158 -goal thy "!!evs. [| Hash {|Key(shrK A), X|} : parts (sees Spy evs);  \
  18.159 -\                   evs : recur;  A ~: lost |]                       \
  18.160 -\                ==> X : parts (sees Spy evs)";
  18.161 +goal thy "!!evs. [| Hash {|Key(shrK A), X|} : parts (spies evs);  \
  18.162 +\                   evs : recur;  A ~: bad |]                       \
  18.163 +\                ==> X : parts (spies evs)";
  18.164  by (etac rev_mp 1);
  18.165  by (parts_induct_tac 1);
  18.166  (*RA3 requires a further induction*)
  18.167  by (etac responses.induct 2);
  18.168  by (ALLGOALS Asm_simp_tac);
  18.169  (*Fake*)
  18.170 -by (simp_tac (!simpset addsimps [parts_insert_sees]) 1);
  18.171 +by (simp_tac (!simpset addsimps [parts_insert_spies]) 1);
  18.172  by (Fake_parts_insert_tac 1);
  18.173  qed "Hash_imp_body";
  18.174  
  18.175 @@ -296,9 +295,9 @@
  18.176  **)
  18.177  
  18.178  goal thy 
  18.179 - "!!evs. [| evs : recur; A ~: lost |]                   \
  18.180 + "!!evs. [| evs : recur; A ~: bad |]                   \
  18.181  \ ==> EX B' P'. ALL B P.                                     \
  18.182 -\        Hash {|Key(shrK A), Agent A, B, NA, P|} : parts (sees Spy evs) \
  18.183 +\        Hash {|Key(shrK A), Agent A, B, NA, P|} : parts (spies evs) \
  18.184  \          -->  B=B' & P=P'";
  18.185  by (parts_induct_tac 1);
  18.186  by (Fake_parts_insert_tac 1);
  18.187 @@ -309,13 +308,13 @@
  18.188  by (ALLGOALS (expand_case_tac "NA = ?y"));
  18.189  by (REPEAT_FIRST (ares_tac [exI]));
  18.190  by (REPEAT (blast_tac (!claset addSDs [Hash_imp_body]
  18.191 -                               addSEs sees_Spy_partsEs) 1));
  18.192 +                               addSEs spies_partsEs) 1));
  18.193  val lemma = result();
  18.194  
  18.195  goalw thy [HPair_def]
  18.196 - "!!A.[| Hash[Key(shrK A)] {|Agent A, B,NA,P|}   : parts(sees Spy evs); \
  18.197 -\        Hash[Key(shrK A)] {|Agent A, B',NA,P'|} : parts(sees Spy evs); \
  18.198 -\        evs : recur;  A ~: lost |]                                     \
  18.199 + "!!A.[| Hash[Key(shrK A)] {|Agent A, B,NA,P|}   : parts(spies evs); \
  18.200 +\        Hash[Key(shrK A)] {|Agent A, B',NA,P'|} : parts(spies evs); \
  18.201 +\        evs : recur;  A ~: bad |]                                     \
  18.202  \      ==> B=B' & P=P'";
  18.203  by (REPEAT (eresolve_tac partsEs 1));
  18.204  by (prove_unique_tac lemma 1);
  18.205 @@ -328,7 +327,7 @@
  18.206  
  18.207  goal thy
  18.208   "!!evs. [| RB : responses evs;  evs : recur |] \
  18.209 -\ ==> (Key (shrK B) : analz (insert RB (sees Spy evs))) = (B:lost)";
  18.210 +\ ==> (Key (shrK B) : analz (insert RB (spies evs))) = (B:bad)";
  18.211  by (etac responses.induct 1);
  18.212  by (ALLGOALS
  18.213      (asm_simp_tac 
  18.214 @@ -417,9 +416,9 @@
  18.215  
  18.216  goal thy 
  18.217   "!!evs. [| (PB,RB,KAB) : respond evs;  evs : recur |]              \
  18.218 -\        ==> ALL A A' N. A ~: lost & A' ~: lost -->                 \
  18.219 +\        ==> ALL A A' N. A ~: bad & A' ~: bad -->                 \
  18.220  \            Crypt (shrK A) {|Key K, Agent A', N|} : parts{RB} -->  \
  18.221 -\            Key K ~: analz (insert RB (sees Spy evs))";
  18.222 +\            Key K ~: analz (insert RB (spies evs))";
  18.223  by (etac respond.induct 1);
  18.224  by (forward_tac [respond_imp_responses] 2);
  18.225  by (forward_tac [respond_imp_not_used] 2);
  18.226 @@ -437,7 +436,7 @@
  18.227  by (Blast_tac 3);
  18.228  by (blast_tac (!claset addSEs partsEs
  18.229                         addDs [Key_in_parts_respond]) 2);
  18.230 -(*by unicity, either B=Aa or B=A', a contradiction since B: lost*)
  18.231 +(*by unicity, either B=Aa or B=A', a contradiction since B: bad*)
  18.232  by (dtac unique_session_keys 1);
  18.233  by (etac respond_certificate 1);
  18.234  by (assume_tac 1);
  18.235 @@ -446,16 +445,15 @@
  18.236  
  18.237  
  18.238  goal thy
  18.239 - "!!evs. [| Crypt (shrK A) {|Key K, Agent A', N|}     \
  18.240 -\              : parts (sees Spy evs);                \
  18.241 -\           A ~: lost;  A' ~: lost;  evs : recur |]   \
  18.242 -\        ==> Key K ~: analz (sees Spy evs)";
  18.243 + "!!evs. [| Crypt (shrK A) {|Key K, Agent A', N|} : parts (spies evs); \
  18.244 +\           A ~: bad;  A' ~: bad;  evs : recur |]   \
  18.245 +\        ==> Key K ~: analz (spies evs)";
  18.246  by (etac rev_mp 1);
  18.247  by (etac recur.induct 1);
  18.248 -by analz_sees_tac;
  18.249 +by analz_spies_tac;
  18.250  by (ALLGOALS
  18.251      (asm_simp_tac
  18.252 -     (!simpset addsimps [parts_insert_sees, analz_insert_freshK] 
  18.253 +     (!simpset addsimps [parts_insert_spies, analz_insert_freshK] 
  18.254                 setloop split_tac [expand_if])));
  18.255  (*RA4*)
  18.256  by (spy_analz_tac 5);
  18.257 @@ -494,9 +492,8 @@
  18.258    it can say nothing about how recent A's message is.  It might later be
  18.259    used to prove B's presence to A at the run's conclusion.*)
  18.260  goalw thy [HPair_def]
  18.261 - "!!evs. [| Hash {|Key(shrK A), Agent A, Agent B, NA, P|}         \
  18.262 -\             : parts (sees Spy evs);                        \
  18.263 -\            A ~: lost;  evs : recur |]                      \
  18.264 + "!!evs. [| Hash {|Key(shrK A), Agent A, Agent B, NA, P|} : parts(spies evs); \
  18.265 +\           A ~: bad;  evs : recur |]                      \
  18.266  \     ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, NA, P|}) : set evs";
  18.267  by (etac rev_mp 1);
  18.268  by (parts_induct_tac 1);
  18.269 @@ -512,8 +509,8 @@
  18.270  
  18.271  (*Certificates can only originate with the Server.*)
  18.272  goal thy 
  18.273 - "!!evs. [| Crypt (shrK A) Y : parts (sees Spy evs);    \
  18.274 -\           A ~: lost;  A ~= Spy;  evs : recur |]       \
  18.275 + "!!evs. [| Crypt (shrK A) Y : parts (spies evs);    \
  18.276 +\           A ~: bad;  A ~= Spy;  evs : recur |]       \
  18.277  \        ==> EX C RC. Says Server C RC : set evs  &     \
  18.278  \                     Crypt (shrK A) Y : parts {RC}";
  18.279  by (etac rev_mp 1);
  18.280 @@ -522,7 +519,7 @@
  18.281  (*RA4*)
  18.282  by (Blast_tac 4);
  18.283  (*RA3*)
  18.284 -by (full_simp_tac (!simpset addsimps [parts_insert_sees]) 3
  18.285 +by (full_simp_tac (!simpset addsimps [parts_insert_spies]) 3
  18.286      THEN Blast_tac 3);
  18.287  (*RA1*)
  18.288  by (Blast_tac 1);
    19.1 --- a/src/HOL/Auth/Recur.thy	Wed Sep 17 16:40:52 1997 +0200
    19.2 +++ b/src/HOL/Auth/Recur.thy	Thu Sep 18 13:24:04 1997 +0200
    19.3 @@ -57,7 +57,7 @@
    19.4           (*The spy MAY say anything he CAN say.  Common to
    19.5             all similar protocols.*)
    19.6      Fake "[| evs: recur;  B ~= Spy;  
    19.7 -             X: synth (analz (sees Spy evs)) |]
    19.8 +             X: synth (analz (spies evs)) |]
    19.9            ==> Says Spy B X  # evs : recur"
   19.10  
   19.11           (*Alice initiates a protocol run.
    20.1 --- a/src/HOL/Auth/Shared.ML	Wed Sep 17 16:40:52 1997 +0200
    20.2 +++ b/src/HOL/Auth/Shared.ML	Thu Sep 18 13:24:04 1997 +0200
    20.3 @@ -29,47 +29,48 @@
    20.4  Addsimps [keysFor_parts_initState];
    20.5  
    20.6  
    20.7 -(*** Function "sees" ***)
    20.8 -
    20.9 -(*Agents see their own shared keys!*)
   20.10 -goal thy "A ~= Spy --> Key (shrK A) : sees A evs";
   20.11 -by (induct_tac "evs" 1);
   20.12 -by (induct_tac "A" 1);
   20.13 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [sees_Cons])));
   20.14 -by (Blast_tac 1);
   20.15 -qed_spec_mp "sees_own_shrK";
   20.16 +(*** Function "spies" ***)
   20.17  
   20.18  (*Spy sees shared keys of agents!*)
   20.19 -goal thy "!!A. A: lost ==> Key (shrK A) : sees Spy evs";
   20.20 +goal thy "!!A. A: bad ==> Key (shrK A) : spies evs";
   20.21  by (induct_tac "evs" 1);
   20.22 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [sees_Cons])));
   20.23 -by (Blast_tac 1);
   20.24 -qed "Spy_sees_lost";
   20.25 +by (ALLGOALS (asm_simp_tac
   20.26 +	      (!simpset addsimps [imageI, spies_Cons]
   20.27 +	                setloop split_tac [expand_event_case, expand_if])));
   20.28 +qed "Spy_spies_bad";
   20.29  
   20.30 -AddSIs [sees_own_shrK, Spy_sees_lost];
   20.31 +AddSIs [Spy_spies_bad];
   20.32  
   20.33 -(*For not_lost_tac*)
   20.34 -goal thy "!!A. [| Crypt (shrK A) X : analz (sees Spy evs);  A: lost |] \
   20.35 -\              ==> X : analz (sees Spy evs)";
   20.36 +(*For not_bad_tac*)
   20.37 +goal thy "!!A. [| Crypt (shrK A) X : analz (spies evs);  A: bad |] \
   20.38 +\              ==> X : analz (spies evs)";
   20.39  by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 1);
   20.40 -qed "Crypt_Spy_analz_lost";
   20.41 +qed "Crypt_Spy_analz_bad";
   20.42  
   20.43  (*Prove that the agent is uncompromised by the confidentiality of 
   20.44    a component of a message she's said.*)
   20.45 -fun not_lost_tac s =
   20.46 -    case_tac ("(" ^ s ^ ") : lost") THEN'
   20.47 +fun not_bad_tac s =
   20.48 +    case_tac ("(" ^ s ^ ") : bad") THEN'
   20.49      SELECT_GOAL 
   20.50 -      (REPEAT_DETERM (dtac (Says_imp_sees_Spy RS analz.Inj) 1) THEN
   20.51 +      (REPEAT_DETERM (dtac (Says_imp_spies RS analz.Inj) 1) THEN
   20.52         REPEAT_DETERM (etac MPair_analz 1) THEN
   20.53         THEN_BEST_FIRST 
   20.54 -         (dres_inst_tac [("A", s)] Crypt_Spy_analz_lost 1 THEN assume_tac 1)
   20.55 +         (dres_inst_tac [("A", s)] Crypt_Spy_analz_bad 1 THEN assume_tac 1)
   20.56           (has_fewer_prems 1, size_of_thm)
   20.57           (Step_tac 1));
   20.58  
   20.59  
   20.60  (** Fresh keys never clash with long-term shared keys **)
   20.61  
   20.62 +(*Agents see their own shared keys!*)
   20.63 +goal thy "Key (shrK A) : initState A";
   20.64 +by (induct_tac "A" 1);
   20.65 +by (Auto_tac());
   20.66 +qed "shrK_in_initState";
   20.67 +AddIffs [shrK_in_initState];
   20.68 +
   20.69  goal thy "Key (shrK A) : used evs";
   20.70 +br initState_into_used 1;
   20.71  by (Blast_tac 1);
   20.72  qed "shrK_in_used";
   20.73  AddIffs [shrK_in_used];
   20.74 @@ -97,7 +98,7 @@
   20.75  AddIffs [Nonce_notin_initState];
   20.76  
   20.77  goal thy "Nonce N ~: used []";
   20.78 -by (simp_tac (!simpset addsimps [used_def]) 1);
   20.79 +by (simp_tac (!simpset addsimps [used_Nil]) 1);
   20.80  qed "Nonce_notin_used_empty";
   20.81  Addsimps [Nonce_notin_used_empty];
   20.82  
   20.83 @@ -105,16 +106,13 @@
   20.84  (*** Supply fresh nonces for possibility theorems. ***)
   20.85  
   20.86  (*In any trace, there is an upper bound N on the greatest nonce in use.*)
   20.87 -goalw thy [used_def] "EX N. ALL n. N<=n --> Nonce n ~: used evs";
   20.88 +goal thy "EX N. ALL n. N<=n --> Nonce n ~: used evs";
   20.89  by (induct_tac "evs" 1);
   20.90  by (res_inst_tac [("x","0")] exI 1);
   20.91 +by (ALLGOALS (asm_simp_tac
   20.92 +	      (!simpset addsimps [used_Cons]
   20.93 +			setloop split_tac [expand_event_case, expand_if])));
   20.94  by (Step_tac 1);
   20.95 -by (Full_simp_tac 1);
   20.96 -(*Inductive step*)
   20.97 -by (induct_tac "a" 1);
   20.98 -by (ALLGOALS (full_simp_tac 
   20.99 -	      (!simpset addsimps [UN_parts_sees_Says,
  20.100 -				  UN_parts_sees_Notes])));
  20.101  by (ALLGOALS (rtac (msg_Nonce_supply RS exE)));
  20.102  by (ALLGOALS (blast_tac (!claset addSEs [add_leE])));
  20.103  val lemma = result();
    21.1 --- a/src/HOL/Auth/Shared.thy	Wed Sep 17 16:40:52 1997 +0200
    21.2 +++ b/src/HOL/Auth/Shared.thy	Thu Sep 18 13:24:04 1997 +0200
    21.3 @@ -21,7 +21,7 @@
    21.4          (*Server knows all long-term keys; other agents know only their own*)
    21.5    initState_Server  "initState Server     = Key `` range shrK"
    21.6    initState_Friend  "initState (Friend i) = {Key (shrK (Friend i))}"
    21.7 -  initState_Spy     "initState Spy        = Key``shrK``lost"
    21.8 +  initState_Spy     "initState Spy        = Key``shrK``bad"
    21.9  
   21.10  
   21.11  rules
    22.1 --- a/src/HOL/Auth/TLS.ML	Wed Sep 17 16:40:52 1997 +0200
    22.2 +++ b/src/HOL/Auth/TLS.ML	Thu Sep 18 13:24:04 1997 +0200
    22.3 @@ -144,8 +144,8 @@
    22.4  
    22.5  
    22.6  (*Induction for regularity theorems.  If induction formula has the form
    22.7 -   X ~: analz (sees Spy evs) --> ... then it shortens the proof by discarding
    22.8 -   needless information about analz (insert X (sees Spy evs))  *)
    22.9 +   X ~: analz (spies evs) --> ... then it shortens the proof by discarding
   22.10 +   needless information about analz (insert X (spies evs))  *)
   22.11  fun parts_induct_tac i = 
   22.12      etac tls.induct i
   22.13      THEN 
   22.14 @@ -155,25 +155,25 @@
   22.15      ALLGOALS (asm_full_simp_tac (!simpset setloop split_tac [expand_if]));
   22.16  
   22.17  
   22.18 -(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
   22.19 +(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
   22.20      sends messages containing X! **)
   22.21  
   22.22 -(*Spy never sees another agent's private key! (unless it's lost at start)*)
   22.23 +(*Spy never sees another agent's private key! (unless it's bad at start)*)
   22.24  goal thy 
   22.25 - "!!evs. evs : tls ==> (Key (priK A) : parts (sees Spy evs)) = (A : lost)";
   22.26 + "!!evs. evs : tls ==> (Key (priK A) : parts (spies evs)) = (A : bad)";
   22.27  by (parts_induct_tac 1);
   22.28  by (Fake_parts_insert_tac 1);
   22.29  qed "Spy_see_priK";
   22.30  Addsimps [Spy_see_priK];
   22.31  
   22.32  goal thy 
   22.33 - "!!evs. evs : tls ==> (Key (priK A) : analz (sees Spy evs)) = (A : lost)";
   22.34 + "!!evs. evs : tls ==> (Key (priK A) : analz (spies evs)) = (A : bad)";
   22.35  by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
   22.36  qed "Spy_analz_priK";
   22.37  Addsimps [Spy_analz_priK];
   22.38  
   22.39 -goal thy  "!!A. [| Key (priK A) : parts (sees Spy evs);       \
   22.40 -\                  evs : tls |] ==> A:lost";
   22.41 +goal thy  "!!A. [| Key (priK A) : parts (spies evs);       \
   22.42 +\                  evs : tls |] ==> A:bad";
   22.43  by (blast_tac (!claset addDs [Spy_see_priK]) 1);
   22.44  qed "Spy_see_priK_D";
   22.45  
   22.46 @@ -187,7 +187,7 @@
   22.47    breach of security.*)
   22.48  goalw thy [certificate_def]
   22.49   "!!evs. evs : tls     \
   22.50 -\        ==> certificate B KB : parts (sees Spy evs) --> KB = pubK B";
   22.51 +\        ==> certificate B KB : parts (spies evs) --> KB = pubK B";
   22.52  by (parts_induct_tac 1);
   22.53  by (Fake_parts_insert_tac 1);
   22.54  bind_thm ("Server_cert_pubB", result() RSN (2, rev_mp));
   22.55 @@ -195,7 +195,7 @@
   22.56  
   22.57  (*Replace key KB in ClientCertKeyEx by (pubK B) *)
   22.58  val ClientCertKeyEx_tac = 
   22.59 -    forward_tac [Says_imp_sees_Spy RS parts.Inj RS 
   22.60 +    forward_tac [Says_imp_spies RS parts.Inj RS 
   22.61  		 parts.Snd RS parts.Snd RS parts.Snd RS Server_cert_pubB]
   22.62      THEN' assume_tac
   22.63      THEN' hyp_subst_tac;
   22.64 @@ -220,27 +220,27 @@
   22.65  
   22.66  (*Every Nonce that's hashed is already in past traffic.  
   22.67    This event occurs in CERTIFICATE VERIFY*)
   22.68 -goal thy "!!evs. [| Hash {|Nonce NB, X|} : parts (sees Spy evs);  \
   22.69 +goal thy "!!evs. [| Hash {|Nonce NB, X|} : parts (spies evs);  \
   22.70  \                   NB ~: range PRF;  evs : tls |]  \
   22.71 -\                ==> Nonce NB : parts (sees Spy evs)";
   22.72 +\                ==> Nonce NB : parts (spies evs)";
   22.73  by (etac rev_mp 1);
   22.74  by (etac rev_mp 1);
   22.75  by (parts_induct_tac 1);
   22.76 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees])));
   22.77 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_spies])));
   22.78  by (Fake_parts_insert_tac 1);
   22.79  (*FINISHED messages are trivial because M : range PRF*)
   22.80  by (REPEAT (Blast_tac 2));
   22.81  (*CERTIFICATE VERIFY is the only interesting case*)
   22.82 -by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
   22.83 +by (blast_tac (!claset addSEs spies_partsEs) 1);
   22.84  qed "Hash_Nonce_CV";
   22.85  
   22.86  
   22.87  goal thy "!!evs. [| Notes A {|Agent B, X|} : set evs;  evs : tls |]  \
   22.88 -\                ==> Crypt (pubK B) X : parts (sees Spy evs)";
   22.89 +\                ==> Crypt (pubK B) X : parts (spies evs)";
   22.90  by (etac rev_mp 1);
   22.91  by (analz_induct_tac 1);
   22.92  by (blast_tac (!claset addIs [parts_insertI]) 1);
   22.93 -qed "Notes_Crypt_parts_sees";
   22.94 +qed "Notes_Crypt_parts_spies";
   22.95  
   22.96  
   22.97  (*** Protocol goal: if B receives CERTIFICATE VERIFY, then A sent it ***)
   22.98 @@ -248,28 +248,28 @@
   22.99  (*B can check A's signature if he has received A's certificate.
  22.100    Perhaps B~=Spy is unnecessary, but there's no obvious proof if the first
  22.101    message is Fake.  We don't need guarantees for the Spy anyway.  We must
  22.102 -  assume A~:lost; otherwise, the Spy can forge A's signature.*)
  22.103 +  assume A~:bad; otherwise, the Spy can forge A's signature.*)
  22.104  goal thy
  22.105   "!!evs. [| X = Crypt (priK A)                                        \
  22.106  \                 (Hash{|Nonce NB, certificate B KB, Nonce PMS|});      \
  22.107 -\           evs : tls;  A ~: lost;  B ~= Spy |]                       \
  22.108 +\           evs : tls;  A ~: bad;  B ~= Spy |]                       \
  22.109  \    ==> Says B A {|Nonce NB, Number SID, Number XB, certificate B KB|}  \
  22.110  \          : set evs --> \
  22.111 -\        X : parts (sees Spy evs) --> Says A B X : set evs";
  22.112 +\        X : parts (spies evs) --> Says A B X : set evs";
  22.113  by (hyp_subst_tac 1);
  22.114  by (parts_induct_tac 1);
  22.115  by (Fake_parts_insert_tac 1);
  22.116  (*ServerHello: nonce NB cannot be in X because it's fresh!*)
  22.117  by (blast_tac (!claset addSDs [Hash_Nonce_CV]
  22.118 -	               addSEs sees_Spy_partsEs) 1);
  22.119 +	               addSEs spies_partsEs) 1);
  22.120  qed_spec_mp "TrustCertVerify";
  22.121  
  22.122  
  22.123  (*If CERTIFICATE VERIFY is present then A has chosen PMS.*)
  22.124  goal thy
  22.125   "!!evs. [| Crypt (priK A) (Hash{|Nonce NB, certificate B KB, Nonce PMS|})  \
  22.126 -\             : parts (sees Spy evs);                                \
  22.127 -\           evs : tls;  A ~: lost |]                                      \
  22.128 +\             : parts (spies evs);                                \
  22.129 +\           evs : tls;  A ~: bad |]                                      \
  22.130  \        ==> Notes A {|Agent B, Nonce PMS|} : set evs";
  22.131  be rev_mp 1;
  22.132  by (parts_induct_tac 1);
  22.133 @@ -280,8 +280,8 @@
  22.134  (*No collection of keys can help the spy get new private keys*)
  22.135  goal thy  
  22.136   "!!evs. evs : tls ==>                                    \
  22.137 -\  ALL KK. (Key(priK B) : analz (Key``KK Un (sees Spy evs))) =  \
  22.138 -\            (priK B : KK | B : lost)";
  22.139 +\  ALL KK. (Key(priK B) : analz (Key``KK Un (spies evs))) =  \
  22.140 +\            (priK B : KK | B : bad)";
  22.141  by (etac tls.induct 1);
  22.142  by (ALLGOALS
  22.143      (asm_simp_tac (analz_image_keys_ss
  22.144 @@ -309,14 +309,14 @@
  22.145  goal thy  
  22.146   "!!evs. evs : tls ==>                                 \
  22.147  \    ALL KK. KK <= range sessionK -->           \
  22.148 -\            (Nonce N : analz (Key``KK Un (sees Spy evs))) = \
  22.149 -\            (Nonce N : analz (sees Spy evs))";
  22.150 +\            (Nonce N : analz (Key``KK Un (spies evs))) = \
  22.151 +\            (Nonce N : analz (spies evs))";
  22.152  by (etac tls.induct 1);
  22.153  by (ClientCertKeyEx_tac 6);
  22.154  by (REPEAT_FIRST (resolve_tac [allI, impI]));
  22.155  by (REPEAT_FIRST (rtac lemma));
  22.156  writeln"SLOW simplification: 55 secs??";
  22.157 -(*ClientCertKeyEx is to blame, causing case splits for A, B: lost*)
  22.158 +(*ClientCertKeyEx is to blame, causing case splits for A, B: bad*)
  22.159  by (ALLGOALS
  22.160      (asm_simp_tac (analz_image_keys_ss 
  22.161  		   addsimps [range_sessionkeys_not_priK, 
  22.162 @@ -337,16 +337,16 @@
  22.163  Addsimps [no_Notes_A_PRF];
  22.164  
  22.165  
  22.166 -goal thy "!!evs. [| Nonce (PRF (PMS,NA,NB)) : parts (sees Spy evs);  \
  22.167 +goal thy "!!evs. [| Nonce (PRF (PMS,NA,NB)) : parts (spies evs);  \
  22.168  \                   evs : tls |]  \
  22.169 -\                ==> Nonce PMS : parts (sees Spy evs)";
  22.170 +\                ==> Nonce PMS : parts (spies evs)";
  22.171  by (etac rev_mp 1);
  22.172  by (parts_induct_tac 1);
  22.173 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees])));
  22.174 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_spies])));
  22.175  by (Fake_parts_insert_tac 1);
  22.176  (*Six others, all trivial or by freshness*)
  22.177 -by (REPEAT (blast_tac (!claset addSDs [Notes_Crypt_parts_sees]
  22.178 -                               addSEs sees_Spy_partsEs) 1));
  22.179 +by (REPEAT (blast_tac (!claset addSDs [Notes_Crypt_parts_spies]
  22.180 +                               addSEs spies_partsEs) 1));
  22.181  qed "MS_imp_PMS";
  22.182  AddSDs [MS_imp_PMS];
  22.183  
  22.184 @@ -360,13 +360,13 @@
  22.185    Converse doesn't hold; betraying M doesn't force the keys to be sent!*)
  22.186  
  22.187  goal thy 
  22.188 - "!!evs. [| Nonce M ~: analz (sees Spy evs);  evs : tls |]   \
  22.189 -\        ==> Key (sessionK(b,NA,NB,M)) ~: parts (sees Spy evs)";
  22.190 + "!!evs. [| Nonce M ~: analz (spies evs);  evs : tls |]   \
  22.191 +\        ==> Key (sessionK(b,NA,NB,M)) ~: parts (spies evs)";
  22.192  by (etac rev_mp 1);
  22.193  by (analz_induct_tac 1);
  22.194  (*SpyKeys*)
  22.195  by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 3);
  22.196 -by (blast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj]) 3);
  22.197 +by (blast_tac (!claset addDs [Says_imp_spies RS analz.Inj]) 3);
  22.198  (*Fake*) 
  22.199  by (spy_analz_tac 2);
  22.200  (*Base*)
  22.201 @@ -385,17 +385,17 @@
  22.202    They are NOT suitable as safe elim rules.*)
  22.203  
  22.204  goal thy 
  22.205 - "!!evs. [| Nonce PMS ~: parts (sees Spy evs);  evs : tls |]             \
  22.206 -\  ==> Crypt (sessionK(b, Na, Nb, PRF(PMS,NA,NB))) Y ~: parts (sees Spy evs)";
  22.207 + "!!evs. [| Nonce PMS ~: parts (spies evs);  evs : tls |]             \
  22.208 +\  ==> Crypt (sessionK(b, Na, Nb, PRF(PMS,NA,NB))) Y ~: parts (spies evs)";
  22.209  by (etac rev_mp 1);
  22.210  by (analz_induct_tac 1);
  22.211  (*Fake*)
  22.212 -by (asm_simp_tac (!simpset addsimps [parts_insert_sees]) 2);
  22.213 +by (asm_simp_tac (!simpset addsimps [parts_insert_spies]) 2);
  22.214  by (Fake_parts_insert_tac 2);
  22.215  (*Base, ClientFinished, ServerFinished: trivial, e.g. by freshness*)
  22.216  by (REPEAT 
  22.217 -    (blast_tac (!claset addSDs [Notes_Crypt_parts_sees]
  22.218 -                        addSEs sees_Spy_partsEs) 1));
  22.219 +    (blast_tac (!claset addSDs [Notes_Crypt_parts_spies]
  22.220 +                        addSEs spies_partsEs) 1));
  22.221  qed "Crypt_sessionK_notin_parts";
  22.222  
  22.223  Addsimps [Crypt_sessionK_notin_parts];
  22.224 @@ -415,9 +415,9 @@
  22.225  
  22.226  (*PMS determines B.  Proof borrowed from NS_Public/unique_NA and from Yahalom*)
  22.227  goal thy 
  22.228 - "!!evs. [| Nonce PMS ~: analz (sees Spy evs);  evs : tls |]   \
  22.229 + "!!evs. [| Nonce PMS ~: analz (spies evs);  evs : tls |]   \
  22.230  \        ==> EX B'. ALL B.   \
  22.231 -\              Crypt (pubK B) (Nonce PMS) : parts (sees Spy evs) --> B=B'";
  22.232 +\              Crypt (pubK B) (Nonce PMS) : parts (spies evs) --> B=B'";
  22.233  by (etac rev_mp 1);
  22.234  by (parts_induct_tac 1);
  22.235  by (Fake_parts_insert_tac 1);
  22.236 @@ -429,9 +429,9 @@
  22.237  val lemma = result();
  22.238  
  22.239  goal thy 
  22.240 - "!!evs. [| Crypt(pubK B)  (Nonce PMS) : parts (sees Spy evs); \
  22.241 -\           Crypt(pubK B') (Nonce PMS) : parts (sees Spy evs); \
  22.242 -\           Nonce PMS ~: analz (sees Spy evs);                 \
  22.243 + "!!evs. [| Crypt(pubK B)  (Nonce PMS) : parts (spies evs); \
  22.244 +\           Crypt(pubK B') (Nonce PMS) : parts (spies evs); \
  22.245 +\           Nonce PMS ~: analz (spies evs);                 \
  22.246  \           evs : tls |]                                          \
  22.247  \        ==> B=B'";
  22.248  by (prove_unique_tac lemma 1);
  22.249 @@ -440,7 +440,7 @@
  22.250  
  22.251  (*In A's internal Note, PMS determines A and B.*)
  22.252  goal thy 
  22.253 - "!!evs. [| Nonce PMS ~: analz (sees Spy evs);  evs : tls |]            \
  22.254 + "!!evs. [| Nonce PMS ~: analz (spies evs);  evs : tls |]            \
  22.255  \ ==> EX A' B'. ALL A B.                                                   \
  22.256  \        Notes A {|Agent B, Nonce PMS|} : set evs --> A=A' & B=B'";
  22.257  by (etac rev_mp 1);
  22.258 @@ -448,13 +448,13 @@
  22.259  by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
  22.260  (*ClientCertKeyEx: if PMS is fresh, then it can't appear in Notes A X.*)
  22.261  by (expand_case_tac "PMS = ?y" 1 THEN
  22.262 -    blast_tac (!claset addSDs [Notes_Crypt_parts_sees] addSEs partsEs) 1);
  22.263 +    blast_tac (!claset addSDs [Notes_Crypt_parts_spies] addSEs partsEs) 1);
  22.264  val lemma = result();
  22.265  
  22.266  goal thy 
  22.267   "!!evs. [| Notes A  {|Agent B,  Nonce PMS|} : set evs;  \
  22.268  \           Notes A' {|Agent B', Nonce PMS|} : set evs;  \
  22.269 -\           Nonce PMS ~: analz (sees Spy evs);      \
  22.270 +\           Nonce PMS ~: analz (spies evs);      \
  22.271  \           evs : tls |]                               \
  22.272  \        ==> A=A' & B=B'";
  22.273  by (prove_unique_tac lemma 1);
  22.274 @@ -464,20 +464,20 @@
  22.275  
  22.276  (*If A sends ClientCertKeyEx to an honest B, then the PMS will stay secret.*)
  22.277  goal thy
  22.278 - "!!evs. [| evs : tls;  A ~: lost;  B ~: lost |]           \
  22.279 + "!!evs. [| evs : tls;  A ~: bad;  B ~: bad |]           \
  22.280  \        ==> Notes A {|Agent B, Nonce PMS|} : set evs  -->   \
  22.281 -\            Nonce PMS ~: analz (sees Spy evs)";
  22.282 +\            Nonce PMS ~: analz (spies evs)";
  22.283  by (analz_induct_tac 1);   (*30 seconds???*)
  22.284  (*ClientAccepts and ServerAccepts: because PMS ~: range PRF*)
  22.285  by (REPEAT (fast_tac (!claset addss (!simpset)) 6));
  22.286  (*ServerHello and ClientCertKeyEx: mostly freshness reasoning*)
  22.287  by (REPEAT (blast_tac (!claset addSEs partsEs
  22.288 -			       addDs  [Notes_Crypt_parts_sees,
  22.289 +			       addDs  [Notes_Crypt_parts_spies,
  22.290  				       impOfSubs analz_subset_parts,
  22.291 -				       Says_imp_sees_Spy RS analz.Inj]) 4));
  22.292 +				       Says_imp_spies RS analz.Inj]) 4));
  22.293  (*ClientHello*)
  22.294 -by (blast_tac (!claset addSDs [Notes_Crypt_parts_sees]
  22.295 -                               addSEs sees_Spy_partsEs) 3);
  22.296 +by (blast_tac (!claset addSDs [Notes_Crypt_parts_spies]
  22.297 +                               addSEs spies_partsEs) 3);
  22.298  (*SpyKeys*)
  22.299  by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 2);
  22.300  by (fast_tac (!claset addss (!simpset)) 2);
  22.301 @@ -492,27 +492,27 @@
  22.302  (*If A sends ClientCertKeyEx to an honest B, then the MASTER SECRET
  22.303    will stay secret.*)
  22.304  goal thy
  22.305 - "!!evs. [| evs : tls;  A ~: lost;  B ~: lost |]           \
  22.306 + "!!evs. [| evs : tls;  A ~: bad;  B ~: bad |]           \
  22.307  \        ==> Notes A {|Agent B, Nonce PMS|} : set evs  -->   \
  22.308 -\            Nonce (PRF(PMS,NA,NB)) ~: analz (sees Spy evs)";
  22.309 +\            Nonce (PRF(PMS,NA,NB)) ~: analz (spies evs)";
  22.310  by (analz_induct_tac 1);   (*35 seconds*)
  22.311  (*ClientAccepts and ServerAccepts: because PMS was already visible*)
  22.312  by (REPEAT (blast_tac (!claset addDs [Spy_not_see_PMS, 
  22.313 -				      Says_imp_sees_Spy RS analz.Inj,
  22.314 -				      Notes_imp_sees_Spy RS analz.Inj]) 6));
  22.315 +				      Says_imp_spies RS analz.Inj,
  22.316 +				      Notes_imp_spies RS analz.Inj]) 6));
  22.317  (*ClientHello*)
  22.318  by (Blast_tac 3);
  22.319  (*SpyKeys: by secrecy of the PMS, Spy cannot make the MS*)
  22.320  by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 2);
  22.321  by (blast_tac (!claset addSDs [Spy_not_see_PMS, 
  22.322 -			       Says_imp_sees_Spy RS analz.Inj]) 2);
  22.323 +			       Says_imp_spies RS analz.Inj]) 2);
  22.324  (*Fake*)
  22.325  by (spy_analz_tac 1);
  22.326  (*ServerHello and ClientCertKeyEx: mostly freshness reasoning*)
  22.327  by (REPEAT (blast_tac (!claset addSEs partsEs
  22.328 -			       addDs  [Notes_Crypt_parts_sees,
  22.329 +			       addDs  [Notes_Crypt_parts_spies,
  22.330  				       impOfSubs analz_subset_parts,
  22.331 -				       Says_imp_sees_Spy RS analz.Inj]) 1));
  22.332 +				       Says_imp_spies RS analz.Inj]) 1));
  22.333  bind_thm ("Spy_not_see_MS", result() RSN (2, rev_mp));
  22.334  
  22.335  
  22.336 @@ -528,16 +528,16 @@
  22.337  \                        Nonce NA, Number XA, Agent A,    \
  22.338  \                        Nonce NB, Number XB, Agent B|}); \
  22.339  \           M = PRF(PMS,NA,NB);                           \
  22.340 -\           evs : tls;  A ~: lost;  B ~: lost |]          \
  22.341 +\           evs : tls;  A ~: bad;  B ~: bad |]          \
  22.342  \        ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
  22.343 -\        X : parts (sees Spy evs) --> Says B A X : set evs";
  22.344 +\        X : parts (spies evs) --> Says B A X : set evs";
  22.345  by (hyp_subst_tac 1);
  22.346  by (analz_induct_tac 1);	(*16 seconds*)
  22.347  (*ClientCertKeyEx*)
  22.348  by (Blast_tac 2);
  22.349  (*Fake: the Spy doesn't have the critical session key!*)
  22.350  by (REPEAT (rtac impI 1));
  22.351 -by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(sees Spy evsa)" 1);
  22.352 +by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
  22.353  by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS, 
  22.354  				     not_parts_not_analz]) 2);
  22.355  by (Fake_parts_insert_tac 1);
  22.356 @@ -550,10 +550,10 @@
  22.357    that B sends his message to A.  If CLIENT KEY EXCHANGE were augmented
  22.358    to bind A's identity with M, then we could replace A' by A below.*)
  22.359  goal thy
  22.360 - "!!evs. [| evs : tls;  A ~: lost;  B ~: lost;                 \
  22.361 + "!!evs. [| evs : tls;  A ~: bad;  B ~: bad;                 \
  22.362  \           M = PRF(PMS,NA,NB) |]            \
  22.363  \        ==> Notes A {|Agent B, Nonce PMS|} : set evs -->              \
  22.364 -\            Crypt (serverK(Na,Nb,M)) Y : parts (sees Spy evs)  -->  \
  22.365 +\            Crypt (serverK(Na,Nb,M)) Y : parts (spies evs)  -->  \
  22.366  \            (EX A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) : set evs)";
  22.367  by (hyp_subst_tac 1);
  22.368  by (analz_induct_tac 1);	(*12 seconds*)
  22.369 @@ -561,7 +561,7 @@
  22.370  (*ClientCertKeyEx*)
  22.371  by (Blast_tac 2);
  22.372  (*Fake: the Spy doesn't have the critical session key!*)
  22.373 -by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(sees Spy evsa)" 1);
  22.374 +by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
  22.375  by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS, 
  22.376  				     not_parts_not_analz]) 2);
  22.377  by (Fake_parts_insert_tac 1);
  22.378 @@ -570,11 +570,11 @@
  22.379  (*...otherwise delete induction hyp and use unicity of PMS.*)
  22.380  by (thin_tac "?PP-->?QQ" 1);
  22.381  by (Step_tac 1);
  22.382 -by (subgoal_tac "Nonce PMS ~: analz(sees Spy evsSF)" 1);
  22.383 +by (subgoal_tac "Nonce PMS ~: analz(spies evsSF)" 1);
  22.384  by (asm_simp_tac (!simpset addsimps [Spy_not_see_PMS]) 2);
  22.385  by (blast_tac (!claset addSEs [MPair_parts]
  22.386 -		       addDs  [Notes_Crypt_parts_sees,
  22.387 -			       Says_imp_sees_Spy RS parts.Inj,
  22.388 +		       addDs  [Notes_Crypt_parts_spies,
  22.389 +			       Says_imp_spies RS parts.Inj,
  22.390  			       unique_PMS]) 1);
  22.391  qed_spec_mp "TrustServerMsg";
  22.392  
  22.393 @@ -585,22 +585,22 @@
  22.394       CLIENT FINISHED, then B can then check the quoted values XA, XB, etc.
  22.395  ***)
  22.396  goal thy
  22.397 - "!!evs. [| evs : tls;  A ~: lost;  B ~: lost |]                         \
  22.398 + "!!evs. [| evs : tls;  A ~: bad;  B ~: bad |]                         \
  22.399  \  ==> Notes A {|Agent B, Nonce PMS|} : set evs -->                  \
  22.400 -\      Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y : parts (sees Spy evs) -->  \
  22.401 +\      Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y : parts (spies evs) -->  \
  22.402  \      Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs";
  22.403  by (analz_induct_tac 1);	(*13 seconds*)
  22.404  by (REPEAT_FIRST (rtac impI));
  22.405  (*ClientCertKeyEx*)
  22.406  by (Blast_tac 2);
  22.407  (*Fake: the Spy doesn't have the critical session key!*)
  22.408 -by (subgoal_tac "Key (clientK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(sees Spy evsa)" 1);
  22.409 +by (subgoal_tac "Key (clientK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
  22.410  by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS, 
  22.411  				     not_parts_not_analz]) 2);
  22.412  by (Fake_parts_insert_tac 1);
  22.413  (*ClientFinished.  If the message is old then apply induction hypothesis...*)
  22.414  by (step_tac (!claset delrules [conjI]) 1);
  22.415 -by (subgoal_tac "Nonce PMS ~: analz (sees Spy evsCF)" 1);
  22.416 +by (subgoal_tac "Nonce PMS ~: analz (spies evsCF)" 1);
  22.417  by (asm_simp_tac (!simpset addsimps [Spy_not_see_PMS]) 2);
  22.418  by (blast_tac (!claset addSEs [MPair_parts]
  22.419  		       addDs  [Notes_unique_PMS]) 1);
  22.420 @@ -618,8 +618,8 @@
  22.421  \           Says A'' B (Crypt (priK A)                                    \
  22.422  \                       (Hash{|Nonce NB, certificate B KB, Nonce PMS|}))  \
  22.423  \             : set evs;                                                  \
  22.424 -\        evs : tls;  A ~: lost;  B ~: lost |]                             \
  22.425 +\        evs : tls;  A ~: bad;  B ~: bad |]                             \
  22.426  \     ==> Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs";
  22.427  by (blast_tac (!claset addSIs [TrustClientMsg, UseCertVerify]
  22.428 -                       addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
  22.429 +                       addDs  [Says_imp_spies RS parts.Inj]) 1);
  22.430  qed "AuthClientFinished";
    23.1 --- a/src/HOL/Auth/TLS.thy	Wed Sep 17 16:40:52 1997 +0200
    23.2 +++ b/src/HOL/Auth/TLS.thy	Thu Sep 18 13:24:04 1997 +0200
    23.3 @@ -83,7 +83,7 @@
    23.4  
    23.5      Fake (*The spy, an active attacker, MAY say anything he CAN say.*)
    23.6           "[| evs: tls;  B ~= Spy;  
    23.7 -             X: synth (analz (sees Spy evs)) |]
    23.8 +             X: synth (analz (spies evs)) |]
    23.9            ==> Says Spy B X # evs : tls"
   23.10  
   23.11      SpyKeys (*The spy may apply PRF, clientK & serverK to available nonces*)
    24.1 --- a/src/HOL/Auth/WooLam.ML	Wed Sep 17 16:40:52 1997 +0200
    24.2 +++ b/src/HOL/Auth/WooLam.ML	Thu Sep 18 13:24:04 1997 +0200
    24.3 @@ -41,39 +41,39 @@
    24.4  
    24.5  (** For reasoning about the encrypted portion of messages **)
    24.6  
    24.7 -goal thy "!!evs. Says A' B X : set evs ==> X : analz (sees Spy evs)";
    24.8 -by (etac (Says_imp_sees_Spy RS analz.Inj) 1);
    24.9 -qed "WL4_analz_sees_Spy";
   24.10 +goal thy "!!evs. Says A' B X : set evs ==> X : analz (spies evs)";
   24.11 +by (etac (Says_imp_spies RS analz.Inj) 1);
   24.12 +qed "WL4_analz_spies";
   24.13  
   24.14 -bind_thm ("WL4_parts_sees_Spy",
   24.15 -          WL4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
   24.16 +bind_thm ("WL4_parts_spies",
   24.17 +          WL4_analz_spies RS (impOfSubs analz_subset_parts));
   24.18  
   24.19 -(*For proving the easier theorems about X ~: parts (sees Spy evs) *)
   24.20 +(*For proving the easier theorems about X ~: parts (spies evs) *)
   24.21  fun parts_induct_tac i = 
   24.22      etac woolam.induct i  THEN 
   24.23 -    forward_tac [WL4_parts_sees_Spy] (i+5)  THEN
   24.24 +    forward_tac [WL4_parts_spies] (i+5)  THEN
   24.25      prove_simple_subgoals_tac 1;
   24.26  
   24.27  
   24.28 -(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
   24.29 +(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
   24.30      sends messages containing X! **)
   24.31  
   24.32 -(*Spy never sees another agent's shared key! (unless it's lost at start)*)
   24.33 +(*Spy never sees another agent's shared key! (unless it's bad at start)*)
   24.34  goal thy 
   24.35 - "!!evs. evs : woolam ==> (Key (shrK A) : parts (sees Spy evs)) = (A : lost)";
   24.36 + "!!evs. evs : woolam ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
   24.37  by (parts_induct_tac 1);
   24.38  by (Fake_parts_insert_tac 1);
   24.39  qed "Spy_see_shrK";
   24.40  Addsimps [Spy_see_shrK];
   24.41  
   24.42  goal thy 
   24.43 - "!!evs. evs : woolam ==> (Key (shrK A) : analz (sees Spy evs)) = (A : lost)";
   24.44 + "!!evs. evs : woolam ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
   24.45  by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
   24.46  qed "Spy_analz_shrK";
   24.47  Addsimps [Spy_analz_shrK];
   24.48  
   24.49 -goal thy  "!!A. [| Key (shrK A) : parts (sees Spy evs);       \
   24.50 -\                  evs : woolam |] ==> A:lost";
   24.51 +goal thy  "!!A. [| Key (shrK A) : parts (spies evs);       \
   24.52 +\                  evs : woolam |] ==> A:bad";
   24.53  by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
   24.54  qed "Spy_see_shrK_D";
   24.55  
   24.56 @@ -88,8 +88,8 @@
   24.57  
   24.58  (*If the encrypted message appears then it originated with Alice*)
   24.59  goal thy 
   24.60 - "!!evs. [| A ~: lost;  evs : woolam |]                        \
   24.61 -\        ==> Crypt (shrK A) (Nonce NB) : parts (sees Spy evs)  \
   24.62 + "!!evs. [| A ~: bad;  evs : woolam |]                        \
   24.63 +\        ==> Crypt (shrK A) (Nonce NB) : parts (spies evs)  \
   24.64  \            --> (EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs)";
   24.65  by (parts_induct_tac 1);
   24.66  by (Fake_parts_insert_tac 1);
   24.67 @@ -100,13 +100,13 @@
   24.68    Alice, then she originated that certificate.  But we DO NOT know that B
   24.69    ever saw it: the Spy may have rerouted the message to the Server.*)
   24.70  goal thy 
   24.71 - "!!evs. [| A ~: lost;  evs : woolam;                      \
   24.72 + "!!evs. [| A ~: bad;  evs : woolam;                      \
   24.73  \           Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|} \
   24.74  \            : set evs |]                                  \
   24.75  \        ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs";
   24.76  by (blast_tac (!claset addSIs [NB_Crypt_imp_Alice_msg]
   24.77                        addSEs [MPair_parts]
   24.78 -                      addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
   24.79 +                      addDs  [Says_imp_spies RS parts.Inj]) 1);
   24.80  qed "Server_trusts_WL4";
   24.81  
   24.82  
   24.83 @@ -126,8 +126,8 @@
   24.84  
   24.85  (*If the encrypted message appears then it originated with the Server!*)
   24.86  goal thy 
   24.87 - "!!evs. [| B ~: lost;  evs : woolam |]                             \
   24.88 -\        ==> Crypt (shrK B) {|Agent A, NB|} : parts (sees Spy evs)  \
   24.89 + "!!evs. [| B ~: bad;  evs : woolam |]                             \
   24.90 +\        ==> Crypt (shrK B) {|Agent A, NB|} : parts (spies evs)  \
   24.91  \        --> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs";
   24.92  by (parts_induct_tac 1);
   24.93  by (Fake_parts_insert_tac 1);
   24.94 @@ -137,10 +137,10 @@
   24.95    sent the same message.*)
   24.96  goal thy 
   24.97   "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, NB|}) : set evs;         \
   24.98 -\           B ~: lost;  evs : woolam |]                                  \
   24.99 +\           B ~: bad;  evs : woolam |]                                  \
  24.100  \        ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs";
  24.101  by (blast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
  24.102 -                      addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
  24.103 +                      addDs  [Says_imp_spies RS parts.Inj]) 1);
  24.104  qed "B_got_WL5";
  24.105  
  24.106  (*Guarantee for B.  If B gets the Server's certificate then A has encrypted
  24.107 @@ -149,7 +149,7 @@
  24.108    the Server via the Spy.*)
  24.109  goal thy 
  24.110   "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, Nonce NB|}): set evs; \
  24.111 -\           A ~: lost;  B ~: lost;  evs : woolam  |]                  \
  24.112 +\           A ~: bad;  B ~: bad;  evs : woolam  |]                  \
  24.113  \        ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs";
  24.114  by (blast_tac (!claset addIs  [Server_trusts_WL4]
  24.115                        addSDs [B_got_WL5 RS Server_sent_WL5]) 1);
  24.116 @@ -169,8 +169,8 @@
  24.117  
  24.118  (**CANNOT be proved because A doesn't know where challenges come from...
  24.119  goal thy 
  24.120 - "!!evs. [| A ~: lost;  B ~= Spy;  evs : woolam |]           \
  24.121 -\    ==> Crypt (shrK A) (Nonce NB) : parts (sees Spy evs) &  \
  24.122 + "!!evs. [| A ~: bad;  B ~= Spy;  evs : woolam |]           \
  24.123 +\    ==> Crypt (shrK A) (Nonce NB) : parts (spies evs) &  \
  24.124  \        Says B A (Nonce NB) : set evs                       \
  24.125  \        --> Says A B (Crypt (shrK A) (Nonce NB)) : set evs";
  24.126  by (parts_induct_tac 1);
    25.1 --- a/src/HOL/Auth/WooLam.thy	Wed Sep 17 16:40:52 1997 +0200
    25.2 +++ b/src/HOL/Auth/WooLam.thy	Thu Sep 18 13:24:04 1997 +0200
    25.3 @@ -26,7 +26,7 @@
    25.4             invent new nonces here, but he can also use NS1.  Common to
    25.5             all similar protocols.*)
    25.6      Fake "[| evs: woolam;  B ~= Spy;  
    25.7 -             X: synth (analz (sees Spy evs)) |]
    25.8 +             X: synth (analz (spies evs)) |]
    25.9            ==> Says Spy B X  # evs : woolam"
   25.10  
   25.11           (*Alice initiates a protocol run*)
   25.12 @@ -49,7 +49,7 @@
   25.13           (*Bob forwards Alice's response to the Server.  NOTE: usually
   25.14             the messages are shown in chronological order, for clarity.
   25.15             But here, exchanging the two events would cause the lemma
   25.16 -           WL4_analz_sees_Spy to pick up the wrong assumption!*)
   25.17 +           WL4_analz_spies to pick up the wrong assumption!*)
   25.18      WL4  "[| evs4: woolam;  B ~= Server;  
   25.19               Says A'  B X         : set evs4;
   25.20               Says A'' B (Agent A) : set evs4 |]
    26.1 --- a/src/HOL/Auth/Yahalom.ML	Wed Sep 17 16:40:52 1997 +0200
    26.2 +++ b/src/HOL/Auth/Yahalom.ML	Thu Sep 18 13:24:04 1997 +0200
    26.3 @@ -44,42 +44,42 @@
    26.4  
    26.5  (*Lets us treat YM4 using a similar argument as for the Fake case.*)
    26.6  goal thy "!!evs. Says S A {|Crypt (shrK A) Y, X|} : set evs ==> \
    26.7 -\                X : analz (sees Spy evs)";
    26.8 -by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    26.9 -qed "YM4_analz_sees_Spy";
   26.10 +\                X : analz (spies evs)";
   26.11 +by (blast_tac (!claset addSDs [Says_imp_spies RS analz.Inj]) 1);
   26.12 +qed "YM4_analz_spies";
   26.13  
   26.14 -bind_thm ("YM4_parts_sees_Spy",
   26.15 -          YM4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
   26.16 +bind_thm ("YM4_parts_spies",
   26.17 +          YM4_analz_spies RS (impOfSubs analz_subset_parts));
   26.18  
   26.19  (*Relates to both YM4 and Oops*)
   26.20  goal thy "!!evs. Says S A {|Crypt (shrK A) {|B,K,NA,NB|}, X|} : set evs ==> \
   26.21 -\                K : parts (sees Spy evs)";
   26.22 +\                K : parts (spies evs)";
   26.23  by (blast_tac (!claset addSEs partsEs
   26.24 -                      addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
   26.25 -qed "YM4_Key_parts_sees_Spy";
   26.26 +                      addSDs [Says_imp_spies RS parts.Inj]) 1);
   26.27 +qed "YM4_Key_parts_spies";
   26.28  
   26.29 -(*For proving the easier theorems about X ~: parts (sees Spy evs).*)
   26.30 -fun parts_sees_tac i = 
   26.31 -    forward_tac [YM4_Key_parts_sees_Spy] (i+6) THEN
   26.32 -    forward_tac [YM4_parts_sees_Spy] (i+5)     THEN
   26.33 +(*For proving the easier theorems about X ~: parts (spies evs).*)
   26.34 +fun parts_spies_tac i = 
   26.35 +    forward_tac [YM4_Key_parts_spies] (i+6) THEN
   26.36 +    forward_tac [YM4_parts_spies] (i+5)     THEN
   26.37      prove_simple_subgoals_tac  i;
   26.38  
   26.39  (*Induction for regularity theorems.  If induction formula has the form
   26.40 -   X ~: analz (sees Spy evs) --> ... then it shortens the proof by discarding
   26.41 -   needless information about analz (insert X (sees Spy evs))  *)
   26.42 +   X ~: analz (spies evs) --> ... then it shortens the proof by discarding
   26.43 +   needless information about analz (insert X (spies evs))  *)
   26.44  fun parts_induct_tac i = 
   26.45      etac yahalom.induct i
   26.46      THEN 
   26.47      REPEAT (FIRSTGOAL analz_mono_contra_tac)
   26.48 -    THEN  parts_sees_tac i;
   26.49 +    THEN  parts_spies_tac i;
   26.50  
   26.51  
   26.52 -(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
   26.53 +(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
   26.54      sends messages containing X! **)
   26.55  
   26.56 -(*Spy never sees another agent's shared key! (unless it's lost at start)*)
   26.57 +(*Spy never sees another agent's shared key! (unless it's bad at start)*)
   26.58  goal thy 
   26.59 - "!!evs. evs : yahalom ==> (Key (shrK A) : parts (sees Spy evs)) = (A : lost)";
   26.60 + "!!evs. evs : yahalom ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
   26.61  by (parts_induct_tac 1);
   26.62  by (Fake_parts_insert_tac 1);
   26.63  by (Blast_tac 1);
   26.64 @@ -87,13 +87,13 @@
   26.65  Addsimps [Spy_see_shrK];
   26.66  
   26.67  goal thy 
   26.68 - "!!evs. evs : yahalom ==> (Key (shrK A) : analz (sees Spy evs)) = (A : lost)";
   26.69 + "!!evs. evs : yahalom ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
   26.70  by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
   26.71  qed "Spy_analz_shrK";
   26.72  Addsimps [Spy_analz_shrK];
   26.73  
   26.74 -goal thy  "!!A. [| Key (shrK A) : parts (sees Spy evs);       \
   26.75 -\                  evs : yahalom |] ==> A:lost";
   26.76 +goal thy  "!!A. [| Key (shrK A) : parts (spies evs);       \
   26.77 +\                  evs : yahalom |] ==> A:bad";
   26.78  by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
   26.79  qed "Spy_see_shrK_D";
   26.80  
   26.81 @@ -103,10 +103,10 @@
   26.82  
   26.83  (*Nobody can have used non-existent keys!  Needed to apply analz_insert_Key*)
   26.84  goal thy "!!evs. evs : yahalom ==>          \
   26.85 -\         Key K ~: used evs --> K ~: keysFor (parts (sees Spy evs))";
   26.86 +\         Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
   26.87  by (parts_induct_tac 1);
   26.88  (*YM4: Key K is not fresh!*)
   26.89 -by (blast_tac (!claset addSEs sees_Spy_partsEs) 3);
   26.90 +by (blast_tac (!claset addSEs spies_partsEs) 3);
   26.91  (*YM3*)
   26.92  by (Blast_tac 2);
   26.93  (*Fake*)
   26.94 @@ -139,8 +139,8 @@
   26.95  
   26.96  
   26.97  (*For proofs involving analz.*)
   26.98 -val analz_sees_tac = 
   26.99 -    forward_tac [YM4_analz_sees_Spy] 6 THEN
  26.100 +val analz_spies_tac = 
  26.101 +    forward_tac [YM4_analz_spies] 6 THEN
  26.102      forward_tac [Says_Server_message_form] 7 THEN
  26.103      assume_tac 7 THEN REPEAT ((etac exE ORELSE' hyp_subst_tac) 7);
  26.104  
  26.105 @@ -148,8 +148,8 @@
  26.106  (****
  26.107   The following is to prove theorems of the form
  26.108  
  26.109 -  Key K : analz (insert (Key KAB) (sees Spy evs)) ==>
  26.110 -  Key K : analz (sees Spy evs)
  26.111 +  Key K : analz (insert (Key KAB) (spies evs)) ==>
  26.112 +  Key K : analz (spies evs)
  26.113  
  26.114   A more general formula must be proved inductively.
  26.115  ****)
  26.116 @@ -159,10 +159,10 @@
  26.117  goal thy  
  26.118   "!!evs. evs : yahalom ==>                                 \
  26.119  \  ALL K KK. KK <= Compl (range shrK) -->                       \
  26.120 -\            (Key K : analz (Key``KK Un (sees Spy evs))) = \
  26.121 -\            (K : KK | Key K : analz (sees Spy evs))";
  26.122 +\            (Key K : analz (Key``KK Un (spies evs))) = \
  26.123 +\            (K : KK | Key K : analz (spies evs))";
  26.124  by (etac yahalom.induct 1);
  26.125 -by analz_sees_tac;
  26.126 +by analz_spies_tac;
  26.127  by (REPEAT_FIRST (resolve_tac [allI, impI]));
  26.128  by (REPEAT_FIRST (rtac analz_image_freshK_lemma));
  26.129  by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
  26.130 @@ -174,8 +174,8 @@
  26.131  
  26.132  goal thy
  26.133   "!!evs. [| evs : yahalom;  KAB ~: range shrK |] ==>             \
  26.134 -\        Key K : analz (insert (Key KAB) (sees Spy evs)) =       \
  26.135 -\        (K = KAB | Key K : analz (sees Spy evs))";
  26.136 +\        Key K : analz (insert (Key KAB) (spies evs)) =       \
  26.137 +\        (K = KAB | Key K : analz (spies evs))";
  26.138  by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
  26.139  qed "analz_insert_freshK";
  26.140  
  26.141 @@ -197,17 +197,15 @@
  26.142  by (expand_case_tac "K = ?y" 1);
  26.143  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
  26.144  (*...we assume X is a recent message and handle this case by contradiction*)
  26.145 -by (blast_tac (!claset addSEs sees_Spy_partsEs
  26.146 +by (blast_tac (!claset addSEs spies_partsEs
  26.147                        delrules [conjI]    (*no split-up to 4 subgoals*)) 1);
  26.148  val lemma = result();
  26.149  
  26.150  goal thy 
  26.151 -"!!evs. [| Says Server A                                            \
  26.152 -\           {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|}        \
  26.153 -\           : set evs;                                              \
  26.154 -\          Says Server A'                                           \
  26.155 -\           {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|}   \
  26.156 -\           : set evs;                                              \
  26.157 +"!!evs. [| Says Server A                                                 \
  26.158 +\            {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} : set evs; \
  26.159 +\          Says Server A'                                                \
  26.160 +\            {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|} : set evs; \
  26.161  \          evs : yahalom |]                                    \
  26.162  \       ==> A=A' & B=B' & na=na' & nb=nb'";
  26.163  by (prove_unique_tac lemma 1);
  26.164 @@ -217,15 +215,15 @@
  26.165  (** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
  26.166  
  26.167  goal thy 
  26.168 - "!!evs. [| A ~: lost;  B ~: lost;  evs : yahalom |]         \
  26.169 + "!!evs. [| A ~: bad;  B ~: bad;  evs : yahalom |]         \
  26.170  \        ==> Says Server A                                        \
  26.171  \              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
  26.172  \                Crypt (shrK B) {|Agent A, Key K|}|}              \
  26.173  \             : set evs -->                                       \
  26.174  \            Says A Spy {|na, nb, Key K|} ~: set evs -->          \
  26.175 -\            Key K ~: analz (sees Spy evs)";
  26.176 +\            Key K ~: analz (spies evs)";
  26.177  by (etac yahalom.induct 1);
  26.178 -by analz_sees_tac;
  26.179 +by analz_spies_tac;
  26.180  by (ALLGOALS
  26.181      (asm_simp_tac 
  26.182       (!simpset addsimps [analz_insert_eq, analz_insert_freshK]
  26.183 @@ -234,7 +232,7 @@
  26.184  by (blast_tac (!claset addDs [unique_session_keys]) 3);
  26.185  (*YM3*)
  26.186  by (blast_tac (!claset delrules [impCE]
  26.187 -                       addSEs sees_Spy_partsEs
  26.188 +                       addSEs spies_partsEs
  26.189                         addIs [impOfSubs analz_subset_parts]) 2);
  26.190  (*Fake*) 
  26.191  by (spy_analz_tac 1);
  26.192 @@ -248,8 +246,8 @@
  26.193  \                Crypt (shrK B) {|Agent A, Key K|}|}              \
  26.194  \             : set evs;                                          \
  26.195  \           Says A Spy {|na, nb, Key K|} ~: set evs;              \
  26.196 -\           A ~: lost;  B ~: lost;  evs : yahalom |]         \
  26.197 -\        ==> Key K ~: analz (sees Spy evs)";
  26.198 +\           A ~: bad;  B ~: bad;  evs : yahalom |]         \
  26.199 +\        ==> Key K ~: analz (spies evs)";
  26.200  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
  26.201  by (blast_tac (!claset addSEs [lemma]) 1);
  26.202  qed "Spy_not_see_encrypted_key";
  26.203 @@ -259,9 +257,8 @@
  26.204  
  26.205  (*If the encrypted message appears then it originated with the Server*)
  26.206  goal thy
  26.207 - "!!evs. [| Crypt (shrK A) {|Agent B, Key K, na, nb|}                  \
  26.208 -\            : parts (sees Spy evs);                              \
  26.209 -\           A ~: lost;  evs : yahalom |]                          \
  26.210 + "!!evs. [| Crypt (shrK A) {|Agent B, Key K, na, nb|} : parts (spies evs); \
  26.211 +\           A ~: bad;  evs : yahalom |]                          \
  26.212  \         ==> Says Server A                                            \
  26.213  \              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},            \
  26.214  \                Crypt (shrK B) {|Agent A, Key K|}|}                   \
  26.215 @@ -277,8 +274,8 @@
  26.216  (*B knows, by the first part of A's message, that the Server distributed 
  26.217    the key for A and B.  But this part says nothing about nonces.*)
  26.218  goal thy 
  26.219 - "!!evs. [| Crypt (shrK B) {|Agent A, Key K|} : parts (sees Spy evs);   \
  26.220 -\           B ~: lost;  evs : yahalom |]                                \
  26.221 + "!!evs. [| Crypt (shrK B) {|Agent A, Key K|} : parts (spies evs);   \
  26.222 +\           B ~: bad;  evs : yahalom |]                                \
  26.223  \        ==> EX NA NB. Says Server A                                    \
  26.224  \                        {|Crypt (shrK A) {|Agent B, Key K,             \
  26.225  \                                           Nonce NA, Nonce NB|},       \
  26.226 @@ -296,8 +293,8 @@
  26.227    Secrecy of NB is crucial.*)
  26.228  goal thy 
  26.229   "!!evs. evs : yahalom                                             \
  26.230 -\        ==> Nonce NB ~: analz (sees Spy evs) -->                  \
  26.231 -\            Crypt K (Nonce NB) : parts (sees Spy evs) -->         \
  26.232 +\        ==> Nonce NB ~: analz (spies evs) -->                  \
  26.233 +\            Crypt K (Nonce NB) : parts (spies evs) -->         \
  26.234  \            (EX A B NA. Says Server A                             \
  26.235  \                        {|Crypt (shrK A) {|Agent B, Key K,        \
  26.236  \                                  Nonce NA, Nonce NB|},           \
  26.237 @@ -310,9 +307,9 @@
  26.238  (*YM4*)
  26.239  by (Step_tac 1);
  26.240  (*A is uncompromised because NB is secure*)
  26.241 -by (not_lost_tac "A" 1);
  26.242 +by (not_bad_tac "A" 1);
  26.243  (*A's certificate guarantees the existence of the Server message*)
  26.244 -by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS
  26.245 +by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj RS parts.Fst RS
  26.246  			      A_trusts_YM3]) 1);
  26.247  bind_thm ("B_trusts_YM4_newK", result() RS mp RSN (2, rev_mp));
  26.248  
  26.249 @@ -342,7 +339,7 @@
  26.250    (with respect to a given trace). *)
  26.251  goalw thy [KeyWithNonce_def]
  26.252   "!!evs. Key K ~: used evs ==> ~ KeyWithNonce K NB evs";
  26.253 -by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
  26.254 +by (blast_tac (!claset addSEs spies_partsEs) 1);
  26.255  qed "fresh_not_KeyWithNonce";
  26.256  
  26.257  (*The Server message associates K with NB' and therefore not with any 
  26.258 @@ -374,10 +371,10 @@
  26.259   "!!evs. evs : yahalom ==>                                         \
  26.260  \        (ALL KK. KK <= Compl (range shrK) -->                          \
  26.261  \             (ALL K: KK. ~ KeyWithNonce K NB evs)   -->                \
  26.262 -\             (Nonce NB : analz (Key``KK Un (sees Spy evs))) =     \
  26.263 -\             (Nonce NB : analz (sees Spy evs)))";
  26.264 +\             (Nonce NB : analz (Key``KK Un (spies evs))) =     \
  26.265 +\             (Nonce NB : analz (spies evs)))";
  26.266  by (etac yahalom.induct 1);
  26.267 -by analz_sees_tac;
  26.268 +by analz_spies_tac;
  26.269  by (REPEAT_FIRST (resolve_tac [impI RS allI]));
  26.270  by (REPEAT_FIRST (rtac lemma));
  26.271  (*For Oops, simplification proves NBa~=NB.  By Says_Server_KeyWithNonce,
  26.272 @@ -395,8 +392,8 @@
  26.273  (*Fake*) 
  26.274  by (spy_analz_tac 1);
  26.275  (*YM4*)  (** LEVEL 7 **)
  26.276 -by (not_lost_tac "A" 1);
  26.277 -by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1
  26.278 +by (not_bad_tac "A" 1);
  26.279 +by (dtac (Says_imp_spies RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1
  26.280      THEN REPEAT (assume_tac 1));
  26.281  by (blast_tac (!claset addIs [KeyWithNonceI]) 1);
  26.282  qed_spec_mp "Nonce_secrecy";
  26.283 @@ -410,8 +407,8 @@
  26.284  \            {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB'|}, X|}    \
  26.285  \           : set evs;                                                    \
  26.286  \           NB ~= NB';  KAB ~: range shrK;  evs : yahalom |]         \
  26.287 -\        ==> (Nonce NB : analz (insert (Key KAB) (sees Spy evs))) =  \
  26.288 -\            (Nonce NB : analz (sees Spy evs))";
  26.289 +\        ==> (Nonce NB : analz (insert (Key KAB) (spies evs))) =  \
  26.290 +\            (Nonce NB : analz (spies evs))";
  26.291  by (asm_simp_tac (analz_image_freshK_ss addsimps 
  26.292  		  [Nonce_secrecy, Says_Server_KeyWithNonce]) 1);
  26.293  qed "single_Nonce_secrecy";
  26.294 @@ -422,8 +419,8 @@
  26.295  goal thy 
  26.296   "!!evs. evs : yahalom ==>                                            \
  26.297  \   EX NA' A' B'. ALL NA A B.                                              \
  26.298 -\      Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts(sees Spy evs) \
  26.299 -\      --> B ~: lost --> NA = NA' & A = A' & B = B'";
  26.300 +\      Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts(spies evs) \
  26.301 +\      --> B ~: bad --> NA = NA' & A = A' & B = B'";
  26.302  by (parts_induct_tac 1);
  26.303  (*Fake*)
  26.304  by (REPEAT (etac (exI RSN (2,exE)) 1)   (*stripping EXs makes proof faster*)
  26.305 @@ -432,31 +429,29 @@
  26.306  (*YM2: creation of new Nonce.  Move assertion into global context*)
  26.307  by (expand_case_tac "nb = ?y" 1);
  26.308  by (REPEAT (resolve_tac [exI, conjI, impI, refl] 1));
  26.309 -by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
  26.310 +by (blast_tac (!claset addSEs spies_partsEs) 1);
  26.311  val lemma = result();
  26.312  
  26.313  goal thy 
  26.314 - "!!evs.[| Crypt (shrK B) {|Agent A, Nonce NA, nb|}        \
  26.315 -\                  : parts (sees Spy evs);            \
  26.316 -\          Crypt (shrK B') {|Agent A', Nonce NA', nb|}     \
  26.317 -\                  : parts (sees Spy evs);            \
  26.318 -\          evs : yahalom;  B ~: lost;  B' ~: lost |]  \
  26.319 + "!!evs.[| Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts (spies evs); \
  26.320 +\          Crypt (shrK B') {|Agent A', Nonce NA', nb|} : parts (spies evs); \
  26.321 +\          evs : yahalom;  B ~: bad;  B' ~: bad |]  \
  26.322  \        ==> NA' = NA & A' = A & B' = B";
  26.323  by (prove_unique_tac lemma 1);
  26.324  qed "unique_NB";
  26.325  
  26.326  
  26.327  (*Variant useful for proving secrecy of NB: the Says... form allows 
  26.328 -  not_lost_tac to remove the assumption B' ~: lost.*)
  26.329 +  not_bad_tac to remove the assumption B' ~: bad.*)
  26.330  goal thy 
  26.331   "!!evs.[| Says C D   {|X,  Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}    \
  26.332 -\            : set evs;          B ~: lost;                               \
  26.333 +\            : set evs;          B ~: bad;                               \
  26.334  \          Says C' D' {|X', Crypt (shrK B') {|Agent A', Nonce NA', nb|}|} \
  26.335  \            : set evs;                                                   \
  26.336 -\          nb ~: analz (sees Spy evs);  evs : yahalom |]        \
  26.337 +\          nb ~: analz (spies evs);  evs : yahalom |]        \
  26.338  \        ==> NA' = NA & A' = A & B' = B";
  26.339 -by (not_lost_tac "B'" 1);
  26.340 -by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
  26.341 +by (not_bad_tac "B'" 1);
  26.342 +by (blast_tac (!claset addSDs [Says_imp_spies RS parts.Inj]
  26.343                         addSEs [MPair_parts]
  26.344                         addDs  [unique_NB]) 1);
  26.345  qed "Says_unique_NB";
  26.346 @@ -465,15 +460,13 @@
  26.347  (** A nonce value is never used both as NA and as NB **)
  26.348  
  26.349  goal thy 
  26.350 - "!!evs. [| B ~: lost;  evs : yahalom  |]            \
  26.351 -\ ==> Nonce NB ~: analz (sees Spy evs) -->           \
  26.352 -\     Crypt (shrK B') {|Agent A', Nonce NB, nb'|}    \
  26.353 -\       : parts(sees Spy evs)                        \
  26.354 -\ --> Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|} \
  26.355 -\       ~: parts(sees Spy evs)";
  26.356 + "!!evs. [| B ~: bad;  evs : yahalom  |]            \
  26.357 +\ ==> Nonce NB ~: analz (spies evs) -->           \
  26.358 +\     Crypt (shrK B') {|Agent A', Nonce NB, nb'|} : parts(spies evs) --> \
  26.359 +\     Crypt (shrK B)  {|Agent A, Nonce NA, Nonce NB|} ~: parts(spies evs)";
  26.360  by (parts_induct_tac 1);
  26.361  by (Fake_parts_insert_tac 1);
  26.362 -by (blast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj]
  26.363 +by (blast_tac (!claset addDs [Says_imp_spies RS analz.Inj]
  26.364                         addSIs [parts_insertI]
  26.365                         addSEs partsEs) 1);
  26.366  bind_thm ("no_nonce_YM1_YM2", result() RS mp RSN (2,rev_mp) RSN (2,rev_notE));
  26.367 @@ -495,37 +488,37 @@
  26.368  
  26.369  (*A vital theorem for B, that nonce NB remains secure from the Spy.*)
  26.370  goal thy 
  26.371 - "!!evs. [| A ~: lost;  B ~: lost;  evs : yahalom |]  \
  26.372 + "!!evs. [| A ~: bad;  B ~: bad;  evs : yahalom |]  \
  26.373  \ ==> Says B Server                                                    \
  26.374  \          {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \
  26.375  \     : set evs -->                                                    \
  26.376  \     (ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs) -->     \
  26.377 -\     Nonce NB ~: analz (sees Spy evs)";
  26.378 +\     Nonce NB ~: analz (spies evs)";
  26.379  by (etac yahalom.induct 1);
  26.380 -by analz_sees_tac;
  26.381 +by analz_spies_tac;
  26.382  by (ALLGOALS
  26.383      (asm_simp_tac 
  26.384       (!simpset addsimps [analz_insert_eq, analz_insert_freshK]
  26.385                 setloop split_tac [expand_if])));
  26.386  (*Prove YM3 by showing that no NB can also be an NA*)
  26.387 -by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj]
  26.388 +by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj]
  26.389  	               addSEs [MPair_parts]
  26.390  		       addDs  [no_nonce_YM1_YM2, Says_unique_NB]) 4
  26.391      THEN flexflex_tac);
  26.392  (*YM2: similar freshness reasoning*) 
  26.393  by (blast_tac (!claset addSEs partsEs
  26.394 -		       addDs  [Says_imp_sees_Spy RS analz.Inj,
  26.395 +		       addDs  [Says_imp_spies RS analz.Inj,
  26.396  			       impOfSubs analz_subset_parts]) 3);
  26.397  (*YM1: NB=NA is impossible anyway, but NA is secret because it is fresh!*)
  26.398  by (blast_tac (!claset addSIs [parts_insertI]
  26.399 -                       addSEs sees_Spy_partsEs) 2);
  26.400 +                       addSEs spies_partsEs) 2);
  26.401  (*Fake*)
  26.402  by (spy_analz_tac 1);
  26.403  (** LEVEL 7: YM4 and Oops remain **)
  26.404  (*YM4: key K is visible to Spy, contradicting session key secrecy theorem*) 
  26.405  by (REPEAT (Safe_step_tac 1));
  26.406 -by (not_lost_tac "Aa" 1);
  26.407 -by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1);
  26.408 +by (not_bad_tac "Aa" 1);
  26.409 +by (dtac (Says_imp_spies RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1);
  26.410  by (forward_tac [Says_Server_message_form] 3);
  26.411  by (forward_tac [Says_Server_imp_YM2] 4);
  26.412  by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, exE, disjE]));
  26.413 @@ -544,7 +537,7 @@
  26.414  (*case NB ~= NBa*)
  26.415  by (asm_simp_tac (!simpset addsimps [single_Nonce_secrecy]) 1);
  26.416  by (blast_tac (!claset addSEs [MPair_parts]
  26.417 -		       addDs  [Says_imp_sees_Spy RS parts.Inj, 
  26.418 +		       addDs  [Says_imp_spies RS parts.Inj, 
  26.419  			       no_nonce_YM1_YM2 (*to prove NB~=NAa*) ]) 1);
  26.420  bind_thm ("Spy_not_see_NB", result() RSN(2,rev_mp) RSN(2,rev_mp));
  26.421  
  26.422 @@ -561,14 +554,14 @@
  26.423  \           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
  26.424  \                       Crypt K (Nonce NB)|} : set evs;                     \
  26.425  \           ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs;         \
  26.426 -\           A ~: lost;  B ~: lost;  evs : yahalom |]       \
  26.427 +\           A ~: bad;  B ~: bad;  evs : yahalom |]       \
  26.428  \         ==> Says Server A                                                 \
  26.429  \                     {|Crypt (shrK A) {|Agent B, Key K,                    \
  26.430  \                               Nonce NA, Nonce NB|},                       \
  26.431  \                       Crypt (shrK B) {|Agent A, Key K|}|}                 \
  26.432  \               : set evs";
  26.433  by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
  26.434 -by (etac (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1 THEN
  26.435 +by (etac (Says_imp_spies RS parts.Inj RS MPair_parts) 1 THEN
  26.436      dtac B_trusts_YM4_shrK 1);
  26.437  by (dtac B_trusts_YM4_newK 3);
  26.438  by (REPEAT_FIRST (eresolve_tac [asm_rl, exE]));
  26.439 @@ -584,9 +577,8 @@
  26.440  (*The encryption in message YM2 tells us it cannot be faked.*)
  26.441  goal thy 
  26.442   "!!evs. evs : yahalom                                            \
  26.443 -\  ==> Crypt (shrK B) {|Agent A, Nonce NA, nb|}                   \
  26.444 -\        : parts (sees Spy evs) -->                               \
  26.445 -\      B ~: lost -->                                              \
  26.446 +\  ==> Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts (spies evs) --> \
  26.447 +\      B ~: bad -->                                              \
  26.448  \      Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}  \
  26.449  \         : set evs";
  26.450  by (parts_induct_tac 1);
  26.451 @@ -598,7 +590,7 @@
  26.452   "!!evs. evs : yahalom                                                      \
  26.453  \  ==> Says Server A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
  26.454  \         : set evs -->                                                     \
  26.455 -\      B ~: lost -->                                                        \
  26.456 +\      B ~: bad -->                                                        \
  26.457  \      Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}  \
  26.458  \                 : set evs";
  26.459  by (etac yahalom.induct 1);
  26.460 @@ -606,7 +598,7 @@
  26.461  (*YM4*)
  26.462  by (Blast_tac 2);
  26.463  (*YM3*)
  26.464 -by (best_tac (!claset addSDs [B_Said_YM2, Says_imp_sees_Spy RS parts.Inj]
  26.465 +by (best_tac (!claset addSDs [B_Said_YM2, Says_imp_spies RS parts.Inj]
  26.466  		      addSEs [MPair_parts]) 1);
  26.467  val lemma = result() RSN (2, rev_mp) RS mp |> standard;
  26.468  
  26.469 @@ -614,11 +606,11 @@
  26.470  goal thy
  26.471   "!!evs. [| Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
  26.472  \             : set evs;                                                    \
  26.473 -\           A ~: lost;  B ~: lost;  evs : yahalom |]                        \
  26.474 +\           A ~: bad;  B ~: bad;  evs : yahalom |]                        \
  26.475  \   ==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \
  26.476  \         : set evs";
  26.477  by (blast_tac (!claset addSDs [A_trusts_YM3, lemma]
  26.478 -		       addEs sees_Spy_partsEs) 1);
  26.479 +		       addEs spies_partsEs) 1);
  26.480  qed "YM3_auth_B_to_A";
  26.481  
  26.482  
  26.483 @@ -629,12 +621,11 @@
  26.484    NB matters for freshness.*)  
  26.485  goal thy 
  26.486   "!!evs. evs : yahalom                                             \
  26.487 -\        ==> Key K ~: analz (sees Spy evs) -->                     \
  26.488 -\            Crypt K (Nonce NB) : parts (sees Spy evs) -->         \
  26.489 -\            Crypt (shrK B) {|Agent A, Key K|}                     \
  26.490 -\              : parts (sees Spy evs) -->                          \
  26.491 -\            B ~: lost -->                                         \
  26.492 -\             (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs)";
  26.493 +\        ==> Key K ~: analz (spies evs) -->                     \
  26.494 +\            Crypt K (Nonce NB) : parts (spies evs) -->         \
  26.495 +\            Crypt (shrK B) {|Agent A, Key K|} : parts (spies evs) --> \
  26.496 +\            B ~: bad -->                                         \
  26.497 +\            (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs)";
  26.498  by (parts_induct_tac 1);
  26.499  (*Fake*)
  26.500  by (Fake_parts_insert_tac 1);
  26.501 @@ -643,10 +634,10 @@
  26.502  (*YM4: was Crypt K (Nonce NB) the very last message?  If not, use ind. hyp.*)
  26.503  by (asm_simp_tac (!simpset addsimps [ex_disj_distrib]) 1);
  26.504  (*yes: apply unicity of session keys*)
  26.505 -by (not_lost_tac "Aa" 1);
  26.506 +by (not_bad_tac "Aa" 1);
  26.507  by (blast_tac (!claset addSEs [MPair_parts]
  26.508                         addSDs [A_trusts_YM3, B_trusts_YM4_shrK]
  26.509 -		       addDs  [Says_imp_sees_Spy RS parts.Inj,
  26.510 +		       addDs  [Says_imp_spies RS parts.Inj,
  26.511  			       unique_session_keys]) 1);
  26.512  val lemma = normalize_thm [RSspec, RSmp] (result()) |> standard;
  26.513  
  26.514 @@ -660,14 +651,14 @@
  26.515  \           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
  26.516  \                       Crypt K (Nonce NB)|} : set evs;                     \
  26.517  \           (ALL NA k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs);    \
  26.518 -\           A ~: lost;  B ~: lost;  evs : yahalom |]       \
  26.519 +\           A ~: bad;  B ~: bad;  evs : yahalom |]       \
  26.520  \        ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
  26.521  by (dtac B_trusts_YM4 1);
  26.522  by (REPEAT_FIRST (eresolve_tac [asm_rl, spec]));
  26.523 -by (etac (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1);
  26.524 +by (etac (Says_imp_spies RS parts.Inj RS MPair_parts) 1);
  26.525  by (rtac lemma 1);
  26.526  by (rtac Spy_not_see_encrypted_key 2);
  26.527  by (REPEAT_FIRST assume_tac);
  26.528  by (blast_tac (!claset addSEs [MPair_parts]
  26.529 -	       	       addDs [Says_imp_sees_Spy RS parts.Inj]) 1);
  26.530 +	       	       addDs [Says_imp_spies RS parts.Inj]) 1);
  26.531  qed_spec_mp "YM4_imp_A_Said_YM3";
    27.1 --- a/src/HOL/Auth/Yahalom.thy	Wed Sep 17 16:40:52 1997 +0200
    27.2 +++ b/src/HOL/Auth/Yahalom.thy	Thu Sep 18 13:24:04 1997 +0200
    27.3 @@ -22,7 +22,7 @@
    27.4             invent new nonces here, but he can also use NS1.  Common to
    27.5             all similar protocols.*)
    27.6      Fake "[| evs: yahalom;  B ~= Spy;  
    27.7 -             X: synth (analz (sees Spy evs)) |]
    27.8 +             X: synth (analz (spies evs)) |]
    27.9            ==> Says Spy B X  # evs : yahalom"
   27.10  
   27.11           (*Alice initiates a protocol run*)
    28.1 --- a/src/HOL/Auth/Yahalom2.ML	Wed Sep 17 16:40:52 1997 +0200
    28.2 +++ b/src/HOL/Auth/Yahalom2.ML	Thu Sep 18 13:24:04 1997 +0200
    28.3 @@ -44,42 +44,42 @@
    28.4  
    28.5  (*Lets us treat YM4 using a similar argument as for the Fake case.*)
    28.6  goal thy "!!evs. Says S A {|NB, Crypt (shrK A) Y, X|} : set evs ==> \
    28.7 -\                X : analz (sees Spy evs)";
    28.8 -by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    28.9 -qed "YM4_analz_sees_Spy";
   28.10 +\                X : analz (spies evs)";
   28.11 +by (blast_tac (!claset addSDs [Says_imp_spies RS analz.Inj]) 1);
   28.12 +qed "YM4_analz_spies";
   28.13  
   28.14 -bind_thm ("YM4_parts_sees_Spy",
   28.15 -          YM4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
   28.16 +bind_thm ("YM4_parts_spies",
   28.17 +          YM4_analz_spies RS (impOfSubs analz_subset_parts));
   28.18  
   28.19  (*Relates to both YM4 and Oops*)
   28.20  goal thy "!!evs. Says S A {|NB, Crypt (shrK A) {|B,K,NA|}, X|} : set evs ==> \
   28.21 -\                K : parts (sees Spy evs)";
   28.22 +\                K : parts (spies evs)";
   28.23  by (blast_tac (!claset addSEs partsEs
   28.24 -                       addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
   28.25 -qed "YM4_Key_parts_sees_Spy";
   28.26 +                       addSDs [Says_imp_spies RS parts.Inj]) 1);
   28.27 +qed "YM4_Key_parts_spies";
   28.28  
   28.29 -(*For proving the easier theorems about X ~: parts (sees Spy evs).*)
   28.30 -fun parts_sees_tac i = 
   28.31 -    forward_tac [YM4_Key_parts_sees_Spy] (i+6) THEN
   28.32 -    forward_tac [YM4_parts_sees_Spy] (i+5)     THEN
   28.33 +(*For proving the easier theorems about X ~: parts (spies evs).*)
   28.34 +fun parts_spies_tac i = 
   28.35 +    forward_tac [YM4_Key_parts_spies] (i+6) THEN
   28.36 +    forward_tac [YM4_parts_spies] (i+5)     THEN
   28.37      prove_simple_subgoals_tac  i;
   28.38  
   28.39  (*Induction for regularity theorems.  If induction formula has the form
   28.40 -   X ~: analz (sees Spy evs) --> ... then it shortens the proof by discarding
   28.41 -   needless information about analz (insert X (sees Spy evs))  *)
   28.42 +   X ~: analz (spies evs) --> ... then it shortens the proof by discarding
   28.43 +   needless information about analz (insert X (spies evs))  *)
   28.44  fun parts_induct_tac i = 
   28.45      etac yahalom.induct i
   28.46      THEN 
   28.47      REPEAT (FIRSTGOAL analz_mono_contra_tac)
   28.48 -    THEN  parts_sees_tac i;
   28.49 +    THEN  parts_spies_tac i;
   28.50  
   28.51  
   28.52 -(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
   28.53 +(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
   28.54      sends messages containing X! **)
   28.55  
   28.56 -(*Spy never sees another agent's shared key! (unless it's lost at start)*)
   28.57 +(*Spy never sees another agent's shared key! (unless it's bad at start)*)
   28.58  goal thy 
   28.59 - "!!evs. evs : yahalom ==> (Key (shrK A) : parts (sees Spy evs)) = (A : lost)";
   28.60 + "!!evs. evs : yahalom ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
   28.61  by (parts_induct_tac 1);
   28.62  by (Fake_parts_insert_tac 1);
   28.63  by (Blast_tac 1);
   28.64 @@ -87,13 +87,13 @@
   28.65  Addsimps [Spy_see_shrK];
   28.66  
   28.67  goal thy 
   28.68 - "!!evs. evs : yahalom ==> (Key (shrK A) : analz (sees Spy evs)) = (A : lost)";
   28.69 + "!!evs. evs : yahalom ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
   28.70  by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
   28.71  qed "Spy_analz_shrK";
   28.72  Addsimps [Spy_analz_shrK];
   28.73  
   28.74 -goal thy  "!!A. [| Key (shrK A) : parts (sees Spy evs);       \
   28.75 -\                  evs : yahalom |] ==> A:lost";
   28.76 +goal thy  "!!A. [| Key (shrK A) : parts (spies evs);       \
   28.77 +\                  evs : yahalom |] ==> A:bad";
   28.78  by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
   28.79  qed "Spy_see_shrK_D";
   28.80  
   28.81 @@ -103,10 +103,10 @@
   28.82  
   28.83  (*Nobody can have used non-existent keys!  Needed to apply analz_insert_Key*)
   28.84  goal thy "!!evs. evs : yahalom ==>          \
   28.85 -\         Key K ~: used evs --> K ~: keysFor (parts (sees Spy evs))";
   28.86 +\         Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
   28.87  by (parts_induct_tac 1);
   28.88  (*YM4: Key K is not fresh!*)
   28.89 -by (blast_tac (!claset addSEs sees_Spy_partsEs) 3);
   28.90 +by (blast_tac (!claset addSEs spies_partsEs) 3);
   28.91  (*YM3*)
   28.92  by (blast_tac (!claset addss (!simpset)) 2);
   28.93  (*Fake*)
   28.94 @@ -137,8 +137,8 @@
   28.95  
   28.96  
   28.97  (*For proofs involving analz.*)
   28.98 -val analz_sees_tac = 
   28.99 -    dtac YM4_analz_sees_Spy 6 THEN
  28.100 +val analz_spies_tac = 
  28.101 +    dtac YM4_analz_spies 6 THEN
  28.102      forward_tac [Says_Server_message_form] 7 THEN
  28.103      assume_tac 7 THEN
  28.104      REPEAT ((etac conjE ORELSE' hyp_subst_tac) 7);
  28.105 @@ -147,8 +147,8 @@
  28.106  (****
  28.107   The following is to prove theorems of the form
  28.108  
  28.109 -          Key K : analz (insert (Key KAB) (sees Spy evs)) ==>
  28.110 -          Key K : analz (sees Spy evs)
  28.111 +          Key K : analz (insert (Key KAB) (spies evs)) ==>
  28.112 +          Key K : analz (spies evs)
  28.113  
  28.114   A more general formula must be proved inductively.
  28.115  
  28.116 @@ -159,10 +159,10 @@
  28.117  goal thy  
  28.118   "!!evs. evs : yahalom ==>                                  \
  28.119  \  ALL K KK. KK <= Compl (range shrK) -->                   \
  28.120 -\            (Key K : analz (Key``KK Un (sees Spy evs))) =  \
  28.121 -\            (K : KK | Key K : analz (sees Spy evs))";
  28.122 +\            (Key K : analz (Key``KK Un (spies evs))) =  \
  28.123 +\            (K : KK | Key K : analz (spies evs))";
  28.124  by (etac yahalom.induct 1);
  28.125 -by analz_sees_tac;
  28.126 +by analz_spies_tac;
  28.127  by (REPEAT_FIRST (resolve_tac [allI, impI]));
  28.128  by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
  28.129  by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
  28.130 @@ -174,8 +174,8 @@
  28.131  
  28.132  goal thy
  28.133   "!!evs. [| evs : yahalom;  KAB ~: range shrK |] ==>        \
  28.134 -\        Key K : analz (insert (Key KAB) (sees Spy evs)) =  \
  28.135 -\        (K = KAB | Key K : analz (sees Spy evs))";
  28.136 +\        Key K : analz (insert (Key KAB) (spies evs)) =  \
  28.137 +\        (K = KAB | Key K : analz (spies evs))";
  28.138  by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
  28.139  qed "analz_insert_freshK";
  28.140  
  28.141 @@ -195,18 +195,16 @@
  28.142  by (expand_case_tac "K = ?y" 1);
  28.143  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
  28.144  (*...we assume X is a recent message and handle this case by contradiction*)
  28.145 -by (blast_tac (!claset addSEs sees_Spy_partsEs
  28.146 +by (blast_tac (!claset addSEs spies_partsEs
  28.147                         delrules [conjI]    (*prevent split-up into 4 subgoals*)
  28.148                         addss (!simpset addsimps [parts_insertI])) 1);
  28.149  val lemma = result();
  28.150  
  28.151  goal thy 
  28.152  "!!evs. [| Says Server A                                            \
  28.153 -\           {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|}        \
  28.154 -\           : set evs;                                              \
  28.155 +\            {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|} : set evs; \
  28.156  \          Says Server A'                                           \
  28.157 -\           {|nb', Crypt (shrK A') {|Agent B', Key K, na'|}, X'|}   \
  28.158 -\           : set evs;                                              \
  28.159 +\            {|nb', Crypt (shrK A') {|Agent B', Key K, na'|}, X'|} : set evs; \
  28.160  \          evs : yahalom |]                                         \
  28.161  \       ==> A=A' & B=B' & na=na' & nb=nb'";
  28.162  by (prove_unique_tac lemma 1);
  28.163 @@ -216,16 +214,16 @@
  28.164  (** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
  28.165  
  28.166  goal thy 
  28.167 - "!!evs. [| A ~: lost;  B ~: lost;  A ~= B;                     \
  28.168 + "!!evs. [| A ~: bad;  B ~: bad;  A ~= B;                     \
  28.169  \           evs : yahalom |]                                    \
  28.170  \        ==> Says Server A                                      \
  28.171  \              {|nb, Crypt (shrK A) {|Agent B, Key K, na|},     \
  28.172  \                    Crypt (shrK B) {|nb, Key K, Agent A|}|}    \
  28.173  \             : set evs -->                                     \
  28.174  \            Says A Spy {|na, nb, Key K|} ~: set evs -->        \
  28.175 -\            Key K ~: analz (sees Spy evs)";
  28.176 +\            Key K ~: analz (spies evs)";
  28.177  by (etac yahalom.induct 1);
  28.178 -by analz_sees_tac;
  28.179 +by analz_spies_tac;
  28.180  by (ALLGOALS
  28.181      (asm_simp_tac 
  28.182       (!simpset addsimps [analz_insert_eq, analz_insert_freshK]
  28.183 @@ -234,7 +232,7 @@
  28.184  by (blast_tac (!claset addDs [unique_session_keys]) 3);
  28.185  (*YM3*)
  28.186  by (blast_tac (!claset delrules [impCE]
  28.187 -                       addSEs sees_Spy_partsEs
  28.188 +                       addSEs spies_partsEs
  28.189                         addIs [impOfSubs analz_subset_parts]) 2);
  28.190  (*Fake*) 
  28.191  by (spy_analz_tac 1);
  28.192 @@ -248,8 +246,8 @@
  28.193  \                    Crypt (shrK B) {|nb, Key K, Agent A|}|} \
  28.194  \           : set evs;                                       \
  28.195  \           Says A Spy {|na, nb, Key K|} ~: set evs;         \
  28.196 -\           A ~: lost;  B ~: lost;  evs : yahalom |]         \
  28.197 -\        ==> Key K ~: analz (sees Spy evs)";
  28.198 +\           A ~: bad;  B ~: bad;  evs : yahalom |]         \
  28.199 +\        ==> Key K ~: analz (spies evs)";
  28.200  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
  28.201  by (blast_tac (!claset addSEs [lemma]) 1);
  28.202  qed "Spy_not_see_encrypted_key";
  28.203 @@ -261,8 +259,8 @@
  28.204    May now apply Spy_not_see_encrypted_key, subject to its conditions.*)
  28.205  goal thy
  28.206   "!!evs. [| Crypt (shrK A) {|Agent B, Key K, na|}                      \
  28.207 -\            : parts (sees Spy evs);                                   \
  28.208 -\           A ~: lost;  evs : yahalom |]                               \
  28.209 +\            : parts (spies evs);                                   \
  28.210 +\           A ~: bad;  evs : yahalom |]                               \
  28.211  \         ==> EX nb. Says Server A                                     \
  28.212  \                      {|nb, Crypt (shrK A) {|Agent B, Key K, na|},    \
  28.213  \                            Crypt (shrK B) {|nb, Key K, Agent A|}|}   \
  28.214 @@ -279,9 +277,8 @@
  28.215  (*B knows, by the first part of A's message, that the Server distributed 
  28.216    the key for A and B, and has associated it with NB. *)
  28.217  goal thy 
  28.218 - "!!evs. [| Crypt (shrK B) {|Nonce NB, Key K, Agent A|}              \
  28.219 -\            : parts (sees Spy evs);                                 \
  28.220 -\           B ~: lost;  evs : yahalom |]                             \
  28.221 + "!!evs. [| Crypt (shrK B) {|Nonce NB, Key K, Agent A|} : parts (spies evs); \
  28.222 +\           B ~: bad;  evs : yahalom |]                             \
  28.223  \        ==> EX NA. Says Server A                                    \
  28.224  \                    {|Nonce NB,                                     \
  28.225  \                      Crypt (shrK A) {|Agent B, Key K, Nonce NA|},  \
  28.226 @@ -303,13 +300,13 @@
  28.227  goal thy 
  28.228   "!!evs. [| Says A' B {|Crypt (shrK B) {|Nonce NB, Key K, Agent A|}, X|} \
  28.229  \             : set evs;                                                 \
  28.230 -\           A ~: lost;  B ~: lost;  evs : yahalom |]                     \
  28.231 +\           A ~: bad;  B ~: bad;  evs : yahalom |]                     \
  28.232  \        ==> EX NA. Says Server A                                        \
  28.233  \                    {|Nonce NB,                                         \
  28.234  \                      Crypt (shrK A) {|Agent B, Key K, Nonce NA|},      \
  28.235  \                      Crypt (shrK B) {|Nonce NB, Key K, Agent A|}|}     \
  28.236  \                   : set evs";
  28.237 -by (etac (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1);
  28.238 +by (etac (Says_imp_spies RS parts.Inj RS MPair_parts) 1);
  28.239  by (blast_tac (!claset addSDs [B_trusts_YM4_shrK]) 1);
  28.240  qed "B_trusts_YM4";
  28.241  
  28.242 @@ -320,8 +317,8 @@
  28.243  (*The encryption in message YM2 tells us it cannot be faked.*)
  28.244  goal thy 
  28.245   "!!evs. evs : yahalom                                                  \
  28.246 -\  ==> Crypt (shrK B) {|Agent A, Nonce NA|} : parts (sees Spy evs) -->  \
  28.247 -\      B ~: lost -->                                                    \
  28.248 +\  ==> Crypt (shrK B) {|Agent A, Nonce NA|} : parts (spies evs) -->  \
  28.249 +\      B ~: bad -->                                                    \
  28.250  \      (EX NB. Says B Server {|Agent B, Nonce NB,                       \
  28.251  \                              Crypt (shrK B) {|Agent A, Nonce NA|}|}   \
  28.252  \         : set evs)";
  28.253 @@ -336,7 +333,7 @@
  28.254   "!!evs. evs : yahalom                                                   \
  28.255  \  ==> Says Server A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \
  28.256  \         : set evs -->                                                  \
  28.257 -\      B ~: lost -->                                                     \
  28.258 +\      B ~: bad -->                                                     \
  28.259  \      (EX nb'. Says B Server {|Agent B, nb',                            \
  28.260  \                               Crypt (shrK B) {|Agent A, Nonce NA|}|}   \
  28.261  \                 : set evs)";
  28.262 @@ -345,7 +342,7 @@
  28.263  (*YM3*)
  28.264  by (blast_tac (!claset addSDs [B_Said_YM2]
  28.265  		       addSEs [MPair_parts]
  28.266 -		       addDs [Says_imp_sees_Spy RS parts.Inj]) 3);
  28.267 +		       addDs [Says_imp_spies RS parts.Inj]) 3);
  28.268  (*Fake, YM2*)
  28.269  by (ALLGOALS Blast_tac);
  28.270  val lemma = result() RSN (2, rev_mp) RS mp |> standard;
  28.271 @@ -354,12 +351,12 @@
  28.272  goal thy
  28.273   "!!evs. [| Says S A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \
  28.274  \             : set evs;                                                    \
  28.275 -\           A ~: lost;  B ~: lost;  evs : yahalom |]                   \
  28.276 +\           A ~: bad;  B ~: bad;  evs : yahalom |]                   \
  28.277  \   ==> EX nb'. Says B Server                                               \
  28.278  \                    {|Agent B, nb', Crypt (shrK B) {|Agent A, Nonce NA|}|} \
  28.279  \                 : set evs";
  28.280  by (blast_tac (!claset addSDs [A_trusts_YM3, lemma]
  28.281 -		       addEs sees_Spy_partsEs) 1);
  28.282 +		       addEs spies_partsEs) 1);
  28.283  qed "YM3_auth_B_to_A";
  28.284  
  28.285  
  28.286 @@ -370,12 +367,12 @@
  28.287    NB matters for freshness.*)  
  28.288  goal thy 
  28.289   "!!evs. evs : yahalom                                        \
  28.290 -\        ==> Key K ~: analz (sees Spy evs) -->                \
  28.291 -\            Crypt K (Nonce NB) : parts (sees Spy evs) -->    \
  28.292 +\        ==> Key K ~: analz (spies evs) -->                \
  28.293 +\            Crypt K (Nonce NB) : parts (spies evs) -->    \
  28.294  \            Crypt (shrK B) {|Nonce NB, Key K, Agent A|}      \
  28.295 -\              : parts (sees Spy evs) -->                     \
  28.296 -\            B ~: lost -->                                    \
  28.297 -\             (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs)";
  28.298 +\              : parts (spies evs) -->                     \
  28.299 +\            B ~: bad -->                                    \
  28.300 +\            (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs)";
  28.301  by (parts_induct_tac 1);
  28.302  (*Fake*)
  28.303  by (Fake_parts_insert_tac 1);
  28.304 @@ -384,10 +381,10 @@
  28.305  (*YM4: was Crypt K (Nonce NB) the very last message?  If not, use ind. hyp.*)
  28.306  by (asm_simp_tac (!simpset addsimps [ex_disj_distrib]) 1);
  28.307  (*yes: apply unicity of session keys*)
  28.308 -by (not_lost_tac "Aa" 1);
  28.309 +by (not_bad_tac "Aa" 1);
  28.310  by (blast_tac (!claset addSEs [MPair_parts]
  28.311                         addSDs [A_trusts_YM3, B_trusts_YM4_shrK]
  28.312 -		       addDs  [Says_imp_sees_Spy RS parts.Inj,
  28.313 +		       addDs  [Says_imp_spies RS parts.Inj,
  28.314  			       unique_session_keys]) 1);
  28.315  val lemma = normalize_thm [RSspec, RSmp] (result()) |> standard;
  28.316  
  28.317 @@ -398,14 +395,14 @@
  28.318   "!!evs. [| Says A' B {|Crypt (shrK B) {|Nonce NB, Key K, Agent A|},    \
  28.319  \                       Crypt K (Nonce NB)|} : set evs;                 \
  28.320  \           (ALL NA. Says A Spy {|Nonce NA, Nonce NB, Key K|} ~: set evs); \
  28.321 -\           A ~: lost;  B ~: lost;  evs : yahalom |]                    \
  28.322 +\           A ~: bad;  B ~: bad;  evs : yahalom |]                    \
  28.323  \        ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
  28.324 -by (etac (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1);
  28.325 +by (etac (Says_imp_spies RS parts.Inj RS MPair_parts) 1);
  28.326  by (dtac B_trusts_YM4_shrK 1);
  28.327  by (safe_tac (!claset));
  28.328  by (rtac lemma 1);
  28.329  by (rtac Spy_not_see_encrypted_key 2);
  28.330  by (REPEAT_FIRST assume_tac);
  28.331  by (ALLGOALS (blast_tac (!claset addSEs [MPair_parts]
  28.332 -			         addDs [Says_imp_sees_Spy RS parts.Inj])));
  28.333 +			         addDs [Says_imp_spies RS parts.Inj])));
  28.334  qed_spec_mp "YM4_imp_A_Said_YM3";
    29.1 --- a/src/HOL/Auth/Yahalom2.thy	Wed Sep 17 16:40:52 1997 +0200
    29.2 +++ b/src/HOL/Auth/Yahalom2.thy	Thu Sep 18 13:24:04 1997 +0200
    29.3 @@ -25,7 +25,7 @@
    29.4             invent new nonces here, but he can also use NS1.  Common to
    29.5             all similar protocols.*)
    29.6      Fake "[| evs: yahalom;  B ~= Spy;  
    29.7 -             X: synth (analz (sees Spy evs)) |]
    29.8 +             X: synth (analz (spies evs)) |]
    29.9            ==> Says Spy B X  # evs : yahalom"
   29.10  
   29.11           (*Alice initiates a protocol run*)