Theory Merchant_Registration

(*  Title:      HOL/SET_Protocol/Merchant_Registration.thy
    Author:     Giampaolo Bella
    Author:     Fabio Massacci
    Author:     Lawrence C Paulson
*)

section‹The SET Merchant Registration Protocol›

theory Merchant_Registration
imports Public_SET
begin

text‹Copmpared with Cardholder Reigstration, ‹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›).›


inductive_set
  set_mr :: "event list set"
where

  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 ⦃Crypt KM1
                (sign K ⦃Agent M, Nonce NM2, Key merSK, Key merEK⦄), X⦄
          ∈ 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 ∪ 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 ∪ 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 ∪ (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 ∪ (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 ‹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 ∪ H)) ⟶ (K∈KK | Key K ∈ analz H)
      ==>
      P ⟶ (Key K ∈ analz (Key`KK ∪ 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 ∪ (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)
  ― ‹5 seconds on a 1.6GHz 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