src/HOL/Auth/WooLam.thy
changeset 2451 ce85a2aafc7a
parent 2283 68829cf138fc
child 2516 4d68fbe6378b
     1.1 --- a/src/HOL/Auth/WooLam.thy	Thu Dec 19 11:54:19 1996 +0100
     1.2 +++ b/src/HOL/Auth/WooLam.thy	Thu Dec 19 11:58:39 1996 +0100
     1.3 @@ -37,7 +37,7 @@
     1.4           (*Bob responds to Alice's message with a challenge.*)
     1.5      WL2  "[| evs: woolam;  A ~= B;
     1.6               Says A' B (Agent A) : set_of_list evs |]
     1.7 -          ==> Says B A (Nonce (newN evs)) # evs : woolam"
     1.8 +          ==> Says B A (Nonce (newN(length evs))) # evs : woolam"
     1.9  
    1.10           (*Alice responds to Bob's challenge by encrypting NB with her key.
    1.11             B is *not* properly determined -- Alice essentially broadcasts