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