src/HOL/Auth/Shared.thy
author wenzelm
Mon Aug 31 21:28:08 2015 +0200 (2015-08-31)
changeset 61070 b72a990adfe2
parent 60754 02924903a6fd
child 61830 4f5ab843cf5b
permissions -rw-r--r--
prefer symbols;
     1 (*  Title:      HOL/Auth/Shared.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1996  University of Cambridge
     4 
     5 Theory of Shared Keys (common to all symmetric-key protocols)
     6 
     7 Shared, long-term keys; initial states of agents
     8 *)
     9 
    10 theory Shared
    11 imports Event All_Symmetric
    12 begin
    13 
    14 consts
    15   shrK    :: "agent => key"  (*symmetric keys*)
    16 
    17 specification (shrK)
    18   inj_shrK: "inj shrK"
    19   --{*No two agents have the same long-term key*}
    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 
    24 text{*Server knows all long-term keys; other agents know only their own*}
    25 
    26 overloading
    27   initState \<equiv> initState
    28 begin
    29 
    30 primrec 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 
    35 end
    36 
    37 
    38 subsection{*Basic properties of shrK*}
    39 
    40 (*Injectiveness: Agents' long-term keys are distinct.*)
    41 lemmas shrK_injective = inj_shrK [THEN inj_eq]
    42 declare shrK_injective [iff]
    43 
    44 lemma invKey_K [simp]: "invKey K = K"
    45 apply (insert isSym_keys)
    46 apply (simp add: symKeys_def) 
    47 done
    48 
    49 
    50 lemma analz_Decrypt' [dest]:
    51      "[| Crypt K X \<in> analz H;  Key K  \<in> analz H |] ==> X \<in> analz H"
    52 by auto
    53 
    54 text{*Now cancel the @{text dest} attribute given to
    55  @{text analz.Decrypt} in its declaration.*}
    56 declare analz.Decrypt [rule del]
    57 
    58 text{*Rewrites should not refer to  @{term "initState(Friend i)"} because
    59   that expression is not in normal form.*}
    60 
    61 lemma keysFor_parts_initState [simp]: "keysFor (parts (initState C)) = {}"
    62 apply (unfold keysFor_def)
    63 apply (induct_tac "C", auto)
    64 done
    65 
    66 (*Specialized to shared-key model: no @{term invKey}*)
    67 lemma 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"
    70 by (metis invKey_K keysFor_parts_insert)
    71 
    72 lemma Crypt_imp_keysFor: "Crypt K X \<in> H ==> K \<in> keysFor H"
    73 by (metis Crypt_imp_invKey_keysFor invKey_K)
    74 
    75 
    76 subsection{*Function "knows"*}
    77 
    78 (*Spy sees shared keys of agents!*)
    79 lemma Spy_knows_Spy_bad [intro!]: "A: bad ==> Key (shrK A) \<in> knows Spy evs"
    80 apply (induct_tac "evs")
    81 apply (simp_all (no_asm_simp) add: imageI knows_Cons split add: event.split)
    82 done
    83 
    84 (*For case analysis on whether or not an agent is compromised*)
    85 lemma Crypt_Spy_analz_bad: "[| Crypt (shrK A) X \<in> analz (knows Spy evs);  A: bad |]  
    86       ==> X \<in> analz (knows Spy evs)"
    87 by (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!*)
    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 by (simp add: used_Nil)
   118 
   119 
   120 subsection{*Supply fresh nonces for possibility theorems.*}
   121 
   122 (*In any trace, there is an upper bound N on the greatest nonce in use.*)
   123 lemma Nonce_supply_lemma: "\<exists>N. ALL n. N<=n --> Nonce n \<notin> used evs"
   124 apply (induct_tac "evs")
   125 apply (rule_tac x = 0 in exI)
   126 apply (simp_all (no_asm_simp) add: used_Cons split add: event.split)
   127 apply (metis le_sup_iff msg_Nonce_supply)
   128 done
   129 
   130 lemma Nonce_supply1: "\<exists>N. Nonce N \<notin> used evs"
   131 by (metis Nonce_supply_lemma order_eq_iff)
   132 
   133 lemma Nonce_supply2: "\<exists>N N'. Nonce N \<notin> used evs & Nonce N' \<notin> used evs' & N \<noteq> N'"
   134 apply (cut_tac evs = evs in Nonce_supply_lemma)
   135 apply (cut_tac evs = "evs'" in Nonce_supply_lemma, clarify)
   136 apply (metis Suc_n_not_le_n nat_le_linear)
   137 done
   138 
   139 lemma Nonce_supply3: "\<exists>N N' N''. Nonce N \<notin> used evs & Nonce N' \<notin> used evs' &  
   140                     Nonce N'' \<notin> used evs'' & N \<noteq> N' & N' \<noteq> N'' & N \<noteq> N''"
   141 apply (cut_tac evs = evs in Nonce_supply_lemma)
   142 apply (cut_tac evs = "evs'" in Nonce_supply_lemma)
   143 apply (cut_tac evs = "evs''" in Nonce_supply_lemma, clarify)
   144 apply (rule_tac x = N in exI)
   145 apply (rule_tac x = "Suc (N+Na)" in exI)
   146 apply (rule_tac x = "Suc (Suc (N+Na+Nb))" in exI)
   147 apply (simp (no_asm_simp) add: less_not_refl3 le_add1 le_add2 less_Suc_eq_le)
   148 done
   149 
   150 lemma Nonce_supply: "Nonce (@ N. Nonce N \<notin> used evs) \<notin> used evs"
   151 apply (rule Nonce_supply_lemma [THEN exE])
   152 apply (rule someI, blast)
   153 done
   154 
   155 text{*Unlike the corresponding property of nonces, we cannot prove
   156     @{term "finite KK ==> \<exists>K. K \<notin> KK & Key K \<notin> used evs"}.
   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.*}
   160 
   161 
   162 subsection{*Specialized Rewriting for Theorems About @{term analz} and Image*}
   163 
   164 lemma subset_Compl_range: "A <= - (range shrK) ==> shrK x \<notin> A"
   165 by blast
   166 
   167 lemma insert_Key_singleton: "insert (Key K) H = Key ` {K} \<union> H"
   168 by blast
   169 
   170 lemma insert_Key_image: "insert (Key K) (Key`KK \<union> C) = Key`(insert K KK) \<union> C"
   171 by 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 
   177 lemmas analz_image_freshK_simps =
   178        simp_thms mem_simps --{*these two allow its use with @{text "only:"}*}
   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*)
   186 lemma analz_image_freshK_lemma:
   187      "(Key K \<in> analz (Key`nE \<union> H)) --> (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)"
   189 by (blast intro: analz_mono [THEN [2] rev_subsetD])
   190 
   191 
   192 subsection{*Tactics for possibility theorems*}
   193 
   194 ML
   195 {*
   196 structure Shared =
   197 struct
   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*)
   201 fun 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*)
   212 fun 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 
   219 val 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 
   225 end
   226 *}
   227 
   228 
   229 
   230 (*Lets blast_tac perform this step without needing the simplifier*)
   231 lemma invKey_shrK_iff [iff]:
   232      "(Key (invKey K) \<in> X) = (Key K \<in> X)"
   233 by auto
   234 
   235 (*Specialized methods*)
   236 
   237 method_setup analz_freshK = {*
   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))]))) *}
   243     "for proving the Session Key Compromise theorem"
   244 
   245 method_setup possibility = {*
   246     Scan.succeed (fn ctxt => SIMPLE_METHOD (Shared.possibility_tac ctxt)) *}
   247     "for proving possibility theorems"
   248 
   249 method_setup basic_possibility = {*
   250     Scan.succeed (fn ctxt => SIMPLE_METHOD (Shared.basic_possibility_tac ctxt)) *}
   251     "for proving possibility theorems"
   252 
   253 lemma knows_subset_knows_Cons: "knows A evs <= knows A (e # evs)"
   254 by (cases e) (auto simp: knows_Cons)
   255 
   256 end