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