# Theory Merchant_Registration

Up to index of Isabelle/HOL/SET-Protocol

theory Merchant_Registration
imports PublicSET
begin

    (*  Title:      HOL/Auth/SET/Merchant_Registration
        ID:         $Id: Merchant_Registration.thy,v 1.3 2005/06/17 14:13:10 haftmann Exp $
        Authors:    Giampaolo Bella, Fabio Massacci, Lawrence C Paulson
    *)

    header{*The SET Merchant Registration Protocol*}

    theory Merchant_Registration imports PublicSET begin

    text{*Copmpared with Cardholder Reigstration, @{text KeyCryptKey} is not
      needed: no session key encrypts another.  Instead we
      prove the "key compromise" theorems for sets KK that contain no private
      encryption keys (@{term "priEK C"}). *}

    consts  set_mr  :: "event list set"
    inductive set_mr
     intros

      Nil:    --{*Initial trace is empty*}
               "[] ∈ set_mr"

      Fake:    --{*The spy MAY say anything he CAN say.*}
               "[| evsf ∈ set_mr; X ∈ synth (analz (knows Spy evsf)) |]
                ==> Says Spy B X  # evsf ∈ set_mr"

      Reception: --{*If A sends a message X to B, then B might receive it*}
                 "[| evsr ∈ set_mr; Says A B X ∈ set evsr |]
                  ==> Gets B X  # evsr ∈ set_mr"

      SET_MR1: --{*RegFormReq: M requires a registration form to a CA*}
               "[| evs1 ∈ set_mr; M = Merchant k; Nonce NM1 ∉ used evs1 |]
                ==> Says M (CA i) {|Agent M, Nonce NM1|} # evs1 ∈ set_mr"

      SET_MR2: --{*RegFormRes: CA replies with the registration form and the
                   certificates for her keys*}
      "[| evs2 ∈ set_mr; Nonce NCA ∉ used evs2;
          Gets (CA i) {|Agent M, Nonce NM1|} ∈ set evs2 |]
       ==> Says (CA i) M {|sign (priSK (CA i)) {|Agent M, Nonce NM1, Nonce NCA|},
                           cert (CA i) (pubEK (CA i)) onlyEnc (priSK RCA),
                           cert (CA i) (pubSK (CA i)) onlySig (priSK RCA) |}
             # evs2 ∈ set_mr"

      SET_MR3:
             --{*CertReq: M submits the key pair to be certified.  The Notes
                 event allows KM1 to be lost if M is compromised. Piero remarks
                 that the agent mentioned inside the signature is not verified to
                 correspond to M.  As in CR, each Merchant has fixed key pairs.  M
                 is only optionally required to send NCA back, so M doesn't do so
                 in the model*}
      "[| evs3 ∈ set_mr; M = Merchant k; Nonce NM2 ∉ used evs3;
          Key KM1 ∉ used evs3;  KM1 ∈ symKeys;
          Gets M {|sign (invKey SKi) {|Agent X, Nonce NM1, Nonce NCA|},
                   cert (CA i) EKi onlyEnc (priSK RCA),
                   cert (CA i) SKi onlySig (priSK RCA) |}
            ∈ set evs3;
          Says M (CA i) {|Agent M, Nonce NM1|} ∈ set evs3 |]
       ==> Says M (CA i)
                {|Crypt KM1 (sign (priSK M) {|Agent M, Nonce NM2,
                                              Key (pubSK M), Key (pubEK M)|}),
                  Crypt EKi (Key KM1)|}
             # Notes M {|Key KM1, Agent (CA i)|}
             # evs3 ∈ set_mr"

      SET_MR4:
             --{*CertRes: CA issues the certificates for merSK and merEK,
                 while checking never to have certified the m even
                 separately. NOTE: In Cardholder Registration the
                 corresponding rule (6) doesn't use the "sign" primitive. "The
                 CertRes shall be signed but not encrypted if the EE is a Merchant
                 or Payment Gateway."-- Programmer's Guide, page 191.*}
        "[| evs4 ∈ set_mr; M = Merchant k;
            merSK ∉ symKeys;  merEK ∉ symKeys;
            Notes (CA i) (Key merSK) ∉ set evs4;
            Notes (CA i) (Key merEK) ∉ set evs4;
            Gets (CA i) {|Crypt KM1 (sign (invKey merSK)
                                     {|Agent M, Nonce NM2, Key merSK, Key merEK|}),
                          Crypt (pubEK (CA i)) (Key KM1) |}
              ∈ set evs4 |]
        ==> Says (CA i) M {|sign (priSK(CA i)) {|Agent M, Nonce NM2, Agent(CA i)|},
                            cert  M      merSK    onlySig (priSK (CA i)),
                            cert  M      merEK    onlyEnc (priSK (CA i)),
                            cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|}
              # Notes (CA i) (Key merSK)
              # Notes (CA i) (Key merEK)
              # evs4 ∈ set_mr"

    text{*Note possibility proofs are missing.*}

    declare Says_imp_knows_Spy [THEN parts.Inj, dest]
    declare parts.Body [dest]
    declare analz_into_parts [dest]
    declare Fake_parts_insert_in_Un [dest]

    text{*General facts about message reception*}
    lemma Gets_imp_Says:
         "[| Gets B X ∈ set evs; evs ∈ set_mr |] ==> ∃A. Says A B X ∈ set evs"
    apply (erule rev_mp)
    apply (erule set_mr.induct, auto)
    done

    lemma Gets_imp_knows_Spy:
         "[| Gets B X ∈ set evs; evs ∈ set_mr |]  ==> X ∈ knows Spy evs"
    by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)

    declare Gets_imp_knows_Spy [THEN parts.Inj, dest]

    subsubsection{*Proofs on keys *}

    text{*Spy never sees an agent's private keys! (unless it's bad at start)*}
    lemma Spy_see_private_Key [simp]:
         "evs ∈ set_mr
          ==> (Key(invKey (publicKey b A)) ∈ parts(knows Spy evs)) = (A ∈ bad)"
    apply (erule set_mr.induct)
    apply (auto dest!: Gets_imp_knows_Spy [THEN parts.Inj])
    done

    lemma Spy_analz_private_Key [simp]:
         "evs ∈ set_mr ==>
         (Key(invKey (publicKey b A)) ∈ analz(knows Spy evs)) = (A ∈ bad)"
    by auto

    declare Spy_see_private_Key [THEN [2] rev_iffD1, dest!]
    declare Spy_analz_private_Key [THEN [2] rev_iffD1, dest!]

    (*This is to state that the signed keys received in step 4
      are into parts - rather than installing sign_def each time.
      Needed in Spy_see_priSK_RCA, Spy_see_priEK and in Spy_see_priSK
    Goal "[|Gets C \<lbrace>Crypt KM1
                    (sign K \<lbrace>Agent M, Nonce NM2, Key merSK, Key merEK\<rbrace>), X\<rbrace>
              ∈ set evs;  evs ∈ set_mr |]
        ==> Key merSK ∈ parts (knows Spy evs) ∧
            Key merEK ∈ parts (knows Spy evs)"
    by (fast_tac (claset() addss (simpset())) 1);
    qed "signed_keys_in_parts";
    ???*)

    text{*Proofs on certificates -
      they hold, as in CR, because RCA's keys are secure*}

    lemma Crypt_valid_pubEK:
         "[| Crypt (priSK RCA) {|Agent (CA i), Key EKi, onlyEnc|}
               ∈ parts (knows Spy evs);
             evs ∈ set_mr |] ==> EKi = pubEK (CA i)"
    apply (erule rev_mp)
    apply (erule set_mr.induct, auto)
    done

    lemma certificate_valid_pubEK:
        "[| cert (CA i) EKi onlyEnc (priSK RCA) ∈ parts (knows Spy evs);
            evs ∈ set_mr |]
         ==> EKi = pubEK (CA i)"
    apply (unfold cert_def signCert_def)
    apply (blast dest!: Crypt_valid_pubEK)
    done

    lemma Crypt_valid_pubSK:
         "[| Crypt (priSK RCA) {|Agent (CA i), Key SKi, onlySig|}
               ∈ parts (knows Spy evs);
             evs ∈ set_mr |] ==> SKi = pubSK (CA i)"
    apply (erule rev_mp)
    apply (erule set_mr.induct, auto)
    done

    lemma certificate_valid_pubSK:
        "[| cert (CA i) SKi onlySig (priSK RCA) ∈ parts (knows Spy evs);
            evs ∈ set_mr |] ==> SKi = pubSK (CA i)"
    apply (unfold cert_def signCert_def)
    apply (blast dest!: Crypt_valid_pubSK)
    done

    lemma Gets_certificate_valid:
         "[| Gets A {| X, cert (CA i) EKi onlyEnc (priSK RCA),
                          cert (CA i) SKi onlySig (priSK RCA)|} ∈ set evs;
             evs ∈ set_mr |]
          ==> EKi = pubEK (CA i) & SKi = pubSK (CA i)"
    by (blast dest: certificate_valid_pubEK certificate_valid_pubSK)

    text{*Nobody can have used non-existent keys!*}
    lemma new_keys_not_used [rule_format,simp]:
         "evs ∈ set_mr
          ==> Key K ∉ used evs --> K ∈ symKeys -->
              K ∉ keysFor (parts (knows Spy evs))"
    apply (erule set_mr.induct, simp_all)
    apply (force dest!: usedI keysFor_parts_insert)  --{*Fake*}
    apply force  --{*Message 2*}
    apply (blast dest: Gets_certificate_valid)  --{*Message 3*}
    apply force  --{*Message 4*}
    done

    subsubsection{*New Versions: As Above, but Generalized with the Kk Argument*}

    lemma gen_new_keys_not_used [rule_format]:
         "evs ∈ set_mr
          ==> Key K ∉ used evs --> K ∈ symKeys -->
              K ∉ keysFor (parts (Key`KK Un knows Spy evs))"
    by auto

    lemma gen_new_keys_not_analzd:
         "[|Key K ∉ used evs; K ∈ symKeys; evs ∈ set_mr |]
          ==> K ∉ keysFor (analz (Key`KK Un knows Spy evs))"
    by (blast intro: keysFor_mono [THEN [2] rev_subsetD]
              dest: gen_new_keys_not_used)

    lemma analz_Key_image_insert_eq:
         "[|Key K ∉ used evs; K ∈ symKeys; evs ∈ set_mr |]
          ==> analz (Key ` (insert K KK) ∪ knows Spy evs) =
              insert (Key K) (analz (Key ` KK ∪ knows Spy evs))"
    by (simp add: gen_new_keys_not_analzd)

    lemma Crypt_parts_imp_used:
         "[|Crypt K X ∈ parts (knows Spy evs);
            K ∈ symKeys; evs ∈ set_mr |] ==> Key K ∈ used evs"
    apply (rule ccontr)
    apply (force dest: new_keys_not_used Crypt_imp_invKey_keysFor)
    done

    lemma Crypt_analz_imp_used:
         "[|Crypt K X ∈ analz (knows Spy evs);
            K ∈ symKeys; evs ∈ set_mr |] ==> Key K ∈ used evs"
    by (blast intro: Crypt_parts_imp_used)

    text{*Rewriting rule for private encryption keys.  Analogous rewriting rules
    for other keys aren't needed.*}

    lemma parts_image_priEK:
         "[|Key (priEK (CA i)) ∈ parts (Key`KK Un (knows Spy evs));
            evs ∈ set_mr|] ==> priEK (CA i) ∈ KK | CA i ∈ bad"
    by auto

    text{*trivial proof because (priEK (CA i)) never appears even in (parts evs)*}
    lemma analz_image_priEK:
         "evs ∈ set_mr ==>
              (Key (priEK (CA i)) ∈ analz (Key`KK Un (knows Spy evs))) =
              (priEK (CA i) ∈ KK | CA i ∈ bad)"
    by (blast dest!: parts_image_priEK intro: analz_mono [THEN [2] rev_subsetD])

    subsection{*Secrecy of Session Keys*}

    text{*This holds because if (priEK (CA i)) appears in any traffic then it must
      be known to the Spy, by @{text Spy_see_private_Key}*}
    lemma merK_neq_priEK:
         "[|Key merK ∉ analz (knows Spy evs);
            Key merK ∈ parts (knows Spy evs);
            evs ∈ set_mr|] ==> merK ≠ priEK C"
    by blast

    text{*Lemma for message 4: either merK is compromised (when we don't care)
      or else merK hasn't been used to encrypt K.*}
    lemma msg4_priEK_disj:
         "[|Gets B {|Crypt KM1
                           (sign K {|Agent M, Nonce NM2, Key merSK, Key merEK|}),
                     Y|} ∈ set evs;
            evs ∈ set_mr|]
      ==> (Key merSK ∈ analz (knows Spy evs) | merSK ∉ range(λC. priEK C))
       &  (Key merEK ∈ analz (knows Spy evs) | merEK ∉ range(λC. priEK C))"
    apply (unfold sign_def)
    apply (blast dest: merK_neq_priEK)
    done

    lemma Key_analz_image_Key_lemma:
         "P --> (Key K ∈ analz (Key`KK Un H)) --> (K∈KK | Key K ∈ analz H)
          ==>
          P --> (Key K ∈ analz (Key`KK Un H)) = (K∈KK | Key K ∈ analz H)"
    by (blast intro: analz_mono [THEN [2] rev_subsetD])

    lemma symKey_compromise:
         "evs ∈ set_mr ==>
          (∀SK KK. SK ∈ symKeys --> (∀K ∈ KK. K ∉ range(λC. priEK C)) -->
                   (Key SK ∈ analz (Key`KK Un (knows Spy evs))) =
                   (SK ∈ KK | Key SK ∈ analz (knows Spy evs)))"
    apply (erule set_mr.induct)
    apply (safe del: impI intro!: Key_analz_image_Key_lemma [THEN impI])
    apply (drule_tac [7] msg4_priEK_disj)
    apply (frule_tac [6] Gets_certificate_valid)
    apply (safe del: impI)
    apply (simp_all del: image_insert image_Un imp_disjL
             add: analz_image_keys_simps abbrev_simps analz_knows_absorb
                  analz_knows_absorb2 analz_Key_image_insert_eq notin_image_iff
                  Spy_analz_private_Key analz_image_priEK)
      --{*23 seconds on a 1.8GHz machine*}
    apply spy_analz  --{*Fake*}
    apply auto  --{*Message 3*}
    done

    lemma symKey_secrecy [rule_format]:
         "[|CA i ∉ bad; K ∈ symKeys;  evs ∈ set_mr|]
          ==> ∀X m. Says (Merchant m) (CA i) X ∈ set evs -->
                    Key K ∈ parts{X} -->
                    Merchant m ∉ bad -->
                    Key K ∉ analz (knows Spy evs)"
    apply (erule set_mr.induct)
    apply (drule_tac [7] msg4_priEK_disj)
    apply (frule_tac [6] Gets_certificate_valid)
    apply (safe del: impI)
    apply (simp_all del: image_insert image_Un imp_disjL
             add: analz_image_keys_simps abbrev_simps analz_knows_absorb
                  analz_knows_absorb2 analz_Key_image_insert_eq
                  symKey_compromise notin_image_iff Spy_analz_private_Key
                  analz_image_priEK)
    apply spy_analz  --{*Fake*}
    apply force  --{*Message 1*}
    apply (auto intro: analz_into_parts [THEN usedI] in_parts_Says_imp_used)  --{*Message 3*}
    done

    subsection{*Unicity *}

    lemma msg4_Says_imp_Notes:
     "[|Says (CA i) M {|sign (priSK (CA i)) {|Agent M, Nonce NM2, Agent (CA i)|},
                        cert  M      merSK    onlySig (priSK (CA i)),
                        cert  M      merEK    onlyEnc (priSK (CA i)),
                        cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|} ∈ set evs;
        evs ∈ set_mr |]
      ==> Notes (CA i) (Key merSK) ∈ set evs
       &  Notes (CA i) (Key merEK) ∈ set evs"
    apply (erule rev_mp)
    apply (erule set_mr.induct)
    apply (simp_all (no_asm_simp))
    done

    text{*Unicity of merSK wrt a given CA:
      merSK uniquely identifies the other components, including merEK*}
    lemma merSK_unicity:
     "[|Says (CA i) M {|sign (priSK(CA i)) {|Agent M, Nonce NM2, Agent (CA i)|},
                        cert  M      merSK    onlySig (priSK (CA i)),
                        cert  M      merEK    onlyEnc (priSK (CA i)),
                        cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|} ∈ set evs;
        Says (CA i) M' {|sign (priSK(CA i)) {|Agent M', Nonce NM2', Agent (CA i)|},
                        cert  M'      merSK    onlySig (priSK (CA i)),
                        cert  M'      merEK'    onlyEnc (priSK (CA i)),
                        cert (CA i) (pubSK(CA i)) onlySig (priSK RCA)|} ∈ set evs;
        evs ∈ set_mr |] ==> M=M' & NM2=NM2' & merEK=merEK'"
    apply (erule rev_mp)
    apply (erule rev_mp)
    apply (erule set_mr.induct)
    apply (simp_all (no_asm_simp))
    apply (blast dest!: msg4_Says_imp_Notes)
    done

    text{*Unicity of merEK wrt a given CA:
      merEK uniquely identifies the other components, including merSK*}
    lemma merEK_unicity:
     "[|Says (CA i) M {|sign (priSK(CA i)) {|Agent M, Nonce NM2, Agent (CA i)|},
                        cert  M      merSK    onlySig (priSK (CA i)),
                        cert  M      merEK    onlyEnc (priSK (CA i)),
                        cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|} ∈ set evs;
        Says (CA i) M' {|sign (priSK(CA i)) {|Agent M', Nonce NM2', Agent (CA i)|},
                         cert  M'      merSK'    onlySig (priSK (CA i)),
                         cert  M'      merEK    onlyEnc (priSK (CA i)),
                         cert (CA i) (pubSK(CA i)) onlySig (priSK RCA)|} ∈ set evs;
        evs ∈ set_mr |]
      ==> M=M' & NM2=NM2' & merSK=merSK'"
    apply (erule rev_mp)
    apply (erule rev_mp)
    apply (erule set_mr.induct)
    apply (simp_all (no_asm_simp))
    apply (blast dest!: msg4_Says_imp_Notes)
    done

    text{* -No interest on secrecy of nonces: they appear to be used
        only for freshness.
       -No interest on secrecy of merSK or merEK, as in CR.
       -There's no equivalent of the PAN*}

    subsection{*Primary Goals of Merchant Registration *}

    subsubsection{*The merchant's certificates really were created by the CA,
    provided the CA is uncompromised *}

    text{*The assumption @{term "CA i ≠ RCA"} is required: step 2 uses
      certificates of the same form.*}
    lemma certificate_merSK_valid_lemma [intro]:
         "[|Crypt (priSK (CA i)) {|Agent M, Key merSK, onlySig|}
              ∈ parts (knows Spy evs);
            CA i ∉ bad;  CA i ≠ RCA;  evs ∈ set_mr|]
     ==> ∃X Y Z. Says (CA i) M
                      {|X, cert M merSK onlySig (priSK (CA i)), Y, Z|} ∈ set evs"
    apply (erule rev_mp)
    apply (erule set_mr.induct)
    apply (simp_all (no_asm_simp))
    apply auto
    done

    lemma certificate_merSK_valid:
         "[| cert M merSK onlySig (priSK (CA i)) ∈ parts (knows Spy evs);
             CA i ∉ bad;  CA i ≠ RCA;  evs ∈ set_mr|]
     ==> ∃X Y Z. Says (CA i) M
                      {|X, cert M merSK onlySig (priSK (CA i)), Y, Z|} ∈ set evs"
    by auto

    lemma certificate_merEK_valid_lemma [intro]:
         "[|Crypt (priSK (CA i)) {|Agent M, Key merEK, onlyEnc|}
              ∈ parts (knows Spy evs);
            CA i ∉ bad;  CA i ≠ RCA;  evs ∈ set_mr|]
     ==> ∃X Y Z. Says (CA i) M
                      {|X, Y, cert M merEK onlyEnc (priSK (CA i)), Z|} ∈ set evs"
    apply (erule rev_mp)
    apply (erule set_mr.induct)
    apply (simp_all (no_asm_simp))
    apply auto
    done

    lemma certificate_merEK_valid:
         "[| cert M merEK onlyEnc (priSK (CA i)) ∈ parts (knows Spy evs);
             CA i ∉ bad;  CA i ≠ RCA;  evs ∈ set_mr|]
     ==> ∃X Y Z. Says (CA i) M
                      {|X, Y, cert M merEK onlyEnc (priSK (CA i)), Z|} ∈ set evs"
    by auto

    text{*The two certificates - for merSK and for merEK - cannot be proved to
      have originated together*}

    end

lemma Gets_imp_Says:

      [| Gets B X ∈ set evs; evs ∈ set_mr |] ==> ∃A. Says A B X ∈ set evs

lemma Gets_imp_knows_Spy:

      [| Gets B X ∈ set evs; evs ∈ set_mr |] ==> X ∈ knows Spy evs

#### Proofs on keys

lemma Spy_see_private_Key:

      evs ∈ set_mr
      ==> (Key (invKey (publicKey b A)) ∈ parts (knows Spy evs)) = (A ∈ bad)

lemma Spy_analz_private_Key:

      evs ∈ set_mr
      ==> (Key (invKey (publicKey b A)) ∈ analz (knows Spy evs)) = (A ∈ bad)

lemma Crypt_valid_pubEK:

      [| Crypt (priSK RCA) {|Agent (CA i), Key EKi, onlyEnc|} ∈ parts (knows Spy evs);
         evs ∈ set_mr |]
      ==> EKi = pubEK (CA i)

lemma certificate_valid_pubEK:

      [| cert (CA i) EKi onlyEnc (priSK RCA) ∈ parts (knows Spy evs); evs ∈ set_mr |]
      ==> EKi = pubEK (CA i)

lemma Crypt_valid_pubSK:

      [| Crypt (priSK RCA) {|Agent (CA i), Key SKi, onlySig|} ∈ parts (knows Spy evs);
         evs ∈ set_mr |]
      ==> SKi = pubSK (CA i)

lemma certificate_valid_pubSK:

      [| cert (CA i) SKi onlySig (priSK RCA) ∈ parts (knows Spy evs); evs ∈ set_mr |]
      ==> SKi = pubSK (CA i)

lemma Gets_certificate_valid:

      [| Gets A
          {|X, cert (CA i) EKi onlyEnc (priSK RCA),
            cert (CA i) SKi onlySig (priSK RCA)|}
         ∈ set evs;
         evs ∈ set_mr |]
      ==> EKi = pubEK (CA i) ∧ SKi = pubSK (CA i)

lemma new_keys_not_used:

      [| evs ∈ set_mr; Key K ∉ used evs; K ∈ symKeys |]
      ==> K ∉ keysFor (parts (knows Spy evs))

#### New Versions: As Above, but Generalized with the Kk Argument

lemma gen_new_keys_not_used:

      [| evs ∈ set_mr; Key K ∉ used evs; K ∈ symKeys |]
      ==> K ∉ keysFor (parts (Key ` KK ∪ knows Spy evs))

lemma gen_new_keys_not_analzd:

      [| Key K ∉ used evs; K ∈ symKeys; evs ∈ set_mr |]
      ==> K ∉ keysFor (analz (Key ` KK ∪ knows Spy evs))

lemma analz_Key_image_insert_eq:

      [| Key K ∉ used evs; K ∈ symKeys; evs ∈ set_mr |]
      ==> analz (Key ` insert K KK ∪ knows Spy evs) =
          insert (Key K) (analz (Key ` KK ∪ knows Spy evs))

lemma Crypt_parts_imp_used:

      [| Crypt K X ∈ parts (knows Spy evs); K ∈ symKeys; evs ∈ set_mr |]
      ==> Key K ∈ used evs

lemma Crypt_analz_imp_used:

      [| Crypt K X ∈ analz (knows Spy evs); K ∈ symKeys; evs ∈ set_mr |]
      ==> Key K ∈ used evs

lemma parts_image_priEK:

      [| Key (priEK (CA i)) ∈ parts (Key ` KK ∪ knows Spy evs); evs ∈ set_mr |]
      ==> priEK (CA i) ∈ KK ∨ CA i ∈ bad

lemma analz_image_priEK:

      evs ∈ set_mr
      ==> (Key (priEK (CA i)) ∈ analz (Key ` KK ∪ knows Spy evs)) =
          (priEK (CA i) ∈ KK ∨ CA i ∈ bad)

### Secrecy of Session Keys

lemma merK_neq_priEK:

      [| Key merK ∉ analz (knows Spy evs); Key merK ∈ parts (knows Spy evs);
         evs ∈ set_mr |]
      ==> merK ≠ priEK C

lemma msg4_priEK_disj:

      [| Gets B
          {|Crypt KM1.0 (sign K {|Agent M, Nonce NM2.0, Key merSK, Key merEK|}), Y|}
         ∈ set evs;
         evs ∈ set_mr |]
      ==> (Key merSK ∈ analz (knows Spy evs) ∨ merSK ∉ range (%C. priEK C)) ∧
          (Key merEK ∈ analz (knows Spy evs) ∨ merEK ∉ range (%C. priEK C))

lemma Key_analz_image_Key_lemma:

      P --> Key K ∈ analz (Key ` KK ∪ H) --> K ∈ KK ∨ Key K ∈ analz H
      ==> P --> (Key K ∈ analz (Key ` KK ∪ H)) = (K ∈ KK ∨ Key K ∈ analz H)

lemma symKey_compromise:

      evs ∈ set_mr
      ==> ∀SK KK.
             SK ∈ symKeys -->
             (∀K∈KK. K ∉ range (%C. priEK C)) -->
             (Key SK ∈ analz (Key ` KK ∪ knows Spy evs)) =
             (SK ∈ KK ∨ Key SK ∈ analz (knows Spy evs))

lemma symKey_secrecy:

      [| CA i ∉ bad; K ∈ symKeys; evs ∈ set_mr; Says (Merchant m) (CA i) X ∈ set evs;
         Key K ∈ parts {X}; Merchant m ∉ bad |]
      ==> Key K ∉ analz (knows Spy evs)

### Unicity

lemma msg4_Says_imp_Notes:

      [| Says (CA i) M
          {|sign (priSK (CA i)) {|Agent M, Nonce NM2.0, Agent (CA i)|},
            cert M merSK onlySig (priSK (CA i)), cert M merEK onlyEnc (priSK (CA i)),
            cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|}
         ∈ set evs;
         evs ∈ set_mr |]
      ==> Notes (CA i) (Key merSK) ∈ set evs ∧ Notes (CA i) (Key merEK) ∈ set evs

lemma merSK_unicity:

      [| Says (CA i) M
          {|sign (priSK (CA i)) {|Agent M, Nonce NM2.0, Agent (CA i)|},
            cert M merSK onlySig (priSK (CA i)), cert M merEK onlyEnc (priSK (CA i)),
            cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|}
         ∈ set evs;
         Says (CA i) M'
          {|sign (priSK (CA i)) {|Agent M', Nonce NM2', Agent (CA i)|},
            cert M' merSK onlySig (priSK (CA i)),
            cert M' merEK' onlyEnc (priSK (CA i)),
            cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|}
         ∈ set evs;
         evs ∈ set_mr |]
      ==> M = M' ∧ NM2.0 = NM2' ∧ merEK = merEK'

lemma merEK_unicity:

      [| Says (CA i) M
          {|sign (priSK (CA i)) {|Agent M, Nonce NM2.0, Agent (CA i)|},
            cert M merSK onlySig (priSK (CA i)), cert M merEK onlyEnc (priSK (CA i)),
            cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|}
         ∈ set evs;
         Says (CA i) M'
          {|sign (priSK (CA i)) {|Agent M', Nonce NM2', Agent (CA i)|},
            cert M' merSK' onlySig (priSK (CA i)),
            cert M' merEK onlyEnc (priSK (CA i)),
            cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|}
         ∈ set evs;
         evs ∈ set_mr |]
      ==> M = M' ∧ NM2.0 = NM2' ∧ merSK = merSK'

### Primary Goals of Merchant Registration

#### The merchant's certificates really were created by the CA, provided the CA is uncompromised

lemma certificate_merSK_valid_lemma:

      [| Crypt (priSK (CA i)) {|Agent M, Key merSK, onlySig|} ∈ parts (knows Spy evs);
         CA i ∉ bad; CA i ≠ RCA; evs ∈ set_mr |]
      ==> ∃X Y Z.
             Says (CA i) M {|X, cert M merSK onlySig (priSK (CA i)), Y, Z|} ∈ set evs

lemma certificate_merSK_valid:

      [| cert M merSK onlySig (priSK (CA i)) ∈ parts (knows Spy evs); CA i ∉ bad;
         CA i ≠ RCA; evs ∈ set_mr |]
      ==> ∃X Y Z.
             Says (CA i) M {|X, cert M merSK onlySig (priSK (CA i)), Y, Z|} ∈ set evs

lemma certificate_merEK_valid_lemma:

      [| Crypt (priSK (CA i)) {|Agent M, Key merEK, onlyEnc|} ∈ parts (knows Spy evs);
         CA i ∉ bad; CA i ≠ RCA; evs ∈ set_mr |]
      ==> ∃X Y Z.
             Says (CA i) M {|X, Y, cert M merEK onlyEnc (priSK (CA i)), Z|} ∈ set evs

lemma certificate_merEK_valid:

      [| cert M merEK onlyEnc (priSK (CA i)) ∈ parts (knows Spy evs); CA i ∉ bad;
         CA i ≠ RCA; evs ∈ set_mr |]
      ==> ∃X Y Z.
             Says (CA i) M {|X, Y, cert M merEK onlyEnc (priSK (CA i)), Z|} ∈ set evs