src/HOL/Auth/WooLam.thy
changeset 2516 4d68fbe6378b
parent 2451 ce85a2aafc7a
child 3465 e85c24717cad
--- a/src/HOL/Auth/WooLam.thy	Fri Jan 17 11:50:09 1997 +0100
+++ b/src/HOL/Auth/WooLam.thy	Fri Jan 17 12:49:31 1997 +0100
@@ -35,16 +35,16 @@
           ==> Says A B (Agent A) # evs : woolam"
 
          (*Bob responds to Alice's message with a challenge.*)
-    WL2  "[| evs: woolam;  A ~= B;
+    WL2  "[| evs: woolam;  A ~= B;  
              Says A' B (Agent A) : set_of_list evs |]
-          ==> Says B A (Nonce (newN(length evs))) # evs : woolam"
+          ==> Says B A (Nonce NB) # 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;  A ~= B;
-             Says B' A (Nonce NB) : set_of_list evs;
-             Says A  B (Agent A)  : set_of_list evs |]
+             Says A  B (Agent A)  : set_of_list evs;
+             Says B' A (Nonce NB) : set_of_list evs |]
           ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs : woolam"
 
          (*Bob forwards Alice's response to the Server.*)