src/HOL/Auth/WooLam.thy
changeset 2274 1b1b46adc9b3
child 2283 68829cf138fc
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Auth/WooLam.thy	Thu Nov 28 15:56:04 1996 +0100
     1.3 @@ -0,0 +1,62 @@
     1.4 +(*  Title:      HOL/Auth/WooLam
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1996  University of Cambridge
     1.8 +
     1.9 +Inductive relation "woolam" for the Woo-Lam protocol.
    1.10 +
    1.11 +Simplified version from page 11 of
    1.12 +  Abadi and Needham.  Prudent Engineering Practice for Cryptographic Protocols.
    1.13 +  IEEE Trans. S.E. 22(1), 1996, pages 6-15.
    1.14 +
    1.15 +Note: this differs from the Woo-Lam protocol discussed by Lowe in his paper
    1.16 +  Some New Attacks upon Security Protocols.
    1.17 +  Computer Security Foundations Workshop, 1996.
    1.18 +*)
    1.19 +
    1.20 +WooLam = Shared + 
    1.21 +
    1.22 +consts  woolam   :: "agent set => event list set"
    1.23 +inductive "woolam lost"
    1.24 +  intrs 
    1.25 +         (*Initial trace is empty*)
    1.26 +    Nil  "[]: woolam lost"
    1.27 +
    1.28 +         (*The spy MAY say anything he CAN say.  We do not expect him to
    1.29 +           invent new nonces here, but he can also use NS1.  Common to
    1.30 +           all similar protocols.*)
    1.31 +    Fake "[| evs: woolam lost;  B ~= Spy;  
    1.32 +             X: synth (analz (sees lost Spy evs)) |]
    1.33 +          ==> Says Spy B X  # evs : woolam lost"
    1.34 +
    1.35 +         (*Alice initiates a protocol run*)
    1.36 +    WL1  "[| evs: woolam lost;  A ~= B |]
    1.37 +          ==> Says A B (Agent A) # evs : woolam lost"
    1.38 +
    1.39 +         (*Bob responds to Alice's message with a challenge.*)
    1.40 +    WL2  "[| evs: woolam lost;  A ~= B;
    1.41 +             Says A' B (Agent A) : set_of_list evs |]
    1.42 +          ==> Says B A (Nonce (newN evs)) # evs : woolam lost"
    1.43 +
    1.44 +         (*Alice responds to Bob's challenge by encrypting NB with her key.
    1.45 +           B is *not* properly determined -- Alice essentially broadcasts
    1.46 +           her reply.*)
    1.47 +    WL3  "[| evs: woolam lost;  A ~= B;
    1.48 +             Says B' A (Nonce NB) : set_of_list evs;
    1.49 +             Says A  B (Agent A)  : set_of_list evs |]
    1.50 +          ==> Says A B (Crypt (Nonce NB) (shrK A)) # evs : woolam lost"
    1.51 +
    1.52 +         (*Bob forwards Alice's response to the Server.*)
    1.53 +    WL4  "[| evs: woolam lost;  B ~= Server;  
    1.54 +             Says A'  B X         : set_of_list evs;
    1.55 +             Says A'' B (Agent A) : set_of_list evs |]
    1.56 +          ==> Says B Server {|Agent A, Agent B, X|} # evs : woolam lost"
    1.57 +
    1.58 +         (*Server decrypts Alice's response for Bob.*)
    1.59 +    WL5  "[| evs: woolam lost;  B ~= Server;
    1.60 +             Says B' Server {|Agent A, Agent B, Crypt (Nonce NB) (shrK A)|}
    1.61 +               : set_of_list evs |]
    1.62 +          ==> Says Server B (Crypt {|Agent A, Nonce NB|} (shrK B))
    1.63 +                 # evs : woolam lost"
    1.64 +
    1.65 +end