paulson@2274: (* Title: HOL/Auth/WooLam
paulson@2274: ID: $Id$
paulson@2274: Author: Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@2274: Copyright 1996 University of Cambridge
paulson@2274:
paulson@2274: Inductive relation "woolam" for the Woo-Lam protocol.
paulson@2274:
paulson@2274: Simplified version from page 11 of
paulson@2274: Abadi and Needham. Prudent Engineering Practice for Cryptographic Protocols.
paulson@2274: IEEE Trans. S.E. 22(1), 1996, pages 6-15.
paulson@2274:
paulson@2274: Note: this differs from the Woo-Lam protocol discussed by Lowe in his paper
paulson@2274: Some New Attacks upon Security Protocols.
paulson@2274: Computer Security Foundations Workshop, 1996.
paulson@2274: *)
paulson@2274:
paulson@2274: WooLam = Shared +
paulson@2274:
paulson@3519: consts woolam :: event list set
paulson@2283: inductive woolam
paulson@2274: intrs
paulson@2274: (*Initial trace is empty*)
paulson@11185: Nil "[] \\ woolam"
paulson@2274:
paulson@5434: (** These rules allow agents to send messages to themselves **)
paulson@5434:
paulson@2274: (*The spy MAY say anything he CAN say. We do not expect him to
paulson@2274: invent new nonces here, but he can also use NS1. Common to
paulson@2274: all similar protocols.*)
paulson@11185: Fake "[| evsf \\ woolam; X \\ synth (analz (spies evsf)) |]
paulson@11185: ==> Says Spy B X # evsf \\ woolam"
paulson@2274:
paulson@2274: (*Alice initiates a protocol run*)
paulson@11185: WL1 "[| evs1 \\ woolam |]
paulson@11185: ==> Says A B (Agent A) # evs1 \\ woolam"
paulson@2274:
paulson@2274: (*Bob responds to Alice's message with a challenge.*)
paulson@11185: WL2 "[| evs2 \\ woolam; Says A' B (Agent A) \\ set evs2 |]
paulson@11185: ==> Says B A (Nonce NB) # evs2 \\ woolam"
paulson@2274:
paulson@2274: (*Alice responds to Bob's challenge by encrypting NB with her key.
paulson@2274: B is *not* properly determined -- Alice essentially broadcasts
paulson@2274: her reply.*)
paulson@11185: WL3 "[| evs3 \\ woolam;
paulson@11185: Says A B (Agent A) \\ set evs3;
paulson@11185: Says B' A (Nonce NB) \\ set evs3 |]
paulson@11185: ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs3 \\ woolam"
paulson@2274:
paulson@3470: (*Bob forwards Alice's response to the Server. NOTE: usually
paulson@3470: the messages are shown in chronological order, for clarity.
paulson@3470: But here, exchanging the two events would cause the lemma
paulson@3683: WL4_analz_spies to pick up the wrong assumption!*)
paulson@11185: WL4 "[| evs4 \\ woolam;
paulson@11185: Says A' B X \\ set evs4;
paulson@11185: Says A'' B (Agent A) \\ set evs4 |]
paulson@11185: ==> Says B Server {|Agent A, Agent B, X|} # evs4 \\ woolam"
paulson@2274:
paulson@2274: (*Server decrypts Alice's response for Bob.*)
paulson@11185: WL5 "[| evs5 \\ woolam;
paulson@2283: Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|}
paulson@11185: \\ set evs5 |]
paulson@2283: ==> Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|})
paulson@11185: # evs5 \\ woolam"
paulson@2274:
paulson@2274: end