src/HOL/Auth/WooLam.thy
changeset 3470 8160cc3f6d40
parent 3465 e85c24717cad
child 3481 256f38c01b98
     1.1 --- a/src/HOL/Auth/WooLam.thy	Tue Jul 01 10:37:03 1997 +0200
     1.2 +++ b/src/HOL/Auth/WooLam.thy	Tue Jul 01 10:37:42 1997 +0200
     1.3 @@ -47,7 +47,10 @@
     1.4               Says B' A (Nonce NB) : set evs |]
     1.5            ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs : woolam"
     1.6  
     1.7 -         (*Bob forwards Alice's response to the Server.*)
     1.8 +         (*Bob forwards Alice's response to the Server.  NOTE: usually
     1.9 +           the messages are shown in chronological order, for clarity.
    1.10 +           But here, exchanging the two events would cause the lemma
    1.11 +           WL4_analz_sees_Spy to pick up the wrong assumption!*)
    1.12      WL4  "[| evs: woolam;  B ~= Server;  
    1.13               Says A'  B X         : set evs;
    1.14               Says A'' B (Agent A) : set evs |]