(* Title: HOL/Auth/OtwayRees_Bad ID: $Id: OtwayRees_Bad.thy,v 1.28 2005/06/17 14:13:06 haftmann Exp $ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1996 University of Cambridge *) header{*The Otway-Rees Protocol: The Faulty BAN Version*} theory OtwayRees_Bad imports Public begin text{*The FAULTY version omitting encryption of Nonce NB, as suggested on page 247 of Burrows, Abadi and Needham (1988). A Logic of Authentication. Proc. Royal Soc. 426 This file illustrates the consequences of such errors. We can still prove impressive-looking properties such as @{text Spy_not_see_encrypted_key}, yet the protocol is open to a middleperson attack. Attempting to prove some key lemmas indicates the possibility of this attack.*} consts otway :: "event list set" inductive "otway" intros Nil: --{*The empty trace*} "[] ∈ otway" Fake: --{*The Spy may say anything he can say. The sender field is correct, but agents don't use that information.*} "[| evsf ∈ otway; X ∈ synth (analz (knows Spy evsf)) |] ==> Says Spy B X # evsf ∈ otway" Reception: --{*A message that has been sent can be received by the intended recipient.*} "[| evsr ∈ otway; Says A B X ∈set evsr |] ==> Gets B X # evsr ∈ otway" OR1: --{*Alice initiates a protocol run*} "[| evs1 ∈ otway; Nonce NA ∉ used evs1 |] ==> Says A B {|Nonce NA, Agent A, Agent B, Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |} # evs1 ∈ otway" OR2: --{*Bob's response to Alice's message. This variant of the protocol does NOT encrypt NB.*} "[| evs2 ∈ otway; Nonce NB ∉ used evs2; Gets B {|Nonce NA, Agent A, Agent B, X|} ∈ set evs2 |] ==> Says B Server {|Nonce NA, Agent A, Agent B, X, Nonce NB, Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|} # evs2 ∈ otway" OR3: --{*The Server receives Bob's message and checks that the three NAs match. Then he sends a new session key to Bob with a packet for forwarding to Alice.*} "[| evs3 ∈ otway; Key KAB ∉ used evs3; Gets Server {|Nonce NA, Agent A, Agent B, Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}, Nonce NB, Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|} ∈ set evs3 |] ==> Says Server B {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key KAB|}, Crypt (shrK B) {|Nonce NB, Key KAB|}|} # evs3 ∈ otway" OR4: --{*Bob receives the Server's (?) message and compares the Nonces with those in the message he previously sent the Server. Need @{term "B ≠ Server"} because we allow messages to self.*} "[| evs4 ∈ otway; B ≠ Server; Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|} ∈ set evs4; Gets B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|} ∈ set evs4 |] ==> Says B A {|Nonce NA, X|} # evs4 ∈ otway" Oops: --{*This message models possible leaks of session keys. The nonces identify the protocol run.*} "[| evso ∈ otway; Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|} ∈ set evso |] ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso ∈ otway" 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] text{*A "possibility property": there are traces that reach the end*} lemma "[| B ≠ Server; Key K ∉ used [] |] ==> ∃NA. ∃evs ∈ otway. Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} ∈ set evs" apply (intro exI bexI) apply (rule_tac [2] otway.Nil [THEN otway.OR1, THEN otway.Reception, THEN otway.OR2, THEN otway.Reception, THEN otway.OR3, THEN otway.Reception, THEN otway.OR4]) apply (possibility, simp add: used_Cons) done lemma Gets_imp_Says [dest!]: "[| Gets B X ∈ set evs; evs ∈ otway |] ==> ∃A. Says A B X ∈ set evs" apply (erule rev_mp) apply (erule otway.induct, auto) done subsection{*For reasoning about the encrypted portion of messages *} lemma OR2_analz_knows_Spy: "[| Gets B {|N, Agent A, Agent B, X|} ∈ set evs; evs ∈ otway |] ==> X ∈ analz (knows Spy evs)" by blast lemma OR4_analz_knows_Spy: "[| Gets B {|N, X, Crypt (shrK B) X'|} ∈ set evs; evs ∈ otway |] ==> X ∈ analz (knows Spy evs)" by blast lemma Oops_parts_knows_Spy: "Says Server B {|NA, X, Crypt K' {|NB,K|}|} ∈ set evs ==> K ∈ parts (knows Spy evs)" by blast text{*Forwarding lemma: see comments in OtwayRees.thy*} lemmas OR2_parts_knows_Spy = OR2_analz_knows_Spy [THEN analz_into_parts, standard] text{*Theorems of the form @{term "X ∉ parts (spies evs)"} imply that NOBODY sends messages containing X! *} text{*Spy never sees a good agent's shared key!*} lemma Spy_see_shrK [simp]: "evs ∈ otway ==> (Key (shrK A) ∈ parts (knows Spy evs)) = (A ∈ bad)" by (erule otway.induct, force, drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+) lemma Spy_analz_shrK [simp]: "evs ∈ otway ==> (Key (shrK A) ∈ analz (knows Spy evs)) = (A ∈ bad)" by auto lemma Spy_see_shrK_D [dest!]: "[|Key (shrK A) ∈ parts (knows Spy evs); evs ∈ otway|] ==> A ∈ bad" by (blast dest: Spy_see_shrK) subsection{*Proofs involving analz *} text{*Describes the form of K and NA when the Server sends this message. Also for Oops case.*} lemma Says_Server_message_form: "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} ∈ set evs; evs ∈ otway |] ==> K ∉ range shrK & (∃i. NA = Nonce i) & (∃j. NB = Nonce j)" apply (erule rev_mp) apply (erule otway.induct, simp_all, blast) done (**** The following is to prove theorems of the form Key K ∈ analz (insert (Key KAB) (knows Spy evs)) ==> Key K ∈ analz (knows Spy evs) A more general formula must be proved inductively. ****) text{*Session keys are not used to encrypt other session keys*} text{*The equality makes the induction hypothesis easier to apply*} lemma analz_image_freshK [rule_format]: "evs ∈ otway ==> ∀K KK. KK <= -(range shrK) --> (Key K ∈ analz (Key`KK Un (knows Spy evs))) = (K ∈ KK | Key K ∈ analz (knows Spy evs))" apply (erule otway.induct) apply (frule_tac [8] Says_Server_message_form) apply (drule_tac [7] OR4_analz_knows_Spy) apply (drule_tac [5] OR2_analz_knows_Spy, analz_freshK, spy_analz, auto) done lemma analz_insert_freshK: "[| evs ∈ otway; KAB ∉ range shrK |] ==> (Key K ∈ analz (insert (Key KAB) (knows Spy evs))) = (K = KAB | Key K ∈ analz (knows Spy evs))" by (simp only: analz_image_freshK analz_image_freshK_simps) text{*The Key K uniquely identifies the Server's message. *} lemma unique_session_keys: "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} ∈ set evs; Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} ∈ set evs; evs ∈ otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'" apply (erule rev_mp) apply (erule rev_mp) apply (erule otway.induct, simp_all) apply blast+ --{*OR3 and OR4*} done text{*Crucial secrecy property: Spy does not see the keys sent in msg OR3 Does not in itself guarantee security: an attack could violate the premises, e.g. by having @{term "A=Spy"} *} lemma secrecy_lemma: "[| A ∉ bad; B ∉ bad; evs ∈ otway |] ==> Says Server B {|NA, Crypt (shrK A) {|NA, Key K|}, Crypt (shrK B) {|NB, Key K|}|} ∈ set evs --> Notes Spy {|NA, NB, Key K|} ∉ set evs --> Key K ∉ analz (knows Spy evs)" apply (erule otway.induct, force) apply (frule_tac [7] Says_Server_message_form) apply (drule_tac [6] OR4_analz_knows_Spy) apply (drule_tac [4] OR2_analz_knows_Spy) apply (simp_all add: analz_insert_eq analz_insert_freshK pushes) apply spy_analz --{*Fake*} apply (blast dest: unique_session_keys)+ --{*OR3, OR4, Oops*} done lemma Spy_not_see_encrypted_key: "[| Says Server B {|NA, Crypt (shrK A) {|NA, Key K|}, Crypt (shrK B) {|NB, Key K|}|} ∈ set evs; Notes Spy {|NA, NB, Key K|} ∉ set evs; A ∉ bad; B ∉ bad; evs ∈ otway |] ==> Key K ∉ analz (knows Spy evs)" by (blast dest: Says_Server_message_form secrecy_lemma) subsection{*Attempting to prove stronger properties *} text{*Only OR1 can have caused such a part of a message to appear. The premise @{term "A ≠ B"} prevents OR2's similar-looking cryptogram from being picked up. Original Otway-Rees doesn't need it.*} lemma Crypt_imp_OR1 [rule_format]: "[| A ∉ bad; A ≠ B; evs ∈ otway |] ==> Crypt (shrK A) {|NA, Agent A, Agent B|} ∈ parts (knows Spy evs) --> Says A B {|NA, Agent A, Agent B, Crypt (shrK A) {|NA, Agent A, Agent B|}|} ∈ set evs" by (erule otway.induct, force, drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+) text{*Crucial property: If the encrypted message appears, and A has used NA to start a run, then it originated with the Server! The premise @{term "A ≠ B"} allows use of @{text Crypt_imp_OR1}*} text{*Only it is FALSE. Somebody could make a fake message to Server substituting some other nonce NA' for NB.*} lemma "[| A ∉ bad; A ≠ B; evs ∈ otway |] ==> Crypt (shrK A) {|NA, Key K|} ∈ parts (knows Spy evs) --> Says A B {|NA, Agent A, Agent B, Crypt (shrK A) {|NA, Agent A, Agent B|}|} ∈ set evs --> (∃B NB. Says Server B {|NA, Crypt (shrK A) {|NA, Key K|}, Crypt (shrK B) {|NB, Key K|}|} ∈ set evs)" apply (erule otway.induct, force, drule_tac [4] OR2_parts_knows_Spy, simp_all) apply blast --{*Fake*} apply blast --{*OR1: it cannot be a new Nonce, contradiction.*} txt{*OR3 and OR4*} apply (simp_all add: ex_disj_distrib) prefer 2 apply (blast intro!: Crypt_imp_OR1) --{*OR4*} txt{*OR3*} apply clarify (*The hypotheses at this point suggest an attack in which nonce NB is used in two different roles: Gets Server {|Nonce NA, Agent Aa, Agent A, Crypt (shrK Aa) {|Nonce NA, Agent Aa, Agent A|}, Nonce NB, Crypt (shrK A) {|Nonce NA, Agent Aa, Agent A|}|} ∈ set evs3 Says A B {|Nonce NB, Agent A, Agent B, Crypt (shrK A) {|Nonce NB, Agent A, Agent B|}|} ∈ set evs3; *) (*Thus the key property A_can_trust probably fails too.*) oops end
lemma
[| B ≠ Server; Key K ∉ used [] |] ==> ∃NA. ∃evs∈otway. Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} ∈ set evs
lemma Gets_imp_Says:
[| Gets B X ∈ set evs; evs ∈ otway |] ==> ∃A. Says A B X ∈ set evs
lemma OR2_analz_knows_Spy:
[| Gets B {|N, Agent A, Agent B, X|} ∈ set evs; evs ∈ otway |] ==> X ∈ analz (knows Spy evs)
lemma OR4_analz_knows_Spy:
[| Gets B {|N, X, Crypt (shrK B) X'|} ∈ set evs; evs ∈ otway |] ==> X ∈ analz (knows Spy evs)
lemma Oops_parts_knows_Spy:
Says Server B {|NA, X, Crypt K' {|NB, K|}|} ∈ set evs ==> K ∈ parts (knows Spy evs)
lemmas OR2_parts_knows_Spy:
[| Gets B {|N, Agent A, Agent B, c|} ∈ set evs; evs ∈ otway |] ==> c ∈ parts (knows Spy evs)
lemmas OR2_parts_knows_Spy:
[| Gets B {|N, Agent A, Agent B, c|} ∈ set evs; evs ∈ otway |] ==> c ∈ parts (knows Spy evs)
lemma Spy_see_shrK:
evs ∈ otway ==> (Key (shrK A) ∈ parts (knows Spy evs)) = (A ∈ bad)
lemma Spy_analz_shrK:
evs ∈ otway ==> (Key (shrK A) ∈ analz (knows Spy evs)) = (A ∈ bad)
lemma Spy_see_shrK_D:
[| Key (shrK A) ∈ parts (knows Spy evs); evs ∈ otway |] ==> A ∈ bad
lemma Says_Server_message_form:
[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} ∈ set evs; evs ∈ otway |] ==> K ∉ range shrK ∧ (∃i. NA = Nonce i) ∧ (∃j. NB = Nonce j)
lemma analz_image_freshK:
[| evs ∈ otway; KK ⊆ - range shrK |] ==> (Key K ∈ analz (Key ` KK ∪ knows Spy evs)) = (K ∈ KK ∨ Key K ∈ analz (knows Spy evs))
lemma analz_insert_freshK:
[| evs ∈ otway; KAB ∉ range shrK |] ==> (Key K ∈ analz (insert (Key KAB) (knows Spy evs))) = (K = KAB ∨ Key K ∈ analz (knows Spy evs))
lemma unique_session_keys:
[| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} ∈ set evs; Says Server B' {|NA', X', Crypt (shrK B') {|NB', K|}|} ∈ set evs; evs ∈ otway |] ==> X = X' ∧ B = B' ∧ NA = NA' ∧ NB = NB'
lemma secrecy_lemma:
[| A ∉ bad; B ∉ bad; evs ∈ otway |] ==> Says Server B {|NA, Crypt (shrK A) {|NA, Key K|}, Crypt (shrK B) {|NB, Key K|}|} ∈ set evs --> Notes Spy {|NA, NB, Key K|} ∉ set evs --> Key K ∉ analz (knows Spy evs)
lemma Spy_not_see_encrypted_key:
[| Says Server B {|NA, Crypt (shrK A) {|NA, Key K|}, Crypt (shrK B) {|NB, Key K|}|} ∈ set evs; Notes Spy {|NA, NB, Key K|} ∉ set evs; A ∉ bad; B ∉ bad; evs ∈ otway |] ==> Key K ∉ analz (knows Spy evs)
lemma Crypt_imp_OR1:
[| A ∉ bad; A ≠ B; evs ∈ otway; Crypt (shrK A) {|NA, Agent A, Agent B|} ∈ parts (knows Spy evs) |] ==> Says A B {|NA, Agent A, Agent B, Crypt (shrK A) {|NA, Agent A, Agent B|}|} ∈ set evs