1(* Title: HOL/Auth/Yahalom_Bad.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1996 University of Cambridge 4*) 5 6section\<open>The Yahalom Protocol: A Flawed Version\<close> 7 8theory Yahalom_Bad imports Public begin 9 10text\<open> 11Demonstrates of why Oops is necessary. This protocol can be attacked because 12it doesn't keep NB secret, but without Oops it can be "verified" anyway. 13The issues are discussed in lcp's LICS 2000 invited lecture. 14\<close> 15 16inductive_set yahalom :: "event list set" 17 where 18 (*Initial trace is empty*) 19 Nil: "[] \<in> yahalom" 20 21 (*The spy MAY say anything he CAN say. We do not expect him to 22 invent new nonces here, but he can also use NS1. Common to 23 all similar protocols.*) 24 | Fake: "[| evsf \<in> yahalom; X \<in> synth (analz (knows Spy evsf)) |] 25 ==> Says Spy B X # evsf \<in> yahalom" 26 27 (*A message that has been sent can be received by the 28 intended recipient.*) 29 | Reception: "[| evsr \<in> yahalom; Says A B X \<in> set evsr |] 30 ==> Gets B X # evsr \<in> yahalom" 31 32 (*Alice initiates a protocol run*) 33 | YM1: "[| evs1 \<in> yahalom; Nonce NA \<notin> used evs1 |] 34 ==> Says A B \<lbrace>Agent A, Nonce NA\<rbrace> # evs1 \<in> yahalom" 35 36 (*Bob's response to Alice's message.*) 37 | YM2: "[| evs2 \<in> yahalom; Nonce NB \<notin> used evs2; 38 Gets B \<lbrace>Agent A, Nonce NA\<rbrace> \<in> set evs2 |] 39 ==> Says B Server 40 \<lbrace>Agent B, Nonce NB, Crypt (shrK B) \<lbrace>Agent A, Nonce NA\<rbrace>\<rbrace> 41 # evs2 \<in> yahalom" 42 43 (*The Server receives Bob's message. He responds by sending a 44 new session key to Alice, with a packet for forwarding to Bob.*) 45 | YM3: "[| evs3 \<in> yahalom; Key KAB \<notin> used evs3; KAB \<in> symKeys; 46 Gets Server 47 \<lbrace>Agent B, Nonce NB, Crypt (shrK B) \<lbrace>Agent A, Nonce NA\<rbrace>\<rbrace> 48 \<in> set evs3 |] 49 ==> Says Server A 50 \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key KAB, Nonce NA, Nonce NB\<rbrace>, 51 Crypt (shrK B) \<lbrace>Agent A, Key KAB\<rbrace>\<rbrace> 52 # evs3 \<in> yahalom" 53 54 (*Alice receives the Server's (?) message, checks her Nonce, and 55 uses the new session key to send Bob his Nonce. The premise 56 A \<noteq> Server is needed to prove Says_Server_not_range.*) 57 | YM4: "[| evs4 \<in> yahalom; A \<noteq> Server; K \<in> symKeys; 58 Gets A \<lbrace>Crypt(shrK A) \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace>, X\<rbrace> 59 \<in> set evs4; 60 Says A B \<lbrace>Agent A, Nonce NA\<rbrace> \<in> set evs4 |] 61 ==> Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> # evs4 \<in> yahalom" 62 63 64declare Says_imp_knows_Spy [THEN analz.Inj, dest] 65declare parts.Body [dest] 66declare Fake_parts_insert_in_Un [dest] 67declare analz_into_parts [dest] 68 69 70text\<open>A "possibility property": there are traces that reach the end\<close> 71lemma "[| A \<noteq> Server; Key K \<notin> used []; K \<in> symKeys |] 72 ==> \<exists>X NB. \<exists>evs \<in> yahalom. 73 Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs" 74apply (intro exI bexI) 75apply (rule_tac [2] yahalom.Nil 76 [THEN yahalom.YM1, THEN yahalom.Reception, 77 THEN yahalom.YM2, THEN yahalom.Reception, 78 THEN yahalom.YM3, THEN yahalom.Reception, 79 THEN yahalom.YM4]) 80apply (possibility, simp add: used_Cons) 81done 82 83subsection\<open>Regularity Lemmas for Yahalom\<close> 84 85lemma Gets_imp_Says: 86 "[| Gets B X \<in> set evs; evs \<in> yahalom |] ==> \<exists>A. Says A B X \<in> set evs" 87by (erule rev_mp, erule yahalom.induct, auto) 88 89(*Must be proved separately for each protocol*) 90lemma Gets_imp_knows_Spy: 91 "[| Gets B X \<in> set evs; evs \<in> yahalom |] ==> X \<in> knows Spy evs" 92by (blast dest!: Gets_imp_Says Says_imp_knows_Spy) 93 94declare Gets_imp_knows_Spy [THEN analz.Inj, dest] 95 96 97subsection\<open>For reasoning about the encrypted portion of messages\<close> 98 99text\<open>Lets us treat YM4 using a similar argument as for the Fake case.\<close> 100lemma YM4_analz_knows_Spy: 101 "[| Gets A \<lbrace>Crypt (shrK A) Y, X\<rbrace> \<in> set evs; evs \<in> yahalom |] 102 ==> X \<in> analz (knows Spy evs)" 103by blast 104 105lemmas YM4_parts_knows_Spy = 106 YM4_analz_knows_Spy [THEN analz_into_parts] 107 108 109text\<open>Theorems of the form \<^term>\<open>X \<notin> parts (knows Spy evs)\<close> imply 110 that NOBODY sends messages containing X!\<close> 111 112text\<open>Spy never sees a good agent's shared key!\<close> 113lemma Spy_see_shrK [simp]: 114 "evs \<in> yahalom ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)" 115apply (erule yahalom.induct, force, 116 drule_tac [6] YM4_parts_knows_Spy, simp_all, blast+) 117done 118 119lemma Spy_analz_shrK [simp]: 120 "evs \<in> yahalom ==> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)" 121by auto 122 123lemma Spy_see_shrK_D [dest!]: 124 "[|Key (shrK A) \<in> parts (knows Spy evs); evs \<in> yahalom|] ==> A \<in> bad" 125by (blast dest: Spy_see_shrK) 126 127text\<open>Nobody can have used non-existent keys! 128 Needed to apply \<open>analz_insert_Key\<close>\<close> 129lemma new_keys_not_used [simp]: 130 "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> yahalom|] 131 ==> K \<notin> keysFor (parts (spies evs))" 132apply (erule rev_mp) 133apply (erule yahalom.induct, force, 134 frule_tac [6] YM4_parts_knows_Spy, simp_all) 135txt\<open>Fake\<close> 136apply (force dest!: keysFor_parts_insert, auto) 137done 138 139 140subsection\<open>Secrecy Theorems\<close> 141 142(**** 143 The following is to prove theorems of the form 144 145 Key K \<in> analz (insert (Key KAB) (knows Spy evs)) ==> 146 Key K \<in> analz (knows Spy evs) 147 148 A more general formula must be proved inductively. 149****) 150 151subsection\<open>Session keys are not used to encrypt other session keys\<close> 152 153lemma analz_image_freshK [rule_format]: 154 "evs \<in> yahalom ==> 155 \<forall>K KK. KK \<subseteq> - (range shrK) \<longrightarrow> 156 (Key K \<in> analz (Key`KK \<union> (knows Spy evs))) = 157 (K \<in> KK | Key K \<in> analz (knows Spy evs))" 158by (erule yahalom.induct, 159 drule_tac [7] YM4_analz_knows_Spy, analz_freshK, spy_analz, blast) 160 161lemma analz_insert_freshK: 162 "[| evs \<in> yahalom; KAB \<notin> range shrK |] ==> 163 (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) = 164 (K = KAB | Key K \<in> analz (knows Spy evs))" 165by (simp only: analz_image_freshK analz_image_freshK_simps) 166 167 168text\<open>The Key K uniquely identifies the Server's message.\<close> 169lemma unique_session_keys: 170 "[| Says Server A 171 \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>, X\<rbrace> \<in> set evs; 172 Says Server A' 173 \<lbrace>Crypt (shrK A') \<lbrace>Agent B', Key K, na', nb'\<rbrace>, X'\<rbrace> \<in> set evs; 174 evs \<in> yahalom |] 175 ==> A=A' \<and> B=B' \<and> na=na' \<and> nb=nb'" 176apply (erule rev_mp, erule rev_mp) 177apply (erule yahalom.induct, simp_all) 178txt\<open>YM3, by freshness, and YM4\<close> 179apply blast+ 180done 181 182 183text\<open>Crucial secrecy property: Spy does not see the keys sent in msg YM3\<close> 184lemma secrecy_lemma: 185 "[| A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] 186 ==> Says Server A 187 \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>, 188 Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace> 189 \<in> set evs \<longrightarrow> 190 Key K \<notin> analz (knows Spy evs)" 191apply (erule yahalom.induct, force, drule_tac [6] YM4_analz_knows_Spy) 192apply (simp_all add: pushes analz_insert_eq analz_insert_freshK, spy_analz) (*Fake*) 193apply (blast dest: unique_session_keys) (*YM3*) 194done 195 196text\<open>Final version\<close> 197lemma Spy_not_see_encrypted_key: 198 "[| Says Server A 199 \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>, 200 Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace> 201 \<in> set evs; 202 A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] 203 ==> Key K \<notin> analz (knows Spy evs)" 204by (blast dest: secrecy_lemma) 205 206 207subsection\<open>Security Guarantee for A upon receiving YM3\<close> 208 209text\<open>If the encrypted message appears then it originated with the Server\<close> 210lemma A_trusts_YM3: 211 "[| Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace> \<in> parts (knows Spy evs); 212 A \<notin> bad; evs \<in> yahalom |] 213 ==> Says Server A 214 \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>, 215 Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace> 216 \<in> set evs" 217apply (erule rev_mp) 218apply (erule yahalom.induct, force, 219 frule_tac [6] YM4_parts_knows_Spy, simp_all) 220txt\<open>Fake, YM3\<close> 221apply blast+ 222done 223 224text\<open>The obvious combination of \<open>A_trusts_YM3\<close> with 225 \<open>Spy_not_see_encrypted_key\<close>\<close> 226lemma A_gets_good_key: 227 "[| Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace> \<in> parts (knows Spy evs); 228 A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] 229 ==> Key K \<notin> analz (knows Spy evs)" 230by (blast dest!: A_trusts_YM3 Spy_not_see_encrypted_key) 231 232subsection\<open>Security Guarantees for B upon receiving YM4\<close> 233 234text\<open>B knows, by the first part of A's message, that the Server distributed 235 the key for A and B. But this part says nothing about nonces.\<close> 236lemma B_trusts_YM4_shrK: 237 "[| Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace> \<in> parts (knows Spy evs); 238 B \<notin> bad; evs \<in> yahalom |] 239 ==> \<exists>NA NB. Says Server A 240 \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace>, 241 Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace> 242 \<in> set evs" 243apply (erule rev_mp) 244apply (erule yahalom.induct, force, 245 frule_tac [6] YM4_parts_knows_Spy, simp_all) 246txt\<open>Fake, YM3\<close> 247apply blast+ 248done 249 250subsection\<open>The Flaw in the Model\<close> 251 252text\<open>Up to now, the reasoning is similar to standard Yahalom. Now the 253 doubtful reasoning occurs. We should not be assuming that an unknown 254 key is secure, but the model allows us to: there is no Oops rule to 255 let session keys become compromised.\<close> 256 257text\<open>B knows, by the second part of A's message, that the Server distributed 258 the key quoting nonce NB. This part says nothing about agent names. 259 Secrecy of K is assumed; the valid Yahalom proof uses (and later proves) 260 the secrecy of NB.\<close> 261lemma B_trusts_YM4_newK [rule_format]: 262 "[|Key K \<notin> analz (knows Spy evs); evs \<in> yahalom|] 263 ==> Crypt K (Nonce NB) \<in> parts (knows Spy evs) \<longrightarrow> 264 (\<exists>A B NA. Says Server A 265 \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, 266 Nonce NA, Nonce NB\<rbrace>, 267 Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace> 268 \<in> set evs)" 269apply (erule rev_mp) 270apply (erule yahalom.induct, force, 271 frule_tac [6] YM4_parts_knows_Spy) 272apply (analz_mono_contra, simp_all) 273txt\<open>Fake\<close> 274apply blast 275txt\<open>YM3\<close> 276apply blast 277txt\<open>A is uncompromised because NB is secure 278 A's certificate guarantees the existence of the Server message\<close> 279apply (blast dest!: Gets_imp_Says Crypt_Spy_analz_bad 280 dest: Says_imp_spies 281 parts.Inj [THEN parts.Fst, THEN A_trusts_YM3]) 282done 283 284 285text\<open>B's session key guarantee from YM4. The two certificates contribute to a 286 single conclusion about the Server's message.\<close> 287lemma B_trusts_YM4: 288 "[| Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>, 289 Crypt K (Nonce NB)\<rbrace> \<in> set evs; 290 Says B Server 291 \<lbrace>Agent B, Nonce NB, Crypt (shrK B) \<lbrace>Agent A, Nonce NA\<rbrace>\<rbrace> 292 \<in> set evs; 293 A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] 294 ==> \<exists>na nb. Says Server A 295 \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>, 296 Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace> 297 \<in> set evs" 298by (blast dest: B_trusts_YM4_newK B_trusts_YM4_shrK Spy_not_see_encrypted_key 299 unique_session_keys) 300 301 302text\<open>The obvious combination of \<open>B_trusts_YM4\<close> with 303 \<open>Spy_not_see_encrypted_key\<close>\<close> 304lemma B_gets_good_key: 305 "[| Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>, 306 Crypt K (Nonce NB)\<rbrace> \<in> set evs; 307 Says B Server 308 \<lbrace>Agent B, Nonce NB, Crypt (shrK B) \<lbrace>Agent A, Nonce NA\<rbrace>\<rbrace> 309 \<in> set evs; 310 A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] 311 ==> Key K \<notin> analz (knows Spy evs)" 312by (blast dest!: B_trusts_YM4 Spy_not_see_encrypted_key) 313 314 315(*** Authenticating B to A: these proofs are not considered. 316 They are irrelevant to showing the need for Oops. ***) 317 318 319(*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***) 320 321text\<open>Assuming the session key is secure, if both certificates are present then 322 A has said NB. We can't be sure about the rest of A's message, but only 323 NB matters for freshness.\<close> 324lemma A_Said_YM3_lemma [rule_format]: 325 "evs \<in> yahalom 326 ==> Key K \<notin> analz (knows Spy evs) \<longrightarrow> 327 Crypt K (Nonce NB) \<in> parts (knows Spy evs) \<longrightarrow> 328 Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace> \<in> parts (knows Spy evs) \<longrightarrow> 329 B \<notin> bad \<longrightarrow> 330 (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs)" 331apply (erule yahalom.induct, force, 332 frule_tac [6] YM4_parts_knows_Spy) 333apply (analz_mono_contra, simp_all) 334txt\<open>Fake\<close> 335apply blast 336txt\<open>YM3: by \<open>new_keys_not_used\<close>, the message 337 \<^term>\<open>Crypt K (Nonce NB)\<close> could not exist\<close> 338apply (force dest!: Crypt_imp_keysFor) 339txt\<open>YM4: was \<^term>\<open>Crypt K (Nonce NB)\<close> the very last message? 340 If not, use the induction hypothesis\<close> 341apply (simp add: ex_disj_distrib) 342txt\<open>yes: apply unicity of session keys\<close> 343apply (blast dest!: Gets_imp_Says A_trusts_YM3 B_trusts_YM4_shrK 344 Crypt_Spy_analz_bad 345 dest: Says_imp_knows_Spy [THEN parts.Inj] unique_session_keys) 346done 347 348text\<open>If B receives YM4 then A has used nonce NB (and therefore is alive). 349 Moreover, A associates K with NB (thus is talking about the same run). 350 Other premises guarantee secrecy of K.\<close> 351lemma YM4_imp_A_Said_YM3 [rule_format]: 352 "[| Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>, 353 Crypt K (Nonce NB)\<rbrace> \<in> set evs; 354 Says B Server 355 \<lbrace>Agent B, Nonce NB, Crypt (shrK B) \<lbrace>Agent A, Nonce NA\<rbrace>\<rbrace> 356 \<in> set evs; 357 A \<notin> bad; B \<notin> bad; evs \<in> yahalom |] 358 ==> \<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs" 359by (blast intro!: A_Said_YM3_lemma 360 dest: Spy_not_see_encrypted_key B_trusts_YM4 Gets_imp_Says) 361 362end 363