diff -r 8ea2645b8132 -r d3b8d972a488 src/HOL/SET-Protocol/Merchant_Registration.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/SET-Protocol/Merchant_Registration.thy Tue Sep 23 15:40:27 2003 +0200 @@ -0,0 +1,435 @@ +(* Title: HOL/Auth/SET/Merchant_Registration + ID: $Id$ + Authors: Giampaolo Bella, Fabio Massacci, Lawrence C Paulson +*) + +header{*The SET Merchant Registration Protocol*} + +theory Merchant_Registration = PublicSET: + +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 \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) +txt{*Fake*} +apply (force dest!: usedI keysFor_parts_insert) +txt{*Message 2*} +apply force +txt{*Message 3*} +apply (blast dest: Gets_certificate_valid) +txt{*Message 4*} +apply force +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*} +txt{*Fake*} +apply spy_analz +txt{*Message 3*} +apply auto +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) +txt{*Fake*} +apply spy_analz +txt{*Message 1*} +apply force +txt{*Message 3*} +apply (auto intro: analz_into_parts [THEN usedI] in_parts_Says_imp_used) +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