1(* Title: HOL/Auth/OtwayRees_Bad.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1996 University of Cambridge 4*) 5 6 7section\<open>The Otway-Rees Protocol: The Faulty BAN Version\<close> 8 9theory OtwayRees_Bad imports Public begin 10 11text\<open>The FAULTY version omitting encryption of Nonce NB, as suggested on 12page 247 of 13 Burrows, Abadi and Needham (1988). A Logic of Authentication. 14 Proc. Royal Soc. 426 15 16This file illustrates the consequences of such errors. We can still prove 17impressive-looking properties such as \<open>Spy_not_see_encrypted_key\<close>, yet 18the protocol is open to a middleperson attack. Attempting to prove some key 19lemmas indicates the possibility of this attack.\<close> 20 21inductive_set otway :: "event list set" 22 where 23 Nil: \<comment> \<open>The empty trace\<close> 24 "[] \<in> otway" 25 26 | Fake: \<comment> \<open>The Spy may say anything he can say. The sender field is correct, 27 but agents don't use that information.\<close> 28 "[| evsf \<in> otway; X \<in> synth (analz (knows Spy evsf)) |] 29 ==> Says Spy B X # evsf \<in> otway" 30 31 32 | Reception: \<comment> \<open>A message that has been sent can be received by the 33 intended recipient.\<close> 34 "[| evsr \<in> otway; Says A B X \<in>set evsr |] 35 ==> Gets B X # evsr \<in> otway" 36 37 | OR1: \<comment> \<open>Alice initiates a protocol run\<close> 38 "[| evs1 \<in> otway; Nonce NA \<notin> used evs1 |] 39 ==> Says A B \<lbrace>Nonce NA, Agent A, Agent B, 40 Crypt (shrK A) \<lbrace>Nonce NA, Agent A, Agent B\<rbrace>\<rbrace> 41 # evs1 \<in> otway" 42 43 | OR2: \<comment> \<open>Bob's response to Alice's message. 44 This variant of the protocol does NOT encrypt NB.\<close> 45 "[| evs2 \<in> otway; Nonce NB \<notin> used evs2; 46 Gets B \<lbrace>Nonce NA, Agent A, Agent B, X\<rbrace> \<in> set evs2 |] 47 ==> Says B Server 48 \<lbrace>Nonce NA, Agent A, Agent B, X, Nonce NB, 49 Crypt (shrK B) \<lbrace>Nonce NA, Agent A, Agent B\<rbrace>\<rbrace> 50 # evs2 \<in> otway" 51 52 | OR3: \<comment> \<open>The Server receives Bob's message and checks that the three NAs 53 match. Then he sends a new session key to Bob with a packet for 54 forwarding to Alice.\<close> 55 "[| evs3 \<in> otway; Key KAB \<notin> used evs3; 56 Gets Server 57 \<lbrace>Nonce NA, Agent A, Agent B, 58 Crypt (shrK A) \<lbrace>Nonce NA, Agent A, Agent B\<rbrace>, 59 Nonce NB, 60 Crypt (shrK B) \<lbrace>Nonce NA, Agent A, Agent B\<rbrace>\<rbrace> 61 \<in> set evs3 |] 62 ==> Says Server B 63 \<lbrace>Nonce NA, 64 Crypt (shrK A) \<lbrace>Nonce NA, Key KAB\<rbrace>, 65 Crypt (shrK B) \<lbrace>Nonce NB, Key KAB\<rbrace>\<rbrace> 66 # evs3 \<in> otway" 67 68 | OR4: \<comment> \<open>Bob receives the Server's (?) message and compares the Nonces with 69 those in the message he previously sent the Server. 70 Need \<^term>\<open>B \<noteq> Server\<close> because we allow messages to self.\<close> 71 "[| evs4 \<in> otway; B \<noteq> Server; 72 Says B Server \<lbrace>Nonce NA, Agent A, Agent B, X', Nonce NB, 73 Crypt (shrK B) \<lbrace>Nonce NA, Agent A, Agent B\<rbrace>\<rbrace> 74 \<in> set evs4; 75 Gets B \<lbrace>Nonce NA, X, Crypt (shrK B) \<lbrace>Nonce NB, Key K\<rbrace>\<rbrace> 76 \<in> set evs4 |] 77 ==> Says B A \<lbrace>Nonce NA, X\<rbrace> # evs4 \<in> otway" 78 79 | Oops: \<comment> \<open>This message models possible leaks of session keys. The nonces 80 identify the protocol run.\<close> 81 "[| evso \<in> otway; 82 Says Server B \<lbrace>Nonce NA, X, Crypt (shrK B) \<lbrace>Nonce NB, Key K\<rbrace>\<rbrace> 83 \<in> set evso |] 84 ==> Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> # evso \<in> otway" 85 86 87declare Says_imp_knows_Spy [THEN analz.Inj, dest] 88declare parts.Body [dest] 89declare analz_into_parts [dest] 90declare Fake_parts_insert_in_Un [dest] 91 92text\<open>A "possibility property": there are traces that reach the end\<close> 93lemma "[| B \<noteq> Server; Key K \<notin> used [] |] 94 ==> \<exists>NA. \<exists>evs \<in> otway. 95 Says B A \<lbrace>Nonce NA, Crypt (shrK A) \<lbrace>Nonce NA, Key K\<rbrace>\<rbrace> 96 \<in> set evs" 97apply (intro exI bexI) 98apply (rule_tac [2] otway.Nil 99 [THEN otway.OR1, THEN otway.Reception, 100 THEN otway.OR2, THEN otway.Reception, 101 THEN otway.OR3, THEN otway.Reception, THEN otway.OR4]) 102apply (possibility, simp add: used_Cons) 103done 104 105lemma Gets_imp_Says [dest!]: 106 "[| Gets B X \<in> set evs; evs \<in> otway |] ==> \<exists>A. Says A B X \<in> set evs" 107apply (erule rev_mp) 108apply (erule otway.induct, auto) 109done 110 111 112subsection\<open>For reasoning about the encrypted portion of messages\<close> 113 114lemma OR2_analz_knows_Spy: 115 "[| Gets B \<lbrace>N, Agent A, Agent B, X\<rbrace> \<in> set evs; evs \<in> otway |] 116 ==> X \<in> analz (knows Spy evs)" 117by blast 118 119lemma OR4_analz_knows_Spy: 120 "[| Gets B \<lbrace>N, X, Crypt (shrK B) X'\<rbrace> \<in> set evs; evs \<in> otway |] 121 ==> X \<in> analz (knows Spy evs)" 122by blast 123 124lemma Oops_parts_knows_Spy: 125 "Says Server B \<lbrace>NA, X, Crypt K' \<lbrace>NB,K\<rbrace>\<rbrace> \<in> set evs 126 ==> K \<in> parts (knows Spy evs)" 127by blast 128 129text\<open>Forwarding lemma: see comments in OtwayRees.thy\<close> 130lemmas OR2_parts_knows_Spy = 131 OR2_analz_knows_Spy [THEN analz_into_parts] 132 133 134text\<open>Theorems of the form \<^term>\<open>X \<notin> parts (spies evs)\<close> imply that 135NOBODY sends messages containing X!\<close> 136 137text\<open>Spy never sees a good agent's shared key!\<close> 138lemma Spy_see_shrK [simp]: 139 "evs \<in> otway ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)" 140by (erule otway.induct, force, 141 drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+) 142 143 144lemma Spy_analz_shrK [simp]: 145 "evs \<in> otway ==> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)" 146by auto 147 148lemma Spy_see_shrK_D [dest!]: 149 "[|Key (shrK A) \<in> parts (knows Spy evs); evs \<in> otway|] ==> A \<in> bad" 150by (blast dest: Spy_see_shrK) 151 152 153subsection\<open>Proofs involving analz\<close> 154 155text\<open>Describes the form of K and NA when the Server sends this message. Also 156 for Oops case.\<close> 157lemma Says_Server_message_form: 158 "[| Says Server B \<lbrace>NA, X, Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs; 159 evs \<in> otway |] 160 ==> K \<notin> range shrK \<and> (\<exists>i. NA = Nonce i) \<and> (\<exists>j. NB = Nonce j)" 161apply (erule rev_mp) 162apply (erule otway.induct, simp_all) 163done 164 165 166(**** 167 The following is to prove theorems of the form 168 169 Key K \<in> analz (insert (Key KAB) (knows Spy evs)) ==> 170 Key K \<in> analz (knows Spy evs) 171 172 A more general formula must be proved inductively. 173****) 174 175 176text\<open>Session keys are not used to encrypt other session keys\<close> 177 178text\<open>The equality makes the induction hypothesis easier to apply\<close> 179lemma analz_image_freshK [rule_format]: 180 "evs \<in> otway ==> 181 \<forall>K KK. KK \<subseteq> -(range shrK) \<longrightarrow> 182 (Key K \<in> analz (Key`KK \<union> (knows Spy evs))) = 183 (K \<in> KK | Key K \<in> analz (knows Spy evs))" 184apply (erule otway.induct) 185apply (frule_tac [8] Says_Server_message_form) 186apply (drule_tac [7] OR4_analz_knows_Spy) 187apply (drule_tac [5] OR2_analz_knows_Spy, analz_freshK, spy_analz, auto) 188done 189 190lemma analz_insert_freshK: 191 "[| evs \<in> otway; KAB \<notin> range shrK |] ==> 192 (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) = 193 (K = KAB | Key K \<in> analz (knows Spy evs))" 194by (simp only: analz_image_freshK analz_image_freshK_simps) 195 196 197text\<open>The Key K uniquely identifies the Server's message.\<close> 198lemma unique_session_keys: 199 "[| Says Server B \<lbrace>NA, X, Crypt (shrK B) \<lbrace>NB, K\<rbrace>\<rbrace> \<in> set evs; 200 Says Server B' \<lbrace>NA',X',Crypt (shrK B') \<lbrace>NB',K\<rbrace>\<rbrace> \<in> set evs; 201 evs \<in> otway |] ==> X=X' \<and> B=B' \<and> NA=NA' \<and> NB=NB'" 202apply (erule rev_mp) 203apply (erule rev_mp) 204apply (erule otway.induct, simp_all) 205apply blast+ \<comment> \<open>OR3 and OR4\<close> 206done 207 208 209text\<open>Crucial secrecy property: Spy does not see the keys sent in msg OR3 210 Does not in itself guarantee security: an attack could violate 211 the premises, e.g. by having \<^term>\<open>A=Spy\<close>\<close> 212lemma secrecy_lemma: 213 "[| A \<notin> bad; B \<notin> bad; evs \<in> otway |] 214 ==> Says Server B 215 \<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>, 216 Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs \<longrightarrow> 217 Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs \<longrightarrow> 218 Key K \<notin> analz (knows Spy evs)" 219apply (erule otway.induct, force) 220apply (frule_tac [7] Says_Server_message_form) 221apply (drule_tac [6] OR4_analz_knows_Spy) 222apply (drule_tac [4] OR2_analz_knows_Spy) 223apply (simp_all add: analz_insert_eq analz_insert_freshK pushes) 224apply spy_analz \<comment> \<open>Fake\<close> 225apply (blast dest: unique_session_keys)+ \<comment> \<open>OR3, OR4, Oops\<close> 226done 227 228 229lemma Spy_not_see_encrypted_key: 230 "[| Says Server B 231 \<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>, 232 Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs; 233 Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs; 234 A \<notin> bad; B \<notin> bad; evs \<in> otway |] 235 ==> Key K \<notin> analz (knows Spy evs)" 236by (blast dest: Says_Server_message_form secrecy_lemma) 237 238 239subsection\<open>Attempting to prove stronger properties\<close> 240 241text\<open>Only OR1 can have caused such a part of a message to appear. The premise 242 \<^term>\<open>A \<noteq> B\<close> prevents OR2's similar-looking cryptogram from being picked 243 up. Original Otway-Rees doesn't need it.\<close> 244lemma Crypt_imp_OR1 [rule_format]: 245 "[| A \<notin> bad; A \<noteq> B; evs \<in> otway |] 246 ==> Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace> \<in> parts (knows Spy evs) \<longrightarrow> 247 Says A B \<lbrace>NA, Agent A, Agent B, 248 Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace> \<in> set evs" 249by (erule otway.induct, force, 250 drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+) 251 252 253text\<open>Crucial property: If the encrypted message appears, and A has used NA 254 to start a run, then it originated with the Server! 255 The premise \<^term>\<open>A \<noteq> B\<close> allows use of \<open>Crypt_imp_OR1\<close>\<close> 256text\<open>Only it is FALSE. Somebody could make a fake message to Server 257 substituting some other nonce NA' for NB.\<close> 258lemma "[| A \<notin> bad; A \<noteq> B; evs \<in> otway |] 259 ==> Crypt (shrK A) \<lbrace>NA, Key K\<rbrace> \<in> parts (knows Spy evs) \<longrightarrow> 260 Says A B \<lbrace>NA, Agent A, Agent B, 261 Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace> 262 \<in> set evs \<longrightarrow> 263 (\<exists>B NB. Says Server B 264 \<lbrace>NA, 265 Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>, 266 Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs)" 267apply (erule otway.induct, force, 268 drule_tac [4] OR2_parts_knows_Spy, simp_all) 269apply blast \<comment> \<open>Fake\<close> 270apply blast \<comment> \<open>OR1: it cannot be a new Nonce, contradiction.\<close> 271txt\<open>OR3 and OR4\<close> 272apply (simp_all add: ex_disj_distrib) 273 prefer 2 apply (blast intro!: Crypt_imp_OR1) \<comment> \<open>OR4\<close> 274txt\<open>OR3\<close> 275apply clarify 276(*The hypotheses at this point suggest an attack in which nonce NB is used 277 in two different roles: 278 Gets Server 279 \<lbrace>Nonce NA, Agent Aa, Agent A, 280 Crypt (shrK Aa) \<lbrace>Nonce NA, Agent Aa, Agent A\<rbrace>, Nonce NB, 281 Crypt (shrK A) \<lbrace>Nonce NA, Agent Aa, Agent A\<rbrace>\<rbrace> 282 \<in> set evs3 283 Says A B 284 \<lbrace>Nonce NB, Agent A, Agent B, 285 Crypt (shrK A) \<lbrace>Nonce NB, Agent A, Agent B\<rbrace>\<rbrace> 286 \<in> set evs3; 287*) 288 289 290(*Thus the key property A_can_trust probably fails too.*) 291oops 292 293end 294