1(* Title: HOL/Auth/Shared.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1996 University of Cambridge 4 5Theory of Shared Keys (common to all symmetric-key protocols) 6 7Shared, long-term keys; initial states of agents 8*) 9 10theory Shared 11imports Event All_Symmetric 12begin 13 14consts 15 shrK :: "agent \<Rightarrow> key" (*symmetric keys*) 16 17specification (shrK) 18 inj_shrK: "inj shrK" 19 \<comment> \<open>No two agents have the same long-term key\<close> 20 apply (rule exI [of _ "case_agent 0 (\<lambda>n. n + 2) 1"]) 21 apply (simp add: inj_on_def split: agent.split) 22 done 23 24text\<open>Server knows all long-term keys; other agents know only their own\<close> 25 26overloading 27 initState \<equiv> initState 28begin 29 30primrec initState where 31 initState_Server: "initState Server = Key ` range shrK" 32| initState_Friend: "initState (Friend i) = {Key (shrK (Friend i))}" 33| initState_Spy: "initState Spy = Key`shrK`bad" 34 35end 36 37 38subsection\<open>Basic properties of shrK\<close> 39 40(*Injectiveness: Agents' long-term keys are distinct.*) 41lemmas shrK_injective = inj_shrK [THEN inj_eq] 42declare shrK_injective [iff] 43 44lemma invKey_K [simp]: "invKey K = K" 45apply (insert isSym_keys) 46apply (simp add: symKeys_def) 47done 48 49 50lemma analz_Decrypt' [dest]: 51 "[| Crypt K X \<in> analz H; Key K \<in> analz H |] ==> X \<in> analz H" 52by auto 53 54text\<open>Now cancel the \<open>dest\<close> attribute given to 55 \<open>analz.Decrypt\<close> in its declaration.\<close> 56declare analz.Decrypt [rule del] 57 58text\<open>Rewrites should not refer to \<^term>\<open>initState(Friend i)\<close> because 59 that expression is not in normal form.\<close> 60 61lemma keysFor_parts_initState [simp]: "keysFor (parts (initState C)) = {}" 62apply (unfold keysFor_def) 63apply (induct_tac "C", auto) 64done 65 66(*Specialized to shared-key model: no @{term invKey}*) 67lemma keysFor_parts_insert: 68 "[| K \<in> keysFor (parts (insert X G)); X \<in> synth (analz H) |] 69 ==> K \<in> keysFor (parts (G \<union> H)) | Key K \<in> parts H" 70by (metis invKey_K keysFor_parts_insert) 71 72lemma Crypt_imp_keysFor: "Crypt K X \<in> H ==> K \<in> keysFor H" 73by (metis Crypt_imp_invKey_keysFor invKey_K) 74 75 76subsection\<open>Function "knows"\<close> 77 78(*Spy sees shared keys of agents!*) 79lemma Spy_knows_Spy_bad [intro!]: "A \<in> bad \<Longrightarrow> Key (shrK A) \<in> knows Spy evs" 80apply (induct_tac "evs") 81apply (simp_all (no_asm_simp) add: imageI knows_Cons split: event.split) 82done 83 84(*For case analysis on whether or not an agent is compromised*) 85lemma Crypt_Spy_analz_bad: "[| Crypt (shrK A) X \<in> analz (knows Spy evs); A \<in> bad |] 86 ==> X \<in> analz (knows Spy evs)" 87by (metis Spy_knows_Spy_bad analz.Inj analz_Decrypt') 88 89 90(** Fresh keys never clash with long-term shared keys **) 91 92(*Agents see their own shared keys!*) 93lemma shrK_in_initState [iff]: "Key (shrK A) \<in> initState A" 94by (induct_tac "A", auto) 95 96lemma shrK_in_used [iff]: "Key (shrK A) \<in> used evs" 97by (rule initState_into_used, blast) 98 99(*Used in parts_induct_tac and analz_Fake_tac to distinguish session keys 100 from long-term shared keys*) 101lemma Key_not_used [simp]: "Key K \<notin> used evs ==> K \<notin> range shrK" 102by blast 103 104lemma shrK_neq [simp]: "Key K \<notin> used evs ==> shrK B \<noteq> K" 105by blast 106 107lemmas shrK_sym_neq = shrK_neq [THEN not_sym] 108declare shrK_sym_neq [simp] 109 110 111subsection\<open>Fresh nonces\<close> 112 113lemma Nonce_notin_initState [iff]: "Nonce N \<notin> parts (initState B)" 114by (induct_tac "B", auto) 115 116lemma Nonce_notin_used_empty [simp]: "Nonce N \<notin> used []" 117by (simp add: used_Nil) 118 119 120subsection\<open>Supply fresh nonces for possibility theorems.\<close> 121 122(*In any trace, there is an upper bound N on the greatest nonce in use.*) 123lemma Nonce_supply_lemma: "\<exists>N. \<forall>n. N \<le> n \<longrightarrow> Nonce n \<notin> used evs" 124apply (induct_tac "evs") 125apply (rule_tac x = 0 in exI) 126apply (simp_all (no_asm_simp) add: used_Cons split: event.split) 127apply (metis le_sup_iff msg_Nonce_supply) 128done 129 130lemma Nonce_supply1: "\<exists>N. Nonce N \<notin> used evs" 131by (metis Nonce_supply_lemma order_eq_iff) 132 133lemma Nonce_supply2: "\<exists>N N'. Nonce N \<notin> used evs \<and> Nonce N' \<notin> used evs' \<and> N \<noteq> N'" 134apply (cut_tac evs = evs in Nonce_supply_lemma) 135apply (cut_tac evs = "evs'" in Nonce_supply_lemma, clarify) 136apply (metis Suc_n_not_le_n nat_le_linear) 137done 138 139lemma Nonce_supply3: "\<exists>N N' N''. Nonce N \<notin> used evs \<and> Nonce N' \<notin> used evs' \<and> 140 Nonce N'' \<notin> used evs'' \<and> N \<noteq> N' \<and> N' \<noteq> N'' \<and> N \<noteq> N''" 141apply (cut_tac evs = evs in Nonce_supply_lemma) 142apply (cut_tac evs = "evs'" in Nonce_supply_lemma) 143apply (cut_tac evs = "evs''" in Nonce_supply_lemma, clarify) 144apply (rule_tac x = N in exI) 145apply (rule_tac x = "Suc (N+Na)" in exI) 146apply (rule_tac x = "Suc (Suc (N+Na+Nb))" in exI) 147apply (simp (no_asm_simp) add: less_not_refl3 le_add1 le_add2 less_Suc_eq_le) 148done 149 150lemma Nonce_supply: "Nonce (SOME N. Nonce N \<notin> used evs) \<notin> used evs" 151apply (rule Nonce_supply_lemma [THEN exE]) 152apply (rule someI, blast) 153done 154 155text\<open>Unlike the corresponding property of nonces, we cannot prove 156 \<^term>\<open>finite KK ==> \<exists>K. K \<notin> KK \<and> Key K \<notin> used evs\<close>. 157 We have infinitely many agents and there is nothing to stop their 158 long-term keys from exhausting all the natural numbers. Instead, 159 possibility theorems must assume the existence of a few keys.\<close> 160 161 162subsection\<open>Specialized Rewriting for Theorems About \<^term>\<open>analz\<close> and Image\<close> 163 164lemma subset_Compl_range: "A \<subseteq> - (range shrK) \<Longrightarrow> shrK x \<notin> A" 165by blast 166 167lemma insert_Key_singleton: "insert (Key K) H = Key ` {K} \<union> H" 168by blast 169 170lemma insert_Key_image: "insert (Key K) (Key`KK \<union> C) = Key`(insert K KK) \<union> C" 171by blast 172 173(** Reverse the normal simplification of "image" to build up (not break down) 174 the set of keys. Use analz_insert_eq with (Un_upper2 RS analz_mono) to 175 erase occurrences of forwarded message components (X). **) 176 177lemmas analz_image_freshK_simps = 178 simp_thms mem_simps \<comment> \<open>these two allow its use with \<open>only:\<close>\<close> 179 disj_comms 180 image_insert [THEN sym] image_Un [THEN sym] empty_subsetI insert_subset 181 analz_insert_eq Un_upper2 [THEN analz_mono, THEN [2] rev_subsetD] 182 insert_Key_singleton subset_Compl_range 183 Key_not_used insert_Key_image Un_assoc [THEN sym] 184 185(*Lemma for the trivial direction of the if-and-only-if*) 186lemma analz_image_freshK_lemma: 187 "(Key K \<in> analz (Key`nE \<union> H)) \<longrightarrow> (K \<in> nE | Key K \<in> analz H) ==> 188 (Key K \<in> analz (Key`nE \<union> H)) = (K \<in> nE | Key K \<in> analz H)" 189by (blast intro: analz_mono [THEN [2] rev_subsetD]) 190 191 192subsection\<open>Tactics for possibility theorems\<close> 193 194ML 195\<open> 196structure Shared = 197struct 198 199(*Omitting used_Says makes the tactic much faster: it leaves expressions 200 such as Nonce ?N \<notin> used evs that match Nonce_supply*) 201fun possibility_tac ctxt = 202 (REPEAT 203 (ALLGOALS (simp_tac (ctxt 204 delsimps [@{thm used_Says}, @{thm used_Notes}, @{thm used_Gets}] 205 setSolver safe_solver)) 206 THEN 207 REPEAT_FIRST (eq_assume_tac ORELSE' 208 resolve_tac ctxt [refl, conjI, @{thm Nonce_supply}]))) 209 210(*For harder protocols (such as Recur) where we have to set up some 211 nonces and keys initially*) 212fun basic_possibility_tac ctxt = 213 REPEAT 214 (ALLGOALS (asm_simp_tac (ctxt setSolver safe_solver)) 215 THEN 216 REPEAT_FIRST (resolve_tac ctxt [refl, conjI])) 217 218 219val analz_image_freshK_ss = 220 simpset_of 221 (\<^context> delsimps [image_insert, image_Un] 222 delsimps [@{thm imp_disjL}] (*reduces blow-up*) 223 addsimps @{thms analz_image_freshK_simps}) 224 225end 226\<close> 227 228 229 230(*Lets blast_tac perform this step without needing the simplifier*) 231lemma invKey_shrK_iff [iff]: 232 "(Key (invKey K) \<in> X) = (Key K \<in> X)" 233by auto 234 235(*Specialized methods*) 236 237method_setup analz_freshK = \<open> 238 Scan.succeed (fn ctxt => 239 (SIMPLE_METHOD 240 (EVERY [REPEAT_FIRST (resolve_tac ctxt [allI, ballI, impI]), 241 REPEAT_FIRST (resolve_tac ctxt @{thms analz_image_freshK_lemma}), 242 ALLGOALS (asm_simp_tac (put_simpset Shared.analz_image_freshK_ss ctxt))])))\<close> 243 "for proving the Session Key Compromise theorem" 244 245method_setup possibility = \<open> 246 Scan.succeed (fn ctxt => SIMPLE_METHOD (Shared.possibility_tac ctxt))\<close> 247 "for proving possibility theorems" 248 249method_setup basic_possibility = \<open> 250 Scan.succeed (fn ctxt => SIMPLE_METHOD (Shared.basic_possibility_tac ctxt))\<close> 251 "for proving possibility theorems" 252 253lemma knows_subset_knows_Cons: "knows A evs \<subseteq> knows A (e # evs)" 254by (cases e) (auto simp: knows_Cons) 255 256end 257