src/HOL/Auth/WooLam.thy
changeset 3659 eddedfe2f3f8
parent 3519 ab0a9fbed4c0
child 3683 aafe719dff14
     1.1 --- a/src/HOL/Auth/WooLam.thy	Thu Sep 04 17:57:56 1997 +0200
     1.2 +++ b/src/HOL/Auth/WooLam.thy	Fri Sep 05 12:24:13 1997 +0200
     1.3 @@ -30,36 +30,36 @@
     1.4            ==> Says Spy B X  # evs : woolam"
     1.5  
     1.6           (*Alice initiates a protocol run*)
     1.7 -    WL1  "[| evs: woolam;  A ~= B |]
     1.8 -          ==> Says A B (Agent A) # evs : woolam"
     1.9 +    WL1  "[| evs1: woolam;  A ~= B |]
    1.10 +          ==> Says A B (Agent A) # evs1 : woolam"
    1.11  
    1.12           (*Bob responds to Alice's message with a challenge.*)
    1.13 -    WL2  "[| evs: woolam;  A ~= B;  
    1.14 -             Says A' B (Agent A) : set evs |]
    1.15 -          ==> Says B A (Nonce NB) # evs : woolam"
    1.16 +    WL2  "[| evs2: woolam;  A ~= B;  
    1.17 +             Says A' B (Agent A) : set evs2 |]
    1.18 +          ==> Says B A (Nonce NB) # evs2 : woolam"
    1.19  
    1.20           (*Alice responds to Bob's challenge by encrypting NB with her key.
    1.21             B is *not* properly determined -- Alice essentially broadcasts
    1.22             her reply.*)
    1.23 -    WL3  "[| evs: woolam;
    1.24 -             Says A  B (Agent A)  : set evs;
    1.25 -             Says B' A (Nonce NB) : set evs |]
    1.26 -          ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs : woolam"
    1.27 +    WL3  "[| evs3: woolam;
    1.28 +             Says A  B (Agent A)  : set evs3;
    1.29 +             Says B' A (Nonce NB) : set evs3 |]
    1.30 +          ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs3 : woolam"
    1.31  
    1.32           (*Bob forwards Alice's response to the Server.  NOTE: usually
    1.33             the messages are shown in chronological order, for clarity.
    1.34             But here, exchanging the two events would cause the lemma
    1.35             WL4_analz_sees_Spy to pick up the wrong assumption!*)
    1.36 -    WL4  "[| evs: woolam;  B ~= Server;  
    1.37 -             Says A'  B X         : set evs;
    1.38 -             Says A'' B (Agent A) : set evs |]
    1.39 -          ==> Says B Server {|Agent A, Agent B, X|} # evs : woolam"
    1.40 +    WL4  "[| evs4: woolam;  B ~= Server;  
    1.41 +             Says A'  B X         : set evs4;
    1.42 +             Says A'' B (Agent A) : set evs4 |]
    1.43 +          ==> Says B Server {|Agent A, Agent B, X|} # evs4 : woolam"
    1.44  
    1.45           (*Server decrypts Alice's response for Bob.*)
    1.46 -    WL5  "[| evs: woolam;  B ~= Server;
    1.47 +    WL5  "[| evs5: woolam;  B ~= Server;
    1.48               Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|}
    1.49 -               : set evs |]
    1.50 +               : set evs5 |]
    1.51            ==> Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|})
    1.52 -                 # evs : woolam"
    1.53 +                 # evs5 : woolam"
    1.54  
    1.55  end