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