1(* Author: Lawrence C Paulson, Cambridge University Computer Laboratory 2 Copyright 1996 University of Cambridge 3 4Datatypes of agents and messages; 5Inductive relations "parts", "analz" and "synth" 6*)(*<*) 7 8section\<open>Theory of Agents and Messages for Security Protocols\<close> 9 10theory Message imports Main begin 11ML_file \<open>../../antiquote_setup.ML\<close> 12 13(*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*) 14lemma [simp] : "A \<union> (B \<union> A) = B \<union> A" 15by blast 16(*>*) 17 18section\<open>Agents and Messages\<close> 19 20text \<open> 21All protocol specifications refer to a syntactic theory of messages. 22Datatype 23\<open>agent\<close> introduces the constant \<open>Server\<close> (a trusted central 24machine, needed for some protocols), an infinite population of 25friendly agents, and the~\<open>Spy\<close>: 26\<close> 27 28datatype agent = Server | Friend nat | Spy 29 30text \<open> 31Keys are just natural numbers. Function \<open>invKey\<close> maps a public key to 32the matching private key, and vice versa: 33\<close> 34 35type_synonym key = nat 36consts invKey :: "key \<Rightarrow> key" 37(*<*) 38consts all_symmetric :: bool \<comment> \<open>true if all keys are symmetric\<close> 39 40specification (invKey) 41 invKey [simp]: "invKey (invKey K) = K" 42 invKey_symmetric: "all_symmetric \<longrightarrow> invKey = id" 43 by (rule exI [of _ id], auto) 44 45 46text\<open>The inverse of a symmetric key is itself; that of a public key 47 is the private key and vice versa\<close> 48 49definition symKeys :: "key set" where 50 "symKeys == {K. invKey K = K}" 51(*>*) 52 53text \<open> 54Datatype 55\<open>msg\<close> introduces the message forms, which include agent names, nonces, 56keys, compound messages, and encryptions. 57\<close> 58 59datatype 60 msg = Agent agent 61 | Nonce nat 62 | Key key 63 | MPair msg msg 64 | Crypt key msg 65 66text \<open> 67\noindent 68The notation $\comp{X\sb 1,\ldots X\sb{n-1},X\sb n}$ 69abbreviates 70$\isa{MPair}\,X\sb 1\,\ldots\allowbreak(\isa{MPair}\,X\sb{n-1}\,X\sb n)$. 71 72Since datatype constructors are injective, we have the theorem 73@{thm [display,indent=0] msg.inject(5) [THEN iffD1, of K X K' X']} 74A ciphertext can be decrypted using only one key and 75can yield only one plaintext. In the real world, decryption with the 76wrong key succeeds but yields garbage. Our model of encryption is 77realistic if encryption adds some redundancy to the plaintext, such as a 78checksum, so that garbage can be detected. 79\<close> 80 81(*<*) 82text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close> 83syntax 84 "_MTuple" :: "['a, args] \<Rightarrow> 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)") 85translations 86 "\<lbrace>x, y, z\<rbrace>" == "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>" 87 "\<lbrace>x, y\<rbrace>" == "CONST MPair x y" 88 89 90definition keysFor :: "msg set \<Rightarrow> key set" where 91 \<comment> \<open>Keys useful to decrypt elements of a message set\<close> 92 "keysFor H == invKey ` {K. \<exists>X. Crypt K X \<in> H}" 93 94 95subsubsection\<open>Inductive Definition of All Parts" of a Message\<close> 96 97inductive_set 98 parts :: "msg set \<Rightarrow> msg set" 99 for H :: "msg set" 100 where 101 Inj [intro]: "X \<in> H \<Longrightarrow> X \<in> parts H" 102 | Fst: "\<lbrace>X,Y\<rbrace> \<in> parts H \<Longrightarrow> X \<in> parts H" 103 | Snd: "\<lbrace>X,Y\<rbrace> \<in> parts H \<Longrightarrow> Y \<in> parts H" 104 | Body: "Crypt K X \<in> parts H \<Longrightarrow> X \<in> parts H" 105 106 107text\<open>Monotonicity\<close> 108lemma parts_mono: "G \<subseteq> H \<Longrightarrow> parts(G) \<subseteq> parts(H)" 109apply auto 110apply (erule parts.induct) 111apply (blast dest: parts.Fst parts.Snd parts.Body)+ 112done 113 114 115text\<open>Equations hold because constructors are injective.\<close> 116lemma Friend_image_eq [simp]: "(Friend x \<in> Friend`A) = (x\<in>A)" 117by auto 118 119lemma Key_image_eq [simp]: "(Key x \<in> Key`A) = (x\<in>A)" 120by auto 121 122lemma Nonce_Key_image_eq [simp]: "(Nonce x \<notin> Key`A)" 123by auto 124 125 126subsubsection\<open>Inverse of keys\<close> 127 128lemma invKey_eq [simp]: "(invKey K = invKey K') = (K=K')" 129apply safe 130apply (drule_tac f = invKey in arg_cong, simp) 131done 132 133 134subsection\<open>keysFor operator\<close> 135 136lemma keysFor_empty [simp]: "keysFor {} = {}" 137by (unfold keysFor_def, blast) 138 139lemma keysFor_Un [simp]: "keysFor (H \<union> H') = keysFor H \<union> keysFor H'" 140by (unfold keysFor_def, blast) 141 142lemma keysFor_UN [simp]: "keysFor (\<Union>i\<in>A. H i) = (\<Union>i\<in>A. keysFor (H i))" 143by (unfold keysFor_def, blast) 144 145text\<open>Monotonicity\<close> 146lemma keysFor_mono: "G \<subseteq> H \<Longrightarrow> keysFor(G) \<subseteq> keysFor(H)" 147by (unfold keysFor_def, blast) 148 149lemma keysFor_insert_Agent [simp]: "keysFor (insert (Agent A) H) = keysFor H" 150by (unfold keysFor_def, auto) 151 152lemma keysFor_insert_Nonce [simp]: "keysFor (insert (Nonce N) H) = keysFor H" 153by (unfold keysFor_def, auto) 154 155lemma keysFor_insert_Key [simp]: "keysFor (insert (Key K) H) = keysFor H" 156by (unfold keysFor_def, auto) 157 158lemma keysFor_insert_MPair [simp]: "keysFor (insert \<lbrace>X,Y\<rbrace> H) = keysFor H" 159by (unfold keysFor_def, auto) 160 161lemma keysFor_insert_Crypt [simp]: 162 "keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)" 163by (unfold keysFor_def, auto) 164 165lemma keysFor_image_Key [simp]: "keysFor (Key`E) = {}" 166by (unfold keysFor_def, auto) 167 168lemma Crypt_imp_invKey_keysFor: "Crypt K X \<in> H \<Longrightarrow> invKey K \<in> keysFor H" 169by (unfold keysFor_def, blast) 170 171 172subsection\<open>Inductive relation "parts"\<close> 173 174lemma MPair_parts: 175 "[| \<lbrace>X,Y\<rbrace> \<in> parts H; 176 [| X \<in> parts H; Y \<in> parts H |] ==> P |] ==> P" 177by (blast dest: parts.Fst parts.Snd) 178 179declare MPair_parts [elim!] parts.Body [dest!] 180text\<open>NB These two rules are UNSAFE in the formal sense, as they discard the 181 compound message. They work well on THIS FILE. 182 \<open>MPair_parts\<close> is left as SAFE because it speeds up proofs. 183 The Crypt rule is normally kept UNSAFE to avoid breaking up certificates.\<close> 184 185lemma parts_increasing: "H \<subseteq> parts(H)" 186by blast 187 188lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD] 189 190lemma parts_empty [simp]: "parts{} = {}" 191apply safe 192apply (erule parts.induct, blast+) 193done 194 195lemma parts_emptyE [elim!]: "X\<in> parts{} \<Longrightarrow> P" 196by simp 197 198text\<open>WARNING: loops if H = {Y}, therefore must not be repeated!\<close> 199lemma parts_singleton: "X\<in> parts H \<Longrightarrow> \<exists>Y\<in>H. X\<in> parts {Y}" 200by (erule parts.induct, fast+) 201 202 203subsubsection\<open>Unions\<close> 204 205lemma parts_Un_subset1: "parts(G) \<union> parts(H) \<subseteq> parts(G \<union> H)" 206by (intro Un_least parts_mono Un_upper1 Un_upper2) 207 208lemma parts_Un_subset2: "parts(G \<union> H) \<subseteq> parts(G) \<union> parts(H)" 209apply (rule subsetI) 210apply (erule parts.induct, blast+) 211done 212 213lemma parts_Un [simp]: "parts(G \<union> H) = parts(G) \<union> parts(H)" 214by (intro equalityI parts_Un_subset1 parts_Un_subset2) 215 216lemma parts_insert: "parts (insert X H) = parts {X} \<union> parts H" 217apply (subst insert_is_Un [of _ H]) 218apply (simp only: parts_Un) 219done 220 221text\<open>TWO inserts to avoid looping. This rewrite is better than nothing. 222 Not suitable for Addsimps: its behaviour can be strange.\<close> 223lemma parts_insert2: 224 "parts (insert X (insert Y H)) = parts {X} \<union> parts {Y} \<union> parts H" 225apply (simp add: Un_assoc) 226apply (simp add: parts_insert [symmetric]) 227done 228 229lemma parts_UN_subset1: "(\<Union>x\<in>A. parts(H x)) \<subseteq> parts(\<Union>x\<in>A. H x)" 230by (intro UN_least parts_mono UN_upper) 231 232lemma parts_UN_subset2: "parts(\<Union>x\<in>A. H x) \<subseteq> (\<Union>x\<in>A. parts(H x))" 233apply (rule subsetI) 234apply (erule parts.induct, blast+) 235done 236 237lemma parts_UN [simp]: "parts(\<Union>x\<in>A. H x) = (\<Union>x\<in>A. parts(H x))" 238by (intro equalityI parts_UN_subset1 parts_UN_subset2) 239 240text\<open>Added to simplify arguments to parts, analz and synth. 241 NOTE: the UN versions are no longer used!\<close> 242 243 244text\<open>This allows \<open>blast\<close> to simplify occurrences of 245 \<^term>\<open>parts(G\<union>H)\<close> in the assumption.\<close> 246lemmas in_parts_UnE = parts_Un [THEN equalityD1, THEN subsetD, THEN UnE] 247declare in_parts_UnE [elim!] 248 249 250lemma parts_insert_subset: "insert X (parts H) \<subseteq> parts(insert X H)" 251by (blast intro: parts_mono [THEN [2] rev_subsetD]) 252 253subsubsection\<open>Idempotence and transitivity\<close> 254 255lemma parts_partsD [dest!]: "X \<in> parts (parts H) \<Longrightarrow> X\<in> parts H" 256by (erule parts.induct, blast+) 257 258lemma parts_idem [simp]: "parts (parts H) = parts H" 259by blast 260 261lemma parts_subset_iff [simp]: "(parts G \<subseteq> parts H) = (G \<subseteq> parts H)" 262apply (rule iffI) 263apply (iprover intro: subset_trans parts_increasing) 264apply (frule parts_mono, simp) 265done 266 267lemma parts_trans: "[| X\<in> parts G; G \<subseteq> parts H |] ==> X\<in> parts H" 268by (drule parts_mono, blast) 269 270text\<open>Cut\<close> 271lemma parts_cut: 272 "[| Y\<in> parts (insert X G); X\<in> parts H |] ==> Y\<in> parts (G \<union> H)" 273by (blast intro: parts_trans) 274 275 276lemma parts_cut_eq [simp]: "X\<in> parts H ==> parts (insert X H) = parts H" 277by (force dest!: parts_cut intro: parts_insertI) 278 279 280subsubsection\<open>Rewrite rules for pulling out atomic messages\<close> 281 282lemmas parts_insert_eq_I = equalityI [OF subsetI parts_insert_subset] 283 284 285lemma parts_insert_Agent [simp]: 286 "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)" 287apply (rule parts_insert_eq_I) 288apply (erule parts.induct, auto) 289done 290 291lemma parts_insert_Nonce [simp]: 292 "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)" 293apply (rule parts_insert_eq_I) 294apply (erule parts.induct, auto) 295done 296 297lemma parts_insert_Key [simp]: 298 "parts (insert (Key K) H) = insert (Key K) (parts H)" 299apply (rule parts_insert_eq_I) 300apply (erule parts.induct, auto) 301done 302 303lemma parts_insert_Crypt [simp]: 304 "parts (insert (Crypt K X) H) = insert (Crypt K X) (parts (insert X H))" 305apply (rule equalityI) 306apply (rule subsetI) 307apply (erule parts.induct, auto) 308apply (blast intro: parts.Body) 309done 310 311lemma parts_insert_MPair [simp]: 312 "parts (insert \<lbrace>X,Y\<rbrace> H) = 313 insert \<lbrace>X,Y\<rbrace> (parts (insert X (insert Y H)))" 314apply (rule equalityI) 315apply (rule subsetI) 316apply (erule parts.induct, auto) 317apply (blast intro: parts.Fst parts.Snd)+ 318done 319 320lemma parts_image_Key [simp]: "parts (Key`N) = Key`N" 321apply auto 322apply (erule parts.induct, auto) 323done 324 325 326text\<open>In any message, there is an upper bound N on its greatest nonce.\<close> 327lemma msg_Nonce_supply: "\<exists>N. \<forall>n. N\<le>n \<longrightarrow> Nonce n \<notin> parts {msg}" 328apply (induct_tac "msg") 329apply (simp_all (no_asm_simp) add: exI parts_insert2) 330 txt\<open>MPair case: blast works out the necessary sum itself!\<close> 331 prefer 2 apply auto apply (blast elim!: add_leE) 332txt\<open>Nonce case\<close> 333apply (rename_tac nat) 334apply (rule_tac x = "N + Suc nat" in exI, auto) 335done 336(*>*) 337 338section\<open>Modelling the Adversary\<close> 339 340text \<open> 341The spy is part of the system and must be built into the model. He is 342a malicious user who does not have to follow the protocol. He 343watches the network and uses any keys he knows to decrypt messages. 344Thus he accumulates additional keys and nonces. These he can use to 345compose new messages, which he may send to anybody. 346 347Two functions enable us to formalize this behaviour: \<open>analz\<close> and 348\<open>synth\<close>. Each function maps a sets of messages to another set of 349messages. The set \<open>analz H\<close> formalizes what the adversary can learn 350from the set of messages~$H$. The closure properties of this set are 351defined inductively. 352\<close> 353 354inductive_set 355 analz :: "msg set \<Rightarrow> msg set" 356 for H :: "msg set" 357 where 358 Inj [intro,simp] : "X \<in> H \<Longrightarrow> X \<in> analz H" 359 | Fst: "\<lbrace>X,Y\<rbrace> \<in> analz H \<Longrightarrow> X \<in> analz H" 360 | Snd: "\<lbrace>X,Y\<rbrace> \<in> analz H \<Longrightarrow> Y \<in> analz H" 361 | Decrypt [dest]: 362 "\<lbrakk>Crypt K X \<in> analz H; Key(invKey K) \<in> analz H\<rbrakk> 363 \<Longrightarrow> X \<in> analz H" 364(*<*) 365text\<open>Monotonicity; Lemma 1 of Lowe's paper\<close> 366lemma analz_mono: "G\<subseteq>H \<Longrightarrow> analz(G) \<subseteq> analz(H)" 367apply auto 368apply (erule analz.induct) 369apply (auto dest: analz.Fst analz.Snd) 370done 371 372text\<open>Making it safe speeds up proofs\<close> 373lemma MPair_analz [elim!]: 374 "[| \<lbrace>X,Y\<rbrace> \<in> analz H; 375 [| X \<in> analz H; Y \<in> analz H |] ==> P 376 |] ==> P" 377by (blast dest: analz.Fst analz.Snd) 378 379lemma analz_increasing: "H \<subseteq> analz(H)" 380by blast 381 382lemma analz_subset_parts: "analz H \<subseteq> parts H" 383apply (rule subsetI) 384apply (erule analz.induct, blast+) 385done 386 387lemmas analz_into_parts = analz_subset_parts [THEN subsetD] 388 389lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD] 390 391 392lemma parts_analz [simp]: "parts (analz H) = parts H" 393apply (rule equalityI) 394apply (rule analz_subset_parts [THEN parts_mono, THEN subset_trans], simp) 395apply (blast intro: analz_increasing [THEN parts_mono, THEN subsetD]) 396done 397 398lemma analz_parts [simp]: "analz (parts H) = parts H" 399apply auto 400apply (erule analz.induct, auto) 401done 402 403lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD] 404 405subsubsection\<open>General equational properties\<close> 406 407lemma analz_empty [simp]: "analz{} = {}" 408apply safe 409apply (erule analz.induct, blast+) 410done 411 412text\<open>Converse fails: we can analz more from the union than from the 413 separate parts, as a key in one might decrypt a message in the other\<close> 414lemma analz_Un: "analz(G) \<union> analz(H) \<subseteq> analz(G \<union> H)" 415by (intro Un_least analz_mono Un_upper1 Un_upper2) 416 417lemma analz_insert: "insert X (analz H) \<subseteq> analz(insert X H)" 418by (blast intro: analz_mono [THEN [2] rev_subsetD]) 419 420subsubsection\<open>Rewrite rules for pulling out atomic messages\<close> 421 422lemmas analz_insert_eq_I = equalityI [OF subsetI analz_insert] 423 424lemma analz_insert_Agent [simp]: 425 "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)" 426apply (rule analz_insert_eq_I) 427apply (erule analz.induct, auto) 428done 429 430lemma analz_insert_Nonce [simp]: 431 "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)" 432apply (rule analz_insert_eq_I) 433apply (erule analz.induct, auto) 434done 435 436text\<open>Can only pull out Keys if they are not needed to decrypt the rest\<close> 437lemma analz_insert_Key [simp]: 438 "K \<notin> keysFor (analz H) \<Longrightarrow> 439 analz (insert (Key K) H) = insert (Key K) (analz H)" 440apply (unfold keysFor_def) 441apply (rule analz_insert_eq_I) 442apply (erule analz.induct, auto) 443done 444 445lemma analz_insert_MPair [simp]: 446 "analz (insert \<lbrace>X,Y\<rbrace> H) = 447 insert \<lbrace>X,Y\<rbrace> (analz (insert X (insert Y H)))" 448apply (rule equalityI) 449apply (rule subsetI) 450apply (erule analz.induct, auto) 451apply (erule analz.induct) 452apply (blast intro: analz.Fst analz.Snd)+ 453done 454 455text\<open>Can pull out enCrypted message if the Key is not known\<close> 456lemma analz_insert_Crypt: 457 "Key (invKey K) \<notin> analz H 458 \<Longrightarrow> analz (insert (Crypt K X) H) = insert (Crypt K X) (analz H)" 459apply (rule analz_insert_eq_I) 460apply (erule analz.induct, auto) 461 462done 463 464lemma lemma1: "Key (invKey K) \<in> analz H \<Longrightarrow> 465 analz (insert (Crypt K X) H) \<subseteq> 466 insert (Crypt K X) (analz (insert X H))" 467apply (rule subsetI) 468apply (erule_tac x = x in analz.induct, auto) 469done 470 471lemma lemma2: "Key (invKey K) \<in> analz H \<Longrightarrow> 472 insert (Crypt K X) (analz (insert X H)) \<subseteq> 473 analz (insert (Crypt K X) H)" 474apply auto 475apply (erule_tac x = x in analz.induct, auto) 476apply (blast intro: analz_insertI analz.Decrypt) 477done 478 479lemma analz_insert_Decrypt: 480 "Key (invKey K) \<in> analz H \<Longrightarrow> 481 analz (insert (Crypt K X) H) = 482 insert (Crypt K X) (analz (insert X H))" 483by (intro equalityI lemma1 lemma2) 484 485text\<open>Case analysis: either the message is secure, or it is not! Effective, 486but can cause subgoals to blow up! Use with \<open>if_split\<close>; apparently 487\<open>split_tac\<close> does not cope with patterns such as \<^term>\<open>analz (insert 488(Crypt K X) H)\<close>\<close> 489lemma analz_Crypt_if [simp]: 490 "analz (insert (Crypt K X) H) = 491 (if (Key (invKey K) \<in> analz H) 492 then insert (Crypt K X) (analz (insert X H)) 493 else insert (Crypt K X) (analz H))" 494by (simp add: analz_insert_Crypt analz_insert_Decrypt) 495 496 497text\<open>This rule supposes "for the sake of argument" that we have the key.\<close> 498lemma analz_insert_Crypt_subset: 499 "analz (insert (Crypt K X) H) \<subseteq> 500 insert (Crypt K X) (analz (insert X H))" 501apply (rule subsetI) 502apply (erule analz.induct, auto) 503done 504 505 506lemma analz_image_Key [simp]: "analz (Key`N) = Key`N" 507apply auto 508apply (erule analz.induct, auto) 509done 510 511 512subsubsection\<open>Idempotence and transitivity\<close> 513 514lemma analz_analzD [dest!]: "X\<in> analz (analz H) \<Longrightarrow> X\<in> analz H" 515by (erule analz.induct, blast+) 516 517lemma analz_idem [simp]: "analz (analz H) = analz H" 518by blast 519 520lemma analz_subset_iff [simp]: "(analz G \<subseteq> analz H) = (G \<subseteq> analz H)" 521apply (rule iffI) 522apply (iprover intro: subset_trans analz_increasing) 523apply (frule analz_mono, simp) 524done 525 526lemma analz_trans: "[| X\<in> analz G; G \<subseteq> analz H |] ==> X\<in> analz H" 527by (drule analz_mono, blast) 528 529text\<open>Cut; Lemma 2 of Lowe\<close> 530lemma analz_cut: "[| Y\<in> analz (insert X H); X\<in> analz H |] ==> Y\<in> analz H" 531by (erule analz_trans, blast) 532 533(*Cut can be proved easily by induction on 534 "Y \<in> analz (insert X H) \<Longrightarrow> X \<in> analz H \<longrightarrow> Y \<in> analz H" 535*) 536 537text\<open>This rewrite rule helps in the simplification of messages that involve 538 the forwarding of unknown components (X). Without it, removing occurrences 539 of X can be very complicated.\<close> 540lemma analz_insert_eq: "X\<in> analz H \<Longrightarrow> analz (insert X H) = analz H" 541by (blast intro: analz_cut analz_insertI) 542 543 544text\<open>A congruence rule for "analz"\<close> 545 546lemma analz_subset_cong: 547 "[| analz G \<subseteq> analz G'; analz H \<subseteq> analz H' |] 548 ==> analz (G \<union> H) \<subseteq> analz (G' \<union> H')" 549apply simp 550apply (iprover intro: conjI subset_trans analz_mono Un_upper1 Un_upper2) 551done 552 553lemma analz_cong: 554 "[| analz G = analz G'; analz H = analz H' |] 555 ==> analz (G \<union> H) = analz (G' \<union> H')" 556by (intro equalityI analz_subset_cong, simp_all) 557 558lemma analz_insert_cong: 559 "analz H = analz H' \<Longrightarrow> analz(insert X H) = analz(insert X H')" 560by (force simp only: insert_def intro!: analz_cong) 561 562text\<open>If there are no pairs or encryptions then analz does nothing\<close> 563lemma analz_trivial: 564 "[| \<forall>X Y. \<lbrace>X,Y\<rbrace> \<notin> H; \<forall>X K. Crypt K X \<notin> H |] ==> analz H = H" 565apply safe 566apply (erule analz.induct, blast+) 567done 568 569text\<open>These two are obsolete (with a single Spy) but cost little to prove...\<close> 570lemma analz_UN_analz_lemma: 571 "X\<in> analz (\<Union>i\<in>A. analz (H i)) \<Longrightarrow> X\<in> analz (\<Union>i\<in>A. H i)" 572apply (erule analz.induct) 573apply (blast intro: analz_mono [THEN [2] rev_subsetD])+ 574done 575 576lemma analz_UN_analz [simp]: "analz (\<Union>i\<in>A. analz (H i)) = analz (\<Union>i\<in>A. H i)" 577by (blast intro: analz_UN_analz_lemma analz_mono [THEN [2] rev_subsetD]) 578(*>*) 579text \<open> 580Note the \<open>Decrypt\<close> rule: the spy can decrypt a 581message encrypted with key~$K$ if he has the matching key,~$K^{-1}$. 582Properties proved by rule induction include the following: 583@{named_thms [display,indent=0] analz_mono [no_vars] (analz_mono) analz_idem [no_vars] (analz_idem)} 584 585The set of fake messages that an intruder could invent 586starting from~\<open>H\<close> is \<open>synth(analz H)\<close>, where \<open>synth H\<close> 587formalizes what the adversary can build from the set of messages~$H$. 588\<close> 589 590inductive_set 591 synth :: "msg set \<Rightarrow> msg set" 592 for H :: "msg set" 593 where 594 Inj [intro]: "X \<in> H \<Longrightarrow> X \<in> synth H" 595 | Agent [intro]: "Agent agt \<in> synth H" 596 | MPair [intro]: 597 "\<lbrakk>X \<in> synth H; Y \<in> synth H\<rbrakk> \<Longrightarrow> \<lbrace>X,Y\<rbrace> \<in> synth H" 598 | Crypt [intro]: 599 "\<lbrakk>X \<in> synth H; Key K \<in> H\<rbrakk> \<Longrightarrow> Crypt K X \<in> synth H" 600(*<*) 601lemma synth_mono: "G\<subseteq>H \<Longrightarrow> synth(G) \<subseteq> synth(H)" 602 by (auto, erule synth.induct, auto) 603 604inductive_cases Key_synth [elim!]: "Key K \<in> synth H" 605inductive_cases MPair_synth [elim!]: "\<lbrace>X,Y\<rbrace> \<in> synth H" 606inductive_cases Crypt_synth [elim!]: "Crypt K X \<in> synth H" 607 608lemma analz_synth_Un [simp]: "analz (synth G \<union> H) = analz (G \<union> H) \<union> synth G" 609apply (rule equalityI) 610apply (rule subsetI) 611apply (erule analz.induct) 612prefer 5 apply (blast intro: analz_mono [THEN [2] rev_subsetD]) 613apply (blast intro: analz.Fst analz.Snd analz.Decrypt)+ 614done 615 616lemma analz_synth [simp]: "analz (synth H) = analz H \<union> synth H" 617apply (cut_tac H = "{}" in analz_synth_Un) 618apply (simp (no_asm_use)) 619done 620(*>*) 621text \<open> 622The set includes all agent names. Nonces and keys are assumed to be 623unguessable, so none are included beyond those already in~$H$. Two 624elements of \<^term>\<open>synth H\<close> can be combined, and an element can be encrypted 625using a key present in~$H$. 626 627Like \<open>analz\<close>, this set operator is monotone and idempotent. It also 628satisfies an interesting equation involving \<open>analz\<close>: 629@{named_thms [display,indent=0] analz_synth [no_vars] (analz_synth)} 630Rule inversion plays a major role in reasoning about \<open>synth\<close>, through 631declarations such as this one: 632\<close> 633 634inductive_cases Nonce_synth [elim!]: "Nonce n \<in> synth H" 635 636text \<open> 637\noindent 638The resulting elimination rule replaces every assumption of the form 639\<^term>\<open>Nonce n \<in> synth H\<close> by \<^term>\<open>Nonce n \<in> H\<close>, 640expressing that a nonce cannot be guessed. 641 642A third operator, \<open>parts\<close>, is useful for stating correctness 643properties. The set 644\<^term>\<open>parts H\<close> consists of the components of elements of~$H$. This set 645includes~\<open>H\<close> and is closed under the projections from a compound 646message to its immediate parts. 647Its definition resembles that of \<open>analz\<close> except in the rule 648corresponding to the constructor \<open>Crypt\<close>: 649@{thm [display,indent=5] parts.Body [no_vars]} 650The body of an encrypted message is always regarded as part of it. We can 651use \<open>parts\<close> to express general well-formedness properties of a protocol, 652for example, that an uncompromised agent's private key will never be 653included as a component of any message. 654\<close> 655(*<*) 656lemma synth_increasing: "H \<subseteq> synth(H)" 657by blast 658 659subsubsection\<open>Unions\<close> 660 661text\<open>Converse fails: we can synth more from the union than from the 662 separate parts, building a compound message using elements of each.\<close> 663lemma synth_Un: "synth(G) \<union> synth(H) \<subseteq> synth(G \<union> H)" 664by (intro Un_least synth_mono Un_upper1 Un_upper2) 665 666lemma synth_insert: "insert X (synth H) \<subseteq> synth(insert X H)" 667by (blast intro: synth_mono [THEN [2] rev_subsetD]) 668 669subsubsection\<open>Idempotence and transitivity\<close> 670 671lemma synth_synthD [dest!]: "X\<in> synth (synth H) \<Longrightarrow> X\<in> synth H" 672by (erule synth.induct, blast+) 673 674lemma synth_idem: "synth (synth H) = synth H" 675by blast 676 677lemma synth_subset_iff [simp]: "(synth G \<subseteq> synth H) = (G \<subseteq> synth H)" 678apply (rule iffI) 679apply (iprover intro: subset_trans synth_increasing) 680apply (frule synth_mono, simp add: synth_idem) 681done 682 683lemma synth_trans: "[| X\<in> synth G; G \<subseteq> synth H |] ==> X\<in> synth H" 684by (drule synth_mono, blast) 685 686text\<open>Cut; Lemma 2 of Lowe\<close> 687lemma synth_cut: "[| Y\<in> synth (insert X H); X\<in> synth H |] ==> Y\<in> synth H" 688by (erule synth_trans, blast) 689 690lemma Agent_synth [simp]: "Agent A \<in> synth H" 691by blast 692 693lemma Nonce_synth_eq [simp]: "(Nonce N \<in> synth H) = (Nonce N \<in> H)" 694by blast 695 696lemma Key_synth_eq [simp]: "(Key K \<in> synth H) = (Key K \<in> H)" 697by blast 698 699lemma Crypt_synth_eq [simp]: 700 "Key K \<notin> H \<Longrightarrow> (Crypt K X \<in> synth H) = (Crypt K X \<in> H)" 701by blast 702 703 704lemma keysFor_synth [simp]: 705 "keysFor (synth H) = keysFor H \<union> invKey`{K. Key K \<in> H}" 706by (unfold keysFor_def, blast) 707 708 709subsubsection\<open>Combinations of parts, analz and synth\<close> 710 711lemma parts_synth [simp]: "parts (synth H) = parts H \<union> synth H" 712apply (rule equalityI) 713apply (rule subsetI) 714apply (erule parts.induct) 715apply (blast intro: synth_increasing [THEN parts_mono, THEN subsetD] 716 parts.Fst parts.Snd parts.Body)+ 717done 718 719lemma analz_analz_Un [simp]: "analz (analz G \<union> H) = analz (G \<union> H)" 720apply (intro equalityI analz_subset_cong)+ 721apply simp_all 722done 723 724 725subsubsection\<open>For reasoning about the Fake rule in traces\<close> 726 727lemma parts_insert_subset_Un: "X \<in> G \<Longrightarrow> parts(insert X H) \<subseteq> parts G \<union> parts H" 728by (rule subset_trans [OF parts_mono parts_Un_subset2], blast) 729 730text\<open>More specifically for Fake. Very occasionally we could do with a version 731 of the form \<^term>\<open>parts{X} \<subseteq> synth (analz H) \<union> parts H\<close>\<close> 732lemma Fake_parts_insert: 733 "X \<in> synth (analz H) \<Longrightarrow> 734 parts (insert X H) \<subseteq> synth (analz H) \<union> parts H" 735apply (drule parts_insert_subset_Un) 736apply (simp (no_asm_use)) 737apply blast 738done 739 740lemma Fake_parts_insert_in_Un: 741 "[|Z \<in> parts (insert X H); X \<in> synth (analz H)|] 742 ==> Z \<in> synth (analz H) \<union> parts H" 743by (blast dest: Fake_parts_insert [THEN subsetD, dest]) 744 745text\<open>\<^term>\<open>H\<close> is sometimes \<^term>\<open>Key ` KK \<union> spies evs\<close>, so can't put 746 \<^term>\<open>G=H\<close>.\<close> 747lemma Fake_analz_insert: 748 "X \<in> synth (analz G) \<Longrightarrow> 749 analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)" 750apply (rule subsetI) 751apply (subgoal_tac "x \<in> analz (synth (analz G) \<union> H) ") 752prefer 2 apply (blast intro: analz_mono [THEN [2] rev_subsetD] analz_mono [THEN synth_mono, THEN [2] rev_subsetD]) 753apply (simp (no_asm_use)) 754apply blast 755done 756 757lemma analz_conj_parts [simp]: 758 "(X \<in> analz H & X \<in> parts H) = (X \<in> analz H)" 759by (blast intro: analz_subset_parts [THEN subsetD]) 760 761lemma analz_disj_parts [simp]: 762 "(X \<in> analz H | X \<in> parts H) = (X \<in> parts H)" 763by (blast intro: analz_subset_parts [THEN subsetD]) 764 765text\<open>Without this equation, other rules for synth and analz would yield 766 redundant cases\<close> 767lemma MPair_synth_analz [iff]: 768 "(\<lbrace>X,Y\<rbrace> \<in> synth (analz H)) = 769 (X \<in> synth (analz H) & Y \<in> synth (analz H))" 770by blast 771 772lemma Crypt_synth_analz: 773 "[| Key K \<in> analz H; Key (invKey K) \<in> analz H |] 774 ==> (Crypt K X \<in> synth (analz H)) = (X \<in> synth (analz H))" 775by blast 776 777 778text\<open>We do NOT want Crypt... messages broken up in protocols!!\<close> 779declare parts.Body [rule del] 780 781 782text\<open>Rewrites to push in Key and Crypt messages, so that other messages can 783 be pulled out using the \<open>analz_insert\<close> rules\<close> 784 785lemmas pushKeys = 786 insert_commute [of "Key K" "Agent C"] 787 insert_commute [of "Key K" "Nonce N"] 788 insert_commute [of "Key K" "MPair X Y"] 789 insert_commute [of "Key K" "Crypt X K'"] 790 for K C N X Y K' 791 792lemmas pushCrypts = 793 insert_commute [of "Crypt X K" "Agent C"] 794 insert_commute [of "Crypt X K" "Agent C"] 795 insert_commute [of "Crypt X K" "Nonce N"] 796 insert_commute [of "Crypt X K" "MPair X' Y"] 797 for X K C N X' Y 798 799text\<open>Cannot be added with \<open>[simp]\<close> -- messages should not always be 800 re-ordered.\<close> 801lemmas pushes = pushKeys pushCrypts 802 803 804subsection\<open>Tactics useful for many protocol proofs\<close> 805ML 806\<open> 807val invKey = @{thm invKey}; 808val keysFor_def = @{thm keysFor_def}; 809val symKeys_def = @{thm symKeys_def}; 810val parts_mono = @{thm parts_mono}; 811val analz_mono = @{thm analz_mono}; 812val synth_mono = @{thm synth_mono}; 813val analz_increasing = @{thm analz_increasing}; 814 815val analz_insertI = @{thm analz_insertI}; 816val analz_subset_parts = @{thm analz_subset_parts}; 817val Fake_parts_insert = @{thm Fake_parts_insert}; 818val Fake_analz_insert = @{thm Fake_analz_insert}; 819val pushes = @{thms pushes}; 820 821 822(*Analysis of Fake cases. Also works for messages that forward unknown parts, 823 but this application is no longer necessary if analz_insert_eq is used. 824 Abstraction over i is ESSENTIAL: it delays the dereferencing of claset 825 DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *) 826 827(*Apply rules to break down assumptions of the form 828 Y \<in> parts(insert X H) and Y \<in> analz(insert X H) 829*) 830fun impOfSubs th = th RSN (2, @{thm rev_subsetD}) 831 832fun Fake_insert_tac ctxt = 833 dresolve_tac ctxt [impOfSubs Fake_analz_insert, 834 impOfSubs Fake_parts_insert] THEN' 835 eresolve_tac ctxt [asm_rl, @{thm synth.Inj}]; 836 837fun Fake_insert_simp_tac ctxt i = 838 REPEAT (Fake_insert_tac ctxt i) THEN asm_full_simp_tac ctxt i; 839 840fun atomic_spy_analz_tac ctxt = 841 SELECT_GOAL 842 (Fake_insert_simp_tac ctxt 1 THEN 843 IF_UNSOLVED (Blast.depth_tac (ctxt addIs [analz_insertI, impOfSubs analz_subset_parts]) 4 1)); 844 845fun spy_analz_tac ctxt i = 846 DETERM 847 (SELECT_GOAL 848 (EVERY 849 [ (*push in occurrences of X...*) 850 (REPEAT o CHANGED) 851 (Rule_Insts.res_inst_tac ctxt [((("x", 1), Position.none), "X")] [] 852 (insert_commute RS ssubst) 1), 853 (*...allowing further simplifications*) 854 simp_tac ctxt 1, 855 REPEAT (FIRSTGOAL (resolve_tac ctxt [allI,impI,notI,conjI,iffI])), 856 DEPTH_SOLVE (atomic_spy_analz_tac ctxt 1)]) i); 857\<close> 858 859text\<open>By default only \<open>o_apply\<close> is built-in. But in the presence of 860eta-expansion this means that some terms displayed as \<^term>\<open>f o g\<close> will be 861rewritten, and others will not!\<close> 862declare o_def [simp] 863 864 865lemma Crypt_notin_image_Key [simp]: "Crypt K X \<notin> Key ` A" 866by auto 867 868lemma synth_analz_mono: "G\<subseteq>H \<Longrightarrow> synth (analz(G)) \<subseteq> synth (analz(H))" 869by (iprover intro: synth_mono analz_mono) 870 871lemma Fake_analz_eq [simp]: 872 "X \<in> synth(analz H) \<Longrightarrow> synth (analz (insert X H)) = synth (analz H)" 873apply (drule Fake_analz_insert[of _ _ "H"]) 874apply (simp add: synth_increasing[THEN Un_absorb2]) 875apply (drule synth_mono) 876apply (simp add: synth_idem) 877apply (rule equalityI) 878apply (simp add: ) 879apply (rule synth_analz_mono, blast) 880done 881 882text\<open>Two generalizations of \<open>analz_insert_eq\<close>\<close> 883lemma gen_analz_insert_eq [rule_format]: 884 "X \<in> analz H \<Longrightarrow> \<forall>G. H \<subseteq> G \<longrightarrow> analz (insert X G) = analz G" 885by (blast intro: analz_cut analz_insertI analz_mono [THEN [2] rev_subsetD]) 886 887lemma synth_analz_insert_eq [rule_format]: 888 "X \<in> synth (analz H) 889 \<Longrightarrow> \<forall>G. H \<subseteq> G \<longrightarrow> (Key K \<in> analz (insert X G)) = (Key K \<in> analz G)" 890apply (erule synth.induct) 891apply (simp_all add: gen_analz_insert_eq subset_trans [OF _ subset_insertI]) 892done 893 894lemma Fake_parts_sing: 895 "X \<in> synth (analz H) \<Longrightarrow> parts{X} \<subseteq> synth (analz H) \<union> parts H" 896apply (rule subset_trans) 897 apply (erule_tac [2] Fake_parts_insert) 898apply (rule parts_mono, blast) 899done 900 901lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD] 902 903method_setup spy_analz = \<open> 904 Scan.succeed (SIMPLE_METHOD' o spy_analz_tac)\<close> 905 "for proving the Fake case when analz is involved" 906 907method_setup atomic_spy_analz = \<open> 908 Scan.succeed (SIMPLE_METHOD' o atomic_spy_analz_tac)\<close> 909 "for debugging spy_analz" 910 911method_setup Fake_insert_simp = \<open> 912 Scan.succeed (SIMPLE_METHOD' o Fake_insert_simp_tac)\<close> 913 "for debugging spy_analz" 914 915 916end 917(*>*) 918