src/HOL/Auth/Public.thy
author wenzelm
Mon Jan 11 21:21:02 2016 +0100 (2016-01-11)
changeset 62145 5b946c81dfbf
parent 61956 38b73f7940af
child 63648 f9f3006a5579
permissions -rw-r--r--
eliminated old defs;
     1 (*  Title:      HOL/Auth/Public.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1996  University of Cambridge
     4 
     5 Theory of Public Keys (common to all public-key protocols)
     6 
     7 Private and public keys; initial states of agents
     8 *)
     9 
    10 theory Public
    11 imports Event
    12 begin
    13 
    14 lemma invKey_K: "K \<in> symKeys ==> invKey K = K"
    15 by (simp add: symKeys_def)
    16 
    17 subsection\<open>Asymmetric Keys\<close>
    18 
    19 datatype keymode = Signature | Encryption
    20 
    21 consts
    22   publicKey :: "[keymode,agent] => key"
    23 
    24 abbreviation
    25   pubEK :: "agent => key" where
    26   "pubEK == publicKey Encryption"
    27 
    28 abbreviation
    29   pubSK :: "agent => key" where
    30   "pubSK == publicKey Signature"
    31 
    32 abbreviation
    33   privateKey :: "[keymode, agent] => key" where
    34   "privateKey b A == invKey (publicKey b A)"
    35 
    36 abbreviation
    37   (*BEWARE!! priEK, priSK DON'T WORK with inj, range, image, etc.*)
    38   priEK :: "agent => key" where
    39   "priEK A == privateKey Encryption A"
    40 
    41 abbreviation
    42   priSK :: "agent => key" where
    43   "priSK A == privateKey Signature A"
    44 
    45 
    46 text\<open>These abbreviations give backward compatibility.  They represent the
    47 simple situation where the signature and encryption keys are the same.\<close>
    48 
    49 abbreviation
    50   pubK :: "agent => key" where
    51   "pubK A == pubEK A"
    52 
    53 abbreviation
    54   priK :: "agent => key" where
    55   "priK A == invKey (pubEK A)"
    56 
    57 
    58 text\<open>By freeness of agents, no two agents have the same key.  Since
    59   @{term "True\<noteq>False"}, no agent has identical signing and encryption keys\<close>
    60 specification (publicKey)
    61   injective_publicKey:
    62     "publicKey b A = publicKey c A' ==> b=c & A=A'"
    63    apply (rule exI [of _ 
    64        "%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 
    71 axiomatization 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 
    76 lemmas publicKey_neq_privateKey = privateKey_neq_publicKey [THEN not_sym]
    77 declare publicKey_neq_privateKey [iff]
    78 
    79 
    80 subsection\<open>Basic properties of @{term pubK} and @{term priK}\<close>
    81 
    82 lemma publicKey_inject [iff]: "(publicKey b A = publicKey c A') = (b=c & A=A')"
    83 by (blast dest!: injective_publicKey) 
    84 
    85 lemma not_symKeys_pubK [iff]: "publicKey b A \<notin> symKeys"
    86 by (simp add: symKeys_def)
    87 
    88 lemma not_symKeys_priK [iff]: "privateKey b A \<notin> symKeys"
    89 by (simp add: symKeys_def)
    90 
    91 lemma symKey_neq_priEK: "K \<in> symKeys ==> K \<noteq> priEK A"
    92 by auto
    93 
    94 lemma symKeys_neq_imp_neq: "(K \<in> symKeys) \<noteq> (K' \<in> symKeys) ==> K \<noteq> K'"
    95 by blast
    96 
    97 lemma symKeys_invKey_iff [iff]: "(invKey K \<in> symKeys) = (K \<in> symKeys)"
    98 by (unfold symKeys_def, auto)
    99 
   100 lemma analz_symKeys_Decrypt:
   101      "[| Crypt K X \<in> analz H;  K \<in> symKeys;  Key K \<in> analz H |]  
   102       ==> X \<in> analz H"
   103 by (auto simp add: symKeys_def)
   104 
   105 
   106 
   107 subsection\<open>"Image" equations that hold for injective functions\<close>
   108 
   109 lemma invKey_image_eq [simp]: "(invKey x \<in> invKey`A) = (x \<in> A)"
   110 by auto
   111 
   112 (*holds because invKey is injective*)
   113 lemma publicKey_image_eq [simp]:
   114      "(publicKey b x \<in> publicKey c ` AA) = (b=c & x \<in> AA)"
   115 by auto
   116 
   117 lemma privateKey_notin_image_publicKey [simp]: "privateKey b x \<notin> publicKey c ` AA"
   118 by auto
   119 
   120 lemma privateKey_image_eq [simp]:
   121      "(privateKey b A \<in> invKey ` publicKey c ` AS) = (b=c & A\<in>AS)"
   122 by auto
   123 
   124 lemma publicKey_notin_image_privateKey [simp]: "publicKey b A \<notin> invKey ` publicKey c ` AS"
   125 by auto
   126 
   127 
   128 subsection\<open>Symmetric Keys\<close>
   129 
   130 text\<open>For some protocols, it is convenient to equip agents with symmetric as
   131 well as asymmetric keys.  The theory \<open>Shared\<close> assumes that all keys
   132 are symmetric.\<close>
   133 
   134 consts
   135   shrK    :: "agent => key"    \<comment>\<open>long-term shared keys\<close>
   136 
   137 specification (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 
   144 axiomatization where
   145   sym_shrK [iff]: "shrK X \<in> symKeys" \<comment>\<open>All shared keys are symmetric\<close>
   146 
   147 text\<open>Injectiveness: Agents' long-term keys are distinct.\<close>
   148 lemmas shrK_injective = inj_shrK [THEN inj_eq]
   149 declare shrK_injective [iff]
   150 
   151 lemma invKey_shrK [simp]: "invKey (shrK A) = shrK A"
   152 by (simp add: invKey_K) 
   153 
   154 lemma analz_shrK_Decrypt:
   155      "[| Crypt (shrK A) X \<in> analz H; Key(shrK A) \<in> analz H |] ==> X \<in> analz H"
   156 by auto
   157 
   158 lemma analz_Decrypt':
   159      "[| Crypt K X \<in> analz H; K \<in> symKeys; Key K \<in> analz H |] ==> X \<in> analz H"
   160 by (auto simp add: invKey_K)
   161 
   162 lemma priK_neq_shrK [iff]: "shrK A \<noteq> privateKey b C"
   163 by (simp add: symKeys_neq_imp_neq)
   164 
   165 lemmas shrK_neq_priK = priK_neq_shrK [THEN not_sym]
   166 declare shrK_neq_priK [simp]
   167 
   168 lemma pubK_neq_shrK [iff]: "shrK A \<noteq> publicKey b C"
   169 by (simp add: symKeys_neq_imp_neq)
   170 
   171 lemmas shrK_neq_pubK = pubK_neq_shrK [THEN not_sym]
   172 declare shrK_neq_pubK [simp]
   173 
   174 lemma priEK_noteq_shrK [simp]: "priEK A \<noteq> shrK B" 
   175 by auto
   176 
   177 lemma publicKey_notin_image_shrK [simp]: "publicKey b x \<notin> shrK ` AA"
   178 by auto
   179 
   180 lemma privateKey_notin_image_shrK [simp]: "privateKey b x \<notin> shrK ` AA"
   181 by auto
   182 
   183 lemma shrK_notin_image_publicKey [simp]: "shrK x \<notin> publicKey b ` AA"
   184 by auto
   185 
   186 lemma shrK_notin_image_privateKey [simp]: "shrK x \<notin> invKey ` publicKey b ` AA" 
   187 by auto
   188 
   189 lemma shrK_image_eq [simp]: "(shrK x \<in> shrK ` AA) = (x \<in> AA)"
   190 by auto
   191 
   192 text\<open>For some reason, moving this up can make some proofs loop!\<close>
   193 declare invKey_K [simp]
   194 
   195 
   196 subsection\<open>Initial States of Agents\<close>
   197 
   198 text\<open>Note: for all practical purposes, all that matters is the initial
   199 knowledge of the Spy.  All other agents are automata, merely following the
   200 protocol.\<close>
   201 
   202 overloading
   203   initState \<equiv> initState
   204 begin
   205 
   206 primrec 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 
   224 end
   225 
   226 
   227 text\<open>These lemmas allow reasoning about @{term "used evs"} rather than
   228    @{term "knows Spy evs"}, which is useful when there are private Notes. 
   229    Because they depend upon the definition of @{term initState}, they cannot
   230    be moved up.\<close>
   231 
   232 lemma used_parts_subset_parts [rule_format]:
   233      "\<forall>X \<in> used evs. parts {X} \<subseteq> used evs"
   234 apply (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)
   238 txt\<open>Base case\<close>
   239 apply (auto dest!: parts_cut simp add: used_Nil) 
   240 done
   241 
   242 lemma MPair_used_D: "\<lbrace>X,Y\<rbrace> \<in> used H ==> X \<in> used H & Y \<in> used H"
   243 by (drule used_parts_subset_parts, simp, blast)
   244 
   245 text\<open>There was a similar theorem in Event.thy, so perhaps this one can
   246   be moved up if proved directly by induction.\<close>
   247 lemma MPair_used [elim!]:
   248      "[| \<lbrace>X,Y\<rbrace> \<in> used H;
   249          [| X \<in> used H; Y \<in> used H |] ==> P |] 
   250       ==> P"
   251 by (blast dest: MPair_used_D) 
   252 
   253 
   254 text\<open>Rewrites should not refer to  @{term "initState(Friend i)"} because
   255   that expression is not in normal form.\<close>
   256 
   257 lemma keysFor_parts_initState [simp]: "keysFor (parts (initState C)) = {}"
   258 apply (unfold keysFor_def)
   259 apply (induct_tac "C")
   260 apply (auto intro: range_eqI)
   261 done
   262 
   263 lemma Crypt_notin_initState: "Crypt K X \<notin> parts (initState B)"
   264 by (induct B, auto)
   265 
   266 lemma Crypt_notin_used_empty [simp]: "Crypt K X \<notin> used []"
   267 by (simp add: Crypt_notin_initState used_Nil)
   268 
   269 (*** Basic properties of shrK ***)
   270 
   271 (*Agents see their own shared keys!*)
   272 lemma shrK_in_initState [iff]: "Key (shrK A) \<in> initState A"
   273 by (induct_tac "A", auto)
   274 
   275 lemma shrK_in_knows [iff]: "Key (shrK A) \<in> knows A evs"
   276 by (simp add: initState_subset_knows [THEN subsetD])
   277 
   278 lemma shrK_in_used [iff]: "Key (shrK A) \<in> used evs"
   279 by (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*)
   286 lemma Key_not_used [simp]: "Key K \<notin> used evs ==> K \<notin> range shrK"
   287 by blast
   288 
   289 lemma shrK_neq: "Key K \<notin> used evs ==> shrK B \<noteq> K"
   290 by blast
   291 
   292 lemmas neq_shrK = shrK_neq [THEN not_sym]
   293 declare neq_shrK [simp]
   294 
   295 
   296 subsection\<open>Function @{term spies}\<close>
   297 
   298 lemma not_SignatureE [elim!]: "b \<noteq> Signature \<Longrightarrow> b = Encryption"
   299   by (cases b, auto) 
   300 
   301 text\<open>Agents see their own private keys!\<close>
   302 lemma priK_in_initState [iff]: "Key (privateKey b A) \<in> initState A"
   303   by (cases A, auto)
   304 
   305 text\<open>Agents see all public keys!\<close>
   306 lemma publicKey_in_initState [iff]: "Key (publicKey b A) \<in> initState B"
   307   by (cases B, auto) 
   308 
   309 text\<open>All public keys are visible\<close>
   310 lemma spies_pubK [iff]: "Key (publicKey b A) \<in> spies evs"
   311 apply (induct_tac "evs")
   312 apply (auto simp add: imageI knows_Cons split add: event.split)
   313 done
   314 
   315 lemmas analz_spies_pubK = spies_pubK [THEN analz.Inj]
   316 declare analz_spies_pubK [iff]
   317 
   318 text\<open>Spy sees private keys of bad agents!\<close>
   319 lemma Spy_spies_bad_privateKey [intro!]:
   320      "A \<in> bad ==> Key (privateKey b A) \<in> spies evs"
   321 apply (induct_tac "evs")
   322 apply (auto simp add: imageI knows_Cons split add: event.split)
   323 done
   324 
   325 text\<open>Spy sees long-term shared keys of bad agents!\<close>
   326 lemma Spy_spies_bad_shrK [intro!]:
   327      "A \<in> bad ==> Key (shrK A) \<in> spies evs"
   328 apply (induct_tac "evs")
   329 apply (simp_all add: imageI knows_Cons split add: event.split)
   330 done
   331 
   332 lemma publicKey_into_used [iff] :"Key (publicKey b A) \<in> used evs"
   333 apply (rule initState_into_used)
   334 apply (rule publicKey_in_initState [THEN parts.Inj])
   335 done
   336 
   337 lemma privateKey_into_used [iff]: "Key (privateKey b A) \<in> used evs"
   338 apply(rule initState_into_used)
   339 apply(rule priK_in_initState [THEN parts.Inj])
   340 done
   341 
   342 (*For case analysis on whether or not an agent is compromised*)
   343 lemma Crypt_Spy_analz_bad:
   344      "[| Crypt (shrK A) X \<in> analz (knows Spy evs);  A \<in> bad |]  
   345       ==> X \<in> analz (knows Spy evs)"
   346 by force
   347 
   348 
   349 subsection\<open>Fresh Nonces\<close>
   350 
   351 lemma Nonce_notin_initState [iff]: "Nonce N \<notin> parts (initState B)"
   352 by (induct_tac "B", auto)
   353 
   354 lemma Nonce_notin_used_empty [simp]: "Nonce N \<notin> used []"
   355 by (simp add: used_Nil)
   356 
   357 
   358 subsection\<open>Supply fresh nonces for possibility theorems\<close>
   359 
   360 text\<open>In any trace, there is an upper bound N on the greatest nonce in use\<close>
   361 lemma Nonce_supply_lemma: "EX N. ALL n. N<=n --> Nonce n \<notin> used evs"
   362 apply (induct_tac "evs")
   363 apply (rule_tac x = 0 in exI)
   364 apply (simp_all (no_asm_simp) add: used_Cons split add: event.split)
   365 apply safe
   366 apply (rule msg_Nonce_supply [THEN exE], blast elim!: add_leE)+
   367 done
   368 
   369 lemma Nonce_supply1: "EX N. Nonce N \<notin> used evs"
   370 by (rule Nonce_supply_lemma [THEN exE], blast)
   371 
   372 lemma Nonce_supply: "Nonce (@ N. Nonce N \<notin> used evs) \<notin> used evs"
   373 apply (rule Nonce_supply_lemma [THEN exE])
   374 apply (rule someI, fast)
   375 done
   376 
   377 subsection\<open>Specialized Rewriting for Theorems About @{term analz} and Image\<close>
   378 
   379 lemma insert_Key_singleton: "insert (Key K) H = Key ` {K} Un H"
   380 by blast
   381 
   382 lemma insert_Key_image: "insert (Key K) (Key`KK \<union> C) = Key ` (insert K KK) \<union> C"
   383 by blast
   384 
   385 
   386 lemma Crypt_imp_keysFor :"[|Crypt K X \<in> H; K \<in> symKeys|] ==> K \<in> keysFor H"
   387 by (drule Crypt_imp_invKey_keysFor, simp)
   388 
   389 text\<open>Lemma for the trivial direction of the if-and-only-if of the 
   390 Session Key Compromise Theorem\<close>
   391 lemma analz_image_freshK_lemma:
   392      "(Key K \<in> analz (Key`nE \<union> H)) --> (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)"
   394 by (blast intro: analz_mono [THEN [2] rev_subsetD])
   395 
   396 lemmas 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 
   404 ML \<open>
   405 structure Public =
   406 struct
   407 
   408 val 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*)
   415 fun 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*)
   424 fun 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 
   430 end
   431 \<close>
   432 
   433 method_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 
   442 subsection\<open>Specialized Methods for Possibility Theorems\<close>
   443 
   444 method_setup possibility = \<open>
   445     Scan.succeed (SIMPLE_METHOD o Public.possibility_tac)\<close>
   446     "for proving possibility theorems"
   447 
   448 method_setup basic_possibility = \<open>
   449     Scan.succeed (SIMPLE_METHOD o Public.basic_possibility_tac)\<close>
   450     "for proving possibility theorems"
   451 
   452 end