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