src/HOL/Auth/WooLam.thy
changeset 2516 4d68fbe6378b
parent 2451 ce85a2aafc7a
child 3465 e85c24717cad
     1.1 --- a/src/HOL/Auth/WooLam.thy	Fri Jan 17 11:50:09 1997 +0100
     1.2 +++ b/src/HOL/Auth/WooLam.thy	Fri Jan 17 12:49:31 1997 +0100
     1.3 @@ -35,16 +35,16 @@
     1.4            ==> Says A B (Agent A) # evs : woolam"
     1.5  
     1.6           (*Bob responds to Alice's message with a challenge.*)
     1.7 -    WL2  "[| evs: woolam;  A ~= B;
     1.8 +    WL2  "[| evs: woolam;  A ~= B;  
     1.9               Says A' B (Agent A) : set_of_list evs |]
    1.10 -          ==> Says B A (Nonce (newN(length evs))) # evs : woolam"
    1.11 +          ==> Says B A (Nonce NB) # evs : woolam"
    1.12  
    1.13           (*Alice responds to Bob's challenge by encrypting NB with her key.
    1.14             B is *not* properly determined -- Alice essentially broadcasts
    1.15             her reply.*)
    1.16      WL3  "[| evs: woolam;  A ~= B;
    1.17 -             Says B' A (Nonce NB) : set_of_list evs;
    1.18 -             Says A  B (Agent A)  : set_of_list evs |]
    1.19 +             Says A  B (Agent A)  : set_of_list evs;
    1.20 +             Says B' A (Nonce NB) : set_of_list evs |]
    1.21            ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs : woolam"
    1.22  
    1.23           (*Bob forwards Alice's response to the Server.*)