# HG changeset patch
# User paulson
# Date 873455053 -7200
# Node ID eddedfe2f3f81ec9a381d00a49f18bd3f1f34423
# Parent  f87dd7b68d8cdd87b1877fc6ea14817086983b85
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition

diff -r f87dd7b68d8c -r eddedfe2f3f8 src/HOL/Auth/NS_Public.thy
--- a/src/HOL/Auth/NS_Public.thy	Thu Sep 04 17:57:56 1997 +0200
+++ b/src/HOL/Auth/NS_Public.thy	Fri Sep 05 12:24:13 1997 +0200
@@ -24,22 +24,22 @@
           ==> Says Spy B X  # evs : ns_public"
 
          (*Alice initiates a protocol run, sending a nonce to Bob*)
-    NS1  "[| evs: ns_public;  A ~= B;  Nonce NA ~: used evs |]
+    NS1  "[| evs1: ns_public;  A ~= B;  Nonce NA ~: used evs1 |]
           ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})
-                 # evs  :  ns_public"
+                 # evs1  :  ns_public"
 
          (*Bob responds to Alice's message with a further nonce*)
-    NS2  "[| evs: ns_public;  A ~= B;  Nonce NB ~: used evs;
-             Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs |]
+    NS2  "[| evs2: ns_public;  A ~= B;  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|})
-                # evs  :  ns_public"
+                # evs2  :  ns_public"
 
          (*Alice proves her existence by sending NB back to Bob.*)
-    NS3  "[| evs: ns_public;
-             Says A  B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs;
+    NS3  "[| evs3: ns_public;
+             Says A  B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs3;
              Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})
-               : set evs |]
-          ==> Says A B (Crypt (pubK B) (Nonce NB)) # evs : ns_public"
+               : set evs3 |]
+          ==> Says A B (Crypt (pubK B) (Nonce NB)) # evs3 : ns_public"
 
   (**Oops message??**)
 
diff -r f87dd7b68d8c -r eddedfe2f3f8 src/HOL/Auth/NS_Public_Bad.thy
--- a/src/HOL/Auth/NS_Public_Bad.thy	Thu Sep 04 17:57:56 1997 +0200
+++ b/src/HOL/Auth/NS_Public_Bad.thy	Fri Sep 05 12:24:13 1997 +0200
@@ -28,21 +28,21 @@
           ==> Says Spy B X  # evs : ns_public"
 
          (*Alice initiates a protocol run, sending a nonce to Bob*)
-    NS1  "[| evs: ns_public;  A ~= B;  Nonce NA ~: used evs |]
+    NS1  "[| evs1: ns_public;  A ~= B;  Nonce NA ~: used evs1 |]
           ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})
-                # evs  :  ns_public"
+                # evs1  :  ns_public"
 
          (*Bob responds to Alice's message with a further nonce*)
-    NS2  "[| evs: ns_public;  A ~= B;  Nonce NB ~: used evs;
-             Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs |]
+    NS2  "[| evs2: ns_public;  A ~= B;  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|})
-                # evs  :  ns_public"
+                # evs2  :  ns_public"
 
          (*Alice proves her existence by sending NB back to Bob.*)
-    NS3  "[| evs: ns_public;
-             Says A  B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs;
-             Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs |]
-          ==> Says A B (Crypt (pubK B) (Nonce NB)) # evs : ns_public"
+    NS3  "[| evs3: ns_public;
+             Says A  B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs3;
+             Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs3 |]
+          ==> Says A B (Crypt (pubK B) (Nonce NB)) # evs3 : ns_public"
 
   (**Oops message??**)
 
diff -r f87dd7b68d8c -r eddedfe2f3f8 src/HOL/Auth/NS_Shared.thy
--- a/src/HOL/Auth/NS_Shared.thy	Thu Sep 04 17:57:56 1997 +0200
+++ b/src/HOL/Auth/NS_Shared.thy	Fri Sep 05 12:24:13 1997 +0200
@@ -26,35 +26,35 @@
           ==> Says Spy B X # evs : ns_shared"
 
          (*Alice initiates a protocol run, requesting to talk to any B*)
-    NS1  "[| evs: ns_shared;  A ~= Server;  Nonce NA ~: used evs |]
-          ==> Says A Server {|Agent A, Agent B, Nonce NA|} # evs
+    NS1  "[| evs1: ns_shared;  A ~= Server;  Nonce NA ~: used evs1 |]
+          ==> Says A Server {|Agent A, Agent B, Nonce NA|} # evs1
                 :  ns_shared"
 
          (*Server's response to Alice's message.
            !! 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  "[| evs: ns_shared;  A ~= B;  A ~= Server;  Key KAB ~: used evs;
-             Says A' Server {|Agent A, Agent B, Nonce NA|} : set evs |]
+    NS2  "[| evs2: ns_shared;  A ~= B;  A ~= Server;  Key KAB ~: used evs2;
+             Says A' Server {|Agent A, Agent B, Nonce NA|} : set evs2 |]
           ==> Says Server A 
                 (Crypt (shrK A)
                    {|Nonce NA, Agent B, Key KAB,
                      (Crypt (shrK B) {|Key KAB, Agent A|})|}) 
-                # evs : ns_shared"
+                # evs2 : ns_shared"
 
           (*We can't assume S=Server.  Agent A "remembers" her nonce.
             Can inductively show A ~= Server*)
-    NS3  "[| evs: ns_shared;  A ~= B;
+    NS3  "[| evs3: ns_shared;  A ~= B;
              Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|}) 
-               : set evs;
-             Says A Server {|Agent A, Agent B, Nonce NA|} : set evs |]
-          ==> Says A B X # evs : ns_shared"
+               : set evs3;
+             Says A Server {|Agent A, Agent B, Nonce NA|} : set evs3 |]
+          ==> Says A B X # evs3 : ns_shared"
 
          (*Bob's nonce exchange.  He does not know who the message came
            from, but responds to A because she is mentioned inside.*)
-    NS4  "[| evs: ns_shared;  A ~= B;  Nonce NB ~: used evs;
-             Says A' B (Crypt (shrK B) {|Key K, Agent A|}) : set evs |]
-          ==> Says B A (Crypt K (Nonce NB)) # evs
+    NS4  "[| evs4: ns_shared;  A ~= B;  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"
 
          (*Alice responds with Nonce NB if she has seen the key before.
@@ -62,19 +62,19 @@
            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  "[| evs: ns_shared;  A ~= B;  
-             Says B' A (Crypt K (Nonce NB)) : set evs;
+    NS5  "[| evs5: ns_shared;  A ~= B;  
+             Says B' A (Crypt K (Nonce NB)) : set evs5;
              Says S  A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
-               : set evs |]
-          ==> Says A B (Crypt K {|Nonce NB, Nonce NB|}) # evs : ns_shared"
+               : set evs5 |]
+          ==> Says A B (Crypt K {|Nonce NB, Nonce NB|}) # evs5 : ns_shared"
   
          (*This message models possible leaks of session keys.
            The two Nonces identify the protocol run: the rule insists upon
            the true senders in order to make them accurate.*)
-    Oops "[| evs: ns_shared;  A ~= Spy;
-             Says B A (Crypt K (Nonce NB)) : set evs;
+    Oops "[| evso: ns_shared;  A ~= Spy;
+             Says B A (Crypt K (Nonce NB)) : set evso;
              Says Server A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
-               : set evs |]
-          ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : ns_shared"
+               : set evso |]
+          ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evso : ns_shared"
 
 end
diff -r f87dd7b68d8c -r eddedfe2f3f8 src/HOL/Auth/OtwayRees.thy
--- a/src/HOL/Auth/OtwayRees.thy	Thu Sep 04 17:57:56 1997 +0200
+++ b/src/HOL/Auth/OtwayRees.thy	Fri Sep 05 12:24:13 1997 +0200
@@ -28,53 +28,53 @@
           ==> Says Spy B X  # evs : otway"
 
          (*Alice initiates a protocol run*)
-    OR1  "[| evs: otway;  A ~= B;  B ~= Server;  Nonce NA ~: used evs |]
+    OR1  "[| evs1: otway;  A ~= B;  B ~= Server;  Nonce NA ~: used evs1 |]
           ==> Says A B {|Nonce NA, Agent A, Agent B, 
                          Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |} 
-                 # evs : otway"
+                 # evs1 : otway"
 
          (*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  "[| evs: otway;  B ~= Server;  Nonce NB ~: used evs;
-             Says A' B {|Nonce NA, Agent A, Agent B, X|} : set evs |]
+    OR2  "[| evs2: otway;  B ~= Server;  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, 
                     Crypt (shrK B)
                       {|Nonce NA, Nonce NB, Agent A, Agent B|}|}
-                 # evs : otway"
+                 # evs2 : otway"
 
          (*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  "[| evs: otway;  B ~= Server;  Key KAB ~: used evs;
+    OR3  "[| evs3: otway;  B ~= Server;  Key KAB ~: used evs3;
              Says B' 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|}|}
-               : set evs |]
+               : set evs3 |]
           ==> Says Server B 
                   {|Nonce NA, 
                     Crypt (shrK A) {|Nonce NA, Key KAB|},
                     Crypt (shrK B) {|Nonce NB, Key KAB|}|}
-                 # evs : otway"
+                 # evs3 : otway"
 
          (*Bob receives the Server's (?) message and compares the Nonces with
 	   those in the message he previously sent the Server.*)
-    OR4  "[| evs: otway;  A ~= B;  
+    OR4  "[| evs4: otway;  A ~= B;  
              Says B Server {|Nonce NA, Agent A, Agent B, X', 
                              Crypt (shrK B)
                                    {|Nonce NA, Nonce NB, Agent A, Agent B|}|}
-               : set evs;
+               : set evs4;
              Says S' B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
-               : set evs |]
-          ==> Says B A {|Nonce NA, X|} # evs : otway"
+               : set evs4 |]
+          ==> Says B A {|Nonce NA, X|} # evs4 : otway"
 
          (*This message models possible leaks of session keys.  The nonces
            identify the protocol run.*)
-    Oops "[| evs: otway;  B ~= Spy;
+    Oops "[| evso: otway;  B ~= Spy;
              Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
-               : set evs |]
-          ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway"
+               : set evso |]
+          ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evso : otway"
 
 end
diff -r f87dd7b68d8c -r eddedfe2f3f8 src/HOL/Auth/OtwayRees_AN.thy
--- a/src/HOL/Auth/OtwayRees_AN.thy	Thu Sep 04 17:57:56 1997 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.thy	Fri Sep 05 12:24:13 1997 +0200
@@ -33,41 +33,41 @@
           ==> Says Spy B X  # evs : otway"
 
          (*Alice initiates a protocol run*)
-    OR1  "[| evs: otway;  A ~= B;  B ~= Server |]
-          ==> Says A B {|Agent A, Agent B, Nonce NA|} # evs : otway"
+    OR1  "[| evs1: otway;  A ~= B;  B ~= Server |]
+          ==> 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  "[| evs: otway;  B ~= Server;
-             Says A' B {|Agent A, Agent B, Nonce NA|} : set evs |]
+    OR2  "[| evs2: otway;  B ~= Server;
+             Says A' B {|Agent A, Agent B, Nonce NA|} : set evs2 |]
           ==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
-                 # evs : otway"
+                 # 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  "[| evs: otway;  B ~= Server;  A ~= B;  Key KAB ~: used evs;
+    OR3  "[| evs3: otway;  B ~= Server;  A ~= B;  Key KAB ~: used evs3;
              Says B' Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
-               : set evs |]
+               : set evs3 |]
           ==> Says Server B 
                {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key KAB|},
                  Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key KAB|}|}
-              # evs : otway"
+              # evs3 : otway"
 
          (*Bob receives the Server's (?) message and compares the Nonces with
 	   those in the message he previously sent the Server.*)
-    OR4  "[| evs: otway;  A ~= B;
-             Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} : set evs;
+    OR4  "[| evs4: otway;  A ~= B;
+             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 evs |]
-          ==> Says B A X # evs : otway"
+               : set evs4 |]
+          ==> Says B A X # evs4 : otway"
 
          (*This message models possible leaks of session keys.  The nonces
            identify the protocol run.  B is not assumed to know shrK A.*)
-    Oops "[| evs: otway;  B ~= Spy;
+    Oops "[| evso: otway;  B ~= Spy;
              Says Server B 
                       {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}, 
                         Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key K|}|}
-               : set evs |]
-          ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway"
+               : set evso |]
+          ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evso : otway"
 
 end
diff -r f87dd7b68d8c -r eddedfe2f3f8 src/HOL/Auth/OtwayRees_Bad.thy
--- a/src/HOL/Auth/OtwayRees_Bad.thy	Thu Sep 04 17:57:56 1997 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.thy	Fri Sep 05 12:24:13 1997 +0200
@@ -26,51 +26,51 @@
           ==> Says Spy B X  # evs : otway"
 
          (*Alice initiates a protocol run*)
-    OR1  "[| evs: otway;  A ~= B;  B ~= Server;  Nonce NA ~: used evs |]
+    OR1  "[| evs1: otway;  A ~= B;  B ~= Server;  Nonce NA ~: used evs1 |]
           ==> Says A B {|Nonce NA, Agent A, Agent B, 
                          Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |} 
-                 # evs : otway"
+                 # evs1 : otway"
 
          (*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  "[| evs: otway;  B ~= Server;  Nonce NB ~: used evs;
-             Says A' B {|Nonce NA, Agent A, Agent B, X|} : set evs |]
+    OR2  "[| evs2: otway;  B ~= Server;  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,
                     Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
-                 # evs : otway"
+                 # evs2 : otway"
 
          (*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  "[| evs: otway;  B ~= Server;  Key KAB ~: used evs;
+    OR3  "[| evs3: otway;  B ~= Server;  Key KAB ~: used evs3;
              Says B' Server 
                   {|Nonce NA, Agent A, Agent B, 
                     Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}, 
                     Nonce NB, 
                     Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
-               : set evs |]
+               : set evs3 |]
           ==> Says Server B 
                   {|Nonce NA, 
                     Crypt (shrK A) {|Nonce NA, Key KAB|},
                     Crypt (shrK B) {|Nonce NB, Key KAB|}|}
-                 # evs : otway"
+                 # evs3 : otway"
 
          (*Bob receives the Server's (?) message and compares the Nonces with
 	   those in the message he previously sent the Server.*)
-    OR4  "[| evs: otway;  A ~= B;
+    OR4  "[| evs4: otway;  A ~= B;
              Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, X''|}
-               : set evs;
+               : set evs4;
              Says S' B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
-               : set evs |]
-          ==> Says B A {|Nonce NA, X|} # evs : otway"
+               : set evs4 |]
+          ==> Says B A {|Nonce NA, X|} # evs4 : otway"
 
          (*This message models possible leaks of session keys.  The nonces
            identify the protocol run.*)
-    Oops "[| evs: otway;  B ~= Spy;
+    Oops "[| evso: otway;  B ~= Spy;
              Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
-               : set evs |]
-          ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway"
+               : set evso |]
+          ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evso : otway"
 
 end
diff -r f87dd7b68d8c -r eddedfe2f3f8 src/HOL/Auth/Recur.thy
--- a/src/HOL/Auth/Recur.thy	Thu Sep 04 17:57:56 1997 +0200
+++ b/src/HOL/Auth/Recur.thy	Fri Sep 05 12:24:13 1997 +0200
@@ -62,11 +62,11 @@
 
          (*Alice initiates a protocol run.
            "Agent Server" is just a placeholder, to terminate the nesting.*)
-    RA1  "[| evs: recur;  A ~= B;  A ~= Server;  Nonce NA ~: used evs |]
+    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|})
-              # evs : recur"
+              # evs1 : recur"
 
          (*Bob's response to Alice's message.  C might be the Server.
            XA should be the Hash of the remaining components with KA, but
@@ -74,27 +74,27 @@
            P is the previous recur message from Alice's caller.
            NOTE: existing proofs don't need PA and are complicated by its
                 presence!  See parts_Fake_tac.*)
-    RA2  "[| evs: recur;  B ~= C;  B ~= Server;  Nonce NB ~: used evs;
-             Says A' B PA : set evs;  
+    RA2  "[| evs2: recur;  B ~= C;  B ~= Server;  Nonce NB ~: used evs2;
+             Says A' B PA : set evs2;  
              PA = {|XA, Agent A, Agent B, Nonce NA, P|} |]
           ==> Says B C (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|})
-              # evs : recur"
+              # evs2 : recur"
 
          (*The Server receives Bob's message and prepares a response.*)
-    RA3  "[| evs: recur;  B ~= Server;
-             Says B' Server PB : set evs;
-             (PB,RB,K) : respond evs |]
-          ==> Says Server B RB # evs : recur"
+    RA3  "[| evs3: recur;  B ~= Server;
+             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  "[| evs: recur;  A ~= B;  
+    RA4  "[| evs4: recur;  A ~= B;  
              Says B  C {|XH, Agent B, Agent C, Nonce NB, 
-                         XA, Agent A, Agent B, Nonce NA, P|} : set evs;
+                         XA, Agent A, Agent B, Nonce NA, P|} : set evs4;
              Says C' B {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, 
                          Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, 
-                         RA|} : set evs |]
-          ==> Says B A RA # evs : recur"
+                         RA|} : set evs4 |]
+          ==> Says B A RA # evs4 : recur"
 
 (**No "oops" message can easily be expressed.  Each session key is
    associated--in two separate messages--with two nonces.
diff -r f87dd7b68d8c -r eddedfe2f3f8 src/HOL/Auth/WooLam.thy
--- a/src/HOL/Auth/WooLam.thy	Thu Sep 04 17:57:56 1997 +0200
+++ b/src/HOL/Auth/WooLam.thy	Fri Sep 05 12:24:13 1997 +0200
@@ -30,36 +30,36 @@
           ==> Says Spy B X  # evs : woolam"
 
          (*Alice initiates a protocol run*)
-    WL1  "[| evs: woolam;  A ~= B |]
-          ==> Says A B (Agent A) # evs : woolam"
+    WL1  "[| evs1: woolam;  A ~= B |]
+          ==> Says A B (Agent A) # evs1 : woolam"
 
          (*Bob responds to Alice's message with a challenge.*)
-    WL2  "[| evs: woolam;  A ~= B;  
-             Says A' B (Agent A) : set evs |]
-          ==> Says B A (Nonce NB) # evs : woolam"
+    WL2  "[| evs2: woolam;  A ~= B;  
+             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.
            B is *not* properly determined -- Alice essentially broadcasts
            her reply.*)
-    WL3  "[| evs: woolam;
-             Says A  B (Agent A)  : set evs;
-             Says B' A (Nonce NB) : set evs |]
-          ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs : woolam"
+    WL3  "[| evs3: woolam;
+             Says A  B (Agent A)  : set evs3;
+             Says B' A (Nonce NB) : set evs3 |]
+          ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs3 : woolam"
 
          (*Bob forwards Alice's response to the Server.  NOTE: usually
            the messages are shown in chronological order, for clarity.
            But here, exchanging the two events would cause the lemma
            WL4_analz_sees_Spy to pick up the wrong assumption!*)
-    WL4  "[| evs: woolam;  B ~= Server;  
-             Says A'  B X         : set evs;
-             Says A'' B (Agent A) : set evs |]
-          ==> Says B Server {|Agent A, Agent B, X|} # evs : woolam"
+    WL4  "[| evs4: woolam;  B ~= Server;  
+             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  "[| evs: woolam;  B ~= Server;
+    WL5  "[| evs5: woolam;  B ~= Server;
              Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|}
-               : set evs |]
+               : set evs5 |]
           ==> Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|})
-                 # evs : woolam"
+                 # evs5 : woolam"
 
 end
diff -r f87dd7b68d8c -r eddedfe2f3f8 src/HOL/Auth/Yahalom.thy
--- a/src/HOL/Auth/Yahalom.thy	Thu Sep 04 17:57:56 1997 +0200
+++ b/src/HOL/Auth/Yahalom.thy	Fri Sep 05 12:24:13 1997 +0200
@@ -26,44 +26,44 @@
           ==> Says Spy B X  # evs : yahalom"
 
          (*Alice initiates a protocol run*)
-    YM1  "[| evs: yahalom;  A ~= B;  Nonce NA ~: used evs |]
-          ==> Says A B {|Agent A, Nonce NA|} # evs : yahalom"
+    YM1  "[| evs1: yahalom;  A ~= B;  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  "[| evs: yahalom;  B ~= Server;  Nonce NB ~: used evs;
-             Says A' B {|Agent A, Nonce NA|} : set evs |]
+    YM2  "[| evs2: yahalom;  B ~= Server;  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|}|}
-                # evs : yahalom"
+                # evs2 : yahalom"
 
          (*The Server receives Bob's message.  He responds by sending a
             new session key to Alice, with a packet for forwarding to Bob.*)
-    YM3  "[| evs: yahalom;  A ~= Server;  Key KAB ~: used evs;
+    YM3  "[| evs3: yahalom;  A ~= Server;  Key KAB ~: used evs3;
              Says B' Server 
                   {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
-               : set evs |]
+               : set evs3 |]
           ==> Says Server A
                    {|Crypt (shrK A) {|Agent B, Key KAB, Nonce NA, Nonce NB|},
                      Crypt (shrK B) {|Agent A, Key KAB|}|}
-                # evs : yahalom"
+                # evs3 : yahalom"
 
          (*Alice receives the Server's (?) message, checks her Nonce, and
            uses the new session key to send Bob his Nonce.*)
-    YM4  "[| evs: yahalom;  A ~= Server;  
+    YM4  "[| evs4: yahalom;  A ~= Server;  
              Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|},
-                        X|}  : set evs;
-             Says A B {|Agent A, Nonce NA|} : set evs |]
-          ==> Says A B {|X, Crypt K (Nonce NB)|} # evs : yahalom"
+                        X|}  : set evs4;
+             Says A B {|Agent A, Nonce NA|} : set evs4 |]
+          ==> Says A B {|X, Crypt K (Nonce NB)|} # evs4 : yahalom"
 
          (*This message models possible leaks of session keys.  The Nonces
            identify the protocol run.  Quoting Server here ensures they are
            correct.*)
-    Oops "[| evs: yahalom;  A ~= Spy;
+    Oops "[| evso: yahalom;  A ~= Spy;
              Says Server A {|Crypt (shrK A)
                                    {|Agent B, Key K, Nonce NA, Nonce NB|},
-                             X|}  : set evs |]
-          ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : yahalom"
+                             X|}  : set evso |]
+          ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evso : yahalom"
 
 
 constdefs 
diff -r f87dd7b68d8c -r eddedfe2f3f8 src/HOL/Auth/Yahalom2.thy
--- a/src/HOL/Auth/Yahalom2.thy	Thu Sep 04 17:57:56 1997 +0200
+++ b/src/HOL/Auth/Yahalom2.thy	Fri Sep 05 12:24:13 1997 +0200
@@ -29,45 +29,45 @@
           ==> Says Spy B X  # evs : yahalom"
 
          (*Alice initiates a protocol run*)
-    YM1  "[| evs: yahalom;  A ~= B;  Nonce NA ~: used evs |]
-          ==> Says A B {|Agent A, Nonce NA|} # evs : yahalom"
+    YM1  "[| evs1: yahalom;  A ~= B;  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  "[| evs: yahalom;  B ~= Server;  Nonce NB ~: used evs;
-             Says A' B {|Agent A, Nonce NA|} : set evs |]
+    YM2  "[| evs2: yahalom;  B ~= Server;  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|}|}
-                # evs : yahalom"
+                # evs2 : yahalom"
 
          (*The Server receives Bob's message.  He responds by sending a
-           new session key to Alice, with a packet for forwarding to Bob.
-           !! Fields are reversed in the 2nd packet to prevent attacks!! *)
-    YM3  "[| evs: yahalom;  A ~= B;  A ~= Server;  Key KAB ~: used evs;
+           new session key to Alice, with a certificate for forwarding to Bob.
+           Fields are reversed in the 2nd certificate to prevent attacks!! *)
+    YM3  "[| evs3: yahalom;  A ~= B;  A ~= Server;  Key KAB ~: used evs3;
              Says B' Server {|Agent B, Nonce NB,
 			      Crypt (shrK B) {|Agent A, Nonce NA|}|}
-               : set evs |]
+               : set evs3 |]
           ==> Says Server A
                {|Nonce NB, 
                  Crypt (shrK A) {|Agent B, Key KAB, Nonce NA|},
                  Crypt (shrK B) {|Nonce NB, Key KAB, Agent A|}|}
-                 # evs : yahalom"
+                 # evs3 : yahalom"
 
          (*Alice receives the Server's (?) message, checks her Nonce, and
            uses the new session key to send Bob his Nonce.*)
-    YM4  "[| evs: yahalom;  A ~= Server;  
+    YM4  "[| evs4: yahalom;  A ~= Server;  
              Says S A {|Nonce NB, Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
-                        X|}  : set evs;
-             Says A B {|Agent A, Nonce NA|} : set evs |]
-          ==> Says A B {|X, Crypt K (Nonce NB)|} # evs : yahalom"
+                        X|}  : set evs4;
+             Says A B {|Agent A, Nonce NA|} : set evs4 |]
+          ==> Says A B {|X, Crypt K (Nonce NB)|} # evs4 : yahalom"
 
          (*This message models possible leaks of session keys.  The nonces
            identify the protocol run.  Quoting Server here ensures they are
            correct. *)
-    Oops "[| evs: yahalom;  A ~= Spy;
+    Oops "[| evso: yahalom;  A ~= Spy;
              Says Server A {|Nonce NB, 
                              Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
-                             X|}  : set evs |]
-          ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : yahalom"
+                             X|}  : set evso |]
+          ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evso : yahalom"
 
 end