# HG changeset patch
# User paulson
# Date 905260631 -7200
# Node ID 9b4bed3f394cf6eade2f0a63e4f04f0337aee932
# Parent  b66a23a453773ac516e3de59df428baea43b0f40
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems

diff -r b66a23a45377 -r 9b4bed3f394c src/HOL/Auth/Kerberos_BAN.ML
--- a/src/HOL/Auth/Kerberos_BAN.ML	Tue Sep 08 14:54:21 1998 +0200
+++ b/src/HOL/Auth/Kerberos_BAN.ML	Tue Sep 08 15:17:11 1998 +0200
@@ -24,8 +24,7 @@
 
 
 (*A "possibility property": there are traces that reach the end.*)
-Goal "[| A ~= B; A ~= Server; B ~= Server |]       \
-\     ==> EX Timestamp K. EX evs: kerberos_ban.    \
+Goal "EX Timestamp K. EX evs: kerberos_ban.    \
 \            Says B A (Crypt K (Number Timestamp)) \
 \                 : set evs";
 by (cut_facts_tac [SesKeyLife_LB] 1);
@@ -41,15 +40,6 @@
 
 (**** Inductive proofs about kerberos_ban ****)
 
-(*Nobody sends themselves messages*)
-Goal "evs : kerberos_ban ==> ALL X. Says A A X ~: set evs";
-by (etac kerberos_ban.induct 1);
-by Auto_tac;
-qed_spec_mp "not_Says_to_self";
-Addsimps [not_Says_to_self];
-AddSEs   [not_Says_to_self RSN (2, rev_notE)];
-
-
 (*Forwarding Lemma for reasoning about the encrypted portion of message Kb3*)
 Goal "Says S A (Crypt KA {|Timestamp, B, K, X|}) : set evs \
 \             ==> X : parts (spies evs)";
diff -r b66a23a45377 -r 9b4bed3f394c src/HOL/Auth/Kerberos_BAN.thy
--- a/src/HOL/Auth/Kerberos_BAN.thy	Tue Sep 08 14:54:21 1998 +0200
+++ b/src/HOL/Auth/Kerberos_BAN.thy	Tue Sep 08 15:17:11 1998 +0200
@@ -48,18 +48,16 @@
 
     Nil  "[]: kerberos_ban"
 
-
-    Fake "[| evs: kerberos_ban;  B ~= Spy;  
-             X: synth (analz (spies evs)) |]
+    Fake "[| evs: kerberos_ban;  X: synth (analz (spies evs)) |]
           ==> Says Spy B X # evs : kerberos_ban"
 
 
-    Kb1  "[| evs1: kerberos_ban;  A ~= Server |]
+    Kb1  "[| evs1: kerberos_ban |]
           ==> Says A Server {|Agent A, Agent B|} # evs1
                 :  kerberos_ban"
 
 
-    Kb2  "[| evs2: kerberos_ban;  A ~= B;  A ~= Server;  Key KAB ~: used evs2;
+    Kb2  "[| evs2: kerberos_ban;  Key KAB ~: used evs2;
              Says A' Server {|Agent A, Agent B|} : set evs2 |]
           ==> Says Server A 
                 (Crypt (shrK A)
@@ -68,7 +66,7 @@
                 # evs2 : kerberos_ban"
 
 
-    Kb3  "[| evs3: kerberos_ban;  A ~= B; 
+    Kb3  "[| evs3: kerberos_ban;  
              Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) 
                : set evs3;
              Says A Server {|Agent A, Agent B|} : set evs3;
@@ -77,21 +75,19 @@
                # evs3 : kerberos_ban"
 
 
-    Kb4  "[| evs4: kerberos_ban;  A ~= B;  
+    Kb4  "[| evs4: kerberos_ban;  
              Says A' B {|(Crypt (shrK B) {|Number Ts, Agent A, Key K|}), 
 		         (Crypt K {|Agent A, Number Ta|}) |}: set evs4;
-             ~ Expired Ts evs4; 
-             RecentAuth Ta evs4|]
+             ~ Expired Ts evs4;  RecentAuth Ta evs4 |]
           ==> Says B A (Crypt K (Number Ta)) # evs4
                 : kerberos_ban"
 
-
-(*The session key has EXPIRED when it gets lost *)
-    Oops "[| evso: kerberos_ban;  A ~= Spy;
+         (*Old session keys may become compromised*)
+    Oops "[| evso: kerberos_ban;  
              Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})
                : set evso;
              Expired Ts evso |]
-          ==> Says A Spy {|Number Ts, Key K|} # evso : kerberos_ban"
+          ==> Notes Spy {|Number Ts, Key K|} # evso : kerberos_ban"
 
 
 end
diff -r b66a23a45377 -r 9b4bed3f394c src/HOL/Auth/NS_Public.ML
--- a/src/HOL/Auth/NS_Public.ML	Tue Sep 08 14:54:21 1998 +0200
+++ b/src/HOL/Auth/NS_Public.ML	Tue Sep 08 15:17:11 1998 +0200
@@ -14,8 +14,8 @@
 AddIffs [Spy_in_bad];
 
 (*A "possibility property": there are traces that reach the end*)
-Goal "A ~= B ==> EX NB. EX evs: ns_public.               \
-\                  Says A B (Crypt (pubK B) (Nonce NB)) : set evs";
+Goal
+   "EX NB. EX evs: ns_public. Says A B (Crypt (pubK B) (Nonce NB)) : set evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
 by (rtac (ns_public.Nil RS ns_public.NS1 RS ns_public.NS2 RS ns_public.NS3) 2);
 by possibility_tac;
@@ -24,15 +24,6 @@
 
 (**** Inductive proofs about ns_public ****)
 
-(*Nobody sends themselves messages*)
-Goal "evs : ns_public ==> ALL X. Says A A X ~: set evs";
-by (etac ns_public.induct 1);
-by Auto_tac;
-qed_spec_mp "not_Says_to_self";
-Addsimps [not_Says_to_self];
-AddSEs   [not_Says_to_self RSN (2, rev_notE)];
-
-
 (*Induction for regularity theorems.  If induction formula has the form
    X ~: analz (spies evs) --> ... then it shortens the proof by discarding
    needless information about analz (insert X (spies evs))  *)
diff -r b66a23a45377 -r 9b4bed3f394c src/HOL/Auth/NS_Public.thy
--- a/src/HOL/Auth/NS_Public.thy	Tue Sep 08 14:54:21 1998 +0200
+++ b/src/HOL/Auth/NS_Public.thy	Tue Sep 08 15:17:11 1998 +0200
@@ -19,17 +19,16 @@
          (*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: ns_public;  B ~= Spy;  
-             X: synth (analz (spies evs)) |]
+    Fake "[| evs: ns_public;  X: synth (analz (spies evs)) |]
           ==> Says Spy B X  # evs : ns_public"
 
          (*Alice initiates a protocol run, sending a nonce to Bob*)
-    NS1  "[| evs1: ns_public;  A ~= B;  Nonce NA ~: used evs1 |]
+    NS1  "[| evs1: ns_public;  Nonce NA ~: used evs1 |]
           ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})
                  # evs1  :  ns_public"
 
          (*Bob responds to Alice's message with a further nonce*)
-    NS2  "[| evs2: ns_public;  A ~= B;  Nonce NB ~: used evs2;
+    NS2  "[| evs2: ns_public;  Nonce NB ~: used evs2;
              Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs2 |]
           ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})
                 # evs2  :  ns_public"
diff -r b66a23a45377 -r 9b4bed3f394c src/HOL/Auth/NS_Public_Bad.ML
--- a/src/HOL/Auth/NS_Public_Bad.ML	Tue Sep 08 14:54:21 1998 +0200
+++ b/src/HOL/Auth/NS_Public_Bad.ML	Tue Sep 08 15:17:11 1998 +0200
@@ -18,8 +18,8 @@
 AddIffs [Spy_in_bad];
 
 (*A "possibility property": there are traces that reach the end*)
-Goal "A ~= B ==> EX NB. EX evs: ns_public.               \
-\                  Says A B (Crypt (pubK B) (Nonce NB)) : set evs";
+Goal
+  "EX NB. EX evs: ns_public. Says A B (Crypt (pubK B) (Nonce NB)) : set evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
 by (rtac (ns_public.Nil RS ns_public.NS1 RS ns_public.NS2 RS ns_public.NS3) 2);
 by possibility_tac;
@@ -28,15 +28,6 @@
 
 (**** Inductive proofs about ns_public ****)
 
-(*Nobody sends themselves messages*)
-Goal "evs : ns_public ==> ALL X. Says A A X ~: set evs";
-by (etac ns_public.induct 1);
-by Auto_tac;
-qed_spec_mp "not_Says_to_self";
-Addsimps [not_Says_to_self];
-AddSEs   [not_Says_to_self RSN (2, rev_notE)];
-
-
 (*Induction for regularity theorems.  If induction formula has the form
    X ~: analz (spies evs) --> ... then it shortens the proof by discarding
    needless information about analz (insert X (spies evs))  *)
diff -r b66a23a45377 -r 9b4bed3f394c src/HOL/Auth/NS_Public_Bad.thy
--- a/src/HOL/Auth/NS_Public_Bad.thy	Tue Sep 08 14:54:21 1998 +0200
+++ b/src/HOL/Auth/NS_Public_Bad.thy	Tue Sep 08 15:17:11 1998 +0200
@@ -23,17 +23,16 @@
          (*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: ns_public;  B ~= Spy;  
-             X: synth (analz (spies evs)) |]
+    Fake "[| evs: ns_public;  X: synth (analz (spies evs)) |]
           ==> Says Spy B X  # evs : ns_public"
 
          (*Alice initiates a protocol run, sending a nonce to Bob*)
-    NS1  "[| evs1: ns_public;  A ~= B;  Nonce NA ~: used evs1 |]
+    NS1  "[| evs1: ns_public;  Nonce NA ~: used evs1 |]
           ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})
                 # evs1  :  ns_public"
 
          (*Bob responds to Alice's message with a further nonce*)
-    NS2  "[| evs2: ns_public;  A ~= B;  Nonce NB ~: used evs2;
+    NS2  "[| evs2: ns_public;  Nonce NB ~: used evs2;
              Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs2 |]
           ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|})
                 # evs2  :  ns_public"
diff -r b66a23a45377 -r 9b4bed3f394c src/HOL/Auth/NS_Shared.ML
--- a/src/HOL/Auth/NS_Shared.ML	Tue Sep 08 14:54:21 1998 +0200
+++ b/src/HOL/Auth/NS_Shared.ML	Tue Sep 08 15:17:11 1998 +0200
@@ -16,7 +16,7 @@
 
 
 (*A "possibility property": there are traces that reach the end*)
-Goal "[| A ~= B; A ~= Server; B ~= Server |]       \
+Goal "[| A ~= Server |]       \
 \        ==> EX N K. EX evs: ns_shared.               \
 \               Says A B (Crypt K {|Nonce N, Nonce N|}) : set evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
@@ -35,14 +35,6 @@
 
 (**** Inductive proofs about ns_shared ****)
 
-(*Nobody sends themselves messages*)
-Goal "evs : ns_shared ==> ALL X. Says A A X ~: set evs";
-by (etac ns_shared.induct 1);
-by Auto_tac;
-qed_spec_mp "not_Says_to_self";
-Addsimps [not_Says_to_self];
-AddSEs   [not_Says_to_self RSN (2, rev_notE)];
-
 (*For reasoning about the encrypted portion of message NS3*)
 Goal "Says S A (Crypt KA {|N, B, K, X|}) : set evs \
 \                ==> X : parts (spies evs)";
diff -r b66a23a45377 -r 9b4bed3f394c src/HOL/Auth/NS_Shared.thy
--- a/src/HOL/Auth/NS_Shared.thy	Tue Sep 08 14:54:21 1998 +0200
+++ b/src/HOL/Auth/NS_Shared.thy	Tue Sep 08 15:17:11 1998 +0200
@@ -21,12 +21,11 @@
          (*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: ns_shared;  B ~= Spy;  
-             X: synth (analz (spies evs)) |]
+    Fake "[| evs: ns_shared;  X: synth (analz (spies evs)) |]
           ==> Says Spy B X # evs : ns_shared"
 
          (*Alice initiates a protocol run, requesting to talk to any B*)
-    NS1  "[| evs1: ns_shared;  A ~= Server;  Nonce NA ~: used evs1 |]
+    NS1  "[| evs1: ns_shared;  Nonce NA ~: used evs1 |]
           ==> Says A Server {|Agent A, Agent B, Nonce NA|} # evs1
                 :  ns_shared"
 
@@ -34,7 +33,7 @@
            !! It may respond more than once to A's request !!
 	   Server doesn't know who the true sender is, hence the A' in
                the sender field.*)
-    NS2  "[| evs2: ns_shared;  A ~= B;  A ~= Server;  Key KAB ~: used evs2;
+    NS2  "[| evs2: ns_shared;  Key KAB ~: used evs2;
              Says A' Server {|Agent A, Agent B, Nonce NA|} : set evs2 |]
           ==> Says Server A 
                 (Crypt (shrK A)
@@ -43,8 +42,8 @@
                 # evs2 : ns_shared"
 
           (*We can't assume S=Server.  Agent A "remembers" her nonce.
-            Can inductively show A ~= Server*)
-    NS3  "[| evs3: ns_shared;  A ~= B;
+            Need A ~= Server because we allow messages to self.*)
+    NS3  "[| evs3: ns_shared;  A ~= Server;
              Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|}) 
                : set evs3;
              Says A Server {|Agent A, Agent B, Nonce NA|} : set evs3 |]
@@ -52,7 +51,7 @@
 
          (*Bob's nonce exchange.  He does not know who the message came
            from, but responds to A because she is mentioned inside.*)
-    NS4  "[| evs4: ns_shared;  A ~= B;  Nonce NB ~: used evs4;
+    NS4  "[| evs4: ns_shared;  Nonce NB ~: used evs4;
              Says A' B (Crypt (shrK B) {|Key K, Agent A|}) : set evs4 |]
           ==> Says B A (Crypt K (Nonce NB)) # evs4
                 : ns_shared"
@@ -62,7 +61,7 @@
            We do NOT send NB-1 or similar as the Spy cannot spoof such things.
            Letting the Spy add or subtract 1 lets him send ALL nonces.
            Instead we distinguish the messages by sending the nonce twice.*)
-    NS5  "[| evs5: ns_shared;  A ~= B;  
+    NS5  "[| evs5: ns_shared;  
              Says B' A (Crypt K (Nonce NB)) : set evs5;
              Says S  A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
                : set evs5 |]
diff -r b66a23a45377 -r 9b4bed3f394c src/HOL/Auth/OtwayRees.ML
--- a/src/HOL/Auth/OtwayRees.ML	Tue Sep 08 14:54:21 1998 +0200
+++ b/src/HOL/Auth/OtwayRees.ML	Tue Sep 08 15:17:11 1998 +0200
@@ -18,7 +18,7 @@
 
 
 (*A "possibility property": there are traces that reach the end*)
-Goal "[| A ~= B; A ~= Server; B ~= Server |]   \
+Goal "[| B ~= Server |]   \
 \     ==> EX K. EX NA. EX evs: otway.          \
 \            Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
 \              : set evs";
@@ -30,15 +30,6 @@
 
 (**** Inductive proofs about otway ****)
 
-(*Nobody sends themselves messages*)
-Goal "evs : otway ==> ALL X. Says A A X ~: set evs";
-by (etac otway.induct 1);
-by Auto_tac;
-qed_spec_mp "not_Says_to_self";
-Addsimps [not_Says_to_self];
-AddSEs   [not_Says_to_self RSN (2, rev_notE)];
-
-
 (** For reasoning about the encrypted portion of messages **)
 
 Goal "Says A' B {|N, Agent A, Agent B, X|} : set evs \
diff -r b66a23a45377 -r 9b4bed3f394c src/HOL/Auth/OtwayRees.thy
--- a/src/HOL/Auth/OtwayRees.thy	Tue Sep 08 14:54:21 1998 +0200
+++ b/src/HOL/Auth/OtwayRees.thy	Tue Sep 08 15:17:11 1998 +0200
@@ -20,15 +20,16 @@
          (*Initial trace is empty*)
     Nil  "[]: otway"
 
+         (** These rules allow agents to send messages to themselves **)
+
          (*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;  B ~= Spy;  
-             X: synth (analz (spies evs)) |]
+    Fake "[| evs: otway;  X: synth (analz (spies evs)) |]
           ==> Says Spy B X  # evs : otway"
 
          (*Alice initiates a protocol run*)
-    OR1  "[| evs1: otway;  A ~= B;  B ~= Server;  Nonce NA ~: used evs1 |]
+    OR1  "[| evs1: otway;  Nonce NA ~: used evs1 |]
           ==> Says A B {|Nonce NA, Agent A, Agent B, 
                          Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |} 
                  # evs1 : otway"
@@ -36,7 +37,7 @@
          (*Bob's response to Alice's message.  Bob doesn't know who 
 	   the sender is, hence the A' in the sender field.
            Note that NB is encrypted.*)
-    OR2  "[| evs2: otway;  B ~= Server;  Nonce NB ~: used evs2;
+    OR2  "[| evs2: otway;  Nonce NB ~: used evs2;
              Says A' B {|Nonce NA, Agent A, Agent B, X|} : set evs2 |]
           ==> Says B Server 
                   {|Nonce NA, Agent A, Agent B, X, 
@@ -47,7 +48,7 @@
          (*The Server receives Bob's message and checks that the three NAs
            match.  Then he sends a new session key to Bob with a packet for
            forwarding to Alice.*)
-    OR3  "[| evs3: otway;  B ~= Server;  Key KAB ~: used evs3;
+    OR3  "[| evs3: otway;  Key KAB ~: used evs3;
              Says B' Server 
                   {|Nonce NA, Agent A, Agent B, 
                     Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}, 
@@ -60,8 +61,9 @@
                  # evs3 : otway"
 
          (*Bob receives the Server's (?) message and compares the Nonces with
-	   those in the message he previously sent the Server.*)
-    OR4  "[| evs4: otway;  A ~= B;  
+	   those in the message he previously sent the Server.
+           Need B ~= Server because we allow messages to self.*)
+    OR4  "[| evs4: otway;  B ~= Server;
              Says B Server {|Nonce NA, Agent A, Agent B, X', 
                              Crypt (shrK B)
                                    {|Nonce NA, Nonce NB, Agent A, Agent B|}|}
diff -r b66a23a45377 -r 9b4bed3f394c src/HOL/Auth/OtwayRees_AN.ML
--- a/src/HOL/Auth/OtwayRees_AN.ML	Tue Sep 08 14:54:21 1998 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.ML	Tue Sep 08 15:17:11 1998 +0200
@@ -18,10 +18,10 @@
 
 
 (*A "possibility property": there are traces that reach the end*)
-Goal "[| A ~= B; A ~= Server; B ~= Server |]                            \
-\  ==> EX K. EX NA. EX evs: otway.                                      \
-\       Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) \
-\       : set evs";
+Goal "[| B ~= Server |]   \
+\     ==> EX K. EX NA. EX evs: otway.                                      \
+\          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 possibility_tac;
@@ -30,15 +30,6 @@
 
 (**** Inductive proofs about otway ****)
 
-(*Nobody sends themselves messages*)
-Goal "evs : otway ==> ALL X. Says A A X ~: set evs";
-by (etac otway.induct 1);
-by Auto_tac;
-qed_spec_mp "not_Says_to_self";
-Addsimps [not_Says_to_self];
-AddSEs   [not_Says_to_self RSN (2, rev_notE)];
-
-
 (** For reasoning about the encrypted portion of messages **)
 
 Goal "Says S' B {|X, Crypt(shrK B) X'|} : set evs ==> \
@@ -196,12 +187,12 @@
 (**** Authenticity properties relating to NA ****)
 
 (*If the encrypted message appears then it originated with the Server!*)
-Goal "[| A ~: bad;  evs : otway |]                 \
-\ ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|} : parts (spies 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|}|}    \
-\               : set evs)";
+Goal "[| A ~: bad;  A ~= B;  evs : otway |]                 \
+\     ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|} : parts (spies 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|}|}    \
+\                   : set evs)";
 by (parts_induct_tac 1);
 by (Blast_tac 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib])));
@@ -214,7 +205,7 @@
   Freshness may be inferred from nonce NA.*)
 Goal "[| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|})  \
 \         : set evs;                                                 \
-\        A ~: bad;  evs : otway |]                                  \
+\        A ~: bad;  A ~= B;  evs : otway |]                          \
 \     ==> 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|}|} \
@@ -266,8 +257,8 @@
   what it is.*)
 Goal "[| Says B' 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;  evs : otway |]                    \
+\        ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs;             \
+\        A ~: bad;  B ~: bad;  A ~= B;  evs : otway |]               \
 \     ==> Key K ~: analz (spies evs)";
 by (blast_tac (claset() addSDs [A_trusts_OR4, Spy_not_see_encrypted_key]) 1);
 qed "A_gets_good_key";
@@ -276,7 +267,7 @@
 (**** Authenticity properties relating to NB ****)
 
 (*If the encrypted message appears then it originated with the Server!*)
-Goal "[| B ~: bad;  evs : otway |]                                 \
+Goal "[| B ~: bad;  A ~= B;  evs : otway |]                              \
 \ ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|} : parts (spies evs) \
 \     --> (EX NA. Says Server B                                          \
 \                  {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
@@ -294,7 +285,7 @@
   has sent the correct message in round 3.*)
 Goal "[| Says S' B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
 \          : set evs;                                                    \
-\        B ~: bad;  evs : otway |]                                       \
+\        B ~: bad;  A ~= B;  evs : otway |]                              \
 \     ==> 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|}|}    \
@@ -305,9 +296,9 @@
 
 (*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|}|} \
-\         : set evs;                                            \
-\        ALL NA. Notes Spy {|NA, NB, Key K|} ~: set evs;                \
-\        A ~: bad;  B ~: bad;  evs : otway |]                   \
+\         : 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)";
 by (blast_tac (claset() addDs [B_trusts_OR3, Spy_not_see_encrypted_key]) 1);
 qed "B_gets_good_key";
diff -r b66a23a45377 -r 9b4bed3f394c src/HOL/Auth/OtwayRees_AN.thy
--- a/src/HOL/Auth/OtwayRees_AN.thy	Tue Sep 08 14:54:21 1998 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.thy	Tue Sep 08 15:17:11 1998 +0200
@@ -28,24 +28,23 @@
          (*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;  B ~= Spy;  
-             X: synth (analz (spies evs)) |]
+    Fake "[| evs: otway;  X: synth (analz (spies evs)) |]
           ==> Says Spy B X  # evs : otway"
 
          (*Alice initiates a protocol run*)
-    OR1  "[| evs1: otway;  A ~= B;  B ~= Server |]
+    OR1  "[| evs1: otway |]
           ==> Says A B {|Agent A, Agent B, Nonce NA|} # evs1 : otway"
 
          (*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;  B ~= Server;
+    OR2  "[| evs2: otway;  
              Says A' 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;  B ~= Server;  A ~= B;  Key KAB ~: used evs3;
+    OR3  "[| evs3: otway;  Key KAB ~: used evs3;
              Says B' Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
                : set evs3 |]
           ==> Says Server B 
@@ -54,8 +53,9 @@
               # evs3 : otway"
 
          (*Bob receives the Server's (?) message and compares the Nonces with
-	   those in the message he previously sent the Server.*)
-    OR4  "[| evs4: otway;  A ~= B;
+	   those in the message he previously sent the Server.
+           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|}|}
                : set evs4 |]
diff -r b66a23a45377 -r 9b4bed3f394c src/HOL/Auth/OtwayRees_Bad.ML
--- a/src/HOL/Auth/OtwayRees_Bad.ML	Tue Sep 08 14:54:21 1998 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.ML	Tue Sep 08 15:17:11 1998 +0200
@@ -21,10 +21,10 @@
 
 
 (*A "possibility property": there are traces that reach the end*)
-Goal "[| A ~= B; A ~= Server; B ~= Server |]   \
-\  ==> EX K. EX NA. EX evs: otway.          \
-\         Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
-\           : set evs";
+Goal "[| A ~= B; B ~= Server |]   \
+\     ==> EX K. EX NA. 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 possibility_tac;
@@ -33,14 +33,6 @@
 
 (**** Inductive proofs about otway ****)
 
-(*Nobody sends themselves messages*)
-Goal "evs : otway ==> ALL X. Says A A X ~: set evs";
-by (etac otway.induct 1);
-by Auto_tac;
-qed_spec_mp "not_Says_to_self";
-Addsimps [not_Says_to_self];
-AddSEs   [not_Says_to_self RSN (2, rev_notE)];
-
 
 (** For reasoning about the encrypted portion of messages **)
 
@@ -232,9 +224,8 @@
 (*** Attempting to prove stronger properties ***)
 
 (*Only OR1 can have caused such a part of a message to appear.
-  I'm not sure why A ~= B premise is needed: OtwayRees.ML doesn't need it.
-  Perhaps it's because OR2 has two similar-looking encrypted messages in
-        this version.*)
+  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) --> \
 \         Says A B {|NA, Agent A, Agent B,                  \
diff -r b66a23a45377 -r 9b4bed3f394c src/HOL/Auth/OtwayRees_Bad.thy
--- a/src/HOL/Auth/OtwayRees_Bad.thy	Tue Sep 08 14:54:21 1998 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.thy	Tue Sep 08 15:17:11 1998 +0200
@@ -22,11 +22,11 @@
          (*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;  B ~= Spy;  X: synth (analz (spies evs)) |]
+    Fake "[| evs: otway;  X: synth (analz (spies evs)) |]
           ==> Says Spy B X  # evs : otway"
 
          (*Alice initiates a protocol run*)
-    OR1  "[| evs1: otway;  A ~= B;  B ~= Server;  Nonce NA ~: used evs1 |]
+    OR1  "[| evs1: otway;  Nonce NA ~: used evs1 |]
           ==> Says A B {|Nonce NA, Agent A, Agent B, 
                          Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |} 
                  # evs1 : otway"
@@ -34,7 +34,7 @@
          (*Bob's response to Alice's message.  Bob doesn't know who 
 	   the sender is, hence the A' in the sender field.
            We modify the published protocol by NOT encrypting NB.*)
-    OR2  "[| evs2: otway;  B ~= Server;  Nonce NB ~: used evs2;
+    OR2  "[| evs2: otway;  Nonce NB ~: used evs2;
              Says A' B {|Nonce NA, Agent A, Agent B, X|} : set evs2 |]
           ==> Says B Server 
                   {|Nonce NA, Agent A, Agent B, X, Nonce NB,
@@ -44,7 +44,7 @@
          (*The Server receives Bob's message and checks that the three NAs
            match.  Then he sends a new session key to Bob with a packet for
            forwarding to Alice.*)
-    OR3  "[| evs3: otway;  B ~= Server;  Key KAB ~: used evs3;
+    OR3  "[| evs3: otway;  Key KAB ~: used evs3;
              Says B' Server 
                   {|Nonce NA, Agent A, Agent B, 
                     Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}, 
@@ -58,8 +58,9 @@
                  # evs3 : otway"
 
          (*Bob receives the Server's (?) message and compares the Nonces with
-	   those in the message he previously sent the Server.*)
-    OR4  "[| evs4: otway;  A ~= B;
+	   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;
              Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB,
                              Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
                : set evs4;
diff -r b66a23a45377 -r 9b4bed3f394c src/HOL/Auth/Recur.ML
--- a/src/HOL/Auth/Recur.ML	Tue Sep 08 14:54:21 1998 +0200
+++ b/src/HOL/Auth/Recur.ML	Tue Sep 08 15:17:11 1998 +0200
@@ -8,7 +8,6 @@
 
 Pretty.setdepth 30;
 
-
 AddEs spies_partsEs;
 AddDs [impOfSubs analz_subset_parts];
 AddDs [impOfSubs Fake_parts_insert];
@@ -21,27 +20,24 @@
 
 
 (*Simplest case: Alice goes directly to the server*)
-Goal "A ~= Server                                                      \
-\ ==> EX K NA. EX evs: recur.                                           \
-\  Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|}, \
-\                  Agent Server|}  : set evs";
+Goal "EX K NA. EX evs: recur.                                           \
+\  Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|},   \
+\                  END|}  : set evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
-by (rtac (recur.Nil RS recur.RA1 RS 
-          (respond.One RSN (4,recur.RA3))) 2);
+by (rtac (recur.Nil RS recur.RA1 RS (respond.One RSN (3,recur.RA3))) 2);
 by possibility_tac;
 result();
 
 
 (*Case two: Alice, Bob and the server*)
-Goal "[| A ~= B; A ~= Server; B ~= Server |]                 \
-\ ==> EX K. EX NA. EX evs: recur.                               \
-\    Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
-\               Agent Server|}  : set evs";
+Goal "EX K. EX NA. EX evs: recur.                               \
+\       Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
+\                  END|}  : set evs";
 by (cut_facts_tac [Nonce_supply2, Key_supply2] 1);
 by (REPEAT (eresolve_tac [exE, conjE] 1));
 by (REPEAT (resolve_tac [exI,bexI] 1));
 by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS 
-          (respond.One RS respond.Cons RSN (4,recur.RA3)) RS
+          (respond.One RS respond.Cons RSN (3,recur.RA3)) RS
           recur.RA4) 2);
 by basic_possibility_tac;
 by (DEPTH_SOLVE (eresolve_tac [asm_rl, less_not_refl2, less_not_refl3] 1));
@@ -50,17 +46,16 @@
 
 (*Case three: Alice, Bob, Charlie and the server
   TOO SLOW to run every time!
-Goal "[| A ~= B; B ~= C; A ~= Server; B ~= Server; C ~= Server |]   \
-\ ==> EX K. EX NA. EX evs: recur.                                      \
-\    Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|},        \
-\               Agent Server|}  : set evs";
+Goal "EX K. EX NA. EX evs: recur.                                      \
+\       Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|},        \
+\                  END|}  : set evs";
 by (cut_facts_tac [Nonce_supply3, Key_supply3] 1);
 by (REPEAT (eresolve_tac [exE, conjE] 1));
 by (REPEAT (resolve_tac [exI,bexI] 1));
 by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS recur.RA2 RS 
           (respond.One RS respond.Cons RS respond.Cons RSN
-           (4,recur.RA3)) RS recur.RA4 RS recur.RA4) 2);
-(*SLOW: 70 seconds*)
+           (3,recur.RA3)) RS recur.RA4 RS recur.RA4) 2);
+(*SLOW: 33 seconds*)
 by basic_possibility_tac;
 by (DEPTH_SOLVE (swap_res_tac [refl, conjI, disjCI] 1 
 		 ORELSE
@@ -70,15 +65,6 @@
 
 (**** Inductive proofs about recur ****)
 
-(*Nobody sends themselves messages*)
-Goal "evs : recur ==> ALL X. Says A A X ~: set evs";
-by (etac recur.induct 1);
-by Auto_tac;
-qed_spec_mp "not_Says_to_self";
-Addsimps [not_Says_to_self];
-AddSEs   [not_Says_to_self RSN (2, rev_notE)];
-
-
 
 Goal "(PA,RB,KAB) : respond evs ==> Key KAB : parts{RB}";
 by (etac respond.induct 1);
@@ -253,7 +239,7 @@
 by (etac responses.induct 2);
 by (ALLGOALS Asm_simp_tac);
 (*Fake*)
-by (Fake_parts_insert_tac 1);
+by (blast_tac (claset() addIs [parts_insertI]) 1);
 qed "Hash_imp_body";
 
 
@@ -323,17 +309,6 @@
             (2, resp_analz_insert_lemma) RSN(2, rev_mp));
 
 
-(*The Server does not send such messages.  This theorem lets us avoid
-  assuming B~=Server in RA4.*)
-Goal "evs : recur \
-\     ==> ALL C X Y. Says Server C {|X, Agent Server, Y|} ~: set evs";
-by (etac recur.induct 1);
-by (etac (respond.induct) 5);
-by Auto_tac;
-qed_spec_mp "Says_Server_not";
-AddSEs [Says_Server_not RSN (2,rev_notE)];
-
-
 (*The last key returned by respond indeed appears in a certificate*)
 Goal "(Hash[Key(shrK A)] {|Agent A, B, NA, P|}, RA, K) : respond evs \
 \   ==> Crypt (shrK A) {|Key K, B, NA|} : parts {RA}";
diff -r b66a23a45377 -r 9b4bed3f394c src/HOL/Auth/Recur.thy
--- a/src/HOL/Auth/Recur.thy	Tue Sep 08 14:54:21 1998 +0200
+++ b/src/HOL/Auth/Recur.thy	Tue Sep 08 15:17:11 1998 +0200
@@ -8,6 +8,10 @@
 
 Recur = Shared +
 
+(*End marker for message bundles*)
+syntax        END :: msg
+translations "END" == "Number 0"
+
 (*Two session keys are distributed to each agent except for the initiator,
         who receives one.
   Perhaps the two session keys could be bundled into a single message.
@@ -15,17 +19,15 @@
 consts     respond :: "event list => (msg*msg*key)set"
 inductive "respond evs" (*Server's response to the nested message*)
   intrs
-    (*The message "Agent Server" marks the end of a list.*)
-    One  "[| A ~= Server;  Key KAB ~: used evs |]
-          ==> (Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, Agent Server|}, 
-               {|Crypt (shrK A) {|Key KAB, Agent B, Nonce NA|}, Agent Server|},
+    One  "[| Key KAB ~: used evs |]
+          ==> (Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, END|}, 
+               {|Crypt (shrK A) {|Key KAB, Agent B, Nonce NA|}, END|},
                KAB)   : respond evs"
 
     (*The most recent session key is passed up to the caller*)
     Cons "[| (PA, RA, KAB) : respond evs;  
              Key KBC ~: used evs;  Key KBC ~: parts {RA};
-             PA = Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, P|};
-             B ~= Server |]
+             PA = Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, P|} |]
           ==> (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|}, 
                {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, 
                  Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
@@ -41,7 +43,7 @@
 inductive "responses evs"       
   intrs
     (*Server terminates lists*)
-    Nil  "Agent Server : responses evs"
+    Nil  "END : responses evs"
 
     Cons "[| RA : responses evs;  Key KAB ~: used evs |]
           ==> {|Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
@@ -56,35 +58,31 @@
 
          (*The spy MAY say anything he CAN say.  Common to
            all similar protocols.*)
-    Fake "[| evs: recur;  B ~= Spy;  
-             X: synth (analz (spies evs)) |]
+    Fake "[| evs: recur;  X: synth (analz (spies evs)) |]
           ==> Says Spy B X  # evs : recur"
 
          (*Alice initiates a protocol run.
-           "Agent Server" is just a placeholder, to terminate the nesting.*)
-    RA1  "[| evs1: recur;  A ~= B;  A ~= Server;  Nonce NA ~: used evs1 |]
-          ==> Says A B 
-                (Hash[Key(shrK A)] 
-                 {|Agent A, Agent B, Nonce NA, Agent Server|})
+           END is a placeholder to terminate the nesting.*)
+    RA1  "[| evs1: recur;  Nonce NA ~: used evs1 |]
+          ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, END|})
               # evs1 : recur"
 
          (*Bob's response to Alice's message.  C might be the Server.
            We omit PA = {|XA, Agent A, Agent B, Nonce NA, P|} because
            it complicates proofs, so B may respond to any message at all!*)
-    RA2  "[| evs2: recur;  B ~= C;  B ~= Server;  Nonce NB ~: used evs2;
+    RA2  "[| evs2: recur;  Nonce NB ~: used evs2;
              Says A' B PA : set evs2 |]
           ==> Says B C (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|})
               # evs2 : recur"
 
          (*The Server receives Bob's message and prepares a response.*)
-    RA3  "[| evs3: recur;  B ~= Server;
-             Says B' Server PB : set evs3;
+    RA3  "[| evs3: recur;  Says B' Server PB : set evs3;
              (PB,RB,K) : respond evs3 |]
           ==> Says Server B RB # evs3 : recur"
 
          (*Bob receives the returned message and compares the Nonces with
            those in the message he previously sent the Server.*)
-    RA4  "[| evs4: recur;  A ~= B;  
+    RA4  "[| evs4: recur;  
              Says B  C {|XH, Agent B, Agent C, Nonce NB, 
                          XA, Agent A, Agent B, Nonce NA, P|} : set evs4;
              Says C' B {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, 
diff -r b66a23a45377 -r 9b4bed3f394c src/HOL/Auth/TLS.thy
--- a/src/HOL/Auth/TLS.thy	Tue Sep 08 14:54:21 1998 +0200
+++ b/src/HOL/Auth/TLS.thy	Tue Sep 08 15:17:11 1998 +0200
@@ -82,8 +82,7 @@
          "[]: tls"
 
     Fake (*The spy, an active attacker, MAY say anything he CAN say.*)
-         "[| evs: tls;  B ~= Spy;  
-             X: synth (analz (spies evs)) |]
+         "[| evs: tls;  X: synth (analz (spies evs)) |]
           ==> Says Spy B X # evs : tls"
 
     SpyKeys (*The spy may apply PRF & sessionK to available nonces*)
@@ -100,7 +99,7 @@
            UNIX TIME is omitted because the protocol doesn't use it.
            May assume NA ~: range PRF because CLIENT RANDOM is 28 bytes
 	   while MASTER SECRET is 48 bytes*)
-         "[| evsCH: tls;  A ~= B;  Nonce NA ~: used evsCH;  NA ~: range PRF |]
+         "[| evsCH: tls;  Nonce NA ~: used evsCH;  NA ~: range PRF |]
           ==> Says A B {|Agent A, Nonce NA, Number SID, Number PA|}
 	        # evsCH  :  tls"
 
@@ -109,14 +108,14 @@
 	   PB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.
            SERVER CERTIFICATE (7.4.2) is always present.
            CERTIFICATE_REQUEST (7.4.4) is implied.*)
-         "[| evsSH: tls;  A ~= B;  Nonce NB ~: used evsSH;  NB ~: range PRF;
+         "[| evsSH: tls;  Nonce NB ~: used evsSH;  NB ~: range PRF;
              Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}
 	       : set evsSH |]
           ==> Says B A {|Nonce NB, Number SID, Number PB|} # evsSH  :  tls"
 
     Certificate
          (*SERVER (7.4.2) or CLIENT (7.4.6) CERTIFICATE.*)
-         "[| evsC: tls;  A ~= B |]
+         "[| evsC: tls |]
           ==> Says B A (certificate B (pubK B)) # evsC  :  tls"
 
     ClientKeyExch
@@ -128,7 +127,7 @@
 	   both items have the same length, 48 bytes).
            The Note event records in the trace that she knows PMS
                (see REMARK at top). *)
-         "[| evsCX: tls;  A ~= B;  Nonce PMS ~: used evsCX;  PMS ~: range PRF;
+         "[| evsCX: tls;  Nonce PMS ~: used evsCX;  PMS ~: range PRF;
              Says B' A (certificate B KB) : set evsCX |]
           ==> Says A B (Crypt KB (Nonce PMS))
 	      # Notes A {|Agent B, Nonce PMS|}
@@ -140,7 +139,7 @@
           It adds the pre-master-secret, which is also essential!
           Checking the signature, which is the only use of A's certificate,
           assures B of A's presence*)
-         "[| evsCV: tls;  A ~= B;  
+         "[| evsCV: tls;  
              Says B' A {|Nonce NB, Number SID, Number PB|} : set evsCV;
 	     Notes A {|Agent B, Nonce PMS|} : set evsCV |]
           ==> Says A B (Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|}))
@@ -206,6 +205,7 @@
           needed to resume this session.  The "Says A'' B ..." premise is
           used to prove Notes_master_imp_Crypt_PMS.*)
          "[| evsSA: tls;
+	     A ~= B;
              Says A'' B (Crypt (pubK B) (Nonce PMS)) : set evsSA;
 	     M = PRF(PMS,NA,NB);  
 	     X = Hash{|Number SID, Nonce M,
@@ -245,8 +245,9 @@
     Oops 
          (*The most plausible compromise is of an old session key.  Losing
            the MASTER SECRET or PREMASTER SECRET is more serious but
-           rather unlikely.*)
-         "[| evso: tls;  A ~= Spy;  
+           rather unlikely.  The assumption A ~= Spy is essential: otherwise
+           the Spy could learn session keys merely by replaying messages!*)
+         "[| evso: tls;  A ~= Spy;
 	     Says A B (Crypt (sessionK((NA,NB,M),b)) X) : set evso |]
           ==> Says A Spy (Key (sessionK((NA,NB,M),b))) # evso  :  tls"
 
diff -r b66a23a45377 -r 9b4bed3f394c src/HOL/Auth/WooLam.ML
--- a/src/HOL/Auth/WooLam.ML	Tue Sep 08 14:54:21 1998 +0200
+++ b/src/HOL/Auth/WooLam.ML	Tue Sep 08 15:17:11 1998 +0200
@@ -16,8 +16,7 @@
 
 
 (*A "possibility property": there are traces that reach the end*)
-Goal "[| A ~= B; A ~= Server; B ~= Server |]   \
-\     ==> EX NB. EX evs: woolam.               \
+Goal "EX NB. EX evs: woolam.  \
 \           Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|}) : set evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
 by (rtac (woolam.Nil RS woolam.WL1 RS woolam.WL2 RS woolam.WL3 RS 
@@ -28,15 +27,6 @@
 
 (**** Inductive proofs about woolam ****)
 
-(*Nobody sends themselves messages*)
-Goal "evs : woolam ==> ALL X. Says A A X ~: set evs";
-by (etac woolam.induct 1);
-by Auto_tac;
-qed_spec_mp "not_Says_to_self";
-Addsimps [not_Says_to_self];
-AddSEs   [not_Says_to_self RSN (2, rev_notE)];
-
-
 (** For reasoning about the encrypted portion of messages **)
 
 Goal "Says A' B X : set evs ==> X : analz (spies evs)";
diff -r b66a23a45377 -r 9b4bed3f394c src/HOL/Auth/WooLam.thy
--- a/src/HOL/Auth/WooLam.thy	Tue Sep 08 14:54:21 1998 +0200
+++ b/src/HOL/Auth/WooLam.thy	Tue Sep 08 15:17:11 1998 +0200
@@ -22,20 +22,20 @@
          (*Initial trace is empty*)
     Nil  "[]: woolam"
 
+         (** These rules allow agents to send messages to themselves **)
+
          (*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: woolam;  B ~= Spy;  
-             X: synth (analz (spies evs)) |]
+    Fake "[| evs: woolam;  X: synth (analz (spies evs)) |]
           ==> Says Spy B X  # evs : woolam"
 
          (*Alice initiates a protocol run*)
-    WL1  "[| evs1: woolam;  A ~= B |]
+    WL1  "[| evs1: woolam |]
           ==> Says A B (Agent A) # evs1 : woolam"
 
          (*Bob responds to Alice's message with a challenge.*)
-    WL2  "[| evs2: woolam;  A ~= B;  
-             Says A' B (Agent A) : set evs2 |]
+    WL2  "[| evs2: woolam;  Says A' B (Agent A) : set evs2 |]
           ==> Says B A (Nonce NB) # evs2 : woolam"
 
          (*Alice responds to Bob's challenge by encrypting NB with her key.
@@ -50,13 +50,13 @@
            the messages are shown in chronological order, for clarity.
            But here, exchanging the two events would cause the lemma
            WL4_analz_spies to pick up the wrong assumption!*)
-    WL4  "[| evs4: woolam;  B ~= Server;  
+    WL4  "[| evs4: woolam;  
              Says A'  B X         : set evs4;
              Says A'' B (Agent A) : set evs4 |]
           ==> Says B Server {|Agent A, Agent B, X|} # evs4 : woolam"
 
          (*Server decrypts Alice's response for Bob.*)
-    WL5  "[| evs5: woolam;  B ~= Server;
+    WL5  "[| evs5: woolam;  
              Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|}
                : set evs5 |]
           ==> Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|})
diff -r b66a23a45377 -r 9b4bed3f394c src/HOL/Auth/Yahalom.ML
--- a/src/HOL/Auth/Yahalom.ML	Tue Sep 08 14:54:21 1998 +0200
+++ b/src/HOL/Auth/Yahalom.ML	Tue Sep 08 15:17:11 1998 +0200
@@ -14,7 +14,7 @@
 
 
 (*A "possibility property": there are traces that reach the end*)
-Goal "[| A ~= B; A ~= Server; B ~= Server |]   \
+Goal "A ~= Server \
 \     ==> EX X NB K. EX evs: yahalom.          \
 \            Says A B {|X, Crypt K (Nonce NB)|} : set evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
@@ -26,14 +26,6 @@
 
 (**** Inductive proofs about yahalom ****)
 
-(*Nobody sends themselves messages*)
-Goal "evs: yahalom ==> ALL X. Says A A X ~: set evs";
-by (etac yahalom.induct 1);
-by Auto_tac;
-qed_spec_mp "not_Says_to_self";
-Addsimps [not_Says_to_self];
-AddSEs   [not_Says_to_self RSN (2, rev_notE)];
-
 
 (** For reasoning about the encrypted portion of messages **)
 
@@ -109,8 +101,7 @@
 (*Describes the form of K when the Server sends this message.  Useful for
   Oops as well as main secrecy property.*)
 Goal "[| Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} \
-\          : set evs;                                                   \
-\        evs : yahalom |]                                          \
+\          : set evs;   evs : yahalom |]                                \
 \     ==> K ~: range shrK";
 by (etac rev_mp 1);
 by (etac yahalom.induct 1);
diff -r b66a23a45377 -r 9b4bed3f394c src/HOL/Auth/Yahalom.thy
--- a/src/HOL/Auth/Yahalom.thy	Tue Sep 08 14:54:21 1998 +0200
+++ b/src/HOL/Auth/Yahalom.thy	Tue Sep 08 15:17:11 1998 +0200
@@ -21,17 +21,16 @@
          (*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: yahalom;  B ~= Spy;  
-             X: synth (analz (spies evs)) |]
+    Fake "[| evs: yahalom;  X: synth (analz (spies evs)) |]
           ==> Says Spy B X  # evs : yahalom"
 
          (*Alice initiates a protocol run*)
-    YM1  "[| evs1: yahalom;  A ~= B;  Nonce NA ~: used evs1 |]
+    YM1  "[| evs1: yahalom;  Nonce NA ~: used evs1 |]
           ==> Says A B {|Agent A, Nonce NA|} # evs1 : yahalom"
 
          (*Bob's response to Alice's message.  Bob doesn't know who 
 	   the sender is, hence the A' in the sender field.*)
-    YM2  "[| evs2: yahalom;  B ~= Server;  Nonce NB ~: used evs2;
+    YM2  "[| evs2: yahalom;  Nonce NB ~: used evs2;
              Says A' B {|Agent A, Nonce NA|} : set evs2 |]
           ==> Says B Server 
                   {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
@@ -39,7 +38,7 @@
 
          (*The Server receives Bob's message.  He responds by sending a
             new session key to Alice, with a packet for forwarding to Bob.*)
-    YM3  "[| evs3: yahalom;  A ~= Server;  Key KAB ~: used evs3;
+    YM3  "[| evs3: yahalom;  Key KAB ~: used evs3;
              Says B' Server 
                   {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
                : set evs3 |]
@@ -50,8 +49,8 @@
 
          (*Alice receives the Server's (?) message, checks her Nonce, and
            uses the new session key to send Bob his Nonce.  The premise
-           A ~= Server is needed to prove Says_Server_message_form.*)
-    YM4  "[| evs4: yahalom;  A ~= Server;  
+           A ~= Server is needed to prove Says_Server_not_range.*)
+    YM4  "[| evs4: yahalom;  A ~= Server;
              Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|},
                         X|}  : set evs4;
              Says A B {|Agent A, Nonce NA|} : set evs4 |]
diff -r b66a23a45377 -r 9b4bed3f394c src/HOL/Auth/Yahalom2.ML
--- a/src/HOL/Auth/Yahalom2.ML	Tue Sep 08 14:54:21 1998 +0200
+++ b/src/HOL/Auth/Yahalom2.ML	Tue Sep 08 15:17:11 1998 +0200
@@ -18,8 +18,7 @@
 
 
 (*A "possibility property": there are traces that reach the end*)
-Goal "[| A ~= B; A ~= Server; B ~= Server |]   \
-\     ==> EX X NB K. EX evs: yahalom.          \
+Goal "EX X NB K. EX evs: yahalom.          \
 \            Says A B {|X, Crypt K (Nonce NB)|} : set evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
 by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS 
@@ -30,15 +29,6 @@
 
 (**** Inductive proofs about yahalom ****)
 
-(*Nobody sends themselves messages*)
-Goal "evs: yahalom ==> ALL X. Says A A X ~: set evs";
-by (etac yahalom.induct 1);
-by Auto_tac;
-qed_spec_mp "not_Says_to_self";
-Addsimps [not_Says_to_self];
-AddSEs   [not_Says_to_self RSN (2, rev_notE)];
-
-
 (** For reasoning about the encrypted portion of messages **)
 
 (*Lets us treat YM4 using a similar argument as for the Fake case.*)
@@ -114,7 +104,7 @@
 Goal "[| Says Server A {|nb', Crypt (shrK A) {|Agent B, Key K, na|}, X|} \
 \         : set evs;                                            \
 \        evs : yahalom |]                                       \
-\     ==> K ~: range shrK & A ~= B";
+\     ==> K ~: range shrK";
 by (etac rev_mp 1);
 by (etac yahalom.induct 1);
 by (ALLGOALS Asm_simp_tac);
@@ -191,8 +181,7 @@
 
 (** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
 
-Goal "[| A ~: bad;  B ~: bad;  A ~= B;                       \
-\        evs : yahalom |]                                    \
+Goal "[| A ~: bad;  B ~: bad;  evs : yahalom |]              \
 \     ==> Says Server A                                      \
 \           {|nb, Crypt (shrK A) {|Agent B, Key K, na|},     \
 \                 Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|} \
diff -r b66a23a45377 -r 9b4bed3f394c src/HOL/Auth/Yahalom2.thy
--- a/src/HOL/Auth/Yahalom2.thy	Tue Sep 08 14:54:21 1998 +0200
+++ b/src/HOL/Auth/Yahalom2.thy	Tue Sep 08 15:17:11 1998 +0200
@@ -24,17 +24,16 @@
          (*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: yahalom;  B ~= Spy;  
-             X: synth (analz (spies evs)) |]
+    Fake "[| evs: yahalom;  X: synth (analz (spies evs)) |]
           ==> Says Spy B X  # evs : yahalom"
 
          (*Alice initiates a protocol run*)
-    YM1  "[| evs1: yahalom;  A ~= B;  Nonce NA ~: used evs1 |]
+    YM1  "[| evs1: yahalom;  Nonce NA ~: used evs1 |]
           ==> Says A B {|Agent A, Nonce NA|} # evs1 : yahalom"
 
          (*Bob's response to Alice's message.  Bob doesn't know who 
 	   the sender is, hence the A' in the sender field.*)
-    YM2  "[| evs2: yahalom;  B ~= Server;  Nonce NB ~: used evs2;
+    YM2  "[| evs2: yahalom;  Nonce NB ~: used evs2;
              Says A' B {|Agent A, Nonce NA|} : set evs2 |]
           ==> Says B Server 
                   {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}
@@ -43,7 +42,7 @@
          (*The Server receives Bob's message.  He responds by sending a
            new session key to Alice, with a certificate for forwarding to Bob.
            Both agents are quoted in the 2nd certificate to prevent attacks!*)
-    YM3  "[| evs3: yahalom;  A ~= B;  A ~= Server;  Key KAB ~: used evs3;
+    YM3  "[| evs3: yahalom;  Key KAB ~: used evs3;
              Says B' Server {|Agent B, Nonce NB,
 			      Crypt (shrK B) {|Agent A, Nonce NA|}|}
                : set evs3 |]
@@ -55,7 +54,7 @@
 
          (*Alice receives the Server's (?) message, checks her Nonce, and
            uses the new session key to send Bob his Nonce.*)
-    YM4  "[| evs4: yahalom;  A ~= Server;  
+    YM4  "[| evs4: yahalom;  
              Says S A {|Nonce NB, Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
                         X|}  : set evs4;
              Says A B {|Agent A, Nonce NA|} : set evs4 |]