1(* Title: HOL/Auth/OtwayRees.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1996 University of Cambridge 4*) 5 6section\<open>The Original Otway-Rees Protocol\<close> 7 8theory OtwayRees imports Public begin 9 10text\<open>From page 244 of 11 Burrows, Abadi and Needham (1989). A Logic of Authentication. 12 Proc. Royal Soc. 426 13 14This is the original version, which encrypts Nonce NB.\<close> 15 16inductive_set otway :: "event list set" 17 where 18 (*Initial trace is empty*) 19 Nil: "[] \<in> otway" 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: "\<lbrakk>evsf \<in> otway; X \<in> synth (analz (knows Spy evsf)) \<rbrakk> 25 \<Longrightarrow> Says Spy B X # evsf \<in> otway" 26 27 (*A message that has been sent can be received by the 28 intended recipient.*) 29 | Reception: "\<lbrakk>evsr \<in> otway; Says A B X \<in>set evsr\<rbrakk> 30 \<Longrightarrow> Gets B X # evsr \<in> otway" 31 32 (*Alice initiates a protocol run*) 33 | OR1: "\<lbrakk>evs1 \<in> otway; Nonce NA \<notin> used evs1\<rbrakk> 34 \<Longrightarrow> Says A B \<lbrace>Nonce NA, Agent A, Agent B, 35 Crypt (shrK A) \<lbrace>Nonce NA, Agent A, Agent B\<rbrace> \<rbrace> 36 # evs1 \<in> otway" 37 38 (*Bob's response to Alice's message. Note that NB is encrypted.*) 39 | OR2: "\<lbrakk>evs2 \<in> otway; Nonce NB \<notin> used evs2; 40 Gets B \<lbrace>Nonce NA, Agent A, Agent B, X\<rbrace> \<in> set evs2\<rbrakk> 41 \<Longrightarrow> Says B Server 42 \<lbrace>Nonce NA, Agent A, Agent B, X, 43 Crypt (shrK B) 44 \<lbrace>Nonce NA, Nonce NB, Agent A, Agent B\<rbrace>\<rbrace> 45 # evs2 \<in> otway" 46 47 (*The Server receives Bob's message and checks that the three NAs 48 match. Then he sends a new session key to Bob with a packet for 49 forwarding to Alice.*) 50 | OR3: "\<lbrakk>evs3 \<in> otway; Key KAB \<notin> used evs3; 51 Gets Server 52 \<lbrace>Nonce NA, Agent A, Agent B, 53 Crypt (shrK A) \<lbrace>Nonce NA, Agent A, Agent B\<rbrace>, 54 Crypt (shrK B) \<lbrace>Nonce NA, Nonce NB, Agent A, Agent B\<rbrace>\<rbrace> 55 \<in> set evs3\<rbrakk> 56 \<Longrightarrow> Says Server B 57 \<lbrace>Nonce NA, 58 Crypt (shrK A) \<lbrace>Nonce NA, Key KAB\<rbrace>, 59 Crypt (shrK B) \<lbrace>Nonce NB, Key KAB\<rbrace>\<rbrace> 60 # evs3 \<in> otway" 61 62 (*Bob receives the Server's (?) message and compares the Nonces with 63 those in the message he previously sent the Server. 64 Need B \<noteq> Server because we allow messages to self.*) 65 | OR4: "\<lbrakk>evs4 \<in> otway; B \<noteq> Server; 66 Says B Server \<lbrace>Nonce NA, Agent A, Agent B, X', 67 Crypt (shrK B) 68 \<lbrace>Nonce NA, Nonce NB, Agent A, Agent B\<rbrace>\<rbrace> 69 \<in> set evs4; 70 Gets B \<lbrace>Nonce NA, X, Crypt (shrK B) \<lbrace>Nonce NB, Key K\<rbrace>\<rbrace> 71 \<in> set evs4\<rbrakk> 72 \<Longrightarrow> Says B A \<lbrace>Nonce NA, X\<rbrace> # evs4 \<in> otway" 73 74 (*This message models possible leaks of session keys. The nonces 75 identify the protocol run.*) 76 | Oops: "\<lbrakk>evso \<in> otway; 77 Says Server B \<lbrace>Nonce NA, X, Crypt (shrK B) \<lbrace>Nonce NB, Key K\<rbrace>\<rbrace> 78 \<in> set evso\<rbrakk> 79 \<Longrightarrow> Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> # evso \<in> otway" 80 81 82declare Says_imp_analz_Spy [dest] 83declare parts.Body [dest] 84declare analz_into_parts [dest] 85declare Fake_parts_insert_in_Un [dest] 86 87 88text\<open>A "possibility property": there are traces that reach the end\<close> 89lemma "\<lbrakk>B \<noteq> Server; Key K \<notin> used []\<rbrakk> 90 \<Longrightarrow> \<exists>evs \<in> otway. 91 Says B A \<lbrace>Nonce NA, Crypt (shrK A) \<lbrace>Nonce NA, Key K\<rbrace>\<rbrace> 92 \<in> set evs" 93apply (intro exI bexI) 94apply (rule_tac [2] otway.Nil 95 [THEN otway.OR1, THEN otway.Reception, 96 THEN otway.OR2, THEN otway.Reception, 97 THEN otway.OR3, THEN otway.Reception, THEN otway.OR4]) 98apply (possibility, simp add: used_Cons) 99done 100 101lemma Gets_imp_Says [dest!]: 102 "\<lbrakk>Gets B X \<in> set evs; evs \<in> otway\<rbrakk> \<Longrightarrow> \<exists>A. Says A B X \<in> set evs" 103apply (erule rev_mp) 104apply (erule otway.induct, auto) 105done 106 107 108(** For reasoning about the encrypted portion of messages **) 109 110lemma OR2_analz_knows_Spy: 111 "\<lbrakk>Gets B \<lbrace>N, Agent A, Agent B, X\<rbrace> \<in> set evs; evs \<in> otway\<rbrakk> 112 \<Longrightarrow> X \<in> analz (knows Spy evs)" 113by blast 114 115lemma OR4_analz_knows_Spy: 116 "\<lbrakk>Gets B \<lbrace>N, X, Crypt (shrK B) X'\<rbrace> \<in> set evs; evs \<in> otway\<rbrakk> 117 \<Longrightarrow> X \<in> analz (knows Spy evs)" 118by blast 119 120(*These lemmas assist simplification by removing forwarded X-variables. 121 We can replace them by rewriting with parts_insert2 and proving using 122 dest: parts_cut, but the proofs become more difficult.*) 123lemmas OR2_parts_knows_Spy = 124 OR2_analz_knows_Spy [THEN analz_into_parts] 125 126(*There could be OR4_parts_knows_Spy and Oops_parts_knows_Spy, but for 127 some reason proofs work without them!*) 128 129 130text\<open>Theorems of the form \<^term>\<open>X \<notin> parts (spies evs)\<close> imply that 131NOBODY sends messages containing X!\<close> 132 133text\<open>Spy never sees a good agent's shared key!\<close> 134lemma Spy_see_shrK [simp]: 135 "evs \<in> otway \<Longrightarrow> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)" 136by (erule otway.induct, force, 137 drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+) 138 139 140lemma Spy_analz_shrK [simp]: 141 "evs \<in> otway \<Longrightarrow> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)" 142by auto 143 144lemma Spy_see_shrK_D [dest!]: 145 "\<lbrakk>Key (shrK A) \<in> parts (knows Spy evs); evs \<in> otway\<rbrakk> \<Longrightarrow> A \<in> bad" 146by (blast dest: Spy_see_shrK) 147 148 149subsection\<open>Towards Secrecy: Proofs Involving \<^term>\<open>analz\<close>\<close> 150 151(*Describes the form of K and NA when the Server sends this message. Also 152 for Oops case.*) 153lemma Says_Server_message_form: 154 "\<lbrakk>Says Server B \<lbrace>NA, X, Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs; 155 evs \<in> otway\<rbrakk> 156 \<Longrightarrow> K \<notin> range shrK \<and> (\<exists>i. NA = Nonce i) \<and> (\<exists>j. NB = Nonce j)" 157by (erule rev_mp, erule otway.induct, simp_all) 158 159 160(**** 161 The following is to prove theorems of the form 162 163 Key K \<in> analz (insert (Key KAB) (knows Spy evs)) \<Longrightarrow> 164 Key K \<in> analz (knows Spy evs) 165 166 A more general formula must be proved inductively. 167****) 168 169 170text\<open>Session keys are not used to encrypt other session keys\<close> 171 172text\<open>The equality makes the induction hypothesis easier to apply\<close> 173lemma analz_image_freshK [rule_format]: 174 "evs \<in> otway \<Longrightarrow> 175 \<forall>K KK. KK \<subseteq> -(range shrK) \<longrightarrow> 176 (Key K \<in> analz (Key`KK \<union> (knows Spy evs))) = 177 (K \<in> KK | Key K \<in> analz (knows Spy evs))" 178apply (erule otway.induct) 179apply (frule_tac [8] Says_Server_message_form) 180apply (drule_tac [7] OR4_analz_knows_Spy) 181apply (drule_tac [5] OR2_analz_knows_Spy, analz_freshK, spy_analz, auto) 182done 183 184lemma analz_insert_freshK: 185 "\<lbrakk>evs \<in> otway; KAB \<notin> range shrK\<rbrakk> \<Longrightarrow> 186 (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) = 187 (K = KAB | Key K \<in> analz (knows Spy evs))" 188by (simp only: analz_image_freshK analz_image_freshK_simps) 189 190 191text\<open>The Key K uniquely identifies the Server's message.\<close> 192lemma unique_session_keys: 193 "\<lbrakk>Says Server B \<lbrace>NA, X, Crypt (shrK B) \<lbrace>NB, K\<rbrace>\<rbrace> \<in> set evs; 194 Says Server B' \<lbrace>NA',X',Crypt (shrK B') \<lbrace>NB',K\<rbrace>\<rbrace> \<in> set evs; 195 evs \<in> otway\<rbrakk> \<Longrightarrow> X=X' \<and> B=B' \<and> NA=NA' \<and> NB=NB'" 196apply (erule rev_mp) 197apply (erule rev_mp) 198apply (erule otway.induct, simp_all) 199apply blast+ \<comment> \<open>OR3 and OR4\<close> 200done 201 202 203subsection\<open>Authenticity properties relating to NA\<close> 204 205text\<open>Only OR1 can have caused such a part of a message to appear.\<close> 206lemma Crypt_imp_OR1 [rule_format]: 207 "\<lbrakk>A \<notin> bad; evs \<in> otway\<rbrakk> 208 \<Longrightarrow> Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace> \<in> parts (knows Spy evs) \<longrightarrow> 209 Says A B \<lbrace>NA, Agent A, Agent B, 210 Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace> 211 \<in> set evs" 212by (erule otway.induct, force, 213 drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+) 214 215lemma Crypt_imp_OR1_Gets: 216 "\<lbrakk>Gets B \<lbrace>NA, Agent A, Agent B, 217 Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace> \<in> set evs; 218 A \<notin> bad; evs \<in> otway\<rbrakk> 219 \<Longrightarrow> Says A B \<lbrace>NA, Agent A, Agent B, 220 Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace> 221 \<in> set evs" 222by (blast dest: Crypt_imp_OR1) 223 224 225text\<open>The Nonce NA uniquely identifies A's message\<close> 226lemma unique_NA: 227 "\<lbrakk>Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace> \<in> parts (knows Spy evs); 228 Crypt (shrK A) \<lbrace>NA, Agent A, Agent C\<rbrace> \<in> parts (knows Spy evs); 229 evs \<in> otway; A \<notin> bad\<rbrakk> 230 \<Longrightarrow> B = C" 231apply (erule rev_mp, erule rev_mp) 232apply (erule otway.induct, force, 233 drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+) 234done 235 236 237text\<open>It is impossible to re-use a nonce in both OR1 and OR2. This holds because 238 OR2 encrypts Nonce NB. It prevents the attack that can occur in the 239 over-simplified version of this protocol: see \<open>OtwayRees_Bad\<close>.\<close> 240lemma no_nonce_OR1_OR2: 241 "\<lbrakk>Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace> \<in> parts (knows Spy evs); 242 A \<notin> bad; evs \<in> otway\<rbrakk> 243 \<Longrightarrow> Crypt (shrK A) \<lbrace>NA', NA, Agent A', Agent A\<rbrace> \<notin> parts (knows Spy evs)" 244apply (erule rev_mp) 245apply (erule otway.induct, force, 246 drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+) 247done 248 249text\<open>Crucial property: If the encrypted message appears, and A has used NA 250 to start a run, then it originated with the Server!\<close> 251lemma NA_Crypt_imp_Server_msg [rule_format]: 252 "\<lbrakk>A \<notin> bad; evs \<in> otway\<rbrakk> 253 \<Longrightarrow> Says A B \<lbrace>NA, Agent A, Agent B, 254 Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace> \<in> set evs \<longrightarrow> 255 Crypt (shrK A) \<lbrace>NA, Key K\<rbrace> \<in> parts (knows Spy evs) 256 \<longrightarrow> (\<exists>NB. Says Server B 257 \<lbrace>NA, 258 Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>, 259 Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs)" 260apply (erule otway.induct, force, 261 drule_tac [4] OR2_parts_knows_Spy, simp_all, blast) 262 subgoal \<comment> \<open>OR1: by freshness\<close> 263 by blast 264 subgoal \<comment> \<open>OR3\<close> 265 by (blast dest!: no_nonce_OR1_OR2 intro: unique_NA) 266 subgoal \<comment> \<open>OR4\<close> 267 by (blast intro!: Crypt_imp_OR1) 268done 269 270 271text\<open>Corollary: if A receives B's OR4 message and the nonce NA agrees 272 then the key really did come from the Server! CANNOT prove this of the 273 bad form of this protocol, even though we can prove 274 \<open>Spy_not_see_encrypted_key\<close>\<close> 275lemma A_trusts_OR4: 276 "\<lbrakk>Says A B \<lbrace>NA, Agent A, Agent B, 277 Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace> \<in> set evs; 278 Says B' A \<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>\<rbrace> \<in> set evs; 279 A \<notin> bad; evs \<in> otway\<rbrakk> 280 \<Longrightarrow> \<exists>NB. Says Server B 281 \<lbrace>NA, 282 Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>, 283 Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> 284 \<in> set evs" 285by (blast intro!: NA_Crypt_imp_Server_msg) 286 287 288text\<open>Crucial secrecy property: Spy does not see the keys sent in msg OR3 289 Does not in itself guarantee security: an attack could violate 290 the premises, e.g. by having \<^term>\<open>A=Spy\<close>\<close> 291lemma secrecy_lemma: 292 "\<lbrakk>A \<notin> bad; B \<notin> bad; evs \<in> otway\<rbrakk> 293 \<Longrightarrow> Says Server B 294 \<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>, 295 Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs \<longrightarrow> 296 Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs \<longrightarrow> 297 Key K \<notin> analz (knows Spy evs)" 298 apply (erule otway.induct, force, simp_all) 299 subgoal \<comment> \<open>Fake\<close> 300 by spy_analz 301 subgoal \<comment> \<open>OR2\<close> 302 by (drule OR2_analz_knows_Spy) (auto simp: analz_insert_eq) 303 subgoal \<comment> \<open>OR3\<close> 304 by (auto simp add: analz_insert_freshK pushes) 305 subgoal \<comment> \<open>OR4\<close> 306 by (drule OR4_analz_knows_Spy) (auto simp: analz_insert_eq) 307 subgoal \<comment> \<open>Oops\<close> 308 by (auto simp add: Says_Server_message_form analz_insert_freshK unique_session_keys) 309 done 310 311theorem Spy_not_see_encrypted_key: 312 "\<lbrakk>Says Server B 313 \<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>, 314 Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs; 315 Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs; 316 A \<notin> bad; B \<notin> bad; evs \<in> otway\<rbrakk> 317 \<Longrightarrow> Key K \<notin> analz (knows Spy evs)" 318by (blast dest: Says_Server_message_form secrecy_lemma) 319 320text\<open>This form is an immediate consequence of the previous result. It is 321similar to the assertions established by other methods. It is equivalent 322to the previous result in that the Spy already has \<^term>\<open>analz\<close> and 323\<^term>\<open>synth\<close> at his disposal. However, the conclusion 324\<^term>\<open>Key K \<notin> knows Spy evs\<close> appears not to be inductive: all the cases 325other than Fake are trivial, while Fake requires 326\<^term>\<open>Key K \<notin> analz (knows Spy evs)\<close>.\<close> 327lemma Spy_not_know_encrypted_key: 328 "\<lbrakk>Says Server B 329 \<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>, 330 Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs; 331 Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs; 332 A \<notin> bad; B \<notin> bad; evs \<in> otway\<rbrakk> 333 \<Longrightarrow> Key K \<notin> knows Spy evs" 334by (blast dest: Spy_not_see_encrypted_key) 335 336 337text\<open>A's guarantee. The Oops premise quantifies over NB because A cannot know 338 what it is.\<close> 339lemma A_gets_good_key: 340 "\<lbrakk>Says A B \<lbrace>NA, Agent A, Agent B, 341 Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace> \<in> set evs; 342 Says B' A \<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>\<rbrace> \<in> set evs; 343 \<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs; 344 A \<notin> bad; B \<notin> bad; evs \<in> otway\<rbrakk> 345 \<Longrightarrow> Key K \<notin> analz (knows Spy evs)" 346by (blast dest!: A_trusts_OR4 Spy_not_see_encrypted_key) 347 348 349subsection\<open>Authenticity properties relating to NB\<close> 350 351text\<open>Only OR2 can have caused such a part of a message to appear. We do not 352 know anything about X: it does NOT have to have the right form.\<close> 353lemma Crypt_imp_OR2: 354 "\<lbrakk>Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace> \<in> parts (knows Spy evs); 355 B \<notin> bad; evs \<in> otway\<rbrakk> 356 \<Longrightarrow> \<exists>X. Says B Server 357 \<lbrace>NA, Agent A, Agent B, X, 358 Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace>\<rbrace> 359 \<in> set evs" 360apply (erule rev_mp) 361apply (erule otway.induct, force, 362 drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+) 363done 364 365 366text\<open>The Nonce NB uniquely identifies B's message\<close> 367lemma unique_NB: 368 "\<lbrakk>Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace> \<in> parts(knows Spy evs); 369 Crypt (shrK B) \<lbrace>NC, NB, Agent C, Agent B\<rbrace> \<in> parts(knows Spy evs); 370 evs \<in> otway; B \<notin> bad\<rbrakk> 371 \<Longrightarrow> NC = NA \<and> C = A" 372apply (erule rev_mp, erule rev_mp) 373apply (erule otway.induct, force, 374 drule_tac [4] OR2_parts_knows_Spy, simp_all) 375apply blast+ \<comment> \<open>Fake, OR2\<close> 376done 377 378text\<open>If the encrypted message appears, and B has used Nonce NB, 379 then it originated with the Server! Quite messy proof.\<close> 380lemma NB_Crypt_imp_Server_msg [rule_format]: 381 "\<lbrakk>B \<notin> bad; evs \<in> otway\<rbrakk> 382 \<Longrightarrow> Crypt (shrK B) \<lbrace>NB, Key K\<rbrace> \<in> parts (knows Spy evs) 383 \<longrightarrow> (\<forall>X'. Says B Server 384 \<lbrace>NA, Agent A, Agent B, X', 385 Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace>\<rbrace> 386 \<in> set evs 387 \<longrightarrow> Says Server B 388 \<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>, 389 Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> 390 \<in> set evs)" 391apply simp 392apply (erule otway.induct, force, simp_all) 393 subgoal \<comment> \<open>Fake\<close> 394 by blast 395 subgoal \<comment> \<open>OR2\<close> 396 by (force dest!: OR2_parts_knows_Spy) 397 subgoal \<comment> \<open>OR3\<close> 398 by (blast dest: unique_NB dest!: no_nonce_OR1_OR2) \<comment> \<open>OR3\<close> 399 subgoal \<comment> \<open>OR4\<close> 400 by (blast dest!: Crypt_imp_OR2) 401done 402 403 404text\<open>Guarantee for B: if it gets a message with matching NB then the Server 405 has sent the correct message.\<close> 406theorem B_trusts_OR3: 407 "\<lbrakk>Says B Server \<lbrace>NA, Agent A, Agent B, X', 408 Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace>\<rbrace> 409 \<in> set evs; 410 Gets B \<lbrace>NA, X, Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs; 411 B \<notin> bad; evs \<in> otway\<rbrakk> 412 \<Longrightarrow> Says Server B 413 \<lbrace>NA, 414 Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>, 415 Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> 416 \<in> set evs" 417by (blast intro!: NB_Crypt_imp_Server_msg) 418 419 420text\<open>The obvious combination of \<open>B_trusts_OR3\<close> with 421 \<open>Spy_not_see_encrypted_key\<close>\<close> 422lemma B_gets_good_key: 423 "\<lbrakk>Says B Server \<lbrace>NA, Agent A, Agent B, X', 424 Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace>\<rbrace> 425 \<in> set evs; 426 Gets B \<lbrace>NA, X, Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs; 427 Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs; 428 A \<notin> bad; B \<notin> bad; evs \<in> otway\<rbrakk> 429 \<Longrightarrow> Key K \<notin> analz (knows Spy evs)" 430by (blast dest!: B_trusts_OR3 Spy_not_see_encrypted_key) 431 432 433lemma OR3_imp_OR2: 434 "\<lbrakk>Says Server B 435 \<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>, 436 Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs; 437 B \<notin> bad; evs \<in> otway\<rbrakk> 438 \<Longrightarrow> \<exists>X. Says B Server \<lbrace>NA, Agent A, Agent B, X, 439 Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace>\<rbrace> 440 \<in> set evs" 441apply (erule rev_mp) 442apply (erule otway.induct, simp_all) 443apply (blast dest!: Crypt_imp_OR2)+ 444done 445 446 447text\<open>After getting and checking OR4, agent A can trust that B has been active. 448 We could probably prove that X has the expected form, but that is not 449 strictly necessary for authentication.\<close> 450theorem A_auths_B: 451 "\<lbrakk>Says B' A \<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>\<rbrace> \<in> set evs; 452 Says A B \<lbrace>NA, Agent A, Agent B, 453 Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace> \<in> set evs; 454 A \<notin> bad; B \<notin> bad; evs \<in> otway\<rbrakk> 455 \<Longrightarrow> \<exists>NB X. Says B Server \<lbrace>NA, Agent A, Agent B, X, 456 Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace>\<rbrace> 457 \<in> set evs" 458by (blast dest!: A_trusts_OR4 OR3_imp_OR2) 459 460end 461