src/HOL/Auth/WooLam.thy
changeset 3470 8160cc3f6d40
parent 3465 e85c24717cad
child 3481 256f38c01b98
--- a/src/HOL/Auth/WooLam.thy	Tue Jul 01 10:37:03 1997 +0200
+++ b/src/HOL/Auth/WooLam.thy	Tue Jul 01 10:37:42 1997 +0200
@@ -47,7 +47,10 @@
              Says B' A (Nonce NB) : set evs |]
           ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs : woolam"
 
-         (*Bob forwards Alice's response to the Server.*)
+         (*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 |]