src/HOL/Auth/Yahalom.thy

--- a/src/HOL/Auth/Yahalom.thy	Fri Sep 13 13:15:48 1996 +0200
+++ b/src/HOL/Auth/Yahalom.thy	Fri Sep 13 13:16:57 1996 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Auth/OtwayRees
+(*  Title:      HOL/Auth/Yahalom
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1996  University of Cambridge
@@ -10,7 +10,7 @@
   Proc. Royal Soc. 426 (1989)
 *)
 
-OtwayRees = Shared + 
+Yahalom = Shared + 
 
 consts  yahalom   :: "event list set"
 inductive yahalom
@@ -26,13 +26,12 @@
 
          (*Alice initiates a protocol run*)
     YM1  "[| evs: yahalom;  A ~= B |]
-          ==> Says A B {|Nonce (newN evs), Agent A |} # evs : yahalom"
+          ==> Says A B {|Agent A, Nonce (newN evs)|} # evs : yahalom"
 
          (*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.*)
+	   the sender is, hence the A' in the sender field.*)
     YM2  "[| evs: yahalom;  B ~= Server;
-             Says A' B {|Nonce NA, Agent A|} : set_of_list evs |]
+             Says A' B {|Agent A, Nonce NA|} : set_of_list evs |]
           ==> Says B Server 
                   {|Agent B, 
                     Crypt {|Agent A, Nonce NA, Nonce (newN evs)|} (shrK B)|}
@@ -40,34 +39,23 @@
 
          (*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;  B ~= Server;
+    YM3  "[| evs: yahalom;  A ~= Server;
              Says B' Server 
-                  {|Nonce NA, Agent A, Agent B, 
-                    Crypt {|Nonce NA, Agent A, Agent B|} (shrK A), 
-                    Nonce NB, 
-                    Crypt {|Nonce NA, Agent A, Agent B|} (shrK B)|}
+                  {|Agent B, Crypt {|Agent A, Nonce NA, Nonce NB|} (shrK B)|}
                : set_of_list evs |]
-          ==> Says Server B 
-                  {|Nonce NA, 
-                    Crypt {|Nonce NA, Key (newK evs)|} (shrK A),
-                    Crypt {|Nonce NB, Key (newK evs)|} (shrK B)|}
+          ==> Says Server A
+                  {|Crypt {|Agent B, Key (newK evs), 
+                            Nonce NA, Nonce NB|} (shrK A),
+                    Crypt {|Agent A, Key (newK evs)|} (shrK B)|}
                  # evs : yahalom"
 
-         (*Bob receives the Server's (?) message and compares the Nonces with
-	   those in the message he previously sent the Server.*)
+         (*Alice receives the Server's (?) message, checks her Nonce, and
+           uses the new session key to send Bob his Nonce.*)
     YM4  "[| evs: yahalom;  A ~= B;  
-             Says S B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|}
+             Says S A {|Crypt {|Agent B, Key K, Nonce NA, Nonce NB|} (shrK A),
+                        X|}
                : set_of_list evs;
-             Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, X''|}
-               : set_of_list evs |]
-          ==> (Says B A {|Nonce NA, X|}) # evs : yahalom"
-
-         (*Alice checks her Nonce, then sends a dummy message to Bob,
-           using the new session key.*)
-    YM5  "[| evs: yahalom;  
-             Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|}
-               : set_of_list evs;
-             Says A  B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |]
-          ==> Says A B (Crypt (Agent A) K)  # evs : yahalom"
+             Says A B {|Agent A, Nonce NA|} : set_of_list evs |]
+          ==> Says A B {|X, Crypt (Nonce NB) K|} # evs : yahalom"
 
 end