1(* Title: HOL/Auth/Recur.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1996 University of Cambridge 4*) 5 6section\<open>The Otway-Bull Recursive Authentication Protocol\<close> 7 8theory Recur imports Public begin 9 10text\<open>End marker for message bundles\<close> 11abbreviation 12 END :: "msg" where 13 "END == Number 0" 14 15(*Two session keys are distributed to each agent except for the initiator, 16 who receives one. 17 Perhaps the two session keys could be bundled into a single message. 18*) 19inductive_set (*Server's response to the nested message*) 20 respond :: "event list \<Rightarrow> (msg*msg*key)set" 21 for evs :: "event list" 22 where 23 One: "Key KAB \<notin> used evs 24 ==> (Hash[Key(shrK A)] \<lbrace>Agent A, Agent B, Nonce NA, END\<rbrace>, 25 \<lbrace>Crypt (shrK A) \<lbrace>Key KAB, Agent B, Nonce NA\<rbrace>, END\<rbrace>, 26 KAB) \<in> respond evs" 27 28 (*The most recent session key is passed up to the caller*) 29 | Cons: "[| (PA, RA, KAB) \<in> respond evs; 30 Key KBC \<notin> used evs; Key KBC \<notin> parts {RA}; 31 PA = Hash[Key(shrK A)] \<lbrace>Agent A, Agent B, Nonce NA, P\<rbrace> |] 32 ==> (Hash[Key(shrK B)] \<lbrace>Agent B, Agent C, Nonce NB, PA\<rbrace>, 33 \<lbrace>Crypt (shrK B) \<lbrace>Key KBC, Agent C, Nonce NB\<rbrace>, 34 Crypt (shrK B) \<lbrace>Key KAB, Agent A, Nonce NB\<rbrace>, 35 RA\<rbrace>, 36 KBC) 37 \<in> respond evs" 38 39 40(*Induction over "respond" can be difficult due to the complexity of the 41 subgoals. Set "responses" captures the general form of certificates. 42*) 43inductive_set 44 responses :: "event list => msg set" 45 for evs :: "event list" 46 where 47 (*Server terminates lists*) 48 Nil: "END \<in> responses evs" 49 50 | Cons: "[| RA \<in> responses evs; Key KAB \<notin> used evs |] 51 ==> \<lbrace>Crypt (shrK B) \<lbrace>Key KAB, Agent A, Nonce NB\<rbrace>, 52 RA\<rbrace> \<in> responses evs" 53 54 55inductive_set recur :: "event list set" 56 where 57 (*Initial trace is empty*) 58 Nil: "[] \<in> recur" 59 60 (*The spy MAY say anything he CAN say. Common to 61 all similar protocols.*) 62 | Fake: "[| evsf \<in> recur; X \<in> synth (analz (knows Spy evsf)) |] 63 ==> Says Spy B X # evsf \<in> recur" 64 65 (*Alice initiates a protocol run. 66 END is a placeholder to terminate the nesting.*) 67 | RA1: "[| evs1 \<in> recur; Nonce NA \<notin> used evs1 |] 68 ==> Says A B (Hash[Key(shrK A)] \<lbrace>Agent A, Agent B, Nonce NA, END\<rbrace>) 69 # evs1 \<in> recur" 70 71 (*Bob's response to Alice's message. C might be the Server. 72 We omit PA = \<lbrace>XA, Agent A, Agent B, Nonce NA, P\<rbrace> because 73 it complicates proofs, so B may respond to any message at all!*) 74 | RA2: "[| evs2 \<in> recur; Nonce NB \<notin> used evs2; 75 Says A' B PA \<in> set evs2 |] 76 ==> Says B C (Hash[Key(shrK B)] \<lbrace>Agent B, Agent C, Nonce NB, PA\<rbrace>) 77 # evs2 \<in> recur" 78 79 (*The Server receives Bob's message and prepares a response.*) 80 | RA3: "[| evs3 \<in> recur; Says B' Server PB \<in> set evs3; 81 (PB,RB,K) \<in> respond evs3 |] 82 ==> Says Server B RB # evs3 \<in> recur" 83 84 (*Bob receives the returned message and compares the Nonces with 85 those in the message he previously sent the Server.*) 86 | RA4: "[| evs4 \<in> recur; 87 Says B C \<lbrace>XH, Agent B, Agent C, Nonce NB, 88 XA, Agent A, Agent B, Nonce NA, P\<rbrace> \<in> set evs4; 89 Says C' B \<lbrace>Crypt (shrK B) \<lbrace>Key KBC, Agent C, Nonce NB\<rbrace>, 90 Crypt (shrK B) \<lbrace>Key KAB, Agent A, Nonce NB\<rbrace>, 91 RA\<rbrace> \<in> set evs4 |] 92 ==> Says B A RA # evs4 \<in> recur" 93 94 (*No "oops" message can easily be expressed. Each session key is 95 associated--in two separate messages--with two nonces. This is 96 one try, but it isn't that useful. Re domino attack, note that 97 Recur.thy proves that each session key is secure provided the two 98 peers are, even if there are compromised agents elsewhere in 99 the chain. Oops cases proved using parts_cut, Key_in_keysFor_parts, 100 etc. 101 102 Oops: "[| evso \<in> recur; Says Server B RB \<in> set evso; 103 RB \<in> responses evs'; Key K \<in> parts {RB} |] 104 ==> Notes Spy \<lbrace>Key K, RB\<rbrace> # evso \<in> recur" 105 *) 106 107 108declare Says_imp_knows_Spy [THEN analz.Inj, dest] 109declare parts.Body [dest] 110declare analz_into_parts [dest] 111declare Fake_parts_insert_in_Un [dest] 112 113 114(** Possibility properties: traces that reach the end 115 ONE theorem would be more elegant and faster! 116 By induction on a list of agents (no repetitions) 117**) 118 119 120text\<open>Simplest case: Alice goes directly to the server\<close> 121lemma "Key K \<notin> used [] 122 ==> \<exists>NA. \<exists>evs \<in> recur. 123 Says Server A \<lbrace>Crypt (shrK A) \<lbrace>Key K, Agent Server, Nonce NA\<rbrace>, 124 END\<rbrace> \<in> set evs" 125apply (intro exI bexI) 126apply (rule_tac [2] recur.Nil [THEN recur.RA1, 127 THEN recur.RA3 [OF _ _ respond.One]]) 128apply (possibility, simp add: used_Cons) 129done 130 131 132text\<open>Case two: Alice, Bob and the server\<close> 133lemma "[| Key K \<notin> used []; Key K' \<notin> used []; K \<noteq> K'; 134 Nonce NA \<notin> used []; Nonce NB \<notin> used []; NA < NB |] 135 ==> \<exists>NA. \<exists>evs \<in> recur. 136 Says B A \<lbrace>Crypt (shrK A) \<lbrace>Key K, Agent B, Nonce NA\<rbrace>, 137 END\<rbrace> \<in> set evs" 138apply (intro exI bexI) 139apply (rule_tac [2] 140 recur.Nil 141 [THEN recur.RA1 [of _ NA], 142 THEN recur.RA2 [of _ NB], 143 THEN recur.RA3 [OF _ _ respond.One 144 [THEN respond.Cons [of _ _ K _ K']]], 145 THEN recur.RA4], possibility) 146apply (auto simp add: used_Cons) 147done 148 149(*Case three: Alice, Bob, Charlie and the server Rather slow (5 seconds)*) 150lemma "[| Key K \<notin> used []; Key K' \<notin> used []; 151 Key K'' \<notin> used []; K \<noteq> K'; K' \<noteq> K''; K \<noteq> K''; 152 Nonce NA \<notin> used []; Nonce NB \<notin> used []; Nonce NC \<notin> used []; 153 NA < NB; NB < NC |] 154 ==> \<exists>K. \<exists>NA. \<exists>evs \<in> recur. 155 Says B A \<lbrace>Crypt (shrK A) \<lbrace>Key K, Agent B, Nonce NA\<rbrace>, 156 END\<rbrace> \<in> set evs" 157apply (intro exI bexI) 158apply (rule_tac [2] 159 recur.Nil [THEN recur.RA1, 160 THEN recur.RA2, THEN recur.RA2, 161 THEN recur.RA3 162 [OF _ _ respond.One 163 [THEN respond.Cons, THEN respond.Cons]], 164 THEN recur.RA4, THEN recur.RA4]) 165apply basic_possibility 166apply (tactic "DEPTH_SOLVE (swap_res_tac \<^context> [refl, conjI, disjCI] 1)") 167done 168 169 170lemma respond_imp_not_used: "(PA,RB,KAB) \<in> respond evs ==> Key KAB \<notin> used evs" 171by (erule respond.induct, simp_all) 172 173lemma Key_in_parts_respond [rule_format]: 174 "[| Key K \<in> parts {RB}; (PB,RB,K') \<in> respond evs |] ==> Key K \<notin> used evs" 175apply (erule rev_mp, erule respond.induct) 176apply (auto dest: Key_not_used respond_imp_not_used) 177done 178 179text\<open>Simple inductive reasoning about responses\<close> 180lemma respond_imp_responses: 181 "(PA,RB,KAB) \<in> respond evs ==> RB \<in> responses evs" 182apply (erule respond.induct) 183apply (blast intro!: respond_imp_not_used responses.intros)+ 184done 185 186 187(** For reasoning about the encrypted portion of messages **) 188 189lemmas RA2_analz_spies = Says_imp_spies [THEN analz.Inj] 190 191lemma RA4_analz_spies: 192 "Says C' B \<lbrace>Crypt K X, X', RA\<rbrace> \<in> set evs ==> RA \<in> analz (spies evs)" 193by blast 194 195 196(*RA2_analz... and RA4_analz... let us treat those cases using the same 197 argument as for the Fake case. This is possible for most, but not all, 198 proofs: Fake does not invent new nonces (as in RA2), and of course Fake 199 messages originate from the Spy. *) 200 201lemmas RA2_parts_spies = RA2_analz_spies [THEN analz_into_parts] 202lemmas RA4_parts_spies = RA4_analz_spies [THEN analz_into_parts] 203 204 205(** Theorems of the form X \<notin> parts (spies evs) imply that NOBODY 206 sends messages containing X! **) 207 208(** Spy never sees another agent's shared key! (unless it's bad at start) **) 209 210lemma Spy_see_shrK [simp]: 211 "evs \<in> recur ==> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)" 212apply (erule recur.induct, auto) 213txt\<open>RA3. It's ugly to call auto twice, but it seems necessary.\<close> 214apply (auto dest: Key_in_parts_respond simp add: parts_insert_spies) 215done 216 217lemma Spy_analz_shrK [simp]: 218 "evs \<in> recur ==> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)" 219by auto 220 221lemma Spy_see_shrK_D [dest!]: 222 "[|Key (shrK A) \<in> parts (knows Spy evs); evs \<in> recur|] ==> A \<in> bad" 223by (blast dest: Spy_see_shrK) 224 225 226(*** Proofs involving analz ***) 227 228(** Session keys are not used to encrypt other session keys **) 229 230(*Version for "responses" relation. Handles case RA3 in the theorem below. 231 Note that it holds for *any* set H (not just "spies evs") 232 satisfying the inductive hypothesis.*) 233lemma resp_analz_image_freshK_lemma: 234 "[| RB \<in> responses evs; 235 \<forall>K KK. KK \<subseteq> - (range shrK) \<longrightarrow> 236 (Key K \<in> analz (Key`KK \<union> H)) = 237 (K \<in> KK | Key K \<in> analz H) |] 238 ==> \<forall>K KK. KK \<subseteq> - (range shrK) \<longrightarrow> 239 (Key K \<in> analz (insert RB (Key`KK \<union> H))) = 240 (K \<in> KK | Key K \<in> analz (insert RB H))" 241apply (erule responses.induct) 242apply (simp_all del: image_insert 243 add: analz_image_freshK_simps, auto) 244done 245 246 247text\<open>Version for the protocol. Proof is easy, thanks to the lemma.\<close> 248lemma raw_analz_image_freshK: 249 "evs \<in> recur ==> 250 \<forall>K KK. KK \<subseteq> - (range shrK) \<longrightarrow> 251 (Key K \<in> analz (Key`KK \<union> (spies evs))) = 252 (K \<in> KK | Key K \<in> analz (spies evs))" 253apply (erule recur.induct) 254apply (drule_tac [4] RA2_analz_spies, 255 drule_tac [5] respond_imp_responses, 256 drule_tac [6] RA4_analz_spies, analz_freshK, spy_analz) 257txt\<open>RA3\<close> 258apply (simp_all add: resp_analz_image_freshK_lemma) 259done 260 261 262(*Instance of the lemma with H replaced by (spies evs): 263 [| RB \<in> responses evs; evs \<in> recur; |] 264 ==> KK \<subseteq> - (range shrK) \<longrightarrow> 265 Key K \<in> analz (insert RB (Key`KK \<union> spies evs)) = 266 (K \<in> KK | Key K \<in> analz (insert RB (spies evs))) 267*) 268lemmas resp_analz_image_freshK = 269 resp_analz_image_freshK_lemma [OF _ raw_analz_image_freshK] 270 271lemma analz_insert_freshK: 272 "[| evs \<in> recur; KAB \<notin> range shrK |] 273 ==> (Key K \<in> analz (insert (Key KAB) (spies evs))) = 274 (K = KAB | Key K \<in> analz (spies evs))" 275by (simp del: image_insert 276 add: analz_image_freshK_simps raw_analz_image_freshK) 277 278 279text\<open>Everything that's hashed is already in past traffic.\<close> 280lemma Hash_imp_body: 281 "[| Hash \<lbrace>Key(shrK A), X\<rbrace> \<in> parts (spies evs); 282 evs \<in> recur; A \<notin> bad |] ==> X \<in> parts (spies evs)" 283apply (erule rev_mp) 284apply (erule recur.induct, 285 drule_tac [6] RA4_parts_spies, 286 drule_tac [5] respond_imp_responses, 287 drule_tac [4] RA2_parts_spies) 288txt\<open>RA3 requires a further induction\<close> 289apply (erule_tac [5] responses.induct, simp_all) 290txt\<open>Fake\<close> 291apply (blast intro: parts_insertI) 292done 293 294 295(** The Nonce NA uniquely identifies A's message. 296 This theorem applies to steps RA1 and RA2! 297 298 Unicity is not used in other proofs but is desirable in its own right. 299**) 300 301lemma unique_NA: 302 "[| Hash \<lbrace>Key(shrK A), Agent A, B, NA, P\<rbrace> \<in> parts (spies evs); 303 Hash \<lbrace>Key(shrK A), Agent A, B',NA, P'\<rbrace> \<in> parts (spies evs); 304 evs \<in> recur; A \<notin> bad |] 305 ==> B=B' \<and> P=P'" 306apply (erule rev_mp, erule rev_mp) 307apply (erule recur.induct, 308 drule_tac [5] respond_imp_responses) 309apply (force, simp_all) 310txt\<open>Fake\<close> 311apply blast 312apply (erule_tac [3] responses.induct) 313txt\<open>RA1,2: creation of new Nonce\<close> 314apply simp_all 315apply (blast dest!: Hash_imp_body)+ 316done 317 318 319(*** Lemmas concerning the Server's response 320 (relations "respond" and "responses") 321***) 322 323lemma shrK_in_analz_respond [simp]: 324 "[| RB \<in> responses evs; evs \<in> recur |] 325 ==> (Key (shrK B) \<in> analz (insert RB (spies evs))) = (B\<in>bad)" 326apply (erule responses.induct) 327apply (simp_all del: image_insert 328 add: analz_image_freshK_simps resp_analz_image_freshK, auto) 329done 330 331 332lemma resp_analz_insert_lemma: 333 "[| Key K \<in> analz (insert RB H); 334 \<forall>K KK. KK \<subseteq> - (range shrK) \<longrightarrow> 335 (Key K \<in> analz (Key`KK \<union> H)) = 336 (K \<in> KK | Key K \<in> analz H); 337 RB \<in> responses evs |] 338 ==> (Key K \<in> parts{RB} | Key K \<in> analz H)" 339apply (erule rev_mp, erule responses.induct) 340apply (simp_all del: image_insert parts_image 341 add: analz_image_freshK_simps resp_analz_image_freshK_lemma) 342txt\<open>Simplification using two distinct treatments of "image"\<close> 343apply (simp add: parts_insert2, blast) 344done 345 346lemmas resp_analz_insert = 347 resp_analz_insert_lemma [OF _ raw_analz_image_freshK] 348 349text\<open>The last key returned by respond indeed appears in a certificate\<close> 350lemma respond_certificate: 351 "(Hash[Key(shrK A)] \<lbrace>Agent A, B, NA, P\<rbrace>, RA, K) \<in> respond evs 352 ==> Crypt (shrK A) \<lbrace>Key K, B, NA\<rbrace> \<in> parts {RA}" 353apply (ind_cases "(Hash[Key (shrK A)] \<lbrace>Agent A, B, NA, P\<rbrace>, RA, K) \<in> respond evs") 354apply simp_all 355done 356 357(*This unicity proof differs from all the others in the HOL/Auth directory. 358 The conclusion isn't quite unicity but duplicity, in that there are two 359 possibilities. Also, the presence of two different matching messages in 360 the inductive step complicates the case analysis. Unusually for such proofs, 361 the quantifiers appear to be necessary.*) 362lemma unique_lemma [rule_format]: 363 "(PB,RB,KXY) \<in> respond evs ==> 364 \<forall>A B N. Crypt (shrK A) \<lbrace>Key K, Agent B, N\<rbrace> \<in> parts {RB} \<longrightarrow> 365 (\<forall>A' B' N'. Crypt (shrK A') \<lbrace>Key K, Agent B', N'\<rbrace> \<in> parts {RB} \<longrightarrow> 366 (A'=A \<and> B'=B) | (A'=B \<and> B'=A))" 367apply (erule respond.induct) 368apply (simp_all add: all_conj_distrib) 369apply (blast dest: respond_certificate) 370done 371 372lemma unique_session_keys: 373 "[| Crypt (shrK A) \<lbrace>Key K, Agent B, N\<rbrace> \<in> parts {RB}; 374 Crypt (shrK A') \<lbrace>Key K, Agent B', N'\<rbrace> \<in> parts {RB}; 375 (PB,RB,KXY) \<in> respond evs |] 376 ==> (A'=A \<and> B'=B) | (A'=B \<and> B'=A)" 377by (rule unique_lemma, auto) 378 379 380(** Crucial secrecy property: Spy does not see the keys sent in msg RA3 381 Does not in itself guarantee security: an attack could violate 382 the premises, e.g. by having A=Spy **) 383 384lemma respond_Spy_not_see_session_key [rule_format]: 385 "[| (PB,RB,KAB) \<in> respond evs; evs \<in> recur |] 386 ==> \<forall>A A' N. A \<notin> bad \<and> A' \<notin> bad \<longrightarrow> 387 Crypt (shrK A) \<lbrace>Key K, Agent A', N\<rbrace> \<in> parts{RB} \<longrightarrow> 388 Key K \<notin> analz (insert RB (spies evs))" 389apply (erule respond.induct) 390apply (frule_tac [2] respond_imp_responses) 391apply (frule_tac [2] respond_imp_not_used) 392apply (simp_all del: image_insert parts_image 393 add: analz_image_freshK_simps split_ifs shrK_in_analz_respond 394 resp_analz_image_freshK parts_insert2) 395txt\<open>Base case of respond\<close> 396apply blast 397txt\<open>Inductive step of respond\<close> 398apply (intro allI conjI impI, simp_all) 399txt\<open>by unicity, either \<^term>\<open>B=Aa\<close> or \<^term>\<open>B=A'\<close>, a contradiction 400 if \<^term>\<open>B \<in> bad\<close>\<close> 401apply (blast dest: unique_session_keys respond_certificate) 402apply (blast dest!: respond_certificate) 403apply (blast dest!: resp_analz_insert) 404done 405 406 407lemma Spy_not_see_session_key: 408 "[| Crypt (shrK A) \<lbrace>Key K, Agent A', N\<rbrace> \<in> parts (spies evs); 409 A \<notin> bad; A' \<notin> bad; evs \<in> recur |] 410 ==> Key K \<notin> analz (spies evs)" 411apply (erule rev_mp) 412apply (erule recur.induct) 413apply (drule_tac [4] RA2_analz_spies, 414 frule_tac [5] respond_imp_responses, 415 drule_tac [6] RA4_analz_spies, 416 simp_all add: split_ifs analz_insert_eq analz_insert_freshK) 417txt\<open>Fake\<close> 418apply spy_analz 419txt\<open>RA2\<close> 420apply blast 421txt\<open>RA3\<close> 422apply (simp add: parts_insert_spies) 423apply (metis Key_in_parts_respond parts.Body parts.Fst resp_analz_insert 424 respond_Spy_not_see_session_key usedI) 425txt\<open>RA4\<close> 426apply blast 427done 428 429(**** Authenticity properties for Agents ****) 430 431text\<open>The response never contains Hashes\<close> 432lemma Hash_in_parts_respond: 433 "[| Hash \<lbrace>Key (shrK B), M\<rbrace> \<in> parts (insert RB H); 434 (PB,RB,K) \<in> respond evs |] 435 ==> Hash \<lbrace>Key (shrK B), M\<rbrace> \<in> parts H" 436apply (erule rev_mp) 437apply (erule respond_imp_responses [THEN responses.induct], auto) 438done 439 440text\<open>Only RA1 or RA2 can have caused such a part of a message to appear. 441 This result is of no use to B, who cannot verify the Hash. Moreover, 442 it can say nothing about how recent A's message is. It might later be 443 used to prove B's presence to A at the run's conclusion.\<close> 444lemma Hash_auth_sender [rule_format]: 445 "[| Hash \<lbrace>Key(shrK A), Agent A, Agent B, NA, P\<rbrace> \<in> parts(spies evs); 446 A \<notin> bad; evs \<in> recur |] 447 ==> Says A B (Hash[Key(shrK A)] \<lbrace>Agent A, Agent B, NA, P\<rbrace>) \<in> set evs" 448apply (unfold HPair_def) 449apply (erule rev_mp) 450apply (erule recur.induct, 451 drule_tac [6] RA4_parts_spies, 452 drule_tac [4] RA2_parts_spies, 453 simp_all) 454txt\<open>Fake, RA3\<close> 455apply (blast dest: Hash_in_parts_respond)+ 456done 457 458(** These two results subsume (for all agents) the guarantees proved 459 separately for A and B in the Otway-Rees protocol. 460**) 461 462 463text\<open>Certificates can only originate with the Server.\<close> 464lemma Cert_imp_Server_msg: 465 "[| Crypt (shrK A) Y \<in> parts (spies evs); 466 A \<notin> bad; evs \<in> recur |] 467 ==> \<exists>C RC. Says Server C RC \<in> set evs \<and> 468 Crypt (shrK A) Y \<in> parts {RC}" 469apply (erule rev_mp, erule recur.induct, simp_all) 470txt\<open>Fake\<close> 471apply blast 472txt\<open>RA1\<close> 473apply blast 474txt\<open>RA2: it cannot be a new Nonce, contradiction.\<close> 475apply blast 476txt\<open>RA3. Pity that the proof is so brittle: this step requires the rewriting, 477 which however would break all other steps.\<close> 478apply (simp add: parts_insert_spies, blast) 479txt\<open>RA4\<close> 480apply blast 481done 482 483end 484