src/HOL/Auth/WooLam.thy
changeset 3481 256f38c01b98
parent 3470 8160cc3f6d40
child 3519 ab0a9fbed4c0
     1.1 --- a/src/HOL/Auth/WooLam.thy	Tue Jul 01 17:37:42 1997 +0200
     1.2 +++ b/src/HOL/Auth/WooLam.thy	Tue Jul 01 17:38:49 1997 +0200
     1.3 @@ -42,7 +42,7 @@
     1.4           (*Alice responds to Bob's challenge by encrypting NB with her key.
     1.5             B is *not* properly determined -- Alice essentially broadcasts
     1.6             her reply.*)
     1.7 -    WL3  "[| evs: woolam;  A ~= B;
     1.8 +    WL3  "[| evs: woolam;
     1.9               Says A  B (Agent A)  : set evs;
    1.10               Says B' A (Nonce NB) : set evs |]
    1.11            ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs : woolam"