1(* Title: HOL/Auth/Public.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1996 University of Cambridge 4 5Theory of Public Keys (common to all public-key protocols) 6 7Private and public keys; initial states of agents 8*) 9 10theory Public 11imports Event 12begin 13 14lemma invKey_K: "K \<in> symKeys ==> invKey K = K" 15by (simp add: symKeys_def) 16 17subsection\<open>Asymmetric Keys\<close> 18 19datatype keymode = Signature | Encryption 20 21consts 22 publicKey :: "[keymode,agent] \<Rightarrow> key" 23 24abbreviation 25 pubEK :: "agent \<Rightarrow> key" where 26 "pubEK == publicKey Encryption" 27 28abbreviation 29 pubSK :: "agent \<Rightarrow> key" where 30 "pubSK == publicKey Signature" 31 32abbreviation 33 privateKey :: "[keymode, agent] \<Rightarrow> key" where 34 "privateKey b A == invKey (publicKey b A)" 35 36abbreviation 37 (*BEWARE!! priEK, priSK DON'T WORK with inj, range, image, etc.*) 38 priEK :: "agent \<Rightarrow> key" where 39 "priEK A == privateKey Encryption A" 40 41abbreviation 42 priSK :: "agent \<Rightarrow> key" where 43 "priSK A == privateKey Signature A" 44 45 46text\<open>These abbreviations give backward compatibility. They represent the 47simple situation where the signature and encryption keys are the same.\<close> 48 49abbreviation 50 pubK :: "agent \<Rightarrow> key" where 51 "pubK A == pubEK A" 52 53abbreviation 54 priK :: "agent \<Rightarrow> key" where 55 "priK A == invKey (pubEK A)" 56 57 58text\<open>By freeness of agents, no two agents have the same key. Since 59 \<^term>\<open>True\<noteq>False\<close>, no agent has identical signing and encryption keys\<close> 60specification (publicKey) 61 injective_publicKey: 62 "publicKey b A = publicKey c A' ==> b=c \<and> A=A'" 63 apply (rule exI [of _ 64 "\<lambda>b A. 2 * case_agent 0 (\<lambda>n. n + 2) 1 A + case_keymode 0 1 b"]) 65 apply (auto simp add: inj_on_def split: agent.split keymode.split) 66 apply presburger 67 apply presburger 68 done 69 70 71axiomatization where 72 (*No private key equals any public key (essential to ensure that private 73 keys are private!) *) 74 privateKey_neq_publicKey [iff]: "privateKey b A \<noteq> publicKey c A'" 75 76lemmas publicKey_neq_privateKey = privateKey_neq_publicKey [THEN not_sym] 77declare publicKey_neq_privateKey [iff] 78 79 80subsection\<open>Basic properties of \<^term>\<open>pubK\<close> and \<^term>\<open>priK\<close>\<close> 81 82lemma publicKey_inject [iff]: "(publicKey b A = publicKey c A') = (b=c \<and> A=A')" 83by (blast dest!: injective_publicKey) 84 85lemma not_symKeys_pubK [iff]: "publicKey b A \<notin> symKeys" 86by (simp add: symKeys_def) 87 88lemma not_symKeys_priK [iff]: "privateKey b A \<notin> symKeys" 89by (simp add: symKeys_def) 90 91lemma symKey_neq_priEK: "K \<in> symKeys ==> K \<noteq> priEK A" 92by auto 93 94lemma symKeys_neq_imp_neq: "(K \<in> symKeys) \<noteq> (K' \<in> symKeys) ==> K \<noteq> K'" 95by blast 96 97lemma symKeys_invKey_iff [iff]: "(invKey K \<in> symKeys) = (K \<in> symKeys)" 98by (unfold symKeys_def, auto) 99 100lemma analz_symKeys_Decrypt: 101 "[| Crypt K X \<in> analz H; K \<in> symKeys; Key K \<in> analz H |] 102 ==> X \<in> analz H" 103by (auto simp add: symKeys_def) 104 105 106 107subsection\<open>"Image" equations that hold for injective functions\<close> 108 109lemma invKey_image_eq [simp]: "(invKey x \<in> invKey`A) = (x \<in> A)" 110by auto 111 112(*holds because invKey is injective*) 113lemma publicKey_image_eq [simp]: 114 "(publicKey b x \<in> publicKey c ` AA) = (b=c \<and> x \<in> AA)" 115by auto 116 117lemma privateKey_notin_image_publicKey [simp]: "privateKey b x \<notin> publicKey c ` AA" 118by auto 119 120lemma privateKey_image_eq [simp]: 121 "(privateKey b A \<in> invKey ` publicKey c ` AS) = (b=c \<and> A\<in>AS)" 122by auto 123 124lemma publicKey_notin_image_privateKey [simp]: "publicKey b A \<notin> invKey ` publicKey c ` AS" 125by auto 126 127 128subsection\<open>Symmetric Keys\<close> 129 130text\<open>For some protocols, it is convenient to equip agents with symmetric as 131well as asymmetric keys. The theory \<open>Shared\<close> assumes that all keys 132are symmetric.\<close> 133 134consts 135 shrK :: "agent => key" \<comment> \<open>long-term shared keys\<close> 136 137specification (shrK) 138 inj_shrK: "inj shrK" 139 \<comment> \<open>No two agents have the same long-term key\<close> 140 apply (rule exI [of _ "case_agent 0 (\<lambda>n. n + 2) 1"]) 141 apply (simp add: inj_on_def split: agent.split) 142 done 143 144axiomatization where 145 sym_shrK [iff]: "shrK X \<in> symKeys" \<comment> \<open>All shared keys are symmetric\<close> 146 147text\<open>Injectiveness: Agents' long-term keys are distinct.\<close> 148lemmas shrK_injective = inj_shrK [THEN inj_eq] 149declare shrK_injective [iff] 150 151lemma invKey_shrK [simp]: "invKey (shrK A) = shrK A" 152by (simp add: invKey_K) 153 154lemma analz_shrK_Decrypt: 155 "[| Crypt (shrK A) X \<in> analz H; Key(shrK A) \<in> analz H |] ==> X \<in> analz H" 156by auto 157 158lemma analz_Decrypt': 159 "[| Crypt K X \<in> analz H; K \<in> symKeys; Key K \<in> analz H |] ==> X \<in> analz H" 160by (auto simp add: invKey_K) 161 162lemma priK_neq_shrK [iff]: "shrK A \<noteq> privateKey b C" 163by (simp add: symKeys_neq_imp_neq) 164 165lemmas shrK_neq_priK = priK_neq_shrK [THEN not_sym] 166declare shrK_neq_priK [simp] 167 168lemma pubK_neq_shrK [iff]: "shrK A \<noteq> publicKey b C" 169by (simp add: symKeys_neq_imp_neq) 170 171lemmas shrK_neq_pubK = pubK_neq_shrK [THEN not_sym] 172declare shrK_neq_pubK [simp] 173 174lemma priEK_noteq_shrK [simp]: "priEK A \<noteq> shrK B" 175by auto 176 177lemma publicKey_notin_image_shrK [simp]: "publicKey b x \<notin> shrK ` AA" 178by auto 179 180lemma privateKey_notin_image_shrK [simp]: "privateKey b x \<notin> shrK ` AA" 181by auto 182 183lemma shrK_notin_image_publicKey [simp]: "shrK x \<notin> publicKey b ` AA" 184by auto 185 186lemma shrK_notin_image_privateKey [simp]: "shrK x \<notin> invKey ` publicKey b ` AA" 187by auto 188 189lemma shrK_image_eq [simp]: "(shrK x \<in> shrK ` AA) = (x \<in> AA)" 190by auto 191 192text\<open>For some reason, moving this up can make some proofs loop!\<close> 193declare invKey_K [simp] 194 195 196subsection\<open>Initial States of Agents\<close> 197 198text\<open>Note: for all practical purposes, all that matters is the initial 199knowledge of the Spy. All other agents are automata, merely following the 200protocol.\<close> 201 202overloading 203 initState \<equiv> initState 204begin 205 206primrec initState where 207 (*Agents know their private key and all public keys*) 208 initState_Server: 209 "initState Server = 210 {Key (priEK Server), Key (priSK Server)} \<union> 211 (Key ` range pubEK) \<union> (Key ` range pubSK) \<union> (Key ` range shrK)" 212 213| initState_Friend: 214 "initState (Friend i) = 215 {Key (priEK(Friend i)), Key (priSK(Friend i)), Key (shrK(Friend i))} \<union> 216 (Key ` range pubEK) \<union> (Key ` range pubSK)" 217 218| initState_Spy: 219 "initState Spy = 220 (Key ` invKey ` pubEK ` bad) \<union> (Key ` invKey ` pubSK ` bad) \<union> 221 (Key ` shrK ` bad) \<union> 222 (Key ` range pubEK) \<union> (Key ` range pubSK)" 223 224end 225 226 227text\<open>These lemmas allow reasoning about \<^term>\<open>used evs\<close> rather than 228 \<^term>\<open>knows Spy evs\<close>, which is useful when there are private Notes. 229 Because they depend upon the definition of \<^term>\<open>initState\<close>, they cannot 230 be moved up.\<close> 231 232lemma used_parts_subset_parts [rule_format]: 233 "\<forall>X \<in> used evs. parts {X} \<subseteq> used evs" 234apply (induct evs) 235 prefer 2 236 apply (simp add: used_Cons split: event.split) 237 apply (metis Un_iff empty_subsetI insert_subset le_supI1 le_supI2 parts_subset_iff) 238txt\<open>Base case\<close> 239apply (auto dest!: parts_cut simp add: used_Nil) 240done 241 242lemma MPair_used_D: "\<lbrace>X,Y\<rbrace> \<in> used H ==> X \<in> used H \<and> Y \<in> used H" 243by (drule used_parts_subset_parts, simp, blast) 244 245text\<open>There was a similar theorem in Event.thy, so perhaps this one can 246 be moved up if proved directly by induction.\<close> 247lemma MPair_used [elim!]: 248 "[| \<lbrace>X,Y\<rbrace> \<in> used H; 249 [| X \<in> used H; Y \<in> used H |] ==> P |] 250 ==> P" 251by (blast dest: MPair_used_D) 252 253 254text\<open>Rewrites should not refer to \<^term>\<open>initState(Friend i)\<close> because 255 that expression is not in normal form.\<close> 256 257lemma keysFor_parts_initState [simp]: "keysFor (parts (initState C)) = {}" 258apply (unfold keysFor_def) 259apply (induct_tac "C") 260apply (auto intro: range_eqI) 261done 262 263lemma Crypt_notin_initState: "Crypt K X \<notin> parts (initState B)" 264by (induct B, auto) 265 266lemma Crypt_notin_used_empty [simp]: "Crypt K X \<notin> used []" 267by (simp add: Crypt_notin_initState used_Nil) 268 269(*** Basic properties of shrK ***) 270 271(*Agents see their own shared keys!*) 272lemma shrK_in_initState [iff]: "Key (shrK A) \<in> initState A" 273by (induct_tac "A", auto) 274 275lemma shrK_in_knows [iff]: "Key (shrK A) \<in> knows A evs" 276by (simp add: initState_subset_knows [THEN subsetD]) 277 278lemma shrK_in_used [iff]: "Key (shrK A) \<in> used evs" 279by (rule initState_into_used, blast) 280 281 282(** Fresh keys never clash with long-term shared keys **) 283 284(*Used in parts_induct_tac and analz_Fake_tac to distinguish session keys 285 from long-term shared keys*) 286lemma Key_not_used [simp]: "Key K \<notin> used evs ==> K \<notin> range shrK" 287by blast 288 289lemma shrK_neq: "Key K \<notin> used evs ==> shrK B \<noteq> K" 290by blast 291 292lemmas neq_shrK = shrK_neq [THEN not_sym] 293declare neq_shrK [simp] 294 295 296subsection\<open>Function \<^term>\<open>spies\<close>\<close> 297 298lemma not_SignatureE [elim!]: "b \<noteq> Signature \<Longrightarrow> b = Encryption" 299 by (cases b, auto) 300 301text\<open>Agents see their own private keys!\<close> 302lemma priK_in_initState [iff]: "Key (privateKey b A) \<in> initState A" 303 by (cases A, auto) 304 305text\<open>Agents see all public keys!\<close> 306lemma publicKey_in_initState [iff]: "Key (publicKey b A) \<in> initState B" 307 by (cases B, auto) 308 309text\<open>All public keys are visible\<close> 310lemma spies_pubK [iff]: "Key (publicKey b A) \<in> spies evs" 311apply (induct_tac "evs") 312apply (auto simp add: imageI knows_Cons split: event.split) 313done 314 315lemmas analz_spies_pubK = spies_pubK [THEN analz.Inj] 316declare analz_spies_pubK [iff] 317 318text\<open>Spy sees private keys of bad agents!\<close> 319lemma Spy_spies_bad_privateKey [intro!]: 320 "A \<in> bad ==> Key (privateKey b A) \<in> spies evs" 321apply (induct_tac "evs") 322apply (auto simp add: imageI knows_Cons split: event.split) 323done 324 325text\<open>Spy sees long-term shared keys of bad agents!\<close> 326lemma Spy_spies_bad_shrK [intro!]: 327 "A \<in> bad ==> Key (shrK A) \<in> spies evs" 328apply (induct_tac "evs") 329apply (simp_all add: imageI knows_Cons split: event.split) 330done 331 332lemma publicKey_into_used [iff] :"Key (publicKey b A) \<in> used evs" 333apply (rule initState_into_used) 334apply (rule publicKey_in_initState [THEN parts.Inj]) 335done 336 337lemma privateKey_into_used [iff]: "Key (privateKey b A) \<in> used evs" 338apply(rule initState_into_used) 339apply(rule priK_in_initState [THEN parts.Inj]) 340done 341 342(*For case analysis on whether or not an agent is compromised*) 343lemma Crypt_Spy_analz_bad: 344 "[| Crypt (shrK A) X \<in> analz (knows Spy evs); A \<in> bad |] 345 ==> X \<in> analz (knows Spy evs)" 346by force 347 348 349subsection\<open>Fresh Nonces\<close> 350 351lemma Nonce_notin_initState [iff]: "Nonce N \<notin> parts (initState B)" 352by (induct_tac "B", auto) 353 354lemma Nonce_notin_used_empty [simp]: "Nonce N \<notin> used []" 355by (simp add: used_Nil) 356 357 358subsection\<open>Supply fresh nonces for possibility theorems\<close> 359 360text\<open>In any trace, there is an upper bound N on the greatest nonce in use\<close> 361lemma Nonce_supply_lemma: "\<exists>N. \<forall>n. N\<le>n \<longrightarrow> Nonce n \<notin> used evs" 362apply (induct_tac "evs") 363apply (rule_tac x = 0 in exI) 364apply (simp_all (no_asm_simp) add: used_Cons split: event.split) 365apply safe 366apply (rule msg_Nonce_supply [THEN exE], blast elim!: add_leE)+ 367done 368 369lemma Nonce_supply1: "\<exists>N. Nonce N \<notin> used evs" 370by (rule Nonce_supply_lemma [THEN exE], blast) 371 372lemma Nonce_supply: "Nonce (SOME N. Nonce N \<notin> used evs) \<notin> used evs" 373apply (rule Nonce_supply_lemma [THEN exE]) 374apply (rule someI, fast) 375done 376 377subsection\<open>Specialized Rewriting for Theorems About \<^term>\<open>analz\<close> and Image\<close> 378 379lemma insert_Key_singleton: "insert (Key K) H = Key ` {K} \<union> H" 380by blast 381 382lemma insert_Key_image: "insert (Key K) (Key`KK \<union> C) = Key ` (insert K KK) \<union> C" 383by blast 384 385 386lemma Crypt_imp_keysFor :"[|Crypt K X \<in> H; K \<in> symKeys|] ==> K \<in> keysFor H" 387by (drule Crypt_imp_invKey_keysFor, simp) 388 389text\<open>Lemma for the trivial direction of the if-and-only-if of the 390Session Key Compromise Theorem\<close> 391lemma analz_image_freshK_lemma: 392 "(Key K \<in> analz (Key`nE \<union> H)) \<longrightarrow> (K \<in> nE | Key K \<in> analz H) ==> 393 (Key K \<in> analz (Key`nE \<union> H)) = (K \<in> nE | Key K \<in> analz H)" 394by (blast intro: analz_mono [THEN [2] rev_subsetD]) 395 396lemmas analz_image_freshK_simps = 397 simp_thms mem_simps \<comment> \<open>these two allow its use with \<open>only:\<close>\<close> 398 disj_comms 399 image_insert [THEN sym] image_Un [THEN sym] empty_subsetI insert_subset 400 analz_insert_eq Un_upper2 [THEN analz_mono, THEN subsetD] 401 insert_Key_singleton 402 Key_not_used insert_Key_image Un_assoc [THEN sym] 403 404ML \<open> 405structure Public = 406struct 407 408val analz_image_freshK_ss = 409 simpset_of 410 (\<^context> delsimps [image_insert, image_Un] 411 delsimps [@{thm imp_disjL}] (*reduces blow-up*) 412 addsimps @{thms analz_image_freshK_simps}) 413 414(*Tactic for possibility theorems*) 415fun possibility_tac ctxt = 416 REPEAT (*omit used_Says so that Nonces start from different traces!*) 417 (ALLGOALS (simp_tac (ctxt setSolver safe_solver delsimps [@{thm used_Says}])) 418 THEN 419 REPEAT_FIRST (eq_assume_tac ORELSE' 420 resolve_tac ctxt [refl, conjI, @{thm Nonce_supply}])) 421 422(*For harder protocols (such as Recur) where we have to set up some 423 nonces and keys initially*) 424fun basic_possibility_tac ctxt = 425 REPEAT 426 (ALLGOALS (asm_simp_tac (ctxt setSolver safe_solver)) 427 THEN 428 REPEAT_FIRST (resolve_tac ctxt [refl, conjI])) 429 430end 431\<close> 432 433method_setup analz_freshK = \<open> 434 Scan.succeed (fn ctxt => 435 (SIMPLE_METHOD 436 (EVERY [REPEAT_FIRST (resolve_tac ctxt [allI, ballI, impI]), 437 REPEAT_FIRST (resolve_tac ctxt @{thms analz_image_freshK_lemma}), 438 ALLGOALS (asm_simp_tac (put_simpset Public.analz_image_freshK_ss ctxt))])))\<close> 439 "for proving the Session Key Compromise theorem" 440 441 442subsection\<open>Specialized Methods for Possibility Theorems\<close> 443 444method_setup possibility = \<open> 445 Scan.succeed (SIMPLE_METHOD o Public.possibility_tac)\<close> 446 "for proving possibility theorems" 447 448method_setup basic_possibility = \<open> 449 Scan.succeed (SIMPLE_METHOD o Public.basic_possibility_tac)\<close> 450 "for proving possibility theorems" 451 452end 453