src/HOL/Auth/WooLam.thy
changeset 3465 e85c24717cad
parent 2516 4d68fbe6378b
child 3470 8160cc3f6d40
     1.1 --- a/src/HOL/Auth/WooLam.thy	Thu Jun 26 11:58:05 1997 +0200
     1.2 +++ b/src/HOL/Auth/WooLam.thy	Thu Jun 26 13:20:50 1997 +0200
     1.3 @@ -36,27 +36,27 @@
     1.4  
     1.5           (*Bob responds to Alice's message with a challenge.*)
     1.6      WL2  "[| evs: woolam;  A ~= B;  
     1.7 -             Says A' B (Agent A) : set_of_list evs |]
     1.8 +             Says A' B (Agent A) : set evs |]
     1.9            ==> Says B A (Nonce NB) # evs : woolam"
    1.10  
    1.11           (*Alice responds to Bob's challenge by encrypting NB with her key.
    1.12             B is *not* properly determined -- Alice essentially broadcasts
    1.13             her reply.*)
    1.14      WL3  "[| evs: woolam;  A ~= B;
    1.15 -             Says A  B (Agent A)  : set_of_list evs;
    1.16 -             Says B' A (Nonce NB) : set_of_list evs |]
    1.17 +             Says A  B (Agent A)  : set evs;
    1.18 +             Says B' A (Nonce NB) : set evs |]
    1.19            ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs : woolam"
    1.20  
    1.21           (*Bob forwards Alice's response to the Server.*)
    1.22      WL4  "[| evs: woolam;  B ~= Server;  
    1.23 -             Says A'  B X         : set_of_list evs;
    1.24 -             Says A'' B (Agent A) : set_of_list evs |]
    1.25 +             Says A'  B X         : set evs;
    1.26 +             Says A'' B (Agent A) : set evs |]
    1.27            ==> Says B Server {|Agent A, Agent B, X|} # evs : woolam"
    1.28  
    1.29           (*Server decrypts Alice's response for Bob.*)
    1.30      WL5  "[| evs: woolam;  B ~= Server;
    1.31               Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|}
    1.32 -               : set_of_list evs |]
    1.33 +               : set evs |]
    1.34            ==> Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|})
    1.35                   # evs : woolam"
    1.36