src/HOL/Auth/Smartcard/Smartcard.thy
author haftmann
Mon Mar 01 13:40:23 2010 +0100 (2010-03-01 ago)
changeset 35416 d8d7d1b785af
parent 32960 69916a850301
child 39246 9e58f0499f57
permissions -rw-r--r--
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
     1 (* Author:     Giampaolo Bella, Catania University
     2 *)
     3 
     4 header{*Theory of smartcards*}
     5 
     6 theory Smartcard
     7 imports EventSC All_Symmetric
     8 begin
     9 
    10 text{*  
    11 As smartcards handle long-term (symmetric) keys, this theoy extends and 
    12 supersedes theory Private.thy
    13 
    14 An agent is bad if she reveals her PIN to the spy, not the shared key that
    15 is embedded in her card. An agent's being bad implies nothing about her 
    16 smartcard, which independently may be stolen or cloned.
    17 *}
    18 
    19 consts
    20   shrK    :: "agent => key"  (*long-term keys saved in smart cards*)
    21   crdK    :: "card  => key"  (*smart cards' symmetric keys*)
    22   pin     :: "agent => key"  (*pin to activate the smart cards*)
    23 
    24   (*Mostly for Shoup-Rubin*)
    25   Pairkey :: "agent * agent => nat"
    26   pairK   :: "agent * agent => key"
    27 
    28 axioms
    29   inj_shrK: "inj shrK"  --{*No two smartcards store the same key*}
    30   inj_crdK: "inj crdK"  --{*Nor do two cards*}
    31   inj_pin : "inj pin"   --{*Nor do two agents have the same pin*}
    32 
    33   (*pairK is injective on each component, if we assume encryption to be a PRF
    34     or at least collision free *)
    35   inj_pairK    [iff]: "(pairK(A,B) = pairK(A',B')) = (A = A' & B = B')"
    36   comm_Pairkey [iff]: "Pairkey(A,B) = Pairkey(B,A)"
    37 
    38   (*long-term keys differ from each other*)
    39   pairK_disj_crdK [iff]: "pairK(A,B) \<noteq> crdK C"
    40   pairK_disj_shrK [iff]: "pairK(A,B) \<noteq> shrK P"
    41   pairK_disj_pin [iff]:  "pairK(A,B) \<noteq> pin P"
    42   shrK_disj_crdK [iff]:  "shrK P \<noteq> crdK C"
    43   shrK_disj_pin [iff]:  "shrK P \<noteq> pin Q"
    44   crdK_disj_pin [iff]:   "crdK C \<noteq> pin P"
    45 
    46 definition legalUse :: "card => bool" ("legalUse (_)") where
    47   "legalUse C == C \<notin> stolen"
    48 
    49 primrec illegalUse :: "card  => bool" where
    50   illegalUse_def: "illegalUse (Card A) = ( (Card A \<in> stolen \<and> A \<in> bad)  \<or>  Card A \<in> cloned )"
    51 
    52 
    53 text{*initState must be defined with care*}
    54 primrec
    55 (*Server knows all long-term keys; adding cards' keys may be redundant but
    56   helps prove crdK_in_initState and crdK_in_used to distinguish cards' keys
    57   from fresh (session) keys*)
    58   initState_Server:  "initState Server = 
    59         (Key`(range shrK \<union> range crdK \<union> range pin \<union> range pairK)) \<union> 
    60         (Nonce`(range Pairkey))"
    61 
    62 (*Other agents know only their own*)
    63   initState_Friend:  "initState (Friend i) = {Key (pin (Friend i))}"
    64 
    65 (*Spy knows bad agents' pins, cloned cards' keys, pairKs, and Pairkeys *)
    66   initState_Spy: "initState Spy  = 
    67                  (Key`((pin`bad) \<union> (pin `{A. Card A \<in> cloned}) \<union> 
    68                                       (shrK`{A. Card A \<in> cloned}) \<union> 
    69                         (crdK`cloned) \<union> 
    70                         (pairK`{(X,A). Card A \<in> cloned})))
    71            \<union> (Nonce`(Pairkey`{(A,B). Card A \<in> cloned & Card B \<in> cloned}))"
    72 
    73 
    74 text{*Still relying on axioms*}
    75 axioms
    76   Key_supply_ax:  "finite KK \<Longrightarrow> \<exists> K. K \<notin> KK & Key K \<notin> used evs"
    77 
    78   (*Needed because of Spy's knowledge of Pairkeys*)
    79   Nonce_supply_ax: "finite NN \<Longrightarrow> \<exists> N. N \<notin> NN & Nonce N \<notin> used evs"
    80 
    81 
    82 
    83 
    84 
    85 
    86 
    87 subsection{*Basic properties of shrK*}
    88 
    89 (*Injectiveness: Agents' long-term keys are distinct.*)
    90 declare inj_shrK [THEN inj_eq, iff]
    91 declare inj_crdK [THEN inj_eq, iff]
    92 declare inj_pin  [THEN inj_eq, iff]
    93 
    94 lemma invKey_K [simp]: "invKey K = K"
    95 apply (insert isSym_keys)
    96 apply (simp add: symKeys_def) 
    97 done
    98 
    99 
   100 lemma analz_Decrypt' [dest]:
   101      "\<lbrakk> Crypt K X \<in> analz H;  Key K  \<in> analz H \<rbrakk> \<Longrightarrow> X \<in> analz H"
   102 by auto
   103 
   104 text{*Now cancel the @{text dest} attribute given to
   105  @{text analz.Decrypt} in its declaration.*}
   106 declare analz.Decrypt [rule del]
   107 
   108 text{*Rewrites should not refer to  @{term "initState(Friend i)"} because
   109   that expression is not in normal form.*}
   110 
   111 text{*Added to extend initstate with set of nonces*}
   112 lemma parts_image_Nonce [simp]: "parts (Nonce`N) = Nonce`N"
   113 apply auto
   114 apply (erule parts.induct)
   115 apply auto
   116 done
   117 
   118 lemma keysFor_parts_initState [simp]: "keysFor (parts (initState C)) = {}"
   119 apply (unfold keysFor_def)
   120 apply (induct_tac "C", auto)
   121 done
   122 
   123 (*Specialized to shared-key model: no @{term invKey}*)
   124 lemma keysFor_parts_insert:
   125      "\<lbrakk> K \<in> keysFor (parts (insert X G));  X \<in> synth (analz H) \<rbrakk> 
   126      \<Longrightarrow> K \<in> keysFor (parts (G \<union> H)) | Key K \<in> parts H";
   127 by (force dest: EventSC.keysFor_parts_insert)  
   128 
   129 lemma Crypt_imp_keysFor: "Crypt K X \<in> H \<Longrightarrow> K \<in> keysFor H"
   130 by (drule Crypt_imp_invKey_keysFor, simp)
   131 
   132 
   133 subsection{*Function "knows"*}
   134 
   135 (*Spy knows the pins of bad agents!*)
   136 lemma Spy_knows_bad [intro!]: "A \<in> bad \<Longrightarrow> Key (pin A) \<in> knows Spy evs"
   137 apply (induct_tac "evs")
   138 apply (simp_all (no_asm_simp) add: imageI knows_Cons split add: event.split)
   139 done
   140 
   141 (*Spy knows the long-term keys of cloned cards!*)
   142 lemma Spy_knows_cloned [intro!]: 
   143      "Card A \<in> cloned \<Longrightarrow>  Key (crdK (Card A)) \<in> knows Spy evs &   
   144                            Key (shrK A) \<in> knows Spy evs &  
   145                            Key (pin A)  \<in> knows Spy evs &  
   146                           (\<forall> B. Key (pairK(B,A)) \<in> knows Spy evs)"
   147 apply (induct_tac "evs")
   148 apply (simp_all (no_asm_simp) add: imageI knows_Cons split add: event.split)
   149 done
   150 
   151 lemma Spy_knows_cloned1 [intro!]: "C \<in> cloned \<Longrightarrow> Key (crdK C) \<in> knows Spy evs"
   152 apply (induct_tac "evs")
   153 apply (simp_all (no_asm_simp) add: imageI knows_Cons split add: event.split)
   154 done
   155 
   156 lemma Spy_knows_cloned2 [intro!]: "\<lbrakk> Card A \<in> cloned; Card B \<in> cloned \<rbrakk>  
   157    \<Longrightarrow> Nonce (Pairkey(A,B))\<in> knows Spy evs"
   158 apply (induct_tac "evs")
   159 apply (simp_all (no_asm_simp) add: imageI knows_Cons split add: event.split)
   160 done
   161 
   162 (*Spy only knows pins of bad agents!*)
   163 lemma Spy_knows_Spy_bad [intro!]: "A\<in> bad \<Longrightarrow> Key (pin A) \<in> knows Spy evs"
   164 apply (induct_tac "evs")
   165 apply (simp_all (no_asm_simp) add: imageI knows_Cons split add: event.split)
   166 done
   167 
   168 
   169 (*For case analysis on whether or not an agent is compromised*)
   170 lemma Crypt_Spy_analz_bad: 
   171   "\<lbrakk> Crypt (pin A) X \<in> analz (knows Spy evs);  A\<in>bad \<rbrakk>   
   172       \<Longrightarrow> X \<in> analz (knows Spy evs)"
   173 apply (force dest!: analz.Decrypt)
   174 done
   175 
   176 (** Fresh keys never clash with other keys **)
   177 
   178 lemma shrK_in_initState [iff]: "Key (shrK A) \<in> initState Server"
   179 apply (induct_tac "A")
   180 apply auto
   181 done
   182 
   183 lemma shrK_in_used [iff]: "Key (shrK A) \<in> used evs"
   184 apply (rule initState_into_used)
   185 apply blast
   186 done
   187 
   188 lemma crdK_in_initState [iff]: "Key (crdK A) \<in> initState Server"
   189 apply (induct_tac "A")
   190 apply auto
   191 done
   192 
   193 lemma crdK_in_used [iff]: "Key (crdK A) \<in> used evs"
   194 apply (rule initState_into_used)
   195 apply blast
   196 done
   197 
   198 lemma pin_in_initState [iff]: "Key (pin A) \<in> initState A"
   199 apply (induct_tac "A")
   200 apply auto
   201 done
   202 
   203 lemma pin_in_used [iff]: "Key (pin A) \<in> used evs"
   204 apply (rule initState_into_used)
   205 apply blast
   206 done
   207 
   208 lemma pairK_in_initState [iff]: "Key (pairK X) \<in> initState Server"
   209 apply (induct_tac "X")
   210 apply auto
   211 done
   212 
   213 lemma pairK_in_used [iff]: "Key (pairK X) \<in> used evs"
   214 apply (rule initState_into_used)
   215 apply blast
   216 done
   217 
   218 
   219 
   220 (*Used in parts_induct_tac and analz_Fake_tac to distinguish session keys
   221   from long-term shared keys*)
   222 lemma Key_not_used [simp]: "Key K \<notin> used evs \<Longrightarrow> K \<notin> range shrK"
   223 by blast
   224 
   225 lemma shrK_neq [simp]: "Key K \<notin> used evs \<Longrightarrow> shrK B \<noteq> K"
   226 by blast
   227 
   228 lemma crdK_not_used [simp]: "Key K \<notin> used evs \<Longrightarrow> K \<notin> range crdK"
   229 apply clarify
   230 done
   231 
   232 lemma crdK_neq [simp]: "Key K \<notin> used evs \<Longrightarrow> crdK C \<noteq> K"
   233 apply clarify
   234 done
   235 
   236 lemma pin_not_used [simp]: "Key K \<notin> used evs \<Longrightarrow> K \<notin> range pin"
   237 apply clarify
   238 done
   239 
   240 lemma pin_neq [simp]: "Key K \<notin> used evs \<Longrightarrow> pin A \<noteq> K"
   241 apply clarify
   242 done
   243 
   244 lemma pairK_not_used [simp]: "Key K \<notin> used evs \<Longrightarrow> K \<notin> range pairK"
   245 apply clarify
   246 done
   247 
   248 lemma pairK_neq [simp]: "Key K \<notin> used evs \<Longrightarrow> pairK(A,B) \<noteq> K"
   249 apply clarify
   250 done
   251 
   252 declare shrK_neq [THEN not_sym, simp]
   253 declare crdK_neq [THEN not_sym, simp]
   254 declare pin_neq [THEN not_sym, simp]
   255 declare pairK_neq [THEN not_sym, simp]
   256 
   257 
   258 subsection{*Fresh nonces*}
   259 
   260 lemma Nonce_notin_initState [iff]: "Nonce N \<notin> parts (initState (Friend i))"
   261 by auto
   262 
   263 
   264 (*This lemma no longer holds of smartcard protocols, where the cards can store
   265   nonces.
   266 
   267 lemma Nonce_notin_used_empty [simp]: "Nonce N \<notin> used []"
   268 apply (simp (no_asm) add: used_Nil)
   269 done
   270 
   271 So, we must use old-style supply fresh nonce theorems relying on the appropriate axiom*)
   272 
   273 
   274 subsection{*Supply fresh nonces for possibility theorems.*}
   275 
   276 
   277 lemma Nonce_supply1: "\<exists>N. Nonce N \<notin> used evs"
   278 apply (rule finite.emptyI [THEN Nonce_supply_ax, THEN exE], blast)
   279 done
   280 
   281 lemma Nonce_supply2: 
   282   "\<exists>N N'. Nonce N \<notin> used evs & Nonce N' \<notin> used evs' & N \<noteq> N'"
   283 apply (cut_tac evs = evs in finite.emptyI [THEN Nonce_supply_ax])
   284 apply (erule exE)
   285 apply (cut_tac evs = evs' in finite.emptyI [THEN finite.insertI, THEN Nonce_supply_ax]) 
   286 apply auto
   287 done
   288 
   289 
   290 lemma Nonce_supply3: "\<exists>N N' N''. Nonce N \<notin> used evs & Nonce N' \<notin> used evs' &  
   291                     Nonce N'' \<notin> used evs'' & N \<noteq> N' & N' \<noteq> N'' & N \<noteq> N''"
   292 apply (cut_tac evs = evs in finite.emptyI [THEN Nonce_supply_ax])
   293 apply (erule exE)
   294 apply (cut_tac evs = evs' and a1 = N in finite.emptyI [THEN finite.insertI, THEN Nonce_supply_ax]) 
   295 apply (erule exE)
   296 apply (cut_tac evs = evs'' and a1 = Na and a2 = N in finite.emptyI [THEN finite.insertI, THEN finite.insertI, THEN Nonce_supply_ax]) 
   297 apply blast
   298 done
   299 
   300 lemma Nonce_supply: "Nonce (@ N. Nonce N \<notin> used evs) \<notin> used evs"
   301 apply (rule finite.emptyI [THEN Nonce_supply_ax, THEN exE])
   302 apply (rule someI, blast)
   303 done
   304 
   305 
   306 
   307 text{*Unlike the corresponding property of nonces, we cannot prove
   308     @{term "finite KK \<Longrightarrow> \<exists>K. K \<notin> KK & Key K \<notin> used evs"}.
   309     We have infinitely many agents and there is nothing to stop their
   310     long-term keys from exhausting all the natural numbers.  Instead,
   311     possibility theorems must assume the existence of a few keys.*}
   312 
   313 
   314 subsection{*Specialized Rewriting for Theorems About @{term analz} and Image*}
   315 
   316 lemma subset_Compl_range_shrK: "A \<subseteq> - (range shrK) \<Longrightarrow> shrK x \<notin> A"
   317 by blast
   318 
   319 lemma subset_Compl_range_crdK: "A \<subseteq> - (range crdK) \<Longrightarrow> crdK x \<notin> A"
   320 apply blast
   321 done
   322 
   323 lemma subset_Compl_range_pin: "A \<subseteq> - (range pin) \<Longrightarrow> pin x \<notin> A"
   324 apply blast
   325 done
   326 
   327 lemma subset_Compl_range_pairK: "A \<subseteq> - (range pairK) \<Longrightarrow> pairK x \<notin> A"
   328 apply blast
   329 done
   330 lemma insert_Key_singleton: "insert (Key K) H = Key ` {K} \<union> H"
   331 by blast
   332 
   333 lemma insert_Key_image: "insert (Key K) (Key`KK \<union> C) = Key`(insert K KK) \<union> C"
   334 by blast
   335 
   336 (** Reverse the normal simplification of "image" to build up (not break down)
   337     the set of keys.  Use analz_insert_eq with (Un_upper2 RS analz_mono) to
   338     erase occurrences of forwarded message components (X). **)
   339 
   340 lemmas analz_image_freshK_simps =
   341        simp_thms mem_simps --{*these two allow its use with @{text "only:"}*}
   342        disj_comms 
   343        image_insert [THEN sym] image_Un [THEN sym] empty_subsetI insert_subset
   344        analz_insert_eq Un_upper2 [THEN analz_mono, THEN [2] rev_subsetD]
   345        insert_Key_singleton subset_Compl_range_shrK subset_Compl_range_crdK
   346        subset_Compl_range_pin subset_Compl_range_pairK
   347        Key_not_used insert_Key_image Un_assoc [THEN sym]
   348 
   349 (*Lemma for the trivial direction of the if-and-only-if*)
   350 lemma analz_image_freshK_lemma:
   351      "(Key K \<in> analz (Key`nE \<union> H)) \<longrightarrow> (K \<in> nE | Key K \<in> analz H)  \<Longrightarrow>  
   352          (Key K \<in> analz (Key`nE \<union> H)) = (K \<in> nE | Key K \<in> analz H)"
   353 by (blast intro: analz_mono [THEN [2] rev_subsetD])
   354 
   355 
   356 subsection{*Tactics for possibility theorems*}
   357 
   358 ML
   359 {*
   360 structure Smartcard =
   361 struct
   362 
   363 (*Omitting used_Says makes the tactic much faster: it leaves expressions
   364     such as  Nonce ?N \<notin> used evs that match Nonce_supply*)
   365 fun possibility_tac ctxt =
   366    (REPEAT 
   367     (ALLGOALS (simp_tac (simpset_of ctxt
   368       delsimps [@{thm used_Says}, @{thm used_Notes}, @{thm used_Gets},
   369         @{thm used_Inputs}, @{thm used_C_Gets}, @{thm used_Outpts}, @{thm used_A_Gets}] 
   370       setSolver safe_solver))
   371      THEN
   372      REPEAT_FIRST (eq_assume_tac ORELSE' 
   373                    resolve_tac [refl, conjI, @{thm Nonce_supply}])))
   374 
   375 (*For harder protocols (such as Recur) where we have to set up some
   376   nonces and keys initially*)
   377 fun basic_possibility_tac ctxt =
   378     REPEAT 
   379     (ALLGOALS (asm_simp_tac (simpset_of ctxt setSolver safe_solver))
   380      THEN
   381      REPEAT_FIRST (resolve_tac [refl, conjI]))
   382 
   383 val analz_image_freshK_ss = 
   384      @{simpset} delsimps [image_insert, image_Un]
   385                delsimps [@{thm imp_disjL}]    (*reduces blow-up*)
   386                addsimps @{thms analz_image_freshK_simps}
   387 end
   388 *}
   389 
   390 
   391 (*Lets blast_tac perform this step without needing the simplifier*)
   392 lemma invKey_shrK_iff [iff]:
   393      "(Key (invKey K) \<in> X) = (Key K \<in> X)"
   394 by auto
   395 
   396 (*Specialized methods*)
   397 
   398 method_setup analz_freshK = {*
   399     Scan.succeed (fn ctxt =>
   400      (SIMPLE_METHOD
   401       (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
   402           REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
   403           ALLGOALS (asm_simp_tac (Simplifier.context ctxt Smartcard.analz_image_freshK_ss))]))) *}
   404     "for proving the Session Key Compromise theorem"
   405 
   406 method_setup possibility = {*
   407     Scan.succeed (fn ctxt =>
   408         SIMPLE_METHOD (Smartcard.possibility_tac ctxt)) *}
   409     "for proving possibility theorems"
   410 
   411 method_setup basic_possibility = {*
   412     Scan.succeed (fn ctxt =>
   413         SIMPLE_METHOD (Smartcard.basic_possibility_tac ctxt)) *}
   414     "for proving possibility theorems"
   415 
   416 lemma knows_subset_knows_Cons: "knows A evs \<subseteq> knows A (e # evs)"
   417 by (induct e) (auto simp: knows_Cons)
   418 
   419 (*Needed for actual protocols that will follow*)
   420 declare shrK_disj_crdK[THEN not_sym, iff]
   421 declare shrK_disj_pin[THEN not_sym, iff]
   422 declare pairK_disj_shrK[THEN not_sym, iff]
   423 declare pairK_disj_crdK[THEN not_sym, iff]
   424 declare pairK_disj_pin[THEN not_sym, iff]
   425 declare crdK_disj_pin[THEN not_sym, iff]
   426 
   427 declare legalUse_def [iff] illegalUse_def [iff]
   428 
   429 end