(* Title: HOL/Auth/WooLam ID: $Id: WooLam.thy,v 1.16 2005/06/17 14:13:06 haftmann Exp $ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1996 University of Cambridge *) header{*The Woo-Lam Protocol*} theory WooLam imports Public begin text{*Simplified version from page 11 of Abadi and Needham (1996). Prudent Engineering Practice for Cryptographic Protocols. IEEE Trans. S.E. 22(1), pages 6-15. Note: this differs from the Woo-Lam protocol discussed by Lowe (1996): Some New Attacks upon Security Protocols. Computer Security Foundations Workshop *} consts woolam :: "event list set" inductive woolam intros (*Initial trace is empty*) Nil: "[] ∈ woolam" (** These rules allow agents to send messages to themselves **) (*The spy MAY say anything he CAN say. We do not expect him to invent new nonces here, but he can also use NS1. Common to all similar protocols.*) Fake: "[| evsf ∈ woolam; X ∈ synth (analz (spies evsf)) |] ==> Says Spy B X # evsf ∈ woolam" (*Alice initiates a protocol run*) WL1: "evs1 ∈ woolam ==> Says A B (Agent A) # evs1 ∈ woolam" (*Bob responds to Alice's message with a challenge.*) WL2: "[| evs2 ∈ woolam; Says A' B (Agent A) ∈ set evs2 |] ==> Says B A (Nonce NB) # evs2 ∈ woolam" (*Alice responds to Bob's challenge by encrypting NB with her key. B is *not* properly determined -- Alice essentially broadcasts her reply.*) WL3: "[| evs3 ∈ woolam; Says A B (Agent A) ∈ set evs3; Says B' A (Nonce NB) ∈ set evs3 |] ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs3 ∈ woolam" (*Bob forwards Alice's response to the Server. NOTE: usually the messages are shown in chronological order, for clarity. But here, exchanging the two events would cause the lemma WL4_analz_spies to pick up the wrong assumption!*) WL4: "[| evs4 ∈ woolam; Says A' B X ∈ set evs4; Says A'' B (Agent A) ∈ set evs4 |] ==> Says B Server {|Agent A, Agent B, X|} # evs4 ∈ woolam" (*Server decrypts Alice's response for Bob.*) WL5: "[| evs5 ∈ woolam; Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|} ∈ set evs5 |] ==> Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|}) # evs5 ∈ woolam" declare Says_imp_knows_Spy [THEN analz.Inj, dest] declare parts.Body [dest] declare analz_into_parts [dest] declare Fake_parts_insert_in_Un [dest] (*A "possibility property": there are traces that reach the end*) lemma "∃NB. ∃evs ∈ woolam. Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|}) ∈ set evs" apply (intro exI bexI) apply (rule_tac [2] woolam.Nil [THEN woolam.WL1, THEN woolam.WL2, THEN woolam.WL3, THEN woolam.WL4, THEN woolam.WL5], possibility) done (*Could prove forwarding lemmas for WL4, but we do not need them!*) (**** Inductive proofs about woolam ****) (** Theorems of the form X ∉ parts (spies evs) imply that NOBODY sends messages containing X! **) (*Spy never sees a good agent's shared key!*) lemma Spy_see_shrK [simp]: "evs ∈ woolam ==> (Key (shrK A) ∈ parts (spies evs)) = (A ∈ bad)" by (erule woolam.induct, force, simp_all, blast+) lemma Spy_analz_shrK [simp]: "evs ∈ woolam ==> (Key (shrK A) ∈ analz (spies evs)) = (A ∈ bad)" by auto lemma Spy_see_shrK_D [dest!]: "[|Key (shrK A) ∈ parts (knows Spy evs); evs ∈ woolam|] ==> A ∈ bad" by (blast dest: Spy_see_shrK) (**** Autheticity properties for Woo-Lam ****) (*** WL4 ***) (*If the encrypted message appears then it originated with Alice*) lemma NB_Crypt_imp_Alice_msg: "[| Crypt (shrK A) (Nonce NB) ∈ parts (spies evs); A ∉ bad; evs ∈ woolam |] ==> ∃B. Says A B (Crypt (shrK A) (Nonce NB)) ∈ set evs" by (erule rev_mp, erule woolam.induct, force, simp_all, blast+) (*Guarantee for Server: if it gets a message containing a certificate from Alice, then she originated that certificate. But we DO NOT know that B ever saw it: the Spy may have rerouted the message to the Server.*) lemma Server_trusts_WL4 [dest]: "[| Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|} ∈ set evs; A ∉ bad; evs ∈ woolam |] ==> ∃B. Says A B (Crypt (shrK A) (Nonce NB)) ∈ set evs" by (blast intro!: NB_Crypt_imp_Alice_msg) (*** WL5 ***) (*Server sent WL5 only if it received the right sort of message*) lemma Server_sent_WL5 [dest]: "[| Says Server B (Crypt (shrK B) {|Agent A, NB|}) ∈ set evs; evs ∈ woolam |] ==> ∃B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|} ∈ set evs" by (erule rev_mp, erule woolam.induct, force, simp_all, blast+) (*If the encrypted message appears then it originated with the Server!*) lemma NB_Crypt_imp_Server_msg [rule_format]: "[| Crypt (shrK B) {|Agent A, NB|} ∈ parts (spies evs); B ∉ bad; evs ∈ woolam |] ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) ∈ set evs" by (erule rev_mp, erule woolam.induct, force, simp_all, blast+) (*Guarantee for B. If B gets the Server's certificate then A has encrypted the nonce using her key. This event can be no older than the nonce itself. But A may have sent the nonce to some other agent and it could have reached the Server via the Spy.*) lemma B_trusts_WL5: "[| Says S B (Crypt (shrK B) {|Agent A, Nonce NB|}): set evs; A ∉ bad; B ∉ bad; evs ∈ woolam |] ==> ∃B. Says A B (Crypt (shrK A) (Nonce NB)) ∈ set evs" by (blast dest!: NB_Crypt_imp_Server_msg) (*B only issues challenges in response to WL1. Not used.*) lemma B_said_WL2: "[| Says B A (Nonce NB) ∈ set evs; B ≠ Spy; evs ∈ woolam |] ==> ∃A'. Says A' B (Agent A) ∈ set evs" by (erule rev_mp, erule woolam.induct, force, simp_all, blast+) (**CANNOT be proved because A doesn't know where challenges come from...*) lemma "[| A ∉ bad; B ≠ Spy; evs ∈ woolam |] ==> Crypt (shrK A) (Nonce NB) ∈ parts (spies evs) & Says B A (Nonce NB) ∈ set evs --> Says A B (Crypt (shrK A) (Nonce NB)) ∈ set evs" apply (erule rev_mp, erule woolam.induct, force, simp_all, blast, auto) oops end
lemma
∃NB. ∃evs∈woolam. Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|}) ∈ set evs
lemma Spy_see_shrK:
evs ∈ woolam ==> (Key (shrK A) ∈ parts (knows Spy evs)) = (A ∈ bad)
lemma Spy_analz_shrK:
evs ∈ woolam ==> (Key (shrK A) ∈ analz (knows Spy evs)) = (A ∈ bad)
lemma Spy_see_shrK_D:
[| Key (shrK A) ∈ parts (knows Spy evs); evs ∈ woolam |] ==> A ∈ bad
lemma NB_Crypt_imp_Alice_msg:
[| Crypt (shrK A) (Nonce NB) ∈ parts (knows Spy evs); A ∉ bad; evs ∈ woolam |] ==> ∃B. Says A B (Crypt (shrK A) (Nonce NB)) ∈ set evs
lemma Server_trusts_WL4:
[| Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|} ∈ set evs; A ∉ bad; evs ∈ woolam |] ==> ∃B. Says A B (Crypt (shrK A) (Nonce NB)) ∈ set evs
lemma Server_sent_WL5:
[| Says Server B (Crypt (shrK B) {|Agent A, NB|}) ∈ set evs; evs ∈ woolam |] ==> ∃B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|} ∈ set evs
lemma NB_Crypt_imp_Server_msg:
[| Crypt (shrK B) {|Agent A, NB|} ∈ parts (knows Spy evs); B ∉ bad; evs ∈ woolam |] ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) ∈ set evs
lemma B_trusts_WL5:
[| Says S B (Crypt (shrK B) {|Agent A, Nonce NB|}) ∈ set evs; A ∉ bad; B ∉ bad; evs ∈ woolam |] ==> ∃B. Says A B (Crypt (shrK A) (Nonce NB)) ∈ set evs
lemma B_said_WL2:
[| Says B A (Nonce NB) ∈ set evs; B ≠ Spy; evs ∈ woolam |] ==> ∃A'. Says A' B (Agent A) ∈ set evs