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