src/HOL/Auth/WooLam.thy
changeset 3659 eddedfe2f3f8
parent 3519 ab0a9fbed4c0
child 3683 aafe719dff14
--- 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