# HG changeset patch
# User paulson
# Date 920973699 -3600
# Node ID 76f3865a2b1d3c674aafe22e3afb8c62ebcddc7f
# Parent  fdf236c98914cfbcd768f27129c676bf2d4cf702
Added Bella's "Gets" model for Otway_Rees.  Also affects some other theories.
Changing "spies" to "knows Spy", etc.  Retaining the constant "spies" as a
translation.

diff -r fdf236c98914 -r 76f3865a2b1d src/HOL/Auth/Event.ML
--- a/src/HOL/Auth/Event.ML	Mon Mar 08 13:49:53 1999 +0100
+++ b/src/HOL/Auth/Event.ML	Tue Mar 09 11:01:39 1999 +0100
@@ -2,90 +2,170 @@
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1996  University of Cambridge
-
-Theory of events for security protocols
-
-Datatype of events; function "sees"; freshness
 *)
 
 AddIffs [Spy_in_bad, Server_not_bad];
 
-(**** Function "spies" ****)
+Addsimps [knows_Cons, used_Cons];
+
+(**** Function "knows" ****)
 
-(** Simplifying   parts (insert X (spies evs))
-      = parts {X} Un parts (spies evs) -- since general case loops*)
+(** Simplifying   parts (insert X (knows Spy evs))
+      = parts {X} Un parts (knows Spy evs) -- since general case loops*)
 
-bind_thm ("parts_insert_spies",
+bind_thm ("parts_insert_knows_Spy",
 	  parts_insert |> 
-	  read_instantiate_sg (sign_of thy) [("H", "spies evs")]);
+	  read_instantiate_sg (sign_of thy) [("H", "knows Spy evs")]);
 
 
-Goal "P(event_case sf nf ev) = \
+Goal "P(event_case sf nf gf ev) = \
 \      ((ALL A B X. ev = Says A B X --> P(sf A B X)) & \
-\       (ALL A X. ev = Notes A X --> P(nf A X)))";
+\       (ALL A X. ev = Notes A X --> P(nf A X)) & \
+\       (ALL A X. ev = Gets A X --> P(gf A X)))";
 by (induct_tac "ev" 1);
 by Auto_tac;
 qed "expand_event_case";
 
-Goal "spies (Says A B X # evs) = insert X (spies evs)";
+Goal "knows Spy (Says A B X # evs) = insert X (knows Spy evs)";
 by (Simp_tac 1);
-qed "spies_Says";
+qed "knows_Spy_Says";
 
 (*The point of letting the Spy see "bad" agents' notes is to prevent
   redundant case-splits on whether A=Spy and whether A:bad*)
-Goal "spies (Notes A X # evs) = \
-\         (if A:bad then insert X (spies evs) else spies evs)";
+Goal "knows Spy (Notes A X # evs) = \
+\         (if A:bad then insert X (knows Spy evs) else knows Spy evs)";
 by (Simp_tac 1);
-qed "spies_Notes";
+qed "knows_Spy_Notes";
 
-Goal "spies evs <= spies (Says A B X # evs)";
+Goal "knows Spy (Gets A X # evs) = knows Spy evs";
+by (Simp_tac 1);
+qed "knows_Spy_Gets";
+
+Goal "knows Spy evs <= knows Spy (Says A B X # evs)";
 by (simp_tac (simpset() addsimps [subset_insertI]) 1);
-qed "spies_subset_spies_Says";
+qed "knows_Spy_subset_knows_Spy_Says";
 
-Goal "spies evs <= spies (Notes A X # evs)";
+Goal "knows Spy evs <= knows Spy (Notes A X # evs)";
 by (Simp_tac 1);
 by (Fast_tac 1);
-qed "spies_subset_spies_Notes";
+qed "knows_Spy_subset_knows_Spy_Notes";
 
-(*Spy sees all traffic*)
-Goal "Says A B X : set evs --> X : spies evs";
+Goal "knows Spy evs <= knows Spy (Gets A X # evs)";
+by (simp_tac (simpset() addsimps [subset_insertI]) 1);
+qed "knows_Spy_subset_knows_Spy_Gets";
+
+(*Spy sees what is sent on the traffic*)
+Goal "Says A B X : set evs --> X : knows Spy evs";
 by (induct_tac "evs" 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
-qed_spec_mp "Says_imp_spies";
+qed_spec_mp "Says_imp_knows_Spy";
 
-(*Spy sees Notes of bad agents*)
-Goal "Notes A X : set evs --> A: bad --> X : spies evs";
+Goal "Notes A X : set evs --> A: bad --> X : knows Spy evs";
 by (induct_tac "evs" 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
-qed_spec_mp "Notes_imp_spies";
+qed_spec_mp "Notes_imp_knows_Spy";
+
 
 (*Use with addSEs to derive contradictions from old Says events containing
   items known to be fresh*)
-val spies_partsEs = make_elim (Says_imp_spies RS parts.Inj) :: partsEs;
+val knows_Spy_partsEs = make_elim (Says_imp_knows_Spy RS parts.Inj) :: partsEs;
+
+Addsimps [knows_Spy_Says, knows_Spy_Notes, knows_Spy_Gets];
+
+
+(*Begin lemmas about agents' knowledge*)
+
+Goal "knows A (Says A B X # evs) = insert X (knows A evs)";
+by (Simp_tac 1);
+qed "knows_Says";
+
+Goal "knows A (Notes A X # evs) = insert X (knows A evs)";
+by (Simp_tac 1);
+qed "knows_Notes";
+
+Goal "A ~= Spy --> knows A (Gets A X # evs) = insert X (knows A evs)";
+by (Simp_tac 1);
+qed "knows_Gets";
+
+
+Goal "knows A evs <= knows A (Says A B X # evs)";
+by (simp_tac (simpset() addsimps [subset_insertI]) 1);
+qed "knows_subset_knows_Says";
+
+Goal "knows A evs <= knows A (Notes A X # evs)";
+by (simp_tac (simpset() addsimps [subset_insertI]) 1);
+qed "knows_subset_knows_Notes";
+
+Goal "knows A evs <= knows A (Gets A X # evs)";
+by (simp_tac (simpset() addsimps [subset_insertI]) 1);
+qed "knows_subset_knows_Gets";
 
-Addsimps [spies_Says, spies_Notes];
+(*Agents know what they say*)
+Goal "Says A B X : set evs --> X : knows A evs";
+by (induct_tac "evs" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
+by (Blast_tac 1);
+qed_spec_mp "Says_imp_knows";
+
+(*Agents know what they note*)
+Goal "Notes A X : set evs --> X : knows A evs";
+by (induct_tac "evs" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
+by (Blast_tac 1);
+qed_spec_mp "Notes_imp_knows";
+
+(*Agents know what they receive*)
+Goal "A ~= Spy --> Gets A X : set evs --> X : knows A evs";
+by (induct_tac "evs" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
+qed_spec_mp "Gets_imp_knows_agents";
+
+
+(*What agents DIFFERENT FROM Spy know 
+  was either said, or noted, or got, or known initially*)
+Goal "[| X : knows A evs; A ~= Spy |] ==> EX B. \
+\ Says A B X : set evs | Gets A X : set evs | Notes A X : set evs | X : initState A";
+by (etac rev_mp 1);
+by (induct_tac "evs" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
+by (Blast_tac 1);
+qed_spec_mp "knows_imp_Says_Gets_Notes_initState";
+
+(*What the Spy knows -- for the time being --
+  was either said or noted, or known initially*)
+Goal "[| X : knows Spy evs |] ==> EX A B. \
+\ Says A B X : set evs | Notes A X : set evs | X : initState Spy";
+by (etac rev_mp 1);
+by (induct_tac "evs" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
+by (Blast_tac 1);
+qed_spec_mp "knows_Spy_imp_Says_Notes_initState";
+
+(*END lemmas about agents' knowledge*)
+
+
 
 (**** NOTE REMOVAL--laws above are cleaner, as they don't involve "case" ****)
-Delsimps [spies_Cons];   
+Delsimps [knows_Cons];   
 
 
 (*** Fresh nonces ***)
 
-Goal "parts (spies evs) <= used evs";
+Goal "parts (knows Spy evs) <= used evs";
 by (induct_tac "evs" 1);
 by (ALLGOALS (asm_simp_tac
-	      (simpset() addsimps [parts_insert_spies]
+	      (simpset() addsimps [parts_insert_knows_Spy]
 	                addsplits [expand_event_case])));
 by (ALLGOALS Blast_tac);
-qed "parts_spies_subset_used";
+qed "parts_knows_Spy_subset_used";
 
-bind_thm ("usedI", impOfSubs parts_spies_subset_used);
+bind_thm ("usedI", impOfSubs parts_knows_Spy_subset_used);
 AddIs [usedI];
 
 Goal "parts (initState B) <= used evs";
 by (induct_tac "evs" 1);
 by (ALLGOALS (asm_simp_tac
-	      (simpset() addsimps [parts_insert_spies]
+	      (simpset() addsimps [parts_insert_knows_Spy]
 	                addsplits [expand_event_case])));
 by (ALLGOALS Blast_tac);
 bind_thm ("initState_into_used", impOfSubs (result()));
@@ -100,6 +180,11 @@
 qed "used_Notes";
 Addsimps [used_Notes];
 
+Goal "used (Gets A X # evs) = used evs";
+by (Simp_tac 1);
+qed "used_Gets";
+Addsimps [used_Gets];
+
 Goal "used [] <= used evs";
 by (Simp_tac 1);
 by (blast_tac (claset() addIs [initState_into_used]) 1);
@@ -109,29 +194,34 @@
 Delsimps [used_Nil, used_Cons];   
 
 
-(*currently unused*)
-Goal "used evs <= used (evs@evs')";
-by (induct_tac "evs" 1);
-by (simp_tac (simpset() addsimps [used_nil_subset]) 1);
-by (induct_tac "a" 1);
-by (ALLGOALS Asm_simp_tac);
-by (ALLGOALS Blast_tac);
-qed "used_subset_append";
-
-
-(*For proving theorems of the form X ~: analz (spies evs) --> P
+(*For proving theorems of the form X ~: analz (knows Spy evs) --> P
   New events added by induction to "evs" are discarded.  Provided 
   this information isn't needed, the proof will be much shorter, since
   it will omit complicated reasoning about analz.*)
 val analz_mono_contra_tac = 
   let val analz_impI = read_instantiate_sg (sign_of thy)
-                [("P", "?Y ~: analz (spies ?evs)")] impI;
+                [("P", "?Y ~: analz (knows Spy ?evs)")] impI;
   in
     rtac analz_impI THEN' 
     REPEAT1 o 
       (dresolve_tac 
-       [spies_subset_spies_Says  RS analz_mono RS contra_subsetD,
-	spies_subset_spies_Notes RS analz_mono RS contra_subsetD])
+       [knows_Spy_subset_knows_Spy_Says RS analz_mono RS contra_subsetD,
+        knows_Spy_subset_knows_Spy_Notes RS analz_mono RS contra_subsetD,
+	knows_Spy_subset_knows_Spy_Gets RS analz_mono RS contra_subsetD])
     THEN'
     mp_tac
   end;
+
+fun Reception_tac i =
+    blast_tac (claset() addDs [Says_imp_knows_Spy RS parts.Inj, 
+                               impOfSubs (parts_insert RS equalityD1), 
+			       parts_trans,
+                               Says_imp_knows_Spy RS analz.Inj,
+                               impOfSubs analz_mono, analz_cut] 
+                        addIs [less_SucI]) i;
+
+
+(*Compatibility for the old "spies" function*)
+val spies_partsEs = knows_Spy_partsEs;
+val Says_imp_spies = Says_imp_knows_Spy;
+val parts_insert_spies = parts_insert_knows_Spy;
diff -r fdf236c98914 -r 76f3865a2b1d src/HOL/Auth/Event.thy
--- a/src/HOL/Auth/Event.thy	Mon Mar 08 13:49:53 1999 +0100
+++ b/src/HOL/Auth/Event.thy	Tue Mar 09 11:01:39 1999 +0100
@@ -19,24 +19,49 @@
 datatype  (*Messages--could add another constructor for agent knowledge*)
   event = Says  agent agent msg
         | Notes agent       msg
+        | Gets  agent       msg
+       
+consts 
+  bad    :: agent set        (*compromised agents*)
+  knows  :: agent => event list => msg set
 
-consts  
-  bad    :: agent set        (*compromised agents*)
+
+(*"spies" is retained for compability's sake*)
+syntax
   spies  :: event list => msg set
 
+translations
+  "spies"   => "knows Spy"
+
+
 rules
   (*Spy has access to his own key for spoof messages, but Server is secure*)
   Spy_in_bad     "Spy: bad"
   Server_not_bad "Server ~: bad"
 
 primrec
-           (*Spy reads all traffic whether addressed to him or not*)
-  spies_Nil   "spies []       = initState Spy"
-  spies_Cons  "spies (ev # evs) =
-	         (case ev of
-		    Says A B X => insert X (spies evs)
-		  | Notes A X  => 
-	              if A:bad then insert X (spies evs) else spies evs)"
+  knows_Nil   "knows A []         = initState A"
+  knows_Cons  "knows A (ev # evs) =
+	        (if A = Spy then 
+                  (case ev of
+		    Says A' B X => insert X (knows Spy evs)
+		  | Notes A' X  => 
+                   if A' : bad then insert X (knows Spy evs) else knows Spy evs
+                  | Gets A' X => knows Spy evs)
+                 else
+                  (case ev of
+		    Says A' B X => 
+                      if A'=A then insert X (knows A evs) else knows A evs
+		  | Notes A' X    => 
+                      if A'=A then insert X (knows A evs) else knows A evs
+		  | Gets A' X    => 
+                      if A'=A then insert X (knows A evs) else knows A evs))"
+
+(*
+  Case A=Spy on the Gets event
+  enforces the fact that if a message is received then it must have been sent,
+  therefore the oops case must use Notes
+*)
 
 consts
   (*Set of items that might be visible to somebody:
@@ -48,6 +73,9 @@
   used_Cons  "used (ev # evs) =
 	         (case ev of
 		    Says A B X => parts {X} Un (used evs)
-		  | Notes A X  => parts {X} Un (used evs))"
+		  | Notes A X  => parts {X} Un (used evs)
+		  | Gets A X   => used evs)"
+
+
 
 end
diff -r fdf236c98914 -r 76f3865a2b1d src/HOL/Auth/OtwayRees.ML
--- a/src/HOL/Auth/OtwayRees.ML	Mon Mar 08 13:49:53 1999 +0100
+++ b/src/HOL/Auth/OtwayRees.ML	Tue Mar 09 11:01:39 1999 +0100
@@ -12,68 +12,81 @@
   Proc. Royal Soc. 426 (1989)
 *)
 
-AddEs spies_partsEs;
+AddEs knows_Spy_partsEs;
 AddDs [impOfSubs analz_subset_parts];
 AddDs [impOfSubs Fake_parts_insert];
 
 
 (*A "possibility property": there are traces that reach the end*)
 Goal "[| B ~= Server |]   \
-\     ==> EX K. EX NA. EX evs: otway.          \
+\     ==> EX NA K. EX evs: otway.          \
 \            Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
 \              : set evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
-by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
+by (rtac (otway.Nil RS 
+          otway.OR1 RS otway.Reception RS
+          otway.OR2 RS otway.Reception RS 
+          otway.OR3 RS otway.Reception RS otway.OR4) 2);
 by possibility_tac;
 result();
 
+Goal "[| Gets B X : set evs; evs : otway |] ==> EX A. Says A B X : set evs";
+by (etac rev_mp 1);
+by (etac otway.induct 1);
+by Auto_tac;
+qed"Gets_imp_Says";
+
+(*Must be proved separately for each protocol*)
+Goal "[| Gets B X : set evs; evs : otway |]  ==> X : knows Spy evs";
+by (blast_tac (claset() addSDs [Gets_imp_Says, Says_imp_knows_Spy]) 1);
+qed"Gets_imp_knows_Spy";
+AddDs [Gets_imp_knows_Spy RS parts.Inj];
+
 
 (**** Inductive proofs about otway ****)
 
 (** For reasoning about the encrypted portion of messages **)
 
-Goal "Says A' B {|N, Agent A, Agent B, X|} : set evs \
-\      ==> X : analz (spies evs)";
-by (dtac (Says_imp_spies RS analz.Inj) 1);
-by (Blast_tac 1);
-qed "OR2_analz_spies";
+Goal "[| Gets B {|N, Agent A, Agent B, X|} : set evs;  evs : otway |]  \
+\     ==> X : analz (knows Spy evs)";
+by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1);
+qed "OR2_analz_knows_Spy";
 
-Goal "Says S' B {|N, X, Crypt (shrK B) X'|} : set evs \
-\      ==> X : analz (spies evs)";
-by (dtac (Says_imp_spies RS analz.Inj) 1);
-by (Blast_tac 1);
-qed "OR4_analz_spies";
+Goal "[| Gets B {|N, X, Crypt (shrK B) X'|} : set evs;  evs : otway |] \
+\     ==> X : analz (knows Spy evs)";
+by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1);
+qed "OR4_analz_knows_Spy";
 
 Goal "Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \
-\      ==> K : parts (spies evs)";
+\     ==> K : parts (knows Spy evs)";
 by (Blast_tac 1);
-qed "Oops_parts_spies";
+qed "Oops_parts_knows_Spy";
 
-bind_thm ("OR2_parts_spies",
-          OR2_analz_spies RS (impOfSubs analz_subset_parts));
-bind_thm ("OR4_parts_spies",
-          OR4_analz_spies RS (impOfSubs analz_subset_parts));
+bind_thm ("OR2_parts_knows_Spy",
+          OR2_analz_knows_Spy RS (impOfSubs analz_subset_parts));
+bind_thm ("OR4_parts_knows_Spy",
+          OR4_analz_knows_Spy RS (impOfSubs analz_subset_parts));
 
-(*For proving the easier theorems about X ~: parts (spies evs).*)
+(*For proving the easier theorems about X ~: parts (knows Spy evs).*)
 fun parts_induct_tac i = 
     etac otway.induct i			THEN 
-    forward_tac [Oops_parts_spies] (i+6) THEN
-    forward_tac [OR4_parts_spies]  (i+5) THEN
-    forward_tac [OR2_parts_spies]  (i+3) THEN 
+    forward_tac [Oops_parts_knows_Spy] (i+7) THEN
+    forward_tac [OR4_parts_knows_Spy]  (i+6) THEN
+    forward_tac [OR2_parts_knows_Spy]  (i+4) THEN 
     prove_simple_subgoals_tac  i;
 
 
-(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
+(** Theorems of the form X ~: parts (knows Spy evs) imply that NOBODY
     sends messages containing X! **)
 
 (*Spy never sees a good agent's shared key!*)
-Goal "evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
+Goal "evs : otway ==> (Key (shrK A) : parts (knows Spy evs)) = (A : bad)";
 by (parts_induct_tac 1);
 by (ALLGOALS Blast_tac);
 qed "Spy_see_shrK";
 Addsimps [Spy_see_shrK];
 
-Goal "evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
+Goal "evs : otway ==> (Key (shrK A) : analz (knows Spy evs)) = (A : bad)";
 by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
 qed "Spy_analz_shrK";
 Addsimps [Spy_analz_shrK];
@@ -83,7 +96,7 @@
 
 
 (*Nobody can have used non-existent keys!*)
-Goal "evs : otway ==> Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
+Goal "evs : otway ==> Key K ~: used evs --> K ~: keysFor (parts (knows Spy evs))";
 by (parts_induct_tac 1);
 (*Fake*)
 by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
@@ -114,18 +127,18 @@
 
 
 (*For proofs involving analz.*)
-val analz_spies_tac = 
-    dtac OR2_analz_spies 4 THEN 
-    dtac OR4_analz_spies 6 THEN
-    forward_tac [Says_Server_message_form] 7 THEN assume_tac 7 THEN
-    REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
+val analz_knows_Spy_tac = 
+    dtac OR2_analz_knows_Spy 5 THEN assume_tac 5 THEN 
+    dtac OR4_analz_knows_Spy 7 THEN assume_tac 7 THEN
+    forward_tac [Says_Server_message_form] 8 THEN assume_tac 8 THEN
+    REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 8);
 
 
 (****
  The following is to prove theorems of the form
 
-  Key K : analz (insert (Key KAB) (spies evs)) ==>
-  Key K : analz (spies evs)
+  Key K : analz (insert (Key KAB) (knows Spy evs)) ==>
+  Key K : analz (knows Spy evs)
 
  A more general formula must be proved inductively.
 ****)
@@ -135,10 +148,10 @@
 
 (*The equality makes the induction hypothesis easier to apply*)
 Goal "evs : otway ==> ALL K KK. KK <= - (range shrK) -->           \
-\                      (Key K : analz (Key``KK Un (spies evs))) =  \
-\                      (K : KK | Key K : analz (spies evs))";
+\                      (Key K : analz (Key``KK Un (knows Spy evs))) =  \
+\                      (K : KK | Key K : analz (knows Spy evs))";
 by (etac otway.induct 1);
-by analz_spies_tac;
+by analz_knows_Spy_tac;
 by (REPEAT_FIRST (resolve_tac [allI, impI]));
 by (REPEAT_FIRST (rtac analz_image_freshK_lemma));
 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
@@ -148,8 +161,8 @@
 
 
 Goal "[| evs : otway;  KAB ~: range shrK |]               \
-\     ==> Key K : analz (insert (Key KAB) (spies evs)) =  \
-\         (K = KAB | Key K : analz (spies evs))";
+\     ==> Key K : analz (insert (Key KAB) (knows Spy evs)) =  \
+\         (K = KAB | Key K : analz (knows Spy evs))";
 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
 qed "analz_insert_freshK";
 
@@ -169,7 +182,7 @@
 by (expand_case_tac "K = ?y" 1);
 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
 (*...we assume X is a recent message, and handle this case by contradiction*)
-by (blast_tac (claset() addSEs spies_partsEs) 1);
+by (blast_tac (claset() addSEs knows_Spy_partsEs) 1);
 val lemma = result();
 
 Goal "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|}   : set evs; \ 
@@ -179,12 +192,11 @@
 qed "unique_session_keys";
 
 
-
 (**** Authenticity properties relating to NA ****)
 
 (*Only OR1 can have caused such a part of a message to appear.*)
 Goal "[| A ~: bad;  evs : otway |]                             \
-\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) --> \
+\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (knows Spy evs) --> \
 \     Says A B {|NA, Agent A, Agent B,                      \
 \                Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \
 \      : set evs";
@@ -192,12 +204,21 @@
 by (Blast_tac 1);
 qed_spec_mp "Crypt_imp_OR1";
 
+Goal "[| Gets B {|NA, Agent A, Agent B,                      \
+\                 Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
+\        A ~: bad; evs : otway |]                             \
+\    ==> Says A B {|NA, Agent A, Agent B,                      \
+\                Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \
+\      : set evs";
+by (blast_tac (claset() addDs [Crypt_imp_OR1]) 1);
+qed"Crypt_imp_OR1_Gets";
+
 
 (** The Nonce NA uniquely identifies A's message. **)
 
 Goal "[| evs : otway; A ~: bad |]               \
 \ ==> EX B'. ALL B.                                 \
-\        Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) \
+\        Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (knows Spy evs) \
 \        --> B = B'";
 by (parts_induct_tac 1);
 by (Blast_tac 1);
@@ -207,8 +228,8 @@
 by (Blast_tac 1);
 val lemma = result();
 
-Goal "[| Crypt (shrK A) {|NA, Agent A, Agent B|}: parts (spies evs); \
-\          Crypt (shrK A) {|NA, Agent A, Agent C|}: parts (spies evs); \
+Goal "[| Crypt (shrK A) {|NA, Agent A, Agent B|}: parts (knows Spy evs); \
+\          Crypt (shrK A) {|NA, Agent A, Agent C|}: parts (knows Spy evs); \
 \          evs : otway;  A ~: bad |]                                   \
 \        ==> B = C";
 by (prove_unique_tac lemma 1);
@@ -219,19 +240,19 @@
   OR2 encrypts Nonce NB.  It prevents the attack that can occur in the
   over-simplified version of this protocol: see OtwayRees_Bad.*)
 Goal "[| A ~: bad;  evs : otway |]                      \
-\        ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) --> \
+\        ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (knows Spy evs) --> \
 \            Crypt (shrK A) {|NA', NA, Agent A', Agent A|}  \
-\             ~: parts (spies evs)";
+\             ~: parts (knows Spy evs)";
 by (parts_induct_tac 1);
-by (ALLGOALS Blast_tac);
-qed_spec_mp"no_nonce_OR1_OR2";
+by Auto_tac;
+qed_spec_mp "no_nonce_OR1_OR2";
 
 val nonce_OR1_OR2_E = no_nonce_OR1_OR2 RSN (2, rev_notE);
 
 (*Crucial property: If the encrypted message appears, and A has used NA
   to start a run, then it originated with the Server!*)
 Goal "[| A ~: bad;  evs : otway |]                                  \
-\    ==> Crypt (shrK A) {|NA, Key K|} : parts (spies evs)              \
+\    ==> Crypt (shrK A) {|NA, Key K|} : parts (knows Spy evs)              \
 \        --> Says A B {|NA, Agent A, Agent B,                          \
 \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}      \
 \             : set evs -->                                            \
@@ -253,7 +274,7 @@
 (*OR3, two cases*)  (** LEVEL 7 **)
 by (blast_tac (claset() addSEs  [nonce_OR1_OR2_E]
                         delrules [conjI] (*stop split-up into 4 subgoals*)) 2);
-by (blast_tac (claset() addIs  [unique_NA]) 1);
+by (blast_tac (claset() addIs [unique_NA]) 1);
 qed_spec_mp "NA_Crypt_imp_Server_msg";
 
 
@@ -263,7 +284,7 @@
   Spy_not_see_encrypted_key*)
 Goal "[| Says A  B {|NA, Agent A, Agent B,                       \
 \                Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
-\    Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \
+\        Gets A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \
 \    A ~: bad;  evs : otway |]                              \
 \ ==> EX NB. Says Server B                                  \
 \              {|NA,                                        \
@@ -283,9 +304,9 @@
 \       {|NA, Crypt (shrK A) {|NA, Key K|},                    \
 \         Crypt (shrK B) {|NB, Key K|}|} : set evs -->         \
 \     Notes Spy {|NA, NB, Key K|} ~: set evs -->               \
-\     Key K ~: analz (spies evs)";
+\     Key K ~: analz (knows Spy evs)";
 by (etac otway.induct 1);
-by analz_spies_tac;
+by analz_knows_Spy_tac;
 by (ALLGOALS
     (asm_simp_tac (simpset() addcongs [conj_cong] 
                              addsimps [analz_insert_eq, analz_insert_freshK]
@@ -305,7 +326,7 @@
 \               Crypt (shrK B) {|NB, Key K|}|} : set evs;        \
 \        Notes Spy {|NA, NB, Key K|} ~: set evs;                 \
 \        A ~: bad;  B ~: bad;  evs : otway |]                    \
-\     ==> Key K ~: analz (spies evs)";
+\     ==> Key K ~: analz (knows Spy evs)";
 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
 by (blast_tac (claset() addSEs [lemma]) 1);
 qed "Spy_not_see_encrypted_key";
@@ -315,10 +336,10 @@
   what it is.*)
 Goal "[| Says A  B {|NA, Agent A, Agent B,                       \
 \                    Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
-\        Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \
+\        Gets A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \
 \        ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs;         \
 \        A ~: bad;  B ~: bad;  evs : otway |]                    \
-\     ==> Key K ~: analz (spies evs)";
+\     ==> Key K ~: analz (knows Spy evs)";
 by (blast_tac (claset() addSDs [A_trusts_OR4, Spy_not_see_encrypted_key]) 1);
 qed "A_gets_good_key";
 
@@ -329,7 +350,7 @@
   know anything about X: it does NOT have to have the right form.*)
 Goal "[| B ~: bad;  evs : otway |]                         \
 \     ==> Crypt (shrK B) {|NA, NB, Agent A, Agent B|}       \
-\          : parts (spies evs) -->                       \
+\          : parts (knows Spy evs) -->                       \
 \         (EX X. Says B Server                              \
 \          {|NA, Agent A, Agent B, X,                       \
 \            Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}  \
@@ -343,7 +364,7 @@
 
 Goal "[| evs : otway; B ~: bad |]  \
 \ ==> EX NA' A'. ALL NA A.            \
-\      Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(spies evs) \
+\      Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(knows Spy evs) \
 \      --> NA = NA' & A = A'";
 by (parts_induct_tac 1);
 by (Blast_tac 1);
@@ -353,18 +374,17 @@
 by (Blast_tac 1);
 val lemma = result();
 
-Goal "[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(spies evs); \
-\          Crypt (shrK B) {|NC, NB, Agent C, Agent B|} : parts(spies evs); \
+Goal "[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(knows Spy evs); \
+\          Crypt (shrK B) {|NC, NB, Agent C, Agent B|} : parts(knows Spy evs); \
 \          evs : otway;  B ~: bad |]             \
 \        ==> NC = NA & C = A";
 by (prove_unique_tac lemma 1);
 qed "unique_NB";
 
-
 (*If the encrypted message appears, and B has used Nonce NB,
   then it originated with the Server!*)
 Goal "[| B ~: bad;  evs : otway |]                                    \
-\ ==> Crypt (shrK B) {|NB, Key K|} : parts (spies evs)                \
+\ ==> Crypt (shrK B) {|NB, Key K|} : parts (knows Spy evs)                \
 \     --> (ALL X'. Says B Server                                      \
 \                    {|NA, Agent A, Agent B, X',                      \
 \                      Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}  \
@@ -385,7 +405,8 @@
 *)
 by (safe_tac (claset() delrules [disjCI, impCE]));
 by (Blast_tac 3); 
-by (blast_tac (claset() addDs  [unique_NB]) 2);
+by (blast_tac (claset() addSDs  [unique_NB]
+                        delrules [impCE] (*stop split-up*)) 2);
 by (blast_tac (claset() addSEs [nonce_OR1_OR2_E]
                         delrules [conjI] (*stop split-up*)) 1);
 qed_spec_mp "NB_Crypt_imp_Server_msg";
@@ -396,7 +417,7 @@
 Goal "[| Says B Server {|NA, Agent A, Agent B, X',              \
 \                        Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
 \         : set evs;                                            \
-\        Says S' B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs;   \
+\        Gets B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs;   \
 \        B ~: bad;  evs : otway |]                              \
 \     ==> Says Server B                                         \
 \              {|NA,                                            \
@@ -411,10 +432,10 @@
 Goal "[| Says B Server {|NA, Agent A, Agent B, X',              \
 \                        Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
 \          : set evs;                                           \
-\        Says S' B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs;   \
+\        Gets B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs;   \
 \        Notes Spy {|NA, NB, Key K|} ~: set evs;                \
 \        A ~: bad;  B ~: bad;  evs : otway |]                   \
-\     ==> Key K ~: analz (spies evs)";
+\     ==> Key K ~: analz (knows Spy evs)";
 by (blast_tac (claset() addSDs [B_trusts_OR3, Spy_not_see_encrypted_key]) 1);
 qed "B_gets_good_key";
 
@@ -436,7 +457,7 @@
 (*After getting and checking OR4, agent A can trust that B has been active.
   We could probably prove that X has the expected form, but that is not
   strictly necessary for authentication.*)
-Goal "[| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs;        \
+Goal "[| Gets A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs;        \
 \        Says A  B {|NA, Agent A, Agent B,                                \
 \                    Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
 \        A ~: bad;  B ~: bad;  evs : otway |]                             \
diff -r fdf236c98914 -r 76f3865a2b1d src/HOL/Auth/OtwayRees.thy
--- a/src/HOL/Auth/OtwayRees.thy	Mon Mar 08 13:49:53 1999 +0100
+++ b/src/HOL/Auth/OtwayRees.thy	Tue Mar 09 11:01:39 1999 +0100
@@ -1,19 +1,14 @@
-(*  Title:      HOL/Auth/OtwayRees
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1996  University of Cambridge
-
-Inductive relation "otway" for the Otway-Rees protocol.
+(*  
+Inductive relation "otway" for the Otway-Rees protocol
+extended by Gets primitive.
 
 Version that encrypts Nonce NB
 
-From page 244 of
-  Burrows, Abadi and Needham.  A Logic of Authentication.
-  Proc. Royal Soc. 426 (1989)
 *)
 
 OtwayRees = Shared + 
 
+
 consts  otway   :: event list set
 inductive "otway"
   intrs 
@@ -25,8 +20,13 @@
          (*The spy MAY say anything he CAN say.  We do not expect him to
            invent new nonces here, but he can also use NS1.  Common to
            all similar protocols.*)
-    Fake "[| evs: otway;  X: synth (analz (spies evs)) |]
-          ==> Says Spy B X  # evs : otway"
+    Fake "[| evsa: otway;  X: synth (analz (knows Spy evsa)) |]
+          ==> Says Spy B X  # evsa : otway"
+
+         (*A message that has been sent can be received by the
+           intended recipient.*)
+    Reception "[| evsr: otway;  Says A B X : set evsr |]
+               ==> Gets B X # evsr : otway"
 
          (*Alice initiates a protocol run*)
     OR1  "[| evs1: otway;  Nonce NA ~: used evs1 |]
@@ -38,7 +38,7 @@
 	   the sender is, hence the A' in the sender field.
            Note that NB is encrypted.*)
     OR2  "[| evs2: otway;  Nonce NB ~: used evs2;
-             Says A' B {|Nonce NA, Agent A, Agent B, X|} : set evs2 |]
+             Gets B {|Nonce NA, Agent A, Agent B, X|} : set evs2 |]
           ==> Says B Server 
                   {|Nonce NA, Agent A, Agent B, X, 
                     Crypt (shrK B)
@@ -49,7 +49,7 @@
            match.  Then he sends a new session key to Bob with a packet for
            forwarding to Alice.*)
     OR3  "[| evs3: otway;  Key KAB ~: used evs3;
-             Says B' Server 
+             Gets Server 
                   {|Nonce NA, Agent A, Agent B, 
                     Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}, 
                     Crypt (shrK B) {|Nonce NA, Nonce NB, Agent A, Agent B|}|}
@@ -68,7 +68,7 @@
                              Crypt (shrK B)
                                    {|Nonce NA, Nonce NB, Agent A, Agent B|}|}
                : set evs4;
-             Says S' B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
+             Gets B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
                : set evs4 |]
           ==> Says B A {|Nonce NA, X|} # evs4 : otway"
 
diff -r fdf236c98914 -r 76f3865a2b1d src/HOL/Auth/OtwayRees_AN.ML
--- a/src/HOL/Auth/OtwayRees_AN.ML	Mon Mar 08 13:49:53 1999 +0100
+++ b/src/HOL/Auth/OtwayRees_AN.ML	Tue Mar 09 11:01:39 1999 +0100
@@ -12,7 +12,7 @@
   IEEE Trans. SE 22 (1), 1996
 *)
 
-AddEs spies_partsEs;
+AddEs knows_Spy_partsEs;
 AddDs [impOfSubs analz_subset_parts];
 AddDs [impOfSubs Fake_parts_insert];
 
@@ -23,48 +23,62 @@
 \          Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) \
 \            : set evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
-by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
+by (rtac (otway.Nil RS 
+          otway.OR1 RS otway.Reception RS
+          otway.OR2 RS otway.Reception RS 
+          otway.OR3 RS otway.Reception RS otway.OR4) 2);
 by possibility_tac;
 result();
 
+Goal "[| Gets B X : set evs; evs : otway |] ==> EX A. Says A B X : set evs";
+by (etac rev_mp 1);
+by (etac otway.induct 1);
+by Auto_tac;
+qed"Gets_imp_Says";
+
+(*Must be proved separately for each protocol*)
+Goal "[| Gets B X : set evs; evs : otway |]  ==> X : knows Spy evs";
+by (blast_tac (claset() addSDs [Gets_imp_Says, Says_imp_knows_Spy]) 1);
+qed"Gets_imp_knows_Spy";
+AddDs [Gets_imp_knows_Spy RS parts.Inj];
+
 
 (**** Inductive proofs about otway ****)
 
 (** For reasoning about the encrypted portion of messages **)
 
-Goal "Says S' B {|X, Crypt(shrK B) X'|} : set evs ==> \
-\          X : analz (spies evs)";
-by (dtac (Says_imp_spies RS analz.Inj) 1);
-by (Blast_tac 1);
-qed "OR4_analz_spies";
+Goal "[| Gets B {|X, Crypt(shrK B) X'|} : set evs;  evs : otway |] ==> \
+\          X : analz (knows Spy evs)";
+by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1);
+qed "OR4_analz_knows_Spy";
 
-Goal "Says Server B {|X, Crypt K' {|NB, a, Agent B, K|}|} \
-\            : set evs ==> K : parts (spies evs)";
+Goal "Says Server B {|X, Crypt K' {|NB, a, Agent B, K|}|} : set evs \
+\     ==> K : parts (knows Spy evs)";
 by (Blast_tac 1);
-qed "Oops_parts_spies";
+qed "Oops_parts_knows_Spy";
 
-bind_thm ("OR4_parts_spies",
-          OR4_analz_spies RS (impOfSubs analz_subset_parts));
+bind_thm ("OR4_parts_knows_Spy",
+          OR4_analz_knows_Spy RS (impOfSubs analz_subset_parts));
 
-(*For proving the easier theorems about X ~: parts (spies evs).*)
+(*For proving the easier theorems about X ~: parts (knows Spy evs).*)
 fun parts_induct_tac i = 
     etac otway.induct i			THEN 
-    forward_tac [Oops_parts_spies] (i+6) THEN
-    forward_tac [OR4_parts_spies]  (i+5) THEN
+    forward_tac [Oops_parts_knows_Spy] (i+7) THEN
+    forward_tac [OR4_parts_knows_Spy]  (i+6) THEN
     prove_simple_subgoals_tac  i;
 
 
-(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
+(** Theorems of the form X ~: parts (knows Spy evs) imply that NOBODY
     sends messages containing X! **)
 
 (*Spy never sees a good agent's shared key!*)
-Goal "evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
+Goal "evs : otway ==> (Key (shrK A) : parts (knows Spy evs)) = (A : bad)";
 by (parts_induct_tac 1);
 by (ALLGOALS Blast_tac);
 qed "Spy_see_shrK";
 Addsimps [Spy_see_shrK];
 
-Goal "evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
+Goal "evs : otway ==> (Key (shrK A) : analz (knows Spy evs)) = (A : bad)";
 by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
 qed "Spy_analz_shrK";
 Addsimps [Spy_analz_shrK];
@@ -74,7 +88,7 @@
 
 
 (*Nobody can have used non-existent keys!*)
-Goal "evs : otway ==> Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
+Goal "evs : otway ==> Key K ~: used evs --> K ~: keysFor (parts (knows Spy evs))";
 by (parts_induct_tac 1);
 (*Fake*)
 by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
@@ -107,18 +121,17 @@
 
 
 (*For proofs involving analz.*)
-val analz_spies_tac = 
-    dtac OR4_analz_spies 6 THEN
-    forward_tac [Says_Server_message_form] 7 THEN
-    assume_tac 7 THEN
-    REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
+val analz_knows_Spy_tac = 
+    dtac OR4_analz_knows_Spy 7 THEN assume_tac 7 THEN
+    forward_tac [Says_Server_message_form] 8 THEN assume_tac 8 THEN
+    REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 8);
 
 
 (****
  The following is to prove theorems of the form
 
-  Key K : analz (insert (Key KAB) (spies evs)) ==>
-  Key K : analz (spies evs)
+  Key K : analz (insert (Key KAB) (knows Spy evs)) ==>
+  Key K : analz (knows Spy evs)
 
  A more general formula must be proved inductively.
 ****)
@@ -129,10 +142,10 @@
 (*The equality makes the induction hypothesis easier to apply*)
 Goal "evs : otway ==>                                 \
 \  ALL K KK. KK <= -(range shrK) -->                  \
-\         (Key K : analz (Key``KK Un (spies evs))) =  \
-\         (K : KK | Key K : analz (spies evs))";
+\         (Key K : analz (Key``KK Un (knows Spy evs))) =  \
+\         (K : KK | Key K : analz (knows Spy evs))";
 by (etac otway.induct 1);
-by analz_spies_tac;
+by analz_knows_Spy_tac;
 by (REPEAT_FIRST (resolve_tac [allI, impI]));
 by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
@@ -142,8 +155,8 @@
 
 
 Goal "[| evs : otway;  KAB ~: range shrK |] ==>       \
-\     Key K : analz (insert (Key KAB) (spies evs)) =  \
-\     (K = KAB | Key K : analz (spies evs))";
+\     Key K : analz (insert (Key KAB) (knows Spy evs)) =  \
+\     (K = KAB | Key K : analz (knows Spy evs))";
 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
 qed "analz_insert_freshK";
 
@@ -165,7 +178,7 @@
 by (expand_case_tac "K = ?y" 1);
 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
 (*...we assume X is a recent message and handle this case by contradiction*)
-by (blast_tac (claset() addSEs spies_partsEs) 1);
+by (blast_tac (claset() addSEs knows_Spy_partsEs) 1);
 val lemma = result();
 
 
@@ -188,7 +201,7 @@
 
 (*If the encrypted message appears then it originated with the Server!*)
 Goal "[| A ~: bad;  A ~= B;  evs : otway |]                 \
-\     ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|} : parts (spies evs) \
+\     ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|} : parts (knows Spy evs) \
 \      --> (EX NB. Says Server B                                          \
 \                   {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
 \                     Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
@@ -203,7 +216,7 @@
 
 (*Corollary: if A receives B's OR4 message then it originated with the Server.
   Freshness may be inferred from nonce NA.*)
-Goal "[| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|})  \
+Goal "[| Gets A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|})  \
 \         : set evs;                                                 \
 \        A ~: bad;  A ~= B;  evs : otway |]                          \
 \     ==> EX NB. Says Server B                                       \
@@ -224,9 +237,9 @@
 \            Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
 \         : set evs -->                                         \
 \         Notes Spy {|NA, NB, Key K|} ~: set evs -->            \
-\         Key K ~: analz (spies evs)";
+\         Key K ~: analz (knows Spy evs)";
 by (etac otway.induct 1);
-by analz_spies_tac;
+by analz_knows_Spy_tac;
 by (ALLGOALS
     (asm_simp_tac (simpset() addcongs [conj_cong, if_weak_cong] 
                              addsimps [analz_insert_eq, analz_insert_freshK]
@@ -247,7 +260,7 @@
 \          : set evs;                                            \
 \        Notes Spy {|NA, NB, Key K|} ~: set evs;                 \
 \        A ~: bad;  B ~: bad;  evs : otway |]                    \
-\     ==> Key K ~: analz (spies evs)";
+\     ==> Key K ~: analz (knows Spy evs)";
 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
 by (blast_tac (claset() addSEs [lemma]) 1);
 qed "Spy_not_see_encrypted_key";
@@ -255,11 +268,11 @@
 
 (*A's guarantee.  The Oops premise quantifies over NB because A cannot know
   what it is.*)
-Goal "[| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|})  \
+Goal "[| Gets A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|})  \
 \         : set evs;                                                 \
 \        ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs;             \
 \        A ~: bad;  B ~: bad;  A ~= B;  evs : otway |]               \
-\     ==> Key K ~: analz (spies evs)";
+\     ==> Key K ~: analz (knows Spy evs)";
 by (blast_tac (claset() addSDs [A_trusts_OR4, Spy_not_see_encrypted_key]) 1);
 qed "A_gets_good_key";
 
@@ -268,7 +281,7 @@
 
 (*If the encrypted message appears then it originated with the Server!*)
 Goal "[| B ~: bad;  A ~= B;  evs : otway |]                              \
-\ ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|} : parts (spies evs) \
+\ ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|} : parts (knows Spy evs) \
 \     --> (EX NA. Says Server B                                          \
 \                  {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
 \                    Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
@@ -283,7 +296,7 @@
 
 (*Guarantee for B: if it gets a well-formed certificate then the Server
   has sent the correct message in round 3.*)
-Goal "[| Says S' B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
+Goal "[| Gets B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
 \          : set evs;                                                    \
 \        B ~: bad;  A ~= B;  evs : otway |]                              \
 \     ==> EX NA. Says Server B                                           \
@@ -295,10 +308,10 @@
 
 
 (*The obvious combination of B_trusts_OR3 with Spy_not_see_encrypted_key*)
-Goal "[| Says S' B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
+Goal "[| Gets B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
 \         : set evs;                                                     \
 \        ALL NA. Notes Spy {|NA, NB, Key K|} ~: set evs;                 \
 \        A ~: bad;  B ~: bad;  A ~= B;  evs : otway |]                   \
-\     ==> Key K ~: analz (spies evs)";
+\     ==> Key K ~: analz (knows Spy evs)";
 by (blast_tac (claset() addDs [B_trusts_OR3, Spy_not_see_encrypted_key]) 1);
 qed "B_gets_good_key";
diff -r fdf236c98914 -r 76f3865a2b1d src/HOL/Auth/OtwayRees_AN.thy
--- a/src/HOL/Auth/OtwayRees_AN.thy	Mon Mar 08 13:49:53 1999 +0100
+++ b/src/HOL/Auth/OtwayRees_AN.thy	Tue Mar 09 11:01:39 1999 +0100
@@ -28,9 +28,14 @@
          (*The spy MAY say anything he CAN say.  We do not expect him to
            invent new nonces here, but he can also use NS1.  Common to
            all similar protocols.*)
-    Fake "[| evs: otway;  X: synth (analz (spies evs)) |]
+    Fake "[| evs: otway;  X: synth (analz (knows Spy evs)) |]
           ==> Says Spy B X  # evs : otway"
 
+         (*A message that has been sent can be received by the
+           intended recipient.*)
+    Reception "[| evsr: otway;  Says A B X : set evsr |]
+               ==> Gets B X # evsr : otway"
+
          (*Alice initiates a protocol run*)
     OR1  "[| evs1: otway |]
           ==> Says A B {|Agent A, Agent B, Nonce NA|} # evs1 : otway"
@@ -38,14 +43,14 @@
          (*Bob's response to Alice's message.  Bob doesn't know who 
 	   the sender is, hence the A' in the sender field.*)
     OR2  "[| evs2: otway;  
-             Says A' B {|Agent A, Agent B, Nonce NA|} : set evs2 |]
+             Gets B {|Agent A, Agent B, Nonce NA|} : set evs2 |]
           ==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
                  # evs2 : otway"
 
          (*The Server receives Bob's message.  Then he sends a new
            session key to Bob with a packet for forwarding to Alice.*)
     OR3  "[| evs3: otway;  Key KAB ~: used evs3;
-             Says B' Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
+             Gets Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
                : set evs3 |]
           ==> Says Server B 
                {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key KAB|},
@@ -57,7 +62,7 @@
            Need B ~= Server because we allow messages to self.*)
     OR4  "[| evs4: otway;  B ~= Server; 
              Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} : set evs4;
-             Says S' B {|X, Crypt(shrK B){|Nonce NB,Agent A,Agent B,Key K|}|}
+             Gets B {|X, Crypt(shrK B){|Nonce NB,Agent A,Agent B,Key K|}|}
                : set evs4 |]
           ==> Says B A X # evs4 : otway"
 
diff -r fdf236c98914 -r 76f3865a2b1d src/HOL/Auth/OtwayRees_Bad.ML
--- a/src/HOL/Auth/OtwayRees_Bad.ML	Mon Mar 08 13:49:53 1999 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.ML	Tue Mar 09 11:01:39 1999 +0100
@@ -15,7 +15,7 @@
 indicates the possibility of this attack.
 *)
 
-AddEs spies_partsEs;
+AddEs knows_Spy_partsEs;
 AddDs [impOfSubs analz_subset_parts];
 AddDs [impOfSubs Fake_parts_insert];
 
@@ -26,58 +26,71 @@
 \           Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
 \             : set evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
-by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
+by (rtac (otway.Nil RS 
+          otway.OR1 RS otway.Reception RS
+          otway.OR2 RS otway.Reception RS 
+          otway.OR3 RS otway.Reception RS otway.OR4) 2);
 by possibility_tac;
 result();
 
+Goal "[| Gets B X : set evs; evs : otway |] ==> EX A. Says A B X : set evs";
+by (etac rev_mp 1);
+by (etac otway.induct 1);
+by Auto_tac;
+qed"Gets_imp_Says";
+
+(*Must be proved separately for each protocol*)
+Goal "[| Gets B X : set evs; evs : otway |]  ==> X : knows Spy evs";
+by (blast_tac (claset() addSDs [Gets_imp_Says, Says_imp_knows_Spy]) 1);
+qed"Gets_imp_knows_Spy";
+AddDs [Gets_imp_knows_Spy RS parts.Inj];
+
 
 (**** Inductive proofs about otway ****)
 
 
 (** For reasoning about the encrypted portion of messages **)
 
-Goal "Says A' B {|N, Agent A, Agent B, X|} : set evs \
-\          ==> X : analz (spies evs)";
-by (dtac (Says_imp_spies RS analz.Inj) 1);
-by (Blast_tac 1);
-qed "OR2_analz_spies";
+Goal "[| Gets B {|N, Agent A, Agent B, X|} : set evs;  evs : otway |] \
+\     ==> X : analz (knows Spy evs)";
+by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1);
+qed "OR2_analz_knows_Spy";
 
-Goal "Says S' B {|N, X, Crypt (shrK B) X'|} : set evs \
-\          ==> X : analz (spies evs)";
-by (dtac (Says_imp_spies RS analz.Inj) 1);
-by (Blast_tac 1);
-qed "OR4_analz_spies";
+Goal "[| Gets B {|N, X, Crypt (shrK B) X'|} : set evs;  evs : otway |] \
+\     ==> X : analz (knows Spy evs)";
+by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1);
+qed "OR4_analz_knows_Spy";
 
 Goal "Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \
-\          ==> K : parts (spies evs)";
+\     ==> K : parts (knows Spy evs)";
 by (Blast_tac 1);
-qed "Oops_parts_spies";
+qed "Oops_parts_knows_Spy";
 
-bind_thm ("OR2_parts_spies",
-          OR2_analz_spies RS (impOfSubs analz_subset_parts));
-bind_thm ("OR4_parts_spies",
-          OR4_analz_spies RS (impOfSubs analz_subset_parts));
+bind_thm ("OR2_parts_knows_Spy",
+          OR2_analz_knows_Spy RS (impOfSubs analz_subset_parts));
+bind_thm ("OR4_parts_knows_Spy",
+          OR4_analz_knows_Spy RS (impOfSubs analz_subset_parts));
 
-(*For proving the easier theorems about X ~: parts (spies evs).*)
+(*For proving the easier theorems about X ~: parts (knows Spy evs).*)
 fun parts_induct_tac i = 
     etac otway.induct i			THEN 
-    forward_tac [Oops_parts_spies] (i+6) THEN
-    forward_tac [OR4_parts_spies]  (i+5) THEN
-    forward_tac [OR2_parts_spies]  (i+3) THEN 
+    forward_tac [Oops_parts_knows_Spy] (i+7) THEN
+    forward_tac [OR4_parts_knows_Spy]  (i+6) THEN
+    forward_tac [OR2_parts_knows_Spy]  (i+4) THEN 
     prove_simple_subgoals_tac  i;
 
 
-(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
+(** Theorems of the form X ~: parts (knows Spy evs) imply that NOBODY
     sends messages containing X! **)
 
 (*Spy never sees a good agent's shared key!*)
-Goal "evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
+Goal "evs : otway ==> (Key (shrK A) : parts (knows Spy evs)) = (A : bad)";
 by (parts_induct_tac 1);
 by (ALLGOALS Blast_tac);
 qed "Spy_see_shrK";
 Addsimps [Spy_see_shrK];
 
-Goal "evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
+Goal "evs : otway ==> (Key (shrK A) : analz (knows Spy evs)) = (A : bad)";
 by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
 qed "Spy_analz_shrK";
 Addsimps [Spy_analz_shrK];
@@ -87,7 +100,7 @@
 
 
 (*Nobody can have used non-existent keys!*)
-Goal "evs : otway ==> Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
+Goal "evs : otway ==> Key K ~: used evs --> K ~: keysFor (parts (knows Spy evs))";
 by (parts_induct_tac 1);
 (*Fake*)
 by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
@@ -118,18 +131,18 @@
 
 
 (*For proofs involving analz.*)
-val analz_spies_tac = 
-    dtac OR2_analz_spies 4 THEN 
-    dtac OR4_analz_spies 6 THEN
-    forward_tac [Says_Server_message_form] 7 THEN assume_tac 7 THEN
-    REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
+val analz_knows_Spy_tac = 
+    dtac OR2_analz_knows_Spy 5 THEN assume_tac 5 THEN 
+    dtac OR4_analz_knows_Spy 7 THEN assume_tac 7 THEN
+    forward_tac [Says_Server_message_form] 8 THEN assume_tac 8 THEN
+    REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 8);
 
 
 (****
  The following is to prove theorems of the form
 
-  Key K : analz (insert (Key KAB) (spies evs)) ==>
-  Key K : analz (spies evs)
+  Key K : analz (insert (Key KAB) (knows Spy evs)) ==>
+  Key K : analz (knows Spy evs)
 
  A more general formula must be proved inductively.
 ****)
@@ -140,10 +153,10 @@
 (*The equality makes the induction hypothesis easier to apply*)
 Goal "evs : otway ==>                                 \
 \  ALL K KK. KK <= - (range shrK) -->                 \
-\         (Key K : analz (Key``KK Un (spies evs))) =  \
-\         (K : KK | Key K : analz (spies evs))";
+\         (Key K : analz (Key``KK Un (knows Spy evs))) =  \
+\         (K : KK | Key K : analz (knows Spy evs))";
 by (etac otway.induct 1);
-by analz_spies_tac;
+by analz_knows_Spy_tac;
 by (REPEAT_FIRST (resolve_tac [allI, impI]));
 by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
@@ -153,8 +166,8 @@
 
 
 Goal "[| evs : otway;  KAB ~: range shrK |] ==>       \
-\     Key K : analz (insert (Key KAB) (spies evs)) =  \
-\     (K = KAB | Key K : analz (spies evs))";
+\     Key K : analz (insert (Key KAB) (knows Spy evs)) =  \
+\     (K = KAB | Key K : analz (knows Spy evs))";
 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
 qed "analz_insert_freshK";
 
@@ -174,7 +187,7 @@
 by (expand_case_tac "K = ?y" 1);
 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
 (*...we assume X is a recent message, and handle this case by contradiction*)
-by (blast_tac (claset() addSEs spies_partsEs) 1);
+by (blast_tac (claset() addSEs knows_Spy_partsEs) 1);
 val lemma = result();
 
 Goal "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|}   : set evs; \ 
@@ -193,9 +206,9 @@
 \           {|NA, Crypt (shrK A) {|NA, Key K|},                    \
 \             Crypt (shrK B) {|NB, Key K|}|} : set evs -->         \
 \         Notes Spy {|NA, NB, Key K|} ~: set evs -->               \
-\         Key K ~: analz (spies evs)";
+\         Key K ~: analz (knows Spy evs)";
 by (etac otway.induct 1);
-by analz_spies_tac;
+by analz_knows_Spy_tac;
 by (ALLGOALS
     (asm_simp_tac (simpset() addcongs [conj_cong] 
                              addsimps [analz_insert_eq, analz_insert_freshK]
@@ -215,7 +228,7 @@
 \               Crypt (shrK B) {|NB, Key K|}|} : set evs;        \
 \        Notes Spy {|NA, NB, Key K|} ~: set evs;                 \
 \        A ~: bad;  B ~: bad;  evs : otway |]                    \
-\     ==> Key K ~: analz (spies evs)";
+\     ==> Key K ~: analz (knows Spy evs)";
 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
 by (blast_tac (claset() addSEs [lemma]) 1);
 qed "Spy_not_see_encrypted_key";
@@ -227,7 +240,7 @@
   The premise A ~= B prevents OR2's similar-looking cryptogram from being
   picked up.  Original Otway-Rees doesn't need it.*)
 Goal "[| A ~: bad;  A ~= B;  evs : otway |]                \
-\     ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) --> \
+\     ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (knows Spy evs) --> \
 \         Says A B {|NA, Agent A, Agent B,                  \
 \                    Crypt (shrK A) {|NA, Agent A, Agent B|}|}  : set evs";
 by (parts_induct_tac 1);
@@ -236,11 +249,12 @@
 
 
 (*Crucial property: If the encrypted message appears, and A has used NA
-  to start a run, then it originated with the Server!*)
+  to start a run, then it originated with the Server!
+  The premise A ~= B allows use of Crypt_imp_OR1*)
 (*Only it is FALSE.  Somebody could make a fake message to Server
           substituting some other nonce NA' for NB.*)
-Goal "[| A ~: bad;  evs : otway |]                                \
-\     ==> Crypt (shrK A) {|NA, Key K|} : parts (spies evs) -->    \
+Goal "[| A ~: bad;  A ~= B;  evs : otway |]                                \
+\     ==> Crypt (shrK A) {|NA, Key K|} : parts (knows Spy evs) -->    \
 \         Says A B {|NA, Agent A, Agent B,                        \
 \                    Crypt (shrK A) {|NA, Agent A, Agent B|}|}    \
 \          : set evs -->                                          \
@@ -261,7 +275,7 @@
 (*OR3*)  (** LEVEL 5 **)
 (*The hypotheses at this point suggest an attack in which nonce NB is used
   in two different roles:
-          Says B' Server
+          Gets Server
            {|Nonce NA, Agent Aa, Agent A,
              Crypt (shrK Aa) {|Nonce NA, Agent Aa, Agent A|}, Nonce NB,
              Crypt (shrK A) {|Nonce NA, Agent Aa, Agent A|}|}
diff -r fdf236c98914 -r 76f3865a2b1d src/HOL/Auth/OtwayRees_Bad.thy
--- a/src/HOL/Auth/OtwayRees_Bad.thy	Mon Mar 08 13:49:53 1999 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.thy	Tue Mar 09 11:01:39 1999 +0100
@@ -22,9 +22,14 @@
          (*The spy MAY say anything he CAN say.  We do not expect him to
            invent new nonces here, but he can also use NS1.  Common to
            all similar protocols.*)
-    Fake "[| evs: otway;  X: synth (analz (spies evs)) |]
+    Fake "[| evs: otway;  X: synth (analz (knows Spy evs)) |]
           ==> Says Spy B X  # evs : otway"
 
+         (*A message that has been sent can be received by the
+           intended recipient.*)
+    Reception "[| evsr: otway;  Says A B X : set evsr |]
+               ==> Gets B X # evsr : otway"
+
          (*Alice initiates a protocol run*)
     OR1  "[| evs1: otway;  Nonce NA ~: used evs1 |]
           ==> Says A B {|Nonce NA, Agent A, Agent B, 
@@ -35,7 +40,7 @@
 	   the sender is, hence the A' in the sender field.
            We modify the published protocol by NOT encrypting NB.*)
     OR2  "[| evs2: otway;  Nonce NB ~: used evs2;
-             Says A' B {|Nonce NA, Agent A, Agent B, X|} : set evs2 |]
+             Gets B {|Nonce NA, Agent A, Agent B, X|} : set evs2 |]
           ==> Says B Server 
                   {|Nonce NA, Agent A, Agent B, X, Nonce NB,
                     Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
@@ -45,7 +50,7 @@
            match.  Then he sends a new session key to Bob with a packet for
            forwarding to Alice.*)
     OR3  "[| evs3: otway;  Key KAB ~: used evs3;
-             Says B' Server 
+             Gets Server 
                   {|Nonce NA, Agent A, Agent B, 
                     Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}, 
                     Nonce NB, 
@@ -60,11 +65,11 @@
          (*Bob receives the Server's (?) message and compares the Nonces with
 	   those in the message he previously sent the Server.
            Need B ~= Server because we allow messages to self.*)
-    OR4  "[| evs4: otway;  A ~= B;  B ~= Server;
+    OR4  "[| evs4: otway;  B ~= Server;
              Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB,
                              Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
                : set evs4;
-             Says S' B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
+             Gets B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
                : set evs4 |]
           ==> Says B A {|Nonce NA, X|} # evs4 : otway"
 
diff -r fdf236c98914 -r 76f3865a2b1d src/HOL/Auth/Public.ML
--- a/src/HOL/Auth/Public.ML	Mon Mar 08 13:49:53 1999 +0100
+++ b/src/HOL/Auth/Public.ML	Tue Mar 09 11:01:39 1999 +0100
@@ -72,7 +72,7 @@
 Goal "Key (pubK A) : spies evs";
 by (induct_tac "evs" 1);
 by (ALLGOALS (asm_simp_tac
-	      (simpset() addsimps [imageI, spies_Cons]
+	      (simpset() addsimps [imageI, knows_Cons]
 	                addsplits [expand_event_case])));
 qed_spec_mp "spies_pubK";
 
@@ -80,7 +80,7 @@
 Goal "A: bad ==> Key (priK A) : spies evs";
 by (induct_tac "evs" 1);
 by (ALLGOALS (asm_simp_tac
-	      (simpset() addsimps [imageI, spies_Cons]
+	      (simpset() addsimps [imageI, knows_Cons]
 	                addsplits [expand_event_case])));
 qed "Spy_spies_bad";
 
diff -r fdf236c98914 -r 76f3865a2b1d src/HOL/Auth/Shared.ML
--- a/src/HOL/Auth/Shared.ML	Mon Mar 08 13:49:53 1999 +0100
+++ b/src/HOL/Auth/Shared.ML	Tue Mar 09 11:01:39 1999 +0100
@@ -28,11 +28,11 @@
 (*Specialized to shared-key model: no need for addss in protocol proofs*)
 Goal "[| K: keysFor (parts (insert X H));  X : synth (analz H) |] \
 \              ==> K : keysFor (parts H) | Key K : parts H";
-by (fast_tac
+by (force_tac
       (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono),
 			impOfSubs (analz_subset_parts RS keysFor_mono)]
-		addIs  [impOfSubs analz_subset_parts]
-                addss  (simpset())) 1);
+		addIs  [impOfSubs analz_subset_parts],
+       simpset()) 1);
 qed "keysFor_parts_insert";
 
 Goal "Crypt K X : H ==> K : keysFor H";
@@ -41,22 +41,21 @@
 qed "Crypt_imp_keysFor";
 
 
-(*** Function "spies" ***)
+(*** Function "knows" ***)
 
 (*Spy sees shared keys of agents!*)
-Goal "A: bad ==> Key (shrK A) : spies evs";
+Goal "A: bad ==> Key (shrK A) : knows Spy evs";
 by (induct_tac "evs" 1);
 by (ALLGOALS (asm_simp_tac
-	      (simpset() addsimps [imageI, spies_Cons]
+	      (simpset() addsimps [imageI, knows_Cons]
 	                addsplits [expand_event_case])));
-qed "Spy_spies_bad";
-
-AddSIs [Spy_spies_bad];
+qed "Spy_knows_Spy_bad";
+AddSIs [Spy_knows_Spy_bad];
 
 (*For not_bad_tac*)
-Goal "[| Crypt (shrK A) X : analz (spies evs);  A: bad |] \
-\              ==> X : analz (spies evs)";
-by (fast_tac (claset() addSDs [analz.Decrypt] addss (simpset())) 1);
+Goal "[| Crypt (shrK A) X : analz (knows Spy evs);  A: bad |] \
+\              ==> X : analz (knows Spy evs)";
+by (force_tac (claset() addSDs [analz.Decrypt], simpset()) 1);
 qed "Crypt_Spy_analz_bad";
 
 (*Prove that the agent is uncompromised by the confidentiality of 
@@ -202,7 +201,8 @@
     such as  Nonce ?N ~: used evs that match Nonce_supply*)
 fun possibility_tac st = st |>
    (REPEAT 
-    (ALLGOALS (simp_tac (simpset() delsimps [used_Says] setSolver safe_solver))
+    (ALLGOALS (simp_tac (simpset() delsimps [used_Says, used_Notes, used_Gets] 
+                         setSolver safe_solver))
      THEN
      REPEAT_FIRST (eq_assume_tac ORELSE' 
                    resolve_tac [refl, conjI, Nonce_supply, Key_supply])));
diff -r fdf236c98914 -r 76f3865a2b1d src/HOL/Auth/TLS.ML
--- a/src/HOL/Auth/TLS.ML	Mon Mar 08 13:49:53 1999 +0100
+++ b/src/HOL/Auth/TLS.ML	Tue Mar 09 11:01:39 1999 +0100
@@ -480,7 +480,7 @@
 (*ClientAccepts and ServerAccepts: because PMS was already visible*)
 by (REPEAT (blast_tac (claset() addDs [Spy_not_see_PMS, 
 				       Says_imp_spies RS analz.Inj,
-				       Notes_imp_spies RS analz.Inj]) 6));
+				       Notes_imp_knows_Spy RS analz.Inj]) 6));
 (*ClientHello*)
 by (Blast_tac 3);
 (*SpyKeys: by secrecy of the PMS, Spy cannot make the MS*)