1(* Title: HOL/Auth/OtwayReesBella.thy 2 Author: Giampaolo Bella, Catania University 3*) 4 5section\<open>Bella's version of the Otway-Rees protocol\<close> 6 7 8theory OtwayReesBella imports Public begin 9 10text\<open>Bella's modifications to a version of the Otway-Rees protocol taken from 11the BAN paper only concern message 7. The updated protocol makes the goal of 12key distribution of the session key available to A. Investigating the 13principle of Goal Availability undermines the BAN claim about the original 14protocol, that "this protocol does not make use of Kab as an encryption key, 15so neither principal can know whether the key is known to the other". The 16updated protocol makes no use of the session key to encrypt but informs A that 17B knows it.\<close> 18 19inductive_set orb :: "event list set" 20 where 21 22 Nil: "[]\<in> orb" 23 24| Fake: "\<lbrakk>evsa\<in> orb; X\<in> synth (analz (knows Spy evsa))\<rbrakk> 25 \<Longrightarrow> Says Spy B X # evsa \<in> orb" 26 27| Reception: "\<lbrakk>evsr\<in> orb; Says A B X \<in> set evsr\<rbrakk> 28 \<Longrightarrow> Gets B X # evsr \<in> orb" 29 30| OR1: "\<lbrakk>evs1\<in> orb; Nonce NA \<notin> used evs1\<rbrakk> 31 \<Longrightarrow> Says A B \<lbrace>Nonce M, Agent A, Agent B, 32 Crypt (shrK A) \<lbrace>Nonce NA, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> 33 # evs1 \<in> orb" 34 35| OR2: "\<lbrakk>evs2\<in> orb; Nonce NB \<notin> used evs2; 36 Gets B \<lbrace>Nonce M, Agent A, Agent B, X\<rbrace> \<in> set evs2\<rbrakk> 37 \<Longrightarrow> Says B Server 38 \<lbrace>Nonce M, Agent A, Agent B, X, 39 Crypt (shrK B) \<lbrace>Nonce NB, Nonce M, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> 40 # evs2 \<in> orb" 41 42| OR3: "\<lbrakk>evs3\<in> orb; Key KAB \<notin> used evs3; 43 Gets Server 44 \<lbrace>Nonce M, Agent A, Agent B, 45 Crypt (shrK A) \<lbrace>Nonce NA, Nonce M, Agent A, Agent B\<rbrace>, 46 Crypt (shrK B) \<lbrace>Nonce NB, Nonce M, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> 47 \<in> set evs3\<rbrakk> 48 \<Longrightarrow> Says Server B \<lbrace>Nonce M, 49 Crypt (shrK B) \<lbrace>Crypt (shrK A) \<lbrace>Nonce NA, Key KAB\<rbrace>, 50 Nonce NB, Key KAB\<rbrace>\<rbrace> 51 # evs3 \<in> orb" 52 53 (*B can only check that the message he is bouncing is a ciphertext*) 54 (*Sending M back is omitted*) 55| OR4: "\<lbrakk>evs4\<in> orb; B \<noteq> Server; \<forall> p q. X \<noteq> \<lbrace>p, q\<rbrace>; 56 Says B Server \<lbrace>Nonce M, Agent A, Agent B, X', 57 Crypt (shrK B) \<lbrace>Nonce NB, Nonce M, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> 58 \<in> set evs4; 59 Gets B \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>X, Nonce NB, Key KAB\<rbrace>\<rbrace> 60 \<in> set evs4\<rbrakk> 61 \<Longrightarrow> Says B A \<lbrace>Nonce M, X\<rbrace> # evs4 \<in> orb" 62 63 64| Oops: "\<lbrakk>evso\<in> orb; 65 Says Server B \<lbrace>Nonce M, 66 Crypt (shrK B) \<lbrace>Crypt (shrK A) \<lbrace>Nonce NA, Key KAB\<rbrace>, 67 Nonce NB, Key KAB\<rbrace>\<rbrace> 68 \<in> set evso\<rbrakk> 69 \<Longrightarrow> Notes Spy \<lbrace>Agent A, Agent B, Nonce NA, Nonce NB, Key KAB\<rbrace> # evso 70 \<in> orb" 71 72 73 74declare knows_Spy_partsEs [elim] 75declare analz_into_parts [dest] 76declare Fake_parts_insert_in_Un [dest] 77 78 79text\<open>Fragile proof, with backtracking in the possibility call.\<close> 80lemma possibility_thm: "\<lbrakk>A \<noteq> Server; B \<noteq> Server; Key K \<notin> used[]\<rbrakk> 81 \<Longrightarrow> \<exists> evs \<in> orb. 82 Says B A \<lbrace>Nonce M, Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>\<rbrace> \<in> set evs" 83apply (intro exI bexI) 84apply (rule_tac [2] orb.Nil 85 [THEN orb.OR1, THEN orb.Reception, 86 THEN orb.OR2, THEN orb.Reception, 87 THEN orb.OR3, THEN orb.Reception, THEN orb.OR4]) 88apply (possibility, simp add: used_Cons) 89done 90 91 92lemma Gets_imp_Says : 93 "\<lbrakk>Gets B X \<in> set evs; evs \<in> orb\<rbrakk> \<Longrightarrow> \<exists>A. Says A B X \<in> set evs" 94apply (erule rev_mp) 95apply (erule orb.induct) 96apply auto 97done 98 99lemma Gets_imp_knows_Spy: 100 "\<lbrakk>Gets B X \<in> set evs; evs \<in> orb\<rbrakk> \<Longrightarrow> X \<in> knows Spy evs" 101by (blast dest!: Gets_imp_Says Says_imp_knows_Spy) 102 103declare Gets_imp_knows_Spy [THEN parts.Inj, dest] 104 105lemma Gets_imp_knows: 106 "\<lbrakk>Gets B X \<in> set evs; evs \<in> orb\<rbrakk> \<Longrightarrow> X \<in> knows B evs" 107by (metis Gets_imp_knows_Spy Gets_imp_knows_agents) 108 109lemma OR2_analz_knows_Spy: 110 "\<lbrakk>Gets B \<lbrace>Nonce M, Agent A, Agent B, X\<rbrace> \<in> set evs; evs \<in> orb\<rbrakk> 111 \<Longrightarrow> X \<in> analz (knows Spy evs)" 112by (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj]) 113 114lemma OR4_parts_knows_Spy: 115 "\<lbrakk>Gets B \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>X, Nonce Nb, Key Kab\<rbrace>\<rbrace> \<in> set evs; 116 evs \<in> orb\<rbrakk> \<Longrightarrow> X \<in> parts (knows Spy evs)" 117by blast 118 119lemma Oops_parts_knows_Spy: 120 "Says Server B \<lbrace>Nonce M, Crypt K' \<lbrace>X, Nonce Nb, K\<rbrace>\<rbrace> \<in> set evs 121 \<Longrightarrow> K \<in> parts (knows Spy evs)" 122by blast 123 124lemmas OR2_parts_knows_Spy = 125 OR2_analz_knows_Spy [THEN analz_into_parts] 126 127ML 128\<open> 129fun parts_explicit_tac ctxt i = 130 forward_tac ctxt [@{thm Oops_parts_knows_Spy}] (i+7) THEN 131 forward_tac ctxt [@{thm OR4_parts_knows_Spy}] (i+6) THEN 132 forward_tac ctxt [@{thm OR2_parts_knows_Spy}] (i+4) 133\<close> 134 135method_setup parts_explicit = \<open> 136 Scan.succeed (SIMPLE_METHOD' o parts_explicit_tac)\<close> 137 "to explicitly state that some message components belong to parts knows Spy" 138 139 140lemma Spy_see_shrK [simp]: 141 "evs \<in> orb \<Longrightarrow> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)" 142by (erule orb.induct, parts_explicit, simp_all, blast+) 143 144lemma Spy_analz_shrK [simp]: 145"evs \<in> orb \<Longrightarrow> (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> orb|] ==> A \<in> bad" 150by (blast dest: Spy_see_shrK) 151 152lemma new_keys_not_used [simp]: 153 "\<lbrakk>Key K \<notin> used evs; K \<in> symKeys; evs \<in> orb\<rbrakk> \<Longrightarrow> K \<notin> keysFor (parts (knows Spy evs))" 154apply (erule rev_mp) 155apply (erule orb.induct, parts_explicit, simp_all) 156apply (force dest!: keysFor_parts_insert) 157apply (blast+) 158done 159 160 161 162subsection\<open>Proofs involving analz\<close> 163 164text\<open>Describes the form of K and NA when the Server sends this message. Also 165 for Oops case.\<close> 166lemma Says_Server_message_form: 167"\<lbrakk>Says Server B \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>X, Nonce Nb, Key K\<rbrace>\<rbrace> \<in> set evs; 168 evs \<in> orb\<rbrakk> 169 \<Longrightarrow> K \<notin> range shrK \<and> (\<exists> A Na. X=(Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>))" 170by (erule rev_mp, erule orb.induct, simp_all) 171 172lemma Says_Server_imp_Gets: 173 "\<lbrakk>Says Server B \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>, 174 Nonce Nb, Key K\<rbrace>\<rbrace> \<in> set evs; 175 evs \<in> orb\<rbrakk> 176 \<Longrightarrow> Gets Server \<lbrace>Nonce M, Agent A, Agent B, 177 Crypt (shrK A) \<lbrace>Nonce Na, Nonce M, Agent A, Agent B\<rbrace>, 178 Crypt (shrK B) \<lbrace>Nonce Nb, Nonce M, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> 179 \<in> set evs" 180by (erule rev_mp, erule orb.induct, simp_all) 181 182 183lemma A_trusts_OR1: 184"\<lbrakk>Crypt (shrK A) \<lbrace>Nonce Na, Nonce M, Agent A, Agent B\<rbrace> \<in> parts (knows Spy evs); 185 A \<notin> bad; evs \<in> orb\<rbrakk> 186 \<Longrightarrow> Says A B \<lbrace>Nonce M, Agent A, Agent B, Crypt (shrK A) \<lbrace>Nonce Na, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> \<in> set evs" 187apply (erule rev_mp, erule orb.induct, parts_explicit, simp_all) 188apply (blast) 189done 190 191 192lemma B_trusts_OR2: 193 "\<lbrakk>Crypt (shrK B) \<lbrace>Nonce Nb, Nonce M, Nonce M, Agent A, Agent B\<rbrace> 194 \<in> parts (knows Spy evs); B \<notin> bad; evs \<in> orb\<rbrakk> 195 \<Longrightarrow> (\<exists> X. Says B Server \<lbrace>Nonce M, Agent A, Agent B, X, 196 Crypt (shrK B) \<lbrace>Nonce Nb, Nonce M, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> 197 \<in> set evs)" 198apply (erule rev_mp, erule orb.induct, parts_explicit, simp_all) 199apply (blast+) 200done 201 202 203lemma B_trusts_OR3: 204"\<lbrakk>Crypt (shrK B) \<lbrace>X, Nonce Nb, Key K\<rbrace> \<in> parts (knows Spy evs); 205 B \<notin> bad; evs \<in> orb\<rbrakk> 206\<Longrightarrow> \<exists> M. Says Server B \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>X, Nonce Nb, Key K\<rbrace>\<rbrace> 207 \<in> set evs" 208apply (erule rev_mp, erule orb.induct, parts_explicit, simp_all) 209apply (blast+) 210done 211 212lemma Gets_Server_message_form: 213"\<lbrakk>Gets B \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>X, Nonce Nb, Key K\<rbrace>\<rbrace> \<in> set evs; 214 evs \<in> orb\<rbrakk> 215 \<Longrightarrow> (K \<notin> range shrK \<and> (\<exists> A Na. X = (Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>))) 216 | X \<in> analz (knows Spy evs)" 217by (metis B_trusts_OR3 Crypt_Spy_analz_bad Gets_imp_Says MPair_analz MPair_parts 218 Says_Server_message_form Says_imp_analz_Spy Says_imp_parts_knows_Spy) 219 220lemma unique_Na: "\<lbrakk>Says A B \<lbrace>Nonce M, Agent A, Agent B, Crypt (shrK A) \<lbrace>Nonce Na, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> \<in> set evs; 221 Says A B' \<lbrace>Nonce M', Agent A, Agent B', Crypt (shrK A) \<lbrace>Nonce Na, Nonce M', Agent A, Agent B'\<rbrace>\<rbrace> \<in> set evs; 222 A \<notin> bad; evs \<in> orb\<rbrakk> \<Longrightarrow> B=B' \<and> M=M'" 223by (erule rev_mp, erule rev_mp, erule orb.induct, simp_all, blast+) 224 225lemma unique_Nb: "\<lbrakk>Says B Server \<lbrace>Nonce M, Agent A, Agent B, X, Crypt (shrK B) \<lbrace>Nonce Nb, Nonce M, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> \<in> set evs; 226 Says B Server \<lbrace>Nonce M', Agent A', Agent B, X', Crypt (shrK B) \<lbrace>Nonce Nb,Nonce M', Nonce M', Agent A', Agent B\<rbrace>\<rbrace> \<in> set evs; 227 B \<notin> bad; evs \<in> orb\<rbrakk> \<Longrightarrow> M=M' \<and> A=A' \<and> X=X'" 228by (erule rev_mp, erule rev_mp, erule orb.induct, simp_all, blast+) 229 230lemma analz_image_freshCryptK_lemma: 231"(Crypt K X \<in> analz (Key`nE \<union> H)) \<longrightarrow> (Crypt K X \<in> analz H) \<Longrightarrow> 232 (Crypt K X \<in> analz (Key`nE \<union> H)) = (Crypt K X \<in> analz H)" 233by (blast intro: analz_mono [THEN [2] rev_subsetD]) 234 235ML 236\<open> 237structure OtwayReesBella = 238struct 239 240val analz_image_freshK_ss = 241 simpset_of 242 (\<^context> delsimps [image_insert, image_Un] 243 delsimps [@{thm imp_disjL}] (*reduces blow-up*) 244 addsimps @{thms analz_image_freshK_simps}) 245 246end 247\<close> 248 249method_setup analz_freshCryptK = \<open> 250 Scan.succeed (fn ctxt => 251 (SIMPLE_METHOD 252 (EVERY [REPEAT_FIRST (resolve_tac ctxt [allI, ballI, impI]), 253 REPEAT_FIRST (resolve_tac ctxt @{thms analz_image_freshCryptK_lemma}), 254 ALLGOALS (asm_simp_tac 255 (put_simpset OtwayReesBella.analz_image_freshK_ss ctxt))])))\<close> 256 "for proving useful rewrite rule" 257 258 259method_setup disentangle = \<open> 260 Scan.succeed 261 (fn ctxt => SIMPLE_METHOD 262 (REPEAT_FIRST (eresolve_tac ctxt [asm_rl, conjE, disjE] 263 ORELSE' hyp_subst_tac ctxt)))\<close> 264 "for eliminating conjunctions, disjunctions and the like" 265 266 267 268lemma analz_image_freshCryptK [rule_format]: 269"evs \<in> orb \<Longrightarrow> 270 Key K \<notin> analz (knows Spy evs) \<longrightarrow> 271 (\<forall> KK. KK \<subseteq> - (range shrK) \<longrightarrow> 272 (Crypt K X \<in> analz (Key`KK \<union> (knows Spy evs))) = 273 (Crypt K X \<in> analz (knows Spy evs)))" 274apply (erule orb.induct) 275apply (analz_mono_contra) 276apply (frule_tac [7] Gets_Server_message_form) 277apply (frule_tac [9] Says_Server_message_form) 278apply disentangle 279apply (drule_tac [5] Gets_imp_knows_Spy [THEN analz.Inj, THEN analz.Snd, THEN analz.Snd, THEN analz.Snd]) 280prefer 8 apply clarify 281apply (analz_freshCryptK, spy_analz, fastforce) 282done 283 284 285 286lemma analz_insert_freshCryptK: 287"\<lbrakk>evs \<in> orb; Key K \<notin> analz (knows Spy evs); 288 Seskey \<notin> range shrK\<rbrakk> \<Longrightarrow> 289 (Crypt K X \<in> analz (insert (Key Seskey) (knows Spy evs))) = 290 (Crypt K X \<in> analz (knows Spy evs))" 291by (simp only: analz_image_freshCryptK analz_image_freshK_simps) 292 293 294lemma analz_hard: 295"\<lbrakk>Says A B \<lbrace>Nonce M, Agent A, Agent B, 296 Crypt (shrK A) \<lbrace>Nonce Na, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> \<in>set evs; 297 Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace> \<in> analz (knows Spy evs); 298 A \<notin> bad; B \<notin> bad; evs \<in> orb\<rbrakk> 299 \<Longrightarrow> Says B A \<lbrace>Nonce M, Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>\<rbrace> \<in> set evs" 300apply (erule rev_mp) 301apply (erule rev_mp) 302apply (erule orb.induct) 303apply (frule_tac [7] Gets_Server_message_form) 304apply (frule_tac [9] Says_Server_message_form) 305apply disentangle 306txt\<open>letting the simplifier solve OR2\<close> 307apply (drule_tac [5] Gets_imp_knows_Spy [THEN analz.Inj, THEN analz.Snd, THEN analz.Snd, THEN analz.Snd]) 308apply (simp_all (no_asm_simp) add: analz_insert_eq pushes split_ifs) 309apply (spy_analz) 310txt\<open>OR1\<close> 311apply blast 312txt\<open>Oops\<close> 313prefer 4 apply (blast dest: analz_insert_freshCryptK) 314txt\<open>OR4 - ii\<close> 315prefer 3 apply (blast) 316txt\<open>OR3\<close> 317(*adding Gets_imp_ and Says_imp_ for efficiency*) 318apply (blast dest: 319 A_trusts_OR1 unique_Na Key_not_used analz_insert_freshCryptK) 320txt\<open>OR4 - i\<close> 321apply clarify 322apply (simp add: pushes split_ifs) 323apply (case_tac "Aaa\<in>bad") 324apply (blast dest: analz_insert_freshCryptK) 325apply clarify 326apply simp 327apply (case_tac "Ba\<in>bad") 328apply (frule Gets_imp_knows_Spy [THEN analz.Inj, THEN analz.Snd, THEN analz.Decrypt, THEN analz.Fst] , assumption) 329apply (simp (no_asm_simp)) 330apply clarify 331apply (frule Gets_imp_knows_Spy 332 [THEN parts.Inj, THEN parts.Snd, THEN B_trusts_OR3], 333 assumption, assumption, assumption, erule exE) 334apply (frule Says_Server_imp_Gets 335 [THEN Gets_imp_knows_Spy, THEN parts.Inj, THEN parts.Snd, 336 THEN parts.Snd, THEN parts.Snd, THEN parts.Fst, THEN A_trusts_OR1], 337 assumption, assumption, assumption, assumption) 338apply (blast dest: Says_Server_imp_Gets B_trusts_OR2 unique_Na unique_Nb) 339done 340 341 342lemma Gets_Server_message_form': 343"\<lbrakk>Gets B \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>X, Nonce Nb, Key K\<rbrace>\<rbrace> \<in> set evs; 344 B \<notin> bad; evs \<in> orb\<rbrakk> 345 \<Longrightarrow> K \<notin> range shrK \<and> (\<exists> A Na. X = (Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>))" 346by (blast dest!: B_trusts_OR3 Says_Server_message_form) 347 348 349lemma OR4_imp_Gets: 350"\<lbrakk>Says B A \<lbrace>Nonce M, Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>\<rbrace> \<in> set evs; 351 B \<notin> bad; evs \<in> orb\<rbrakk> 352 \<Longrightarrow> (\<exists> Nb. Gets B \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>, 353 Nonce Nb, Key K\<rbrace>\<rbrace> \<in> set evs)" 354apply (erule rev_mp, erule orb.induct, parts_explicit, simp_all) 355prefer 3 apply (blast dest: Gets_Server_message_form') 356apply blast+ 357done 358 359 360lemma A_keydist_to_B: 361"\<lbrakk>Says A B \<lbrace>Nonce M, Agent A, Agent B, 362 Crypt (shrK A) \<lbrace>Nonce Na, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> \<in>set evs; 363 Gets A \<lbrace>Nonce M, Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>\<rbrace> \<in> set evs; 364 A \<notin> bad; B \<notin> bad; evs \<in> orb\<rbrakk> 365 \<Longrightarrow> Key K \<in> analz (knows B evs)" 366apply (drule Gets_imp_knows_Spy [THEN analz.Inj, THEN analz.Snd], assumption) 367apply (drule analz_hard, assumption, assumption, assumption, assumption) 368apply (drule OR4_imp_Gets, assumption, assumption) 369apply (fastforce dest!: Gets_imp_knows [THEN analz.Inj] analz.Decrypt) 370done 371 372 373text\<open>Other properties as for the original protocol\<close> 374 375 376end 377