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