src/HOL/Auth/WooLam.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Auth/WooLam.thy	Thu Nov 28 15:56:04 1996 +0100
@@ -0,0 +1,62 @@
+(*  Title:      HOL/Auth/WooLam
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1996  University of Cambridge
+
+Inductive relation "woolam" for the Woo-Lam protocol.
+
+Simplified version from page 11 of
+  Abadi and Needham.  Prudent Engineering Practice for Cryptographic Protocols.
+  IEEE Trans. S.E. 22(1), 1996, pages 6-15.
+
+Note: this differs from the Woo-Lam protocol discussed by Lowe in his paper
+  Some New Attacks upon Security Protocols.
+  Computer Security Foundations Workshop, 1996.
+*)
+
+WooLam = Shared + 
+
+consts  woolam   :: "agent set => event list set"
+inductive "woolam lost"
+  intrs 
+         (*Initial trace is empty*)
+    Nil  "[]: woolam lost"
+
+         (*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;  
+             X: synth (analz (sees lost Spy evs)) |]
+          ==> Says Spy B X  # evs : woolam lost"
+
+         (*Alice initiates a protocol run*)
+    WL1  "[| evs: woolam lost;  A ~= B |]
+          ==> Says A B (Agent A) # evs : woolam lost"
+
+         (*Bob responds to Alice's message with a challenge.*)
+    WL2  "[| evs: woolam lost;  A ~= B;
+             Says A' B (Agent A) : set_of_list evs |]
+          ==> Says B A (Nonce (newN evs)) # evs : woolam lost"
+
+         (*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;
+             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"
+
+         (*Bob forwards Alice's response to the Server.*)
+    WL4  "[| evs: woolam lost;  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"
+
+         (*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)|}
+               : set_of_list evs |]
+          ==> Says Server B (Crypt {|Agent A, Nonce NB|} (shrK B))
+                 # evs : woolam lost"
+
+end