src/HOL/Auth/WooLam.thy
changeset 2283 68829cf138fc
parent 2274 1b1b46adc9b3
child 2451 ce85a2aafc7a
--- a/src/HOL/Auth/WooLam.thy	Fri Nov 29 15:31:13 1996 +0100
+++ b/src/HOL/Auth/WooLam.thy	Fri Nov 29 17:58:18 1996 +0100
@@ -16,47 +16,48 @@
 
 WooLam = Shared + 
 
-consts  woolam   :: "agent set => event list set"
-inductive "woolam lost"
+consts  lost    :: agent set        (*No need for it to be a variable*)
+	woolam  :: event list set
+inductive woolam
   intrs 
          (*Initial trace is empty*)
-    Nil  "[]: woolam lost"
+    Nil  "[]: woolam"
 
          (*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 lost;  B ~= Spy;  
+    Fake "[| evs: woolam;  B ~= Spy;  
              X: synth (analz (sees lost Spy evs)) |]
-          ==> Says Spy B X  # evs : woolam lost"
+          ==> Says Spy B X  # evs : woolam"
 
          (*Alice initiates a protocol run*)
-    WL1  "[| evs: woolam lost;  A ~= B |]
-          ==> Says A B (Agent A) # evs : woolam lost"
+    WL1  "[| evs: woolam;  A ~= B |]
+          ==> Says A B (Agent A) # evs : woolam"
 
          (*Bob responds to Alice's message with a challenge.*)
-    WL2  "[| evs: woolam lost;  A ~= B;
+    WL2  "[| evs: woolam;  A ~= B;
              Says A' B (Agent A) : set_of_list evs |]
-          ==> Says B A (Nonce (newN evs)) # evs : woolam lost"
+          ==> Says B A (Nonce (newN evs)) # evs : 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 lost;  A ~= B;
+    WL3  "[| evs: woolam;  A ~= B;
              Says B' A (Nonce NB) : set_of_list evs;
              Says A  B (Agent A)  : set_of_list evs |]
-          ==> Says A B (Crypt (Nonce NB) (shrK A)) # evs : woolam lost"
+          ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs : woolam"
 
          (*Bob forwards Alice's response to the Server.*)
-    WL4  "[| evs: woolam lost;  B ~= Server;  
+    WL4  "[| evs: woolam;  B ~= Server;  
              Says A'  B X         : set_of_list evs;
              Says A'' B (Agent A) : set_of_list evs |]
-          ==> Says B Server {|Agent A, Agent B, X|} # evs : woolam lost"
+          ==> Says B Server {|Agent A, Agent B, X|} # evs : woolam"
 
          (*Server decrypts Alice's response for Bob.*)
-    WL5  "[| evs: woolam lost;  B ~= Server;
-             Says B' Server {|Agent A, Agent B, Crypt (Nonce NB) (shrK A)|}
+    WL5  "[| evs: woolam;  B ~= Server;
+             Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|}
                : set_of_list evs |]
-          ==> Says Server B (Crypt {|Agent A, Nonce NB|} (shrK B))
-                 # evs : woolam lost"
+          ==> Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|})
+                 # evs : woolam"
 
 end