src/HOL/SET_Protocol/Merchant_Registration.thy
author wenzelm
Sat Jul 18 22:58:50 2015 +0200 (2015-07-18)
changeset 60758 d8d85a8172b5
parent 58889 5b7a9633cfa8
child 61984 cdea44c775fa
permissions -rw-r--r--
isabelle update_cartouches;
     1 (*  Title:      HOL/SET_Protocol/Merchant_Registration.thy
     2     Author:     Giampaolo Bella
     3     Author:     Fabio Massacci
     4     Author:     Lawrence C Paulson
     5 *)
     6 
     7 section{*The SET Merchant Registration Protocol*}
     8 
     9 theory Merchant_Registration
    10 imports Public_SET
    11 begin
    12 
    13 text{*Copmpared with Cardholder Reigstration, @{text KeyCryptKey} is not
    14   needed: no session key encrypts another.  Instead we
    15   prove the "key compromise" theorems for sets KK that contain no private
    16   encryption keys (@{term "priEK C"}). *}
    17 
    18 
    19 inductive_set
    20   set_mr :: "event list set"
    21 where
    22 
    23   Nil:    --{*Initial trace is empty*}
    24            "[] \<in> set_mr"
    25 
    26 
    27 | Fake:    --{*The spy MAY say anything he CAN say.*}
    28            "[| evsf \<in> set_mr; X \<in> synth (analz (knows Spy evsf)) |]
    29             ==> Says Spy B X  # evsf \<in> set_mr"
    30         
    31 
    32 | Reception: --{*If A sends a message X to B, then B might receive it*}
    33              "[| evsr \<in> set_mr; Says A B X \<in> set evsr |]
    34               ==> Gets B X  # evsr \<in> set_mr"
    35 
    36 
    37 | SET_MR1: --{*RegFormReq: M requires a registration form to a CA*}
    38            "[| evs1 \<in> set_mr; M = Merchant k; Nonce NM1 \<notin> used evs1 |]
    39             ==> Says M (CA i) {|Agent M, Nonce NM1|} # evs1 \<in> set_mr"
    40 
    41 
    42 | SET_MR2: --{*RegFormRes: CA replies with the registration form and the 
    43                certificates for her keys*}
    44   "[| evs2 \<in> set_mr; Nonce NCA \<notin> used evs2;
    45       Gets (CA i) {|Agent M, Nonce NM1|} \<in> set evs2 |]
    46    ==> Says (CA i) M {|sign (priSK (CA i)) {|Agent M, Nonce NM1, Nonce NCA|},
    47                        cert (CA i) (pubEK (CA i)) onlyEnc (priSK RCA),
    48                        cert (CA i) (pubSK (CA i)) onlySig (priSK RCA) |}
    49          # evs2 \<in> set_mr"
    50 
    51 | SET_MR3:
    52          --{*CertReq: M submits the key pair to be certified.  The Notes
    53              event allows KM1 to be lost if M is compromised. Piero remarks
    54              that the agent mentioned inside the signature is not verified to
    55              correspond to M.  As in CR, each Merchant has fixed key pairs.  M
    56              is only optionally required to send NCA back, so M doesn't do so
    57              in the model*}
    58   "[| evs3 \<in> set_mr; M = Merchant k; Nonce NM2 \<notin> used evs3;
    59       Key KM1 \<notin> used evs3;  KM1 \<in> symKeys;
    60       Gets M {|sign (invKey SKi) {|Agent X, Nonce NM1, Nonce NCA|},
    61                cert (CA i) EKi onlyEnc (priSK RCA),
    62                cert (CA i) SKi onlySig (priSK RCA) |}
    63         \<in> set evs3;
    64       Says M (CA i) {|Agent M, Nonce NM1|} \<in> set evs3 |]
    65    ==> Says M (CA i)
    66             {|Crypt KM1 (sign (priSK M) {|Agent M, Nonce NM2,
    67                                           Key (pubSK M), Key (pubEK M)|}),
    68               Crypt EKi (Key KM1)|}
    69          # Notes M {|Key KM1, Agent (CA i)|}
    70          # evs3 \<in> set_mr"
    71 
    72 | SET_MR4:
    73          --{*CertRes: CA issues the certificates for merSK and merEK,
    74              while checking never to have certified the m even
    75              separately. NOTE: In Cardholder Registration the
    76              corresponding rule (6) doesn't use the "sign" primitive. "The
    77              CertRes shall be signed but not encrypted if the EE is a Merchant
    78              or Payment Gateway."-- Programmer's Guide, page 191.*}
    79     "[| evs4 \<in> set_mr; M = Merchant k;
    80         merSK \<notin> symKeys;  merEK \<notin> symKeys;
    81         Notes (CA i) (Key merSK) \<notin> set evs4;
    82         Notes (CA i) (Key merEK) \<notin> set evs4;
    83         Gets (CA i) {|Crypt KM1 (sign (invKey merSK)
    84                                  {|Agent M, Nonce NM2, Key merSK, Key merEK|}),
    85                       Crypt (pubEK (CA i)) (Key KM1) |}
    86           \<in> set evs4 |]
    87     ==> Says (CA i) M {|sign (priSK(CA i)) {|Agent M, Nonce NM2, Agent(CA i)|},
    88                         cert  M      merSK    onlySig (priSK (CA i)),
    89                         cert  M      merEK    onlyEnc (priSK (CA i)),
    90                         cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|}
    91           # Notes (CA i) (Key merSK)
    92           # Notes (CA i) (Key merEK)
    93           # evs4 \<in> set_mr"
    94 
    95 
    96 text{*Note possibility proofs are missing.*}
    97 
    98 declare Says_imp_knows_Spy [THEN parts.Inj, dest]
    99 declare parts.Body [dest]
   100 declare analz_into_parts [dest]
   101 declare Fake_parts_insert_in_Un [dest]
   102 
   103 text{*General facts about message reception*}
   104 lemma Gets_imp_Says:
   105      "[| Gets B X \<in> set evs; evs \<in> set_mr |] ==> \<exists>A. Says A B X \<in> set evs"
   106 apply (erule rev_mp)
   107 apply (erule set_mr.induct, auto)
   108 done
   109 
   110 lemma Gets_imp_knows_Spy:
   111      "[| Gets B X \<in> set evs; evs \<in> set_mr |]  ==> X \<in> knows Spy evs"
   112 by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
   113 
   114 
   115 declare Gets_imp_knows_Spy [THEN parts.Inj, dest]
   116 
   117 subsubsection{*Proofs on keys *}
   118 
   119 text{*Spy never sees an agent's private keys! (unless it's bad at start)*}
   120 lemma Spy_see_private_Key [simp]:
   121      "evs \<in> set_mr
   122       ==> (Key(invKey (publicKey b A)) \<in> parts(knows Spy evs)) = (A \<in> bad)"
   123 apply (erule set_mr.induct)
   124 apply (auto dest!: Gets_imp_knows_Spy [THEN parts.Inj])
   125 done
   126 
   127 lemma Spy_analz_private_Key [simp]:
   128      "evs \<in> set_mr ==>
   129      (Key(invKey (publicKey b A)) \<in> analz(knows Spy evs)) = (A \<in> bad)"
   130 by auto
   131 
   132 declare Spy_see_private_Key [THEN [2] rev_iffD1, dest!]
   133 declare Spy_analz_private_Key [THEN [2] rev_iffD1, dest!]
   134 
   135 (*This is to state that the signed keys received in step 4
   136   are into parts - rather than installing sign_def each time.
   137   Needed in Spy_see_priSK_RCA, Spy_see_priEK and in Spy_see_priSK
   138 Goal "[|Gets C \<lbrace>Crypt KM1
   139                 (sign K \<lbrace>Agent M, Nonce NM2, Key merSK, Key merEK\<rbrace>), X\<rbrace>
   140           \<in> set evs;  evs \<in> set_mr |]
   141     ==> Key merSK \<in> parts (knows Spy evs) \<and>
   142         Key merEK \<in> parts (knows Spy evs)"
   143 by (fast_tac (claset() addss (simpset())) 1);
   144 qed "signed_keys_in_parts";
   145 ???*)
   146 
   147 text{*Proofs on certificates -
   148   they hold, as in CR, because RCA's keys are secure*}
   149 
   150 lemma Crypt_valid_pubEK:
   151      "[| Crypt (priSK RCA) {|Agent (CA i), Key EKi, onlyEnc|}
   152            \<in> parts (knows Spy evs);
   153          evs \<in> set_mr |] ==> EKi = pubEK (CA i)"
   154 apply (erule rev_mp)
   155 apply (erule set_mr.induct, auto)
   156 done
   157 
   158 lemma certificate_valid_pubEK:
   159     "[| cert (CA i) EKi onlyEnc (priSK RCA) \<in> parts (knows Spy evs);
   160         evs \<in> set_mr |]
   161      ==> EKi = pubEK (CA i)"
   162 apply (unfold cert_def signCert_def)
   163 apply (blast dest!: Crypt_valid_pubEK)
   164 done
   165 
   166 lemma Crypt_valid_pubSK:
   167      "[| Crypt (priSK RCA) {|Agent (CA i), Key SKi, onlySig|}
   168            \<in> parts (knows Spy evs);
   169          evs \<in> set_mr |] ==> SKi = pubSK (CA i)"
   170 apply (erule rev_mp)
   171 apply (erule set_mr.induct, auto)
   172 done
   173 
   174 lemma certificate_valid_pubSK:
   175     "[| cert (CA i) SKi onlySig (priSK RCA) \<in> parts (knows Spy evs);
   176         evs \<in> set_mr |] ==> SKi = pubSK (CA i)"
   177 apply (unfold cert_def signCert_def)
   178 apply (blast dest!: Crypt_valid_pubSK)
   179 done
   180 
   181 lemma Gets_certificate_valid:
   182      "[| Gets A {| X, cert (CA i) EKi onlyEnc (priSK RCA),
   183                       cert (CA i) SKi onlySig (priSK RCA)|} \<in> set evs;
   184          evs \<in> set_mr |]
   185       ==> EKi = pubEK (CA i) & SKi = pubSK (CA i)"
   186 by (blast dest: certificate_valid_pubEK certificate_valid_pubSK)
   187 
   188 
   189 text{*Nobody can have used non-existent keys!*}
   190 lemma new_keys_not_used [rule_format,simp]:
   191      "evs \<in> set_mr
   192       ==> Key K \<notin> used evs --> K \<in> symKeys -->
   193           K \<notin> keysFor (parts (knows Spy evs))"
   194 apply (erule set_mr.induct, simp_all)
   195 apply (force dest!: usedI keysFor_parts_insert)  --{*Fake*}
   196 apply force  --{*Message 2*}
   197 apply (blast dest: Gets_certificate_valid)  --{*Message 3*}
   198 apply force  --{*Message 4*}
   199 done
   200 
   201 
   202 subsubsection{*New Versions: As Above, but Generalized with the Kk Argument*}
   203 
   204 lemma gen_new_keys_not_used [rule_format]:
   205      "evs \<in> set_mr
   206       ==> Key K \<notin> used evs --> K \<in> symKeys -->
   207           K \<notin> keysFor (parts (Key`KK Un knows Spy evs))"
   208 by auto
   209 
   210 lemma gen_new_keys_not_analzd:
   211      "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_mr |]
   212       ==> K \<notin> keysFor (analz (Key`KK Un knows Spy evs))"
   213 by (blast intro: keysFor_mono [THEN [2] rev_subsetD]
   214           dest: gen_new_keys_not_used)
   215 
   216 lemma analz_Key_image_insert_eq:
   217      "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_mr |]
   218       ==> analz (Key ` (insert K KK) \<union> knows Spy evs) =
   219           insert (Key K) (analz (Key ` KK \<union> knows Spy evs))"
   220 by (simp add: gen_new_keys_not_analzd)
   221 
   222 
   223 lemma Crypt_parts_imp_used:
   224      "[|Crypt K X \<in> parts (knows Spy evs);
   225         K \<in> symKeys; evs \<in> set_mr |] ==> Key K \<in> used evs"
   226 apply (rule ccontr)
   227 apply (force dest: new_keys_not_used Crypt_imp_invKey_keysFor)
   228 done
   229 
   230 lemma Crypt_analz_imp_used:
   231      "[|Crypt K X \<in> analz (knows Spy evs);
   232         K \<in> symKeys; evs \<in> set_mr |] ==> Key K \<in> used evs"
   233 by (blast intro: Crypt_parts_imp_used)
   234 
   235 text{*Rewriting rule for private encryption keys.  Analogous rewriting rules
   236 for other keys aren't needed.*}
   237 
   238 lemma parts_image_priEK:
   239      "[|Key (priEK (CA i)) \<in> parts (Key`KK Un (knows Spy evs));
   240         evs \<in> set_mr|] ==> priEK (CA i) \<in> KK | CA i \<in> bad"
   241 by auto
   242 
   243 text{*trivial proof because (priEK (CA i)) never appears even in (parts evs)*}
   244 lemma analz_image_priEK:
   245      "evs \<in> set_mr ==>
   246           (Key (priEK (CA i)) \<in> analz (Key`KK Un (knows Spy evs))) =
   247           (priEK (CA i) \<in> KK | CA i \<in> bad)"
   248 by (blast dest!: parts_image_priEK intro: analz_mono [THEN [2] rev_subsetD])
   249 
   250 
   251 subsection{*Secrecy of Session Keys*}
   252 
   253 text{*This holds because if (priEK (CA i)) appears in any traffic then it must
   254   be known to the Spy, by @{text Spy_see_private_Key}*}
   255 lemma merK_neq_priEK:
   256      "[|Key merK \<notin> analz (knows Spy evs);
   257         Key merK \<in> parts (knows Spy evs);
   258         evs \<in> set_mr|] ==> merK \<noteq> priEK C"
   259 by blast
   260 
   261 text{*Lemma for message 4: either merK is compromised (when we don't care)
   262   or else merK hasn't been used to encrypt K.*}
   263 lemma msg4_priEK_disj:
   264      "[|Gets B {|Crypt KM1
   265                        (sign K {|Agent M, Nonce NM2, Key merSK, Key merEK|}),
   266                  Y|} \<in> set evs;
   267         evs \<in> set_mr|]
   268   ==> (Key merSK \<in> analz (knows Spy evs) | merSK \<notin> range(\<lambda>C. priEK C))
   269    &  (Key merEK \<in> analz (knows Spy evs) | merEK \<notin> range(\<lambda>C. priEK C))"
   270 apply (unfold sign_def)
   271 apply (blast dest: merK_neq_priEK)
   272 done
   273 
   274 
   275 lemma Key_analz_image_Key_lemma:
   276      "P --> (Key K \<in> analz (Key`KK Un H)) --> (K\<in>KK | Key K \<in> analz H)
   277       ==>
   278       P --> (Key K \<in> analz (Key`KK Un H)) = (K\<in>KK | Key K \<in> analz H)"
   279 by (blast intro: analz_mono [THEN [2] rev_subsetD])
   280 
   281 lemma symKey_compromise:
   282      "evs \<in> set_mr ==>
   283       (\<forall>SK KK. SK \<in> symKeys \<longrightarrow> (\<forall>K \<in> KK. K \<notin> range(\<lambda>C. priEK C)) -->
   284                (Key SK \<in> analz (Key`KK Un (knows Spy evs))) =
   285                (SK \<in> KK | Key SK \<in> analz (knows Spy evs)))"
   286 apply (erule set_mr.induct)
   287 apply (safe del: impI intro!: Key_analz_image_Key_lemma [THEN impI])
   288 apply (drule_tac [7] msg4_priEK_disj)
   289 apply (frule_tac [6] Gets_certificate_valid)
   290 apply (safe del: impI)
   291 apply (simp_all del: image_insert image_Un imp_disjL
   292          add: analz_image_keys_simps abbrev_simps analz_knows_absorb
   293               analz_knows_absorb2 analz_Key_image_insert_eq notin_image_iff
   294               Spy_analz_private_Key analz_image_priEK)
   295   --{*5 seconds on a 1.6GHz machine*}
   296 apply spy_analz  --{*Fake*}
   297 apply auto  --{*Message 3*}
   298 done
   299 
   300 lemma symKey_secrecy [rule_format]:
   301      "[|CA i \<notin> bad; K \<in> symKeys;  evs \<in> set_mr|]
   302       ==> \<forall>X m. Says (Merchant m) (CA i) X \<in> set evs -->
   303                 Key K \<in> parts{X} -->
   304                 Merchant m \<notin> bad -->
   305                 Key K \<notin> analz (knows Spy evs)"
   306 apply (erule set_mr.induct)
   307 apply (drule_tac [7] msg4_priEK_disj)
   308 apply (frule_tac [6] Gets_certificate_valid)
   309 apply (safe del: impI)
   310 apply (simp_all del: image_insert image_Un imp_disjL
   311          add: analz_image_keys_simps abbrev_simps analz_knows_absorb
   312               analz_knows_absorb2 analz_Key_image_insert_eq
   313               symKey_compromise notin_image_iff Spy_analz_private_Key
   314               analz_image_priEK)
   315 apply spy_analz  --{*Fake*}
   316 apply force  --{*Message 1*}
   317 apply (auto intro: analz_into_parts [THEN usedI] in_parts_Says_imp_used)  --{*Message 3*}
   318 done
   319 
   320 subsection{*Unicity *}
   321 
   322 lemma msg4_Says_imp_Notes:
   323  "[|Says (CA i) M {|sign (priSK (CA i)) {|Agent M, Nonce NM2, Agent (CA i)|},
   324                     cert  M      merSK    onlySig (priSK (CA i)),
   325                     cert  M      merEK    onlyEnc (priSK (CA i)),
   326                     cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|} \<in> set evs;
   327     evs \<in> set_mr |]
   328   ==> Notes (CA i) (Key merSK) \<in> set evs
   329    &  Notes (CA i) (Key merEK) \<in> set evs"
   330 apply (erule rev_mp)
   331 apply (erule set_mr.induct)
   332 apply (simp_all (no_asm_simp))
   333 done
   334 
   335 text{*Unicity of merSK wrt a given CA:
   336   merSK uniquely identifies the other components, including merEK*}
   337 lemma merSK_unicity:
   338  "[|Says (CA i) M {|sign (priSK(CA i)) {|Agent M, Nonce NM2, Agent (CA i)|},
   339                     cert  M      merSK    onlySig (priSK (CA i)),
   340                     cert  M      merEK    onlyEnc (priSK (CA i)),
   341                     cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|} \<in> set evs;
   342     Says (CA i) M' {|sign (priSK(CA i)) {|Agent M', Nonce NM2', Agent (CA i)|},
   343                     cert  M'      merSK    onlySig (priSK (CA i)),
   344                     cert  M'      merEK'    onlyEnc (priSK (CA i)),
   345                     cert (CA i) (pubSK(CA i)) onlySig (priSK RCA)|} \<in> set evs;
   346     evs \<in> set_mr |] ==> M=M' & NM2=NM2' & merEK=merEK'"
   347 apply (erule rev_mp)
   348 apply (erule rev_mp)
   349 apply (erule set_mr.induct)
   350 apply (simp_all (no_asm_simp))
   351 apply (blast dest!: msg4_Says_imp_Notes)
   352 done
   353 
   354 text{*Unicity of merEK wrt a given CA:
   355   merEK uniquely identifies the other components, including merSK*}
   356 lemma merEK_unicity:
   357  "[|Says (CA i) M {|sign (priSK(CA i)) {|Agent M, Nonce NM2, Agent (CA i)|},
   358                     cert  M      merSK    onlySig (priSK (CA i)),
   359                     cert  M      merEK    onlyEnc (priSK (CA i)),
   360                     cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|} \<in> set evs;
   361     Says (CA i) M' {|sign (priSK(CA i)) {|Agent M', Nonce NM2', Agent (CA i)|},
   362                      cert  M'      merSK'    onlySig (priSK (CA i)),
   363                      cert  M'      merEK    onlyEnc (priSK (CA i)),
   364                      cert (CA i) (pubSK(CA i)) onlySig (priSK RCA)|} \<in> set evs;
   365     evs \<in> set_mr |] 
   366   ==> M=M' & NM2=NM2' & merSK=merSK'"
   367 apply (erule rev_mp)
   368 apply (erule rev_mp)
   369 apply (erule set_mr.induct)
   370 apply (simp_all (no_asm_simp))
   371 apply (blast dest!: msg4_Says_imp_Notes)
   372 done
   373 
   374 
   375 text{* -No interest on secrecy of nonces: they appear to be used
   376     only for freshness.
   377    -No interest on secrecy of merSK or merEK, as in CR.
   378    -There's no equivalent of the PAN*}
   379 
   380 
   381 subsection{*Primary Goals of Merchant Registration *}
   382 
   383 subsubsection{*The merchant's certificates really were created by the CA,
   384 provided the CA is uncompromised *}
   385 
   386 text{*The assumption @{term "CA i \<noteq> RCA"} is required: step 2 uses 
   387   certificates of the same form.*}
   388 lemma certificate_merSK_valid_lemma [intro]:
   389      "[|Crypt (priSK (CA i)) {|Agent M, Key merSK, onlySig|}
   390           \<in> parts (knows Spy evs);
   391         CA i \<notin> bad;  CA i \<noteq> RCA;  evs \<in> set_mr|]
   392  ==> \<exists>X Y Z. Says (CA i) M
   393                   {|X, cert M merSK onlySig (priSK (CA i)), Y, Z|} \<in> set evs"
   394 apply (erule rev_mp)
   395 apply (erule set_mr.induct)
   396 apply (simp_all (no_asm_simp))
   397 apply auto
   398 done
   399 
   400 lemma certificate_merSK_valid:
   401      "[| cert M merSK onlySig (priSK (CA i)) \<in> parts (knows Spy evs);
   402          CA i \<notin> bad;  CA i \<noteq> RCA;  evs \<in> set_mr|]
   403  ==> \<exists>X Y Z. Says (CA i) M
   404                   {|X, cert M merSK onlySig (priSK (CA i)), Y, Z|} \<in> set evs"
   405 by auto
   406 
   407 lemma certificate_merEK_valid_lemma [intro]:
   408      "[|Crypt (priSK (CA i)) {|Agent M, Key merEK, onlyEnc|}
   409           \<in> parts (knows Spy evs);
   410         CA i \<notin> bad;  CA i \<noteq> RCA;  evs \<in> set_mr|]
   411  ==> \<exists>X Y Z. Says (CA i) M
   412                   {|X, Y, cert M merEK onlyEnc (priSK (CA i)), Z|} \<in> set evs"
   413 apply (erule rev_mp)
   414 apply (erule set_mr.induct)
   415 apply (simp_all (no_asm_simp))
   416 apply auto
   417 done
   418 
   419 lemma certificate_merEK_valid:
   420      "[| cert M merEK onlyEnc (priSK (CA i)) \<in> parts (knows Spy evs);
   421          CA i \<notin> bad;  CA i \<noteq> RCA;  evs \<in> set_mr|]
   422  ==> \<exists>X Y Z. Says (CA i) M
   423                   {|X, Y, cert M merEK onlyEnc (priSK (CA i)), Z|} \<in> set evs"
   424 by auto
   425 
   426 text{*The two certificates - for merSK and for merEK - cannot be proved to
   427   have originated together*}
   428 
   429 end