src/HOL/SET_Protocol/Public_SET.thy
author wenzelm
Sat Jul 18 22:58:50 2015 +0200 (2015-07-18)
changeset 60758 d8d85a8172b5
parent 59498 50b60f501b05
child 61984 cdea44c775fa
permissions -rw-r--r--
isabelle update_cartouches;
     1 (*  Title:      HOL/SET_Protocol/Public_SET.thy
     2     Author:     Giampaolo Bella
     3     Author:     Fabio Massacci
     4     Author:     Lawrence C Paulson
     5 *)
     6 
     7 section{*The Public-Key Theory, Modified for SET*}
     8 
     9 theory Public_SET
    10 imports Event_SET
    11 begin
    12 
    13 subsection{*Symmetric and Asymmetric Keys*}
    14 
    15 text{*definitions influenced by the wish to assign asymmetric keys 
    16   - since the beginning - only to RCA and CAs, namely we need a partial 
    17   function on type Agent*}
    18 
    19 
    20 text{*The SET specs mention two signature keys for CAs - we only have one*}
    21 
    22 consts
    23   publicKey :: "[bool, agent] => key"
    24     --{*the boolean is TRUE if a signing key*}
    25 
    26 abbreviation "pubEK == publicKey False"
    27 abbreviation "pubSK == publicKey True"
    28 
    29 (*BEWARE!! priEK, priSK DON'T WORK with inj, range, image, etc.*)
    30 abbreviation "priEK A == invKey (pubEK A)"
    31 abbreviation "priSK A == invKey (pubSK A)"
    32 
    33 text{*By freeness of agents, no two agents have the same key. Since
    34  @{term "True\<noteq>False"}, no agent has the same signing and encryption keys.*}
    35 
    36 specification (publicKey)
    37   injective_publicKey:
    38     "publicKey b A = publicKey c A' ==> b=c & A=A'"
    39 (*<*)
    40    apply (rule exI [of _ "%b A. 2 * nat_of_agent A + (if b then 1 else 0)"]) 
    41    apply (auto simp add: inj_on_def inj_nat_of_agent [THEN inj_eq] split: agent.split) 
    42    apply (drule_tac f="%x. x mod 2" in arg_cong, simp add: mod_Suc)+
    43 (*or this, but presburger won't abstract out the function applications
    44    apply presburger+
    45 *)
    46    done                       
    47 (*>*)
    48 
    49 axiomatization where
    50   (*No private key equals any public key (essential to ensure that private
    51     keys are private!) *)
    52   privateKey_neq_publicKey [iff]:
    53       "invKey (publicKey b A) \<noteq> publicKey b' A'"
    54 
    55 declare privateKey_neq_publicKey [THEN not_sym, iff]
    56 
    57   
    58 subsection{*Initial Knowledge*}
    59 
    60 text{*This information is not necessary.  Each protocol distributes any needed
    61 certificates, and anyway our proofs require a formalization of the Spy's 
    62 knowledge only.  However, the initial knowledge is as follows:
    63    All agents know RCA's public keys;
    64    RCA and CAs know their own respective keys;
    65    RCA (has already certified and therefore) knows all CAs public keys; 
    66    Spy knows all keys of all bad agents.*}
    67 
    68 overloading initState \<equiv> "initState"
    69 begin
    70 
    71 primrec initState where
    72 (*<*)
    73   initState_CA:
    74     "initState (CA i)  =
    75        (if i=0 then Key ` ({priEK RCA, priSK RCA} Un
    76                             pubEK ` (range CA) Un pubSK ` (range CA))
    77         else {Key (priEK (CA i)), Key (priSK (CA i)),
    78               Key (pubEK (CA i)), Key (pubSK (CA i)),
    79               Key (pubEK RCA), Key (pubSK RCA)})"
    80 
    81 | initState_Cardholder:
    82     "initState (Cardholder i)  =    
    83        {Key (priEK (Cardholder i)), Key (priSK (Cardholder i)),
    84         Key (pubEK (Cardholder i)), Key (pubSK (Cardholder i)),
    85         Key (pubEK RCA), Key (pubSK RCA)}"
    86 
    87 | initState_Merchant:
    88     "initState (Merchant i)  =    
    89        {Key (priEK (Merchant i)), Key (priSK (Merchant i)),
    90         Key (pubEK (Merchant i)), Key (pubSK (Merchant i)),
    91         Key (pubEK RCA), Key (pubSK RCA)}"
    92 
    93 | initState_PG:
    94     "initState (PG i)  = 
    95        {Key (priEK (PG i)), Key (priSK (PG i)),
    96         Key (pubEK (PG i)), Key (pubSK (PG i)),
    97         Key (pubEK RCA), Key (pubSK RCA)}"
    98 (*>*)
    99 | initState_Spy:
   100     "initState Spy = Key ` (invKey ` pubEK ` bad Un
   101                             invKey ` pubSK ` bad Un
   102                             range pubEK Un range pubSK)"
   103 
   104 end
   105 
   106 
   107 text{*Injective mapping from agents to PANs: an agent can have only one card*}
   108 
   109 consts  pan :: "agent => nat"
   110 
   111 specification (pan)
   112   inj_pan: "inj pan"
   113   --{*No two agents have the same PAN*}
   114 (*<*)
   115    apply (rule exI [of _ "nat_of_agent"]) 
   116    apply (simp add: inj_on_def inj_nat_of_agent [THEN inj_eq]) 
   117    done
   118 (*>*)
   119 
   120 declare inj_pan [THEN inj_eq, iff]
   121 
   122 consts
   123   XOR :: "nat*nat => nat"  --{*no properties are assumed of exclusive-or*}
   124 
   125 
   126 subsection{*Signature Primitives*}
   127 
   128 definition
   129  (* Signature = Message + signed Digest *)
   130   sign :: "[key, msg]=>msg"
   131   where "sign K X = {|X, Crypt K (Hash X) |}"
   132 
   133 definition
   134  (* Signature Only = signed Digest Only *)
   135   signOnly :: "[key, msg]=>msg"
   136   where "signOnly K X = Crypt K (Hash X)"
   137 
   138 definition
   139  (* Signature for Certificates = Message + signed Message *)
   140   signCert :: "[key, msg]=>msg"
   141   where "signCert K X = {|X, Crypt K X |}"
   142 
   143 definition
   144  (* Certification Authority's Certificate.
   145     Contains agent name, a key, a number specifying the key's target use,
   146               a key to sign the entire certificate.
   147 
   148     Should prove if signK=priSK RCA and C=CA i,
   149                   then Ka=pubEK i or pubSK i depending on T  ??
   150  *)
   151   cert :: "[agent, key, msg, key] => msg"
   152   where "cert A Ka T signK = signCert signK {|Agent A, Key Ka, T|}"
   153 
   154 definition
   155  (* Cardholder's Certificate.
   156     Contains a PAN, the certified key Ka, the PANSecret PS,
   157     a number specifying the target use for Ka, the signing key signK.
   158  *)
   159   certC :: "[nat, key, nat, msg, key] => msg"
   160   where "certC PAN Ka PS T signK =
   161     signCert signK {|Hash {|Nonce PS, Pan PAN|}, Key Ka, T|}"
   162 
   163 (*cert and certA have no repeated elements, so they could be abbreviations,
   164   but that's tricky and makes proofs slower*)
   165 
   166 abbreviation "onlyEnc == Number 0"
   167 abbreviation "onlySig == Number (Suc 0)"
   168 abbreviation "authCode == Number (Suc (Suc 0))"
   169 
   170 subsection{*Encryption Primitives*}
   171 
   172 definition EXcrypt :: "[key,key,msg,msg] => msg" where
   173   --{*Extra Encryption*}
   174     (*K: the symmetric key   EK: the public encryption key*)
   175     "EXcrypt K EK M m =
   176        {|Crypt K {|M, Hash m|}, Crypt EK {|Key K, m|}|}"
   177 
   178 definition EXHcrypt :: "[key,key,msg,msg] => msg" where
   179   --{*Extra Encryption with Hashing*}
   180     (*K: the symmetric key   EK: the public encryption key*)
   181     "EXHcrypt K EK M m =
   182        {|Crypt K {|M, Hash m|}, Crypt EK {|Key K, m, Hash M|}|}"
   183 
   184 definition Enc :: "[key,key,key,msg] => msg" where
   185   --{*Simple Encapsulation with SIGNATURE*}
   186     (*SK: the sender's signing key
   187       K: the symmetric key
   188       EK: the public encryption key*)
   189     "Enc SK K EK M =
   190        {|Crypt K (sign SK M), Crypt EK (Key K)|}"
   191 
   192 definition EncB :: "[key,key,key,msg,msg] => msg" where
   193   --{*Encapsulation with Baggage.  Keys as above, and baggage b.*}
   194     "EncB SK K EK M b =
   195        {|Enc SK K EK {|M, Hash b|}, b|}"
   196 
   197 
   198 subsection{*Basic Properties of pubEK, pubSK, priEK and priSK *}
   199 
   200 lemma publicKey_eq_iff [iff]:
   201      "(publicKey b A = publicKey b' A') = (b=b' & A=A')"
   202 by (blast dest: injective_publicKey)
   203 
   204 lemma privateKey_eq_iff [iff]:
   205      "(invKey (publicKey b A) = invKey (publicKey b' A')) = (b=b' & A=A')"
   206 by auto
   207 
   208 lemma not_symKeys_publicKey [iff]: "publicKey b A \<notin> symKeys"
   209 by (simp add: symKeys_def)
   210 
   211 lemma not_symKeys_privateKey [iff]: "invKey (publicKey b A) \<notin> symKeys"
   212 by (simp add: symKeys_def)
   213 
   214 lemma symKeys_invKey_eq [simp]: "K \<in> symKeys ==> invKey K = K"
   215 by (simp add: symKeys_def)
   216 
   217 lemma symKeys_invKey_iff [simp]: "(invKey K \<in> symKeys) = (K \<in> symKeys)"
   218 by (unfold symKeys_def, auto)
   219 
   220 text{*Can be slow (or even loop) as a simprule*}
   221 lemma symKeys_neq_imp_neq: "(K \<in> symKeys) \<noteq> (K' \<in> symKeys) ==> K \<noteq> K'"
   222 by blast
   223 
   224 text{*These alternatives to @{text symKeys_neq_imp_neq} don't seem any better
   225 in practice.*}
   226 lemma publicKey_neq_symKey: "K \<in> symKeys ==> publicKey b A \<noteq> K"
   227 by blast
   228 
   229 lemma symKey_neq_publicKey: "K \<in> symKeys ==> K \<noteq> publicKey b A"
   230 by blast
   231 
   232 lemma privateKey_neq_symKey: "K \<in> symKeys ==> invKey (publicKey b A) \<noteq> K"
   233 by blast
   234 
   235 lemma symKey_neq_privateKey: "K \<in> symKeys ==> K \<noteq> invKey (publicKey b A)"
   236 by blast
   237 
   238 lemma analz_symKeys_Decrypt:
   239      "[| Crypt K X \<in> analz H;  K \<in> symKeys;  Key K \<in> analz H |]  
   240       ==> X \<in> analz H"
   241 by auto
   242 
   243 
   244 subsection{*"Image" Equations That Hold for Injective Functions *}
   245 
   246 lemma invKey_image_eq [iff]: "(invKey x \<in> invKey`A) = (x\<in>A)"
   247 by auto
   248 
   249 text{*holds because invKey is injective*}
   250 lemma publicKey_image_eq [iff]:
   251      "(publicKey b A \<in> publicKey c ` AS) = (b=c & A\<in>AS)"
   252 by auto
   253 
   254 lemma privateKey_image_eq [iff]:
   255      "(invKey (publicKey b A) \<in> invKey ` publicKey c ` AS) = (b=c & A\<in>AS)"
   256 by auto
   257 
   258 lemma privateKey_notin_image_publicKey [iff]:
   259      "invKey (publicKey b A) \<notin> publicKey c ` AS"
   260 by auto
   261 
   262 lemma publicKey_notin_image_privateKey [iff]:
   263      "publicKey b A \<notin> invKey ` publicKey c ` AS"
   264 by auto
   265 
   266 lemma keysFor_parts_initState [simp]: "keysFor (parts (initState C)) = {}"
   267 apply (simp add: keysFor_def)
   268 apply (induct_tac "C")
   269 apply (auto intro: range_eqI)
   270 done
   271 
   272 text{*for proving @{text new_keys_not_used}*}
   273 lemma keysFor_parts_insert:
   274      "[| K \<in> keysFor (parts (insert X H));  X \<in> synth (analz H) |]  
   275       ==> K \<in> keysFor (parts H) | Key (invKey K) \<in> parts H"
   276 by (force dest!: 
   277          parts_insert_subset_Un [THEN keysFor_mono, THEN [2] rev_subsetD]
   278          analz_subset_parts [THEN keysFor_mono, THEN [2] rev_subsetD] 
   279             intro: analz_into_parts)
   280 
   281 lemma Crypt_imp_keysFor [intro]:
   282      "[|K \<in> symKeys; Crypt K X \<in> H|] ==> K \<in> keysFor H"
   283 by (drule Crypt_imp_invKey_keysFor, simp)
   284 
   285 text{*Agents see their own private keys!*}
   286 lemma privateKey_in_initStateCA [iff]:
   287      "Key (invKey (publicKey b A)) \<in> initState A"
   288 by (case_tac "A", auto)
   289 
   290 text{*Agents see their own public keys!*}
   291 lemma publicKey_in_initStateCA [iff]: "Key (publicKey b A) \<in> initState A"
   292 by (case_tac "A", auto)
   293 
   294 text{*RCA sees CAs' public keys! *}
   295 lemma pubK_CA_in_initState_RCA [iff]:
   296      "Key (publicKey b (CA i)) \<in> initState RCA"
   297 by auto
   298 
   299 
   300 text{*Spy knows all public keys*}
   301 lemma knows_Spy_pubEK_i [iff]: "Key (publicKey b A) \<in> knows Spy evs"
   302 apply (induct_tac "evs")
   303 apply (simp_all add: imageI knows_Cons split add: event.split)
   304 done
   305 
   306 declare knows_Spy_pubEK_i [THEN analz.Inj, iff]
   307                             (*needed????*)
   308 
   309 text{*Spy sees private keys of bad agents! [and obviously public keys too]*}
   310 lemma knows_Spy_bad_privateKey [intro!]:
   311      "A \<in> bad ==> Key (invKey (publicKey b A)) \<in> knows Spy evs"
   312 by (rule initState_subset_knows [THEN subsetD], simp)
   313 
   314 
   315 subsection{*Fresh Nonces for Possibility Theorems*}
   316 
   317 lemma Nonce_notin_initState [iff]: "Nonce N \<notin> parts (initState B)"
   318 by (induct_tac "B", auto)
   319 
   320 lemma Nonce_notin_used_empty [simp]: "Nonce N \<notin> used []"
   321 by (simp add: used_Nil)
   322 
   323 text{*In any trace, there is an upper bound N on the greatest nonce in use.*}
   324 lemma Nonce_supply_lemma: "\<exists>N. \<forall>n. N<=n --> Nonce n \<notin> used evs"
   325 apply (induct_tac "evs")
   326 apply (rule_tac x = 0 in exI)
   327 apply (simp_all add: used_Cons split add: event.split, safe)
   328 apply (rule msg_Nonce_supply [THEN exE], blast elim!: add_leE)+
   329 done
   330 
   331 lemma Nonce_supply1: "\<exists>N. Nonce N \<notin> used evs"
   332 by (rule Nonce_supply_lemma [THEN exE], blast)
   333 
   334 lemma Nonce_supply: "Nonce (@ N. Nonce N \<notin> used evs) \<notin> used evs"
   335 apply (rule Nonce_supply_lemma [THEN exE])
   336 apply (rule someI, fast)
   337 done
   338 
   339 
   340 subsection{*Specialized Methods for Possibility Theorems*}
   341 
   342 ML
   343 {*
   344 (*Tactic for possibility theorems*)
   345 fun possibility_tac ctxt =
   346     REPEAT (*omit used_Says so that Nonces start from different traces!*)
   347     (ALLGOALS (simp_tac (ctxt delsimps [@{thm used_Says}, @{thm used_Notes}]))
   348      THEN
   349      REPEAT_FIRST (eq_assume_tac ORELSE' 
   350                    resolve_tac ctxt [refl, conjI, @{thm Nonce_supply}]))
   351 
   352 (*For harder protocols (such as SET_CR!), where we have to set up some
   353   nonces and keys initially*)
   354 fun basic_possibility_tac ctxt =
   355     REPEAT 
   356     (ALLGOALS (asm_simp_tac (ctxt setSolver safe_solver))
   357      THEN
   358      REPEAT_FIRST (resolve_tac ctxt [refl, conjI]))
   359 *}
   360 
   361 method_setup possibility = {*
   362     Scan.succeed (SIMPLE_METHOD o possibility_tac) *}
   363     "for proving possibility theorems"
   364 
   365 method_setup basic_possibility = {*
   366     Scan.succeed (SIMPLE_METHOD o basic_possibility_tac) *}
   367     "for proving possibility theorems"
   368 
   369 
   370 subsection{*Specialized Rewriting for Theorems About @{term analz} and Image*}
   371 
   372 lemma insert_Key_singleton: "insert (Key K) H = Key ` {K} Un H"
   373 by blast
   374 
   375 lemma insert_Key_image:
   376      "insert (Key K) (Key`KK Un C) = Key ` (insert K KK) Un C"
   377 by blast
   378 
   379 text{*Needed for @{text DK_fresh_not_KeyCryptKey}*}
   380 lemma publicKey_in_used [iff]: "Key (publicKey b A) \<in> used evs"
   381 by auto
   382 
   383 lemma privateKey_in_used [iff]: "Key (invKey (publicKey b A)) \<in> used evs"
   384 by (blast intro!: initState_into_used)
   385 
   386 text{*Reverse the normal simplification of "image" to build up (not break down)
   387   the set of keys.  Based on @{text analz_image_freshK_ss}, but simpler.*}
   388 lemmas analz_image_keys_simps =
   389        simp_thms mem_simps --{*these two allow its use with @{text "only:"}*}
   390        image_insert [THEN sym] image_Un [THEN sym] 
   391        rangeI symKeys_neq_imp_neq
   392        insert_Key_singleton insert_Key_image Un_assoc [THEN sym]
   393 
   394 
   395 (*General lemmas proved by Larry*)
   396 
   397 subsection{*Controlled Unfolding of Abbreviations*}
   398 
   399 text{*A set is expanded only if a relation is applied to it*}
   400 lemma def_abbrev_simp_relation:
   401      "A = B ==> (A \<in> X) = (B \<in> X) &  
   402                  (u = A) = (u = B) &  
   403                  (A = u) = (B = u)"
   404 by auto
   405 
   406 text{*A set is expanded only if one of the given functions is applied to it*}
   407 lemma def_abbrev_simp_function:
   408      "A = B  
   409       ==> parts (insert A X) = parts (insert B X) &  
   410           analz (insert A X) = analz (insert B X) &  
   411           keysFor (insert A X) = keysFor (insert B X)"
   412 by auto
   413 
   414 subsubsection{*Special Simplification Rules for @{term signCert}*}
   415 
   416 text{*Avoids duplicating X and its components!*}
   417 lemma parts_insert_signCert:
   418      "parts (insert (signCert K X) H) =  
   419       insert {|X, Crypt K X|} (parts (insert (Crypt K X) H))"
   420 by (simp add: signCert_def insert_commute [of X])
   421 
   422 text{*Avoids a case split! [X is always available]*}
   423 lemma analz_insert_signCert:
   424      "analz (insert (signCert K X) H) =  
   425       insert {|X, Crypt K X|} (insert (Crypt K X) (analz (insert X H)))"
   426 by (simp add: signCert_def insert_commute [of X])
   427 
   428 lemma keysFor_insert_signCert: "keysFor (insert (signCert K X) H) = keysFor H"
   429 by (simp add: signCert_def)
   430 
   431 text{*Controlled rewrite rules for @{term signCert}, just the definitions
   432   of the others. Encryption primitives are just expanded, despite their huge
   433   redundancy!*}
   434 lemmas abbrev_simps [simp] =
   435     parts_insert_signCert analz_insert_signCert keysFor_insert_signCert
   436     sign_def     [THEN def_abbrev_simp_relation]
   437     sign_def     [THEN def_abbrev_simp_function]
   438     signCert_def [THEN def_abbrev_simp_relation]
   439     signCert_def [THEN def_abbrev_simp_function]
   440     certC_def    [THEN def_abbrev_simp_relation]
   441     certC_def    [THEN def_abbrev_simp_function]
   442     cert_def     [THEN def_abbrev_simp_relation]
   443     cert_def     [THEN def_abbrev_simp_function]
   444     EXcrypt_def  [THEN def_abbrev_simp_relation]
   445     EXcrypt_def  [THEN def_abbrev_simp_function]
   446     EXHcrypt_def [THEN def_abbrev_simp_relation]
   447     EXHcrypt_def [THEN def_abbrev_simp_function]
   448     Enc_def      [THEN def_abbrev_simp_relation]
   449     Enc_def      [THEN def_abbrev_simp_function]
   450     EncB_def     [THEN def_abbrev_simp_relation]
   451     EncB_def     [THEN def_abbrev_simp_function]
   452 
   453 
   454 subsubsection{*Elimination Rules for Controlled Rewriting *}
   455 
   456 lemma Enc_partsE: 
   457      "!!R. [|Enc SK K EK M \<in> parts H;  
   458              [|Crypt K (sign SK M) \<in> parts H;  
   459                Crypt EK (Key K) \<in> parts H|] ==> R|]  
   460            ==> R"
   461 
   462 by (unfold Enc_def, blast)
   463 
   464 lemma EncB_partsE: 
   465      "!!R. [|EncB SK K EK M b \<in> parts H;  
   466              [|Crypt K (sign SK {|M, Hash b|}) \<in> parts H;  
   467                Crypt EK (Key K) \<in> parts H;  
   468                b \<in> parts H|] ==> R|]  
   469            ==> R"
   470 by (unfold EncB_def Enc_def, blast)
   471 
   472 lemma EXcrypt_partsE: 
   473      "!!R. [|EXcrypt K EK M m \<in> parts H;  
   474              [|Crypt K {|M, Hash m|} \<in> parts H;  
   475                Crypt EK {|Key K, m|} \<in> parts H|] ==> R|]  
   476            ==> R"
   477 by (unfold EXcrypt_def, blast)
   478 
   479 
   480 subsection{*Lemmas to Simplify Expressions Involving @{term analz} *}
   481 
   482 lemma analz_knows_absorb:
   483      "Key K \<in> analz (knows Spy evs)  
   484       ==> analz (Key ` (insert K H) \<union> knows Spy evs) =  
   485           analz (Key ` H \<union> knows Spy evs)"
   486 by (simp add: analz_insert_eq Un_upper2 [THEN analz_mono, THEN subsetD])
   487 
   488 lemma analz_knows_absorb2:
   489      "Key K \<in> analz (knows Spy evs)  
   490       ==> analz (Key ` (insert X (insert K H)) \<union> knows Spy evs) =  
   491           analz (Key ` (insert X H) \<union> knows Spy evs)"
   492 apply (subst insert_commute)
   493 apply (erule analz_knows_absorb)
   494 done
   495 
   496 lemma analz_insert_subset_eq:
   497      "[|X \<in> analz (knows Spy evs);  knows Spy evs \<subseteq> H|]  
   498       ==> analz (insert X H) = analz H"
   499 apply (rule analz_insert_eq)
   500 apply (blast intro: analz_mono [THEN [2] rev_subsetD])
   501 done
   502 
   503 lemmas analz_insert_simps = 
   504          analz_insert_subset_eq Un_upper2
   505          subset_insertI [THEN [2] subset_trans] 
   506 
   507 
   508 subsection{*Freshness Lemmas*}
   509 
   510 lemma in_parts_Says_imp_used:
   511      "[|Key K \<in> parts {X}; Says A B X \<in> set evs|] ==> Key K \<in> used evs"
   512 by (blast intro: parts_trans dest!: Says_imp_knows_Spy [THEN parts.Inj])
   513 
   514 text{*A useful rewrite rule with @{term analz_image_keys_simps}*}
   515 lemma Crypt_notin_image_Key: "Crypt K X \<notin> Key ` KK"
   516 by auto
   517 
   518 lemma fresh_notin_analz_knows_Spy:
   519      "Key K \<notin> used evs ==> Key K \<notin> analz (knows Spy evs)"
   520 by (auto dest: analz_into_parts)
   521 
   522 end