(* Title: HOL/Auth/SET/Purchase ID: $Id: Purchase.thy,v 1.8 2005/06/20 13:54:39 paulson Exp $ Authors: Giampaolo Bella, Fabio Massacci, Lawrence C Paulson *) header{*Purchase Phase of SET*} theory Purchase imports PublicSET begin text{* Note: nonces seem to consist of 20 bytes. That includes both freshness challenges (Chall-EE, etc.) and important secrets (CardSecret, PANsecret) This version omits @{text LID_C} but retains @{text LID_M}. At first glance (Programmer's Guide page 267) it seems that both numbers are just introduced for the respective convenience of the Cardholder's and Merchant's system. However, omitting both of them would create a problem of identification: how can the Merchant's system know what transaction is it supposed to process? Further reading (Programmer's guide page 309) suggest that there is an outside bootstrapping message (SET initiation message) which is used by the Merchant and the Cardholder to agree on the actual transaction. This bootstrapping message is described in the SET External Interface Guide and ought to generate @{text LID_M}. According SET Extern Interface Guide, this number might be a cookie, an invoice number etc. The Programmer's Guide on page 310, states that in absence of @{text LID_M} the protocol must somehow ("outside SET") identify the transaction from OrderDesc, which is assumed to be a searchable text only field. Thus, it is assumed that the Merchant or the Cardholder somehow agreed out-of-bad on the value of @{text LID_M} (for instance a cookie in a web transaction etc.). This out-of-band agreement is expressed with a preliminary start action in which the merchant and the Cardholder agree on the appropriate values. Agreed values are stored with a suitable notes action. "XID is a transaction ID that is usually generated by the Merchant system, unless there is no PInitRes, in which case it is generated by the Cardholder system. It is a randomly generated 20 byte variable that is globally unique (statistically). Merchant and Cardholder systems shall use appropriate random number generators to ensure the global uniqueness of XID." --Programmer's Guide, page 267. PI (Payment Instruction) is the most central and sensitive data structure in SET. It is used to pass the data required to authorize a payment card payment from the Cardholder to the Payment Gateway, which will use the data to initiate a payment card transaction through the traditional payment card financial network. The data is encrypted by the Cardholder and sent via the Merchant, such that the data is hidden from the Merchant unless the Acquirer passes the data back to the Merchant. --Programmer's Guide, page 271.*} consts CardSecret :: "nat => nat" --{*Maps Cardholders to CardSecrets. A CardSecret of 0 means no cerificate, must use unsigned format.*} PANSecret :: "nat => nat" --{*Maps Cardholders to PANSecrets.*} set_pur :: "event list set" inductive set_pur intros Nil: --{*Initial trace is empty*} "[] ∈ set_pur" Fake: --{*The spy MAY say anything he CAN say.*} "[| evsf ∈ set_pur; X ∈ synth(analz(knows Spy evsf)) |] ==> Says Spy B X # evsf ∈ set_pur" Reception: --{*If A sends a message X to B, then B might receive it*} "[| evsr ∈ set_pur; Says A B X ∈ set evsr |] ==> Gets B X # evsr ∈ set_pur" Start: --{*Added start event which is out-of-band for SET: the Cardholder and the merchant agree on the amounts and uses @{text LID_M} as an identifier. This is suggested by the External Interface Guide. The Programmer's Guide, in absence of @{text LID_M}, states that the merchant uniquely identifies the order out of some data contained in OrderDesc.*} "[|evsStart ∈ set_pur; Number LID_M ∉ used evsStart; C = Cardholder k; M = Merchant i; P = PG j; Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|}; LID_M ∉ range CardSecret; LID_M ∉ range PANSecret |] ==> Notes C {|Number LID_M, Transaction|} # Notes M {|Number LID_M, Agent P, Transaction|} # evsStart ∈ set_pur" PInitReq: --{*Purchase initialization, page 72 of Formal Protocol Desc.*} "[|evsPIReq ∈ set_pur; Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|}; Nonce Chall_C ∉ used evsPIReq; Chall_C ∉ range CardSecret; Chall_C ∉ range PANSecret; Notes C {|Number LID_M, Transaction |} ∈ set evsPIReq |] ==> Says C M {|Number LID_M, Nonce Chall_C|} # evsPIReq ∈ set_pur" PInitRes: --{*Merchant replies with his own label XID and the encryption key certificate of his chosen Payment Gateway. Page 74 of Formal Protocol Desc. We use @{text LID_M} to identify Cardholder*} "[|evsPIRes ∈ set_pur; Gets M {|Number LID_M, Nonce Chall_C|} ∈ set evsPIRes; Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|}; Notes M {|Number LID_M, Agent P, Transaction|} ∈ set evsPIRes; Nonce Chall_M ∉ used evsPIRes; Chall_M ∉ range CardSecret; Chall_M ∉ range PANSecret; Number XID ∉ used evsPIRes; XID ∉ range CardSecret; XID ∉ range PANSecret|] ==> Says M C (sign (priSK M) {|Number LID_M, Number XID, Nonce Chall_C, Nonce Chall_M, cert P (pubEK P) onlyEnc (priSK RCA)|}) # evsPIRes ∈ set_pur" PReqUns: --{*UNSIGNED Purchase request (CardSecret = 0). Page 79 of Formal Protocol Desc. Merchant never sees the amount in clear. This holds of the real protocol, where XID identifies the transaction. We omit Hash{|Number XID, Nonce (CardSecret k)|} from PIHead because the CardSecret is 0 and because AuthReq treated the unsigned case very differently from the signed one anyway.*} "[|evsPReqU ∈ set_pur; C = Cardholder k; CardSecret k = 0; Key KC1 ∉ used evsPReqU; KC1 ∈ symKeys; Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|}; HOD = Hash{|Number OrderDesc, Number PurchAmt|}; OIData = {|Number LID_M, Number XID, Nonce Chall_C, HOD,Nonce Chall_M|}; PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M|}; Gets C (sign (priSK M) {|Number LID_M, Number XID, Nonce Chall_C, Nonce Chall_M, cert P EKj onlyEnc (priSK RCA)|}) ∈ set evsPReqU; Says C M {|Number LID_M, Nonce Chall_C|} ∈ set evsPReqU; Notes C {|Number LID_M, Transaction|} ∈ set evsPReqU |] ==> Says C M {|EXHcrypt KC1 EKj {|PIHead, Hash OIData|} (Pan (pan C)), OIData, Hash{|PIHead, Pan (pan C)|} |} # Notes C {|Key KC1, Agent M|} # evsPReqU ∈ set_pur" PReqS: --{*SIGNED Purchase request. Page 77 of Formal Protocol Desc. We could specify the equation @{term "PIReqSigned = {| PIDualSigned, OIDualSigned |}"}, since the Formal Desc. gives PIHead the same format in the unsigned case. However, there's little point, as P treats the signed and unsigned cases differently.*} "[|evsPReqS ∈ set_pur; C = Cardholder k; CardSecret k ≠ 0; Key KC2 ∉ used evsPReqS; KC2 ∈ symKeys; Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|}; HOD = Hash{|Number OrderDesc, Number PurchAmt|}; OIData = {|Number LID_M, Number XID, Nonce Chall_C, HOD, Nonce Chall_M|}; PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M, Hash{|Number XID, Nonce (CardSecret k)|}|}; PANData = {|Pan (pan C), Nonce (PANSecret k)|}; PIData = {|PIHead, PANData|}; PIDualSigned = {|sign (priSK C) {|Hash PIData, Hash OIData|}, EXcrypt KC2 EKj {|PIHead, Hash OIData|} PANData|}; OIDualSigned = {|OIData, Hash PIData|}; Gets C (sign (priSK M) {|Number LID_M, Number XID, Nonce Chall_C, Nonce Chall_M, cert P EKj onlyEnc (priSK RCA)|}) ∈ set evsPReqS; Says C M {|Number LID_M, Nonce Chall_C|} ∈ set evsPReqS; Notes C {|Number LID_M, Transaction|} ∈ set evsPReqS |] ==> Says C M {|PIDualSigned, OIDualSigned|} # Notes C {|Key KC2, Agent M|} # evsPReqS ∈ set_pur" --{*Authorization Request. Page 92 of Formal Protocol Desc. Sent in response to Purchase Request.*} AuthReq: "[| evsAReq ∈ set_pur; Key KM ∉ used evsAReq; KM ∈ symKeys; Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|}; HOD = Hash{|Number OrderDesc, Number PurchAmt|}; OIData = {|Number LID_M, Number XID, Nonce Chall_C, HOD, Nonce Chall_M|}; CardSecret k ≠ 0 --> P_I = {|sign (priSK C) {|HPIData, Hash OIData|}, encPANData|}; Gets M {|P_I, OIData, HPIData|} ∈ set evsAReq; Says M C (sign (priSK M) {|Number LID_M, Number XID, Nonce Chall_C, Nonce Chall_M, cert P EKj onlyEnc (priSK RCA)|}) ∈ set evsAReq; Notes M {|Number LID_M, Agent P, Transaction|} ∈ set evsAReq |] ==> Says M P (EncB (priSK M) KM (pubEK P) {|Number LID_M, Number XID, Hash OIData, HOD|} P_I) # evsAReq ∈ set_pur" --{*Authorization Response has two forms: for UNSIGNED and SIGNED PIs. Page 99 of Formal Protocol Desc. PI is a keyword (product!), so we call it @{text P_I}. The hashes HOD and HOIData occur independently in @{text P_I} and in M's message. The authCode in AuthRes represents the baggage of EncB, which in the full protocol is [CapToken], [AcqCardMsg], [AuthToken]: optional items for split shipments, recurring payments, etc.*} AuthResUns: --{*Authorization Response, UNSIGNED*} "[| evsAResU ∈ set_pur; C = Cardholder k; M = Merchant i; Key KP ∉ used evsAResU; KP ∈ symKeys; CardSecret k = 0; KC1 ∈ symKeys; KM ∈ symKeys; PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M|}; P_I = EXHcrypt KC1 EKj {|PIHead, HOIData|} (Pan (pan C)); Gets P (EncB (priSK M) KM (pubEK P) {|Number LID_M, Number XID, HOIData, HOD|} P_I) ∈ set evsAResU |] ==> Says P M (EncB (priSK P) KP (pubEK M) {|Number LID_M, Number XID, Number PurchAmt|} authCode) # evsAResU ∈ set_pur" AuthResS: --{*Authorization Response, SIGNED*} "[| evsAResS ∈ set_pur; C = Cardholder k; Key KP ∉ used evsAResS; KP ∈ symKeys; CardSecret k ≠ 0; KC2 ∈ symKeys; KM ∈ symKeys; P_I = {|sign (priSK C) {|Hash PIData, HOIData|}, EXcrypt KC2 (pubEK P) {|PIHead, HOIData|} PANData|}; PANData = {|Pan (pan C), Nonce (PANSecret k)|}; PIData = {|PIHead, PANData|}; PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M, Hash{|Number XID, Nonce (CardSecret k)|}|}; Gets P (EncB (priSK M) KM (pubEK P) {|Number LID_M, Number XID, HOIData, HOD|} P_I) ∈ set evsAResS |] ==> Says P M (EncB (priSK P) KP (pubEK M) {|Number LID_M, Number XID, Number PurchAmt|} authCode) # evsAResS ∈ set_pur" PRes: --{*Purchase response.*} "[| evsPRes ∈ set_pur; KP ∈ symKeys; M = Merchant i; Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|}; Gets M (EncB (priSK P) KP (pubEK M) {|Number LID_M, Number XID, Number PurchAmt|} authCode) ∈ set evsPRes; Gets M {|Number LID_M, Nonce Chall_C|} ∈ set evsPRes; Says M P (EncB (priSK M) KM (pubEK P) {|Number LID_M, Number XID, Hash OIData, HOD|} P_I) ∈ set evsPRes; Notes M {|Number LID_M, Agent P, Transaction|} ∈ set evsPRes |] ==> Says M C (sign (priSK M) {|Number LID_M, Number XID, Nonce Chall_C, Hash (Number PurchAmt)|}) # evsPRes ∈ set_pur" specification (CardSecret PANSecret) inj_CardSecret: "inj CardSecret" inj_PANSecret: "inj PANSecret" CardSecret_neq_PANSecret: "CardSecret k ≠ PANSecret k'" --{*No CardSecret equals any PANSecret*} apply (rule_tac x="curry nat2_to_nat 0" in exI) apply (rule_tac x="curry nat2_to_nat 1" in exI) apply (simp add: nat2_to_nat_inj [THEN inj_eq] inj_on_def) done 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] declare CardSecret_neq_PANSecret [iff] CardSecret_neq_PANSecret [THEN not_sym, iff] declare inj_CardSecret [THEN inj_eq, iff] inj_PANSecret [THEN inj_eq, iff] subsection{*Possibility Properties*} lemma Says_to_Gets: "Says A B X # evs ∈ set_pur ==> Gets B X # Says A B X # evs ∈ set_pur" by (rule set_pur.Reception, auto) text{*Possibility for UNSIGNED purchases. Note that we need to ensure that XID differs from OrderDesc and PurchAmt, since it is supposed to be a unique number!*} lemma possibility_Uns: "[| CardSecret k = 0; C = Cardholder k; M = Merchant i; Key KC ∉ used []; Key KM ∉ used []; Key KP ∉ used []; KC ∈ symKeys; KM ∈ symKeys; KP ∈ symKeys; KC < KM; KM < KP; Nonce Chall_C ∉ used []; Chall_C ∉ range CardSecret ∪ range PANSecret; Nonce Chall_M ∉ used []; Chall_M ∉ range CardSecret ∪ range PANSecret; Chall_C < Chall_M; Number LID_M ∉ used []; LID_M ∉ range CardSecret ∪ range PANSecret; Number XID ∉ used []; XID ∉ range CardSecret ∪ range PANSecret; LID_M < XID; XID < OrderDesc; OrderDesc < PurchAmt |] ==> ∃evs ∈ set_pur. Says M C (sign (priSK M) {|Number LID_M, Number XID, Nonce Chall_C, Hash (Number PurchAmt)|}) ∈ set evs" apply (intro exI bexI) apply (rule_tac [2] set_pur.Nil [THEN set_pur.Start [of _ LID_M C k M i _ _ _ OrderDesc PurchAmt], THEN set_pur.PInitReq [of concl: C M LID_M Chall_C], THEN Says_to_Gets, THEN set_pur.PInitRes [of concl: M C LID_M XID Chall_C Chall_M], THEN Says_to_Gets, THEN set_pur.PReqUns [of concl: C M KC], THEN Says_to_Gets, THEN set_pur.AuthReq [of concl: M "PG j" KM LID_M XID], THEN Says_to_Gets, THEN set_pur.AuthResUns [of concl: "PG j" M KP LID_M XID], THEN Says_to_Gets, THEN set_pur.PRes]) apply (tactic "basic_possibility_tac") apply (simp_all add: used_Cons symKeys_neq_imp_neq) done lemma possibility_S: "[| CardSecret k ≠ 0; C = Cardholder k; M = Merchant i; Key KC ∉ used []; Key KM ∉ used []; Key KP ∉ used []; KC ∈ symKeys; KM ∈ symKeys; KP ∈ symKeys; KC < KM; KM < KP; Nonce Chall_C ∉ used []; Chall_C ∉ range CardSecret ∪ range PANSecret; Nonce Chall_M ∉ used []; Chall_M ∉ range CardSecret ∪ range PANSecret; Chall_C < Chall_M; Number LID_M ∉ used []; LID_M ∉ range CardSecret ∪ range PANSecret; Number XID ∉ used []; XID ∉ range CardSecret ∪ range PANSecret; LID_M < XID; XID < OrderDesc; OrderDesc < PurchAmt |] ==> ∃evs ∈ set_pur. Says M C (sign (priSK M) {|Number LID_M, Number XID, Nonce Chall_C, Hash (Number PurchAmt)|}) ∈ set evs" apply (intro exI bexI) apply (rule_tac [2] set_pur.Nil [THEN set_pur.Start [of _ LID_M C k M i _ _ _ OrderDesc PurchAmt], THEN set_pur.PInitReq [of concl: C M LID_M Chall_C], THEN Says_to_Gets, THEN set_pur.PInitRes [of concl: M C LID_M XID Chall_C Chall_M], THEN Says_to_Gets, THEN set_pur.PReqS [of concl: C M _ _ KC], THEN Says_to_Gets, THEN set_pur.AuthReq [of concl: M "PG j" KM LID_M XID], THEN Says_to_Gets, THEN set_pur.AuthResS [of concl: "PG j" M KP LID_M XID], THEN Says_to_Gets, THEN set_pur.PRes]) apply (tactic "basic_possibility_tac") apply (auto simp add: used_Cons symKeys_neq_imp_neq) done text{*General facts about message reception*} lemma Gets_imp_Says: "[| Gets B X ∈ set evs; evs ∈ set_pur |] ==> ∃A. Says A B X ∈ set evs" apply (erule rev_mp) apply (erule set_pur.induct, auto) done lemma Gets_imp_knows_Spy: "[| Gets B X ∈ set evs; evs ∈ set_pur |] ==> X ∈ knows Spy evs" by (blast dest!: Gets_imp_Says Says_imp_knows_Spy) declare Gets_imp_knows_Spy [THEN parts.Inj, dest] text{*Forwarding lemmas, to aid simplification*} lemma AuthReq_msg_in_parts_spies: "[|Gets M {|P_I, OIData, HPIData|} ∈ set evs; evs ∈ set_pur|] ==> P_I ∈ parts (knows Spy evs)" by auto lemma AuthReq_msg_in_analz_spies: "[|Gets M {|P_I, OIData, HPIData|} ∈ set evs; evs ∈ set_pur|] ==> P_I ∈ analz (knows Spy evs)" by (blast dest: Gets_imp_knows_Spy [THEN analz.Inj]) subsection{*Proofs on Asymmetric Keys*} text{*Private Keys are Secret*} text{*Spy never sees an agent's private keys! (unless it's bad at start)*} lemma Spy_see_private_Key [simp]: "evs ∈ set_pur ==> (Key(invKey (publicKey b A)) ∈ parts(knows Spy evs)) = (A ∈ bad)" apply (erule set_pur.induct) apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*} apply auto done declare Spy_see_private_Key [THEN [2] rev_iffD1, dest!] lemma Spy_analz_private_Key [simp]: "evs ∈ set_pur ==> (Key(invKey (publicKey b A)) ∈ analz(knows Spy evs)) = (A ∈ bad)" by auto declare Spy_analz_private_Key [THEN [2] rev_iffD1, dest!] text{*rewriting rule for priEK's*} lemma parts_image_priEK: "[|Key (priEK C) ∈ parts (Key`KK Un (knows Spy evs)); evs ∈ set_pur|] ==> priEK C ∈ KK | C ∈ bad" by auto text{*trivial proof because @{term"priEK C"} never appears even in @{term "parts evs"}. *} lemma analz_image_priEK: "evs ∈ set_pur ==> (Key (priEK C) ∈ analz (Key`KK Un (knows Spy evs))) = (priEK C ∈ KK | C ∈ bad)" by (blast dest!: parts_image_priEK intro: analz_mono [THEN [2] rev_subsetD]) subsection{*Public Keys in Certificates are Correct*} lemma Crypt_valid_pubEK [dest!]: "[| Crypt (priSK RCA) {|Agent C, Key EKi, onlyEnc|} ∈ parts (knows Spy evs); evs ∈ set_pur |] ==> EKi = pubEK C" by (erule rev_mp, erule set_pur.induct, auto) lemma Crypt_valid_pubSK [dest!]: "[| Crypt (priSK RCA) {|Agent C, Key SKi, onlySig|} ∈ parts (knows Spy evs); evs ∈ set_pur |] ==> SKi = pubSK C" by (erule rev_mp, erule set_pur.induct, auto) lemma certificate_valid_pubEK: "[| cert C EKi onlyEnc (priSK RCA) ∈ parts (knows Spy evs); evs ∈ set_pur |] ==> EKi = pubEK C" by (unfold cert_def signCert_def, auto) lemma certificate_valid_pubSK: "[| cert C SKi onlySig (priSK RCA) ∈ parts (knows Spy evs); evs ∈ set_pur |] ==> SKi = pubSK C" by (unfold cert_def signCert_def, auto) lemma Says_certificate_valid [simp]: "[| Says A B (sign SK {|lid, xid, cc, cm, cert C EK onlyEnc (priSK RCA)|}) ∈ set evs; evs ∈ set_pur |] ==> EK = pubEK C" by (unfold sign_def, auto) lemma Gets_certificate_valid [simp]: "[| Gets A (sign SK {|lid, xid, cc, cm, cert C EK onlyEnc (priSK RCA)|}) ∈ set evs; evs ∈ set_pur |] ==> EK = pubEK C" by (frule Gets_imp_Says, auto) ML {* val Gets_certificate_valid = thm "Gets_certificate_valid"; fun valid_certificate_tac i = EVERY [ftac Gets_certificate_valid i, assume_tac i, REPEAT (hyp_subst_tac i)]; *} subsection{*Proofs on Symmetric Keys*} text{*Nobody can have used non-existent keys!*} lemma new_keys_not_used [rule_format,simp]: "evs ∈ set_pur ==> Key K ∉ used evs --> K ∈ symKeys --> K ∉ keysFor (parts (knows Spy evs))" apply (erule set_pur.induct) apply (tactic{*valid_certificate_tac 8*}) --{*PReqS*} apply (tactic{*valid_certificate_tac 7*}) --{*PReqUns*} apply auto apply (force dest!: usedI keysFor_parts_insert) --{*Fake*} done lemma new_keys_not_analzd: "[|Key K ∉ used evs; K ∈ symKeys; evs ∈ set_pur |] ==> K ∉ keysFor (analz (knows Spy evs))" by (blast intro: keysFor_mono [THEN [2] rev_subsetD] dest: new_keys_not_used) lemma Crypt_parts_imp_used: "[|Crypt K X ∈ parts (knows Spy evs); K ∈ symKeys; evs ∈ set_pur |] ==> 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_pur |] ==> Key K ∈ used evs" by (blast intro: Crypt_parts_imp_used) text{*New versions: as above, but generalized to have the KK argument*} lemma gen_new_keys_not_used: "[|Key K ∉ used evs; K ∈ symKeys; evs ∈ set_pur |] ==> 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_pur |] ==> K ∉ keysFor (analz (Key`KK Un knows Spy evs))" by (blast intro: keysFor_mono [THEN subsetD] dest: gen_new_keys_not_used) lemma analz_Key_image_insert_eq: "[|Key K ∉ used evs; K ∈ symKeys; evs ∈ set_pur |] ==> 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) subsection{*Secrecy of Symmetric Keys*} 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_pur ==> (∀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_pur.induct) apply (rule_tac [!] allI)+ apply (rule_tac [!] impI [THEN Key_analz_image_Key_lemma, THEN impI])+ apply (frule_tac [9] AuthReq_msg_in_analz_spies) --{*AReq*} apply (tactic{*valid_certificate_tac 8*}) --{*PReqS*} apply (tactic{*valid_certificate_tac 7*}) --{*PReqUns*} apply (simp_all del: image_insert image_Un imp_disjL add: analz_image_keys_simps disj_simps analz_Key_image_insert_eq notin_image_iff analz_insert_simps analz_image_priEK) --{*35 seconds on a 1.8GHz machine*} apply spy_analz --{*Fake*} apply (blast elim!: ballE)+ --{*PReq: unsigned and signed*} done subsection{*Secrecy of Nonces*} text{*As usual: we express the property as a logical equivalence*} lemma Nonce_analz_image_Key_lemma: "P --> (Nonce N ∈ analz (Key`KK Un H)) --> (Nonce N ∈ analz H) ==> P --> (Nonce N ∈ analz (Key`KK Un H)) = (Nonce N ∈ analz H)" by (blast intro: analz_mono [THEN [2] rev_subsetD]) text{*The @{text "(no_asm)"} attribute is essential, since it retains the quantifier and allows the simprule's condition to itself be simplified.*} lemma Nonce_compromise [rule_format (no_asm)]: "evs ∈ set_pur ==> (∀N KK. (∀K ∈ KK. K ∉ range(λC. priEK C)) --> (Nonce N ∈ analz (Key`KK ∪ (knows Spy evs))) = (Nonce N ∈ analz (knows Spy evs)))" apply (erule set_pur.induct) apply (rule_tac [!] allI)+ apply (rule_tac [!] impI [THEN Nonce_analz_image_Key_lemma])+ apply (frule_tac [9] AuthReq_msg_in_analz_spies) --{*AReq*} apply (tactic{*valid_certificate_tac 8*}) --{*PReqS*} apply (tactic{*valid_certificate_tac 7*}) --{*PReqUns*} apply (simp_all del: image_insert image_Un imp_disjL add: analz_image_keys_simps disj_simps symKey_compromise analz_Key_image_insert_eq notin_image_iff analz_insert_simps analz_image_priEK) --{*35 seconds on a 1.8GHz machine*} apply spy_analz --{*Fake*} apply (blast elim!: ballE) --{*PReqS*} done lemma PANSecret_notin_spies: "[|Nonce (PANSecret k) ∈ analz (knows Spy evs); evs ∈ set_pur|] ==> (∃V W X Y KC2 M. ∃P ∈ bad. Says (Cardholder k) M {|{|W, EXcrypt KC2 (pubEK P) X {|Y, Nonce (PANSecret k)|}|}, V|} ∈ set evs)" apply (erule rev_mp) apply (erule set_pur.induct) apply (frule_tac [9] AuthReq_msg_in_analz_spies) apply (tactic{*valid_certificate_tac 8*}) --{*PReqS*} apply (simp_all del: image_insert image_Un imp_disjL add: analz_image_keys_simps disj_simps symKey_compromise pushes sign_def Nonce_compromise analz_Key_image_insert_eq notin_image_iff analz_insert_simps analz_image_priEK) --{*13 seconds on a 1.8GHz machine*} apply spy_analz apply (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj]) apply (blast dest: Says_imp_knows_Spy [THEN analz.Inj] Gets_imp_knows_Spy [THEN analz.Inj]) apply (blast dest: Gets_imp_knows_Spy [THEN analz.Inj]) --{*PReqS*} apply (blast dest: Says_imp_knows_Spy [THEN analz.Inj] Gets_imp_knows_Spy [THEN analz.Inj]) --{*PRes*} done text{*This theorem is a bit silly, in that many CardSecrets are 0! But then we don't care. NOT USED*} lemma CardSecret_notin_spies: "evs ∈ set_pur ==> Nonce (CardSecret i) ∉ parts (knows Spy evs)" by (erule set_pur.induct, auto) subsection{*Confidentiality of PAN*} lemma analz_image_pan_lemma: "(Pan P ∈ analz (Key`nE Un H)) --> (Pan P ∈ analz H) ==> (Pan P ∈ analz (Key`nE Un H)) = (Pan P ∈ analz H)" by (blast intro: analz_mono [THEN [2] rev_subsetD]) text{*The @{text "(no_asm)"} attribute is essential, since it retains the quantifier and allows the simprule's condition to itself be simplified.*} lemma analz_image_pan [rule_format (no_asm)]: "evs ∈ set_pur ==> ∀KK. (∀K ∈ KK. K ∉ range(λC. priEK C)) --> (Pan P ∈ analz (Key`KK Un (knows Spy evs))) = (Pan P ∈ analz (knows Spy evs))" apply (erule set_pur.induct) apply (rule_tac [!] allI impI)+ apply (rule_tac [!] analz_image_pan_lemma)+ apply (frule_tac [9] AuthReq_msg_in_analz_spies) --{*AReq*} apply (tactic{*valid_certificate_tac 8*}) --{*PReqS*} apply (tactic{*valid_certificate_tac 7*}) --{*PReqUns*} apply (simp_all del: image_insert image_Un imp_disjL add: analz_image_keys_simps symKey_compromise pushes sign_def analz_Key_image_insert_eq notin_image_iff analz_insert_simps analz_image_priEK) --{*32 seconds on a 1.8GHz machine*} apply spy_analz --{*Fake*} apply auto done lemma analz_insert_pan: "[| evs ∈ set_pur; K ∉ range(λC. priEK C) |] ==> (Pan P ∈ analz (insert (Key K) (knows Spy evs))) = (Pan P ∈ analz (knows Spy evs))" by (simp del: image_insert image_Un add: analz_image_keys_simps analz_image_pan) text{*Confidentiality of the PAN, unsigned case.*} theorem pan_confidentiality_unsigned: "[| Pan (pan C) ∈ analz(knows Spy evs); C = Cardholder k; CardSecret k = 0; evs ∈ set_pur|] ==> ∃P M KC1 K X Y. Says C M {|EXHcrypt KC1 (pubEK P) X (Pan (pan C)), Y|} ∈ set evs & P ∈ bad" apply (erule rev_mp) apply (erule set_pur.induct) apply (frule_tac [9] AuthReq_msg_in_analz_spies) --{*AReq*} apply (tactic{*valid_certificate_tac 8*}) --{*PReqS*} apply (tactic{*valid_certificate_tac 7*}) --{*PReqUns*} apply (simp_all del: image_insert image_Un imp_disjL add: analz_image_keys_simps analz_insert_pan analz_image_pan notin_image_iff analz_insert_simps analz_image_priEK) --{*15 seconds on a 1.8GHz machine*} apply spy_analz --{*Fake*} apply blast --{*PReqUns: unsigned*} apply force --{*PReqS: signed*} done text{*Confidentiality of the PAN, signed case.*} theorem pan_confidentiality_signed: "[|Pan (pan C) ∈ analz(knows Spy evs); C = Cardholder k; CardSecret k ≠ 0; evs ∈ set_pur|] ==> ∃P M KC2 PIDualSign_1 PIDualSign_2 other OIDualSign. Says C M {|{|PIDualSign_1, EXcrypt KC2 (pubEK P) PIDualSign_2 {|Pan (pan C), other|}|}, OIDualSign|} ∈ set evs & P ∈ bad" apply (erule rev_mp) apply (erule set_pur.induct) apply (frule_tac [9] AuthReq_msg_in_analz_spies) --{*AReq*} apply (tactic{*valid_certificate_tac 8*}) --{*PReqS*} apply (tactic{*valid_certificate_tac 7*}) --{*PReqUns*} apply (simp_all del: image_insert image_Un imp_disjL add: analz_image_keys_simps analz_insert_pan analz_image_pan notin_image_iff analz_insert_simps analz_image_priEK) --{*17 seconds on a 1.8GHz machine*} apply spy_analz --{*Fake*} apply force --{*PReqUns: unsigned*} apply blast --{*PReqS: signed*} done text{*General goal: that C, M and PG agree on those details of the transaction that they are allowed to know about. PG knows about price and account details. M knows about the order description and price. C knows both.*} subsection{*Proofs Common to Signed and Unsigned Versions*} lemma M_Notes_PG: "[|Notes M {|Number LID_M, Agent P, Agent M, Agent C, etc|} ∈ set evs; evs ∈ set_pur|] ==> ∃j. P = PG j" by (erule rev_mp, erule set_pur.induct, simp_all) text{*If we trust M, then @{term LID_M} determines his choice of P (Payment Gateway)*} lemma goodM_gives_correct_PG: "[| MsgPInitRes = {|Number LID_M, xid, cc, cm, cert P EKj onlyEnc (priSK RCA)|}; Crypt (priSK M) (Hash MsgPInitRes) ∈ parts (knows Spy evs); evs ∈ set_pur; M ∉ bad |] ==> ∃j trans. P = PG j & Notes M {|Number LID_M, Agent P, trans|} ∈ set evs" apply clarify apply (erule rev_mp) apply (erule set_pur.induct) apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*} apply simp_all apply (blast intro: M_Notes_PG)+ done lemma C_gets_correct_PG: "[| Gets A (sign (priSK M) {|Number LID_M, xid, cc, cm, cert P EKj onlyEnc (priSK RCA)|}) ∈ set evs; evs ∈ set_pur; M ∉ bad|] ==> ∃j trans. P = PG j & Notes M {|Number LID_M, Agent P, trans|} ∈ set evs & EKj = pubEK P" by (rule refl [THEN goodM_gives_correct_PG, THEN exE], auto) text{*When C receives PInitRes, he learns M's choice of P*} lemma C_verifies_PInitRes: "[| MsgPInitRes = {|Number LID_M, Number XID, Nonce Chall_C, Nonce Chall_M, cert P EKj onlyEnc (priSK RCA)|}; Crypt (priSK M) (Hash MsgPInitRes) ∈ parts (knows Spy evs); evs ∈ set_pur; M ∉ bad|] ==> ∃j trans. Notes M {|Number LID_M, Agent P, trans|} ∈ set evs & P = PG j & EKj = pubEK P" apply clarify apply (erule rev_mp) apply (erule set_pur.induct) apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*} apply simp_all apply (blast intro: M_Notes_PG)+ done text{*Corollary of previous one*} lemma Says_C_PInitRes: "[|Says A C (sign (priSK M) {|Number LID_M, Number XID, Nonce Chall_C, Nonce Chall_M, cert P EKj onlyEnc (priSK RCA)|}) ∈ set evs; M ∉ bad; evs ∈ set_pur|] ==> ∃j trans. Notes M {|Number LID_M, Agent P, trans|} ∈ set evs & P = PG j & EKj = pubEK (PG j)" apply (frule Says_certificate_valid) apply (auto simp add: sign_def) apply (blast dest: refl [THEN goodM_gives_correct_PG]) apply (blast dest: refl [THEN C_verifies_PInitRes]) done text{*When P receives an AuthReq, he knows that the signed part originated with M. PIRes also has a signed message from M....*} lemma P_verifies_AuthReq: "[| AuthReqData = {|Number LID_M, Number XID, HOIData, HOD|}; Crypt (priSK M) (Hash {|AuthReqData, Hash P_I|}) ∈ parts (knows Spy evs); evs ∈ set_pur; M ∉ bad|] ==> ∃j trans KM OIData HPIData. Notes M {|Number LID_M, Agent (PG j), trans|} ∈ set evs & Gets M {|P_I, OIData, HPIData|} ∈ set evs & Says M (PG j) (EncB (priSK M) KM (pubEK (PG j)) AuthReqData P_I) ∈ set evs" apply clarify apply (erule rev_mp) apply (erule set_pur.induct, simp_all) apply (frule_tac [4] M_Notes_PG, auto) done text{*When M receives AuthRes, he knows that P signed it, including the identifying tags and the purchase amount, which he can verify. (Although the spec has SIGNED and UNSIGNED forms of AuthRes, they send the same message to M.) The conclusion is weak: M is existentially quantified! That is because Authorization Response does not refer to M, while the digital envelope weakens the link between @{term MsgAuthRes} and @{term"priSK M"}. Changing the precondition to refer to @{term "Crypt K (sign SK M)"} requires assuming @{term K} to be secure, since otherwise the Spy could create that message.*} theorem M_verifies_AuthRes: "[| MsgAuthRes = {|{|Number LID_M, Number XID, Number PurchAmt|}, Hash authCode|}; Crypt (priSK (PG j)) (Hash MsgAuthRes) ∈ parts (knows Spy evs); PG j ∉ bad; evs ∈ set_pur|] ==> ∃M KM KP HOIData HOD P_I. Gets (PG j) (EncB (priSK M) KM (pubEK (PG j)) {|Number LID_M, Number XID, HOIData, HOD|} P_I) ∈ set evs & Says (PG j) M (EncB (priSK (PG j)) KP (pubEK M) {|Number LID_M, Number XID, Number PurchAmt|} authCode) ∈ set evs" apply clarify apply (erule rev_mp) apply (erule set_pur.induct) apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*} apply simp_all apply blast+ done subsection{*Proofs for Unsigned Purchases*} text{*What we can derive from the ASSUMPTION that C issued a purchase request. In the unsigned case, we must trust "C": there's no authentication.*} lemma C_determines_EKj: "[| Says C M {|EXHcrypt KC1 EKj {|PIHead, Hash OIData|} (Pan (pan C)), OIData, Hash{|PIHead, Pan (pan C)|} |} ∈ set evs; PIHead = {|Number LID_M, Trans_details|}; evs ∈ set_pur; C = Cardholder k; M ∉ bad|] ==> ∃trans j. Notes M {|Number LID_M, Agent (PG j), trans |} ∈ set evs & EKj = pubEK (PG j)" apply clarify apply (erule rev_mp) apply (erule set_pur.induct, simp_all) apply (tactic{*valid_certificate_tac 2*}) --{*PReqUns*} apply auto apply (blast dest: Gets_imp_Says Says_C_PInitRes) done text{*Unicity of @{term LID_M} between Merchant and Cardholder notes*} lemma unique_LID_M: "[|Notes (Merchant i) {|Number LID_M, Agent P, Trans|} ∈ set evs; Notes C {|Number LID_M, Agent M, Agent C, Number OD, Number PA|} ∈ set evs; evs ∈ set_pur|] ==> M = Merchant i & Trans = {|Agent M, Agent C, Number OD, Number PA|}" apply (erule rev_mp) apply (erule rev_mp) apply (erule set_pur.induct, simp_all) apply (force dest!: Notes_imp_parts_subset_used) done text{*Unicity of @{term LID_M}, for two Merchant Notes events*} lemma unique_LID_M2: "[|Notes M {|Number LID_M, Trans|} ∈ set evs; Notes M {|Number LID_M, Trans'|} ∈ set evs; evs ∈ set_pur|] ==> Trans' = Trans" apply (erule rev_mp) apply (erule rev_mp) apply (erule set_pur.induct, simp_all) apply (force dest!: Notes_imp_parts_subset_used) done text{*Lemma needed below: for the case that if PRes is present, then @{term LID_M} has been used.*} lemma signed_imp_used: "[| Crypt (priSK M) (Hash X) ∈ parts (knows Spy evs); M ∉ bad; evs ∈ set_pur|] ==> parts {X} ⊆ used evs" apply (erule rev_mp) apply (erule set_pur.induct) apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*} apply simp_all apply safe apply blast+ done text{*Similar, with nested Hash*} lemma signed_Hash_imp_used: "[| Crypt (priSK C) (Hash {|H, Hash X|}) ∈ parts (knows Spy evs); C ∉ bad; evs ∈ set_pur|] ==> parts {X} ⊆ used evs" apply (erule rev_mp) apply (erule set_pur.induct) apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*} apply simp_all apply safe apply blast+ done text{*Lemma needed below: for the case that if PRes is present, then @{text LID_M} has been used.*} lemma PRes_imp_LID_used: "[| Crypt (priSK M) (Hash {|N, X|}) ∈ parts (knows Spy evs); M ∉ bad; evs ∈ set_pur|] ==> N ∈ used evs" by (drule signed_imp_used, auto) text{*When C receives PRes, he knows that M and P agreed to the purchase details. He also knows that P is the same PG as before*} lemma C_verifies_PRes_lemma: "[| Crypt (priSK M) (Hash MsgPRes) ∈ parts (knows Spy evs); Notes C {|Number LID_M, Trans |} ∈ set evs; Trans = {| Agent M, Agent C, Number OrderDesc, Number PurchAmt |}; MsgPRes = {|Number LID_M, Number XID, Nonce Chall_C, Hash (Number PurchAmt)|}; evs ∈ set_pur; M ∉ bad|] ==> ∃j KP. Notes M {|Number LID_M, Agent (PG j), Trans |} ∈ set evs & Gets M (EncB (priSK (PG j)) KP (pubEK M) {|Number LID_M, Number XID, Number PurchAmt|} authCode) ∈ set evs & Says M C (sign (priSK M) MsgPRes) ∈ set evs" apply clarify apply (erule rev_mp) apply (erule rev_mp) apply (erule set_pur.induct) apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*} apply simp_all apply blast apply blast apply (blast dest: PRes_imp_LID_used) apply (frule M_Notes_PG, auto) apply (blast dest: unique_LID_M) done text{*When the Cardholder receives Purchase Response from an uncompromised Merchant, he knows that M sent it. He also knows that M received a message signed by a Payment Gateway chosen by M to authorize the purchase.*} theorem C_verifies_PRes: "[| MsgPRes = {|Number LID_M, Number XID, Nonce Chall_C, Hash (Number PurchAmt)|}; Gets C (sign (priSK M) MsgPRes) ∈ set evs; Notes C {|Number LID_M, Agent M, Agent C, Number OrderDesc, Number PurchAmt|} ∈ set evs; evs ∈ set_pur; M ∉ bad|] ==> ∃P KP trans. Notes M {|Number LID_M,Agent P, trans|} ∈ set evs & Gets M (EncB (priSK P) KP (pubEK M) {|Number LID_M, Number XID, Number PurchAmt|} authCode) ∈ set evs & Says M C (sign (priSK M) MsgPRes) ∈ set evs" apply (rule C_verifies_PRes_lemma [THEN exE]) apply (auto simp add: sign_def) done subsection{*Proofs for Signed Purchases*} text{*Some Useful Lemmas: the cardholder knows what he is doing*} lemma Crypt_imp_Says_Cardholder: "[| Crypt K {|{|{|Number LID_M, others|}, Hash OIData|}, Hash PANData|} ∈ parts (knows Spy evs); PANData = {|Pan (pan (Cardholder k)), Nonce (PANSecret k)|}; Key K ∉ analz (knows Spy evs); evs ∈ set_pur|] ==> ∃M shash EK HPIData. Says (Cardholder k) M {|{|shash, Crypt K {|{|{|Number LID_M, others|}, Hash OIData|}, Hash PANData|}, Crypt EK {|Key K, PANData|}|}, OIData, HPIData|} ∈ set evs" apply (erule rev_mp) apply (erule rev_mp) apply (erule rev_mp) apply (erule set_pur.induct, analz_mono_contra) apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*} apply simp_all apply auto done lemma Says_PReqS_imp_trans_details_C: "[| MsgPReqS = {|{|shash, Crypt K {|{|{|Number LID_M, PIrest|}, Hash OIData|}, hashpd|}, cryptek|}, data|}; Says (Cardholder k) M MsgPReqS ∈ set evs; evs ∈ set_pur |] ==> ∃trans. Notes (Cardholder k) {|Number LID_M, Agent M, Agent (Cardholder k), trans|} ∈ set evs" apply (erule rev_mp) apply (erule rev_mp) apply (erule set_pur.induct) apply (simp_all (no_asm_simp)) apply auto done text{*Can't happen: only Merchants create this type of Note*} lemma Notes_Cardholder_self_False: "[|Notes (Cardholder k) {|Number n, Agent P, Agent (Cardholder k), Agent C, etc|} ∈ set evs; evs ∈ set_pur|] ==> False" by (erule rev_mp, erule set_pur.induct, auto) text{*When M sees a dual signature, he knows that it originated with C. Using XID he knows it was intended for him. This guarantee isn't useful to P, who never gets OIData.*} theorem M_verifies_Signed_PReq: "[| MsgDualSign = {|HPIData, Hash OIData|}; OIData = {|Number LID_M, etc|}; Crypt (priSK C) (Hash MsgDualSign) ∈ parts (knows Spy evs); Notes M {|Number LID_M, Agent P, extras|} ∈ set evs; M = Merchant i; C = Cardholder k; C ∉ bad; evs ∈ set_pur|] ==> ∃PIData PICrypt. HPIData = Hash PIData & Says C M {|{|sign (priSK C) MsgDualSign, PICrypt|}, OIData, Hash PIData|} ∈ set evs" apply clarify apply (erule rev_mp) apply (erule rev_mp) apply (erule set_pur.induct) apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*} apply simp_all apply blast apply (force dest!: signed_Hash_imp_used) apply (clarify) --{*speeds next step*} apply (blast dest: unique_LID_M) apply (blast dest!: Notes_Cardholder_self_False) done text{*When P sees a dual signature, he knows that it originated with C. and was intended for M. This guarantee isn't useful to M, who never gets PIData. I don't see how to link @{term "PG j"} and @{text LID_M} without assuming @{term "M ∉ bad"}.*} theorem P_verifies_Signed_PReq: "[| MsgDualSign = {|Hash PIData, HOIData|}; PIData = {|PIHead, PANData|}; PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M, TransStain|}; Crypt (priSK C) (Hash MsgDualSign) ∈ parts (knows Spy evs); evs ∈ set_pur; C ∉ bad; M ∉ bad|] ==> ∃OIData OrderDesc K j trans. HOD = Hash{|Number OrderDesc, Number PurchAmt|} & HOIData = Hash OIData & Notes M {|Number LID_M, Agent (PG j), trans|} ∈ set evs & Says C M {|{|sign (priSK C) MsgDualSign, EXcrypt K (pubEK (PG j)) {|PIHead, Hash OIData|} PANData|}, OIData, Hash PIData|} ∈ set evs" apply clarify apply (erule rev_mp) apply (erule set_pur.induct, simp_all) apply (auto dest!: C_gets_correct_PG) done lemma C_determines_EKj_signed: "[| Says C M {|{|sign (priSK C) text, EXcrypt K EKj {|PIHead, X|} Y|}, Z|} ∈ set evs; PIHead = {|Number LID_M, Number XID, W|}; C = Cardholder k; evs ∈ set_pur; M ∉ bad|] ==> ∃ trans j. Notes M {|Number LID_M, Agent (PG j), trans|} ∈ set evs & EKj = pubEK (PG j)" apply clarify apply (erule rev_mp) apply (erule set_pur.induct, simp_all, auto) apply (blast dest: C_gets_correct_PG) done lemma M_Says_AuthReq: "[| AuthReqData = {|Number LID_M, Number XID, HOIData, HOD|}; sign (priSK M) {|AuthReqData, Hash P_I|} ∈ parts (knows Spy evs); evs ∈ set_pur; M ∉ bad|] ==> ∃j trans KM. Notes M {|Number LID_M, Agent (PG j), trans |} ∈ set evs & Says M (PG j) (EncB (priSK M) KM (pubEK (PG j)) AuthReqData P_I) ∈ set evs" apply (rule refl [THEN P_verifies_AuthReq, THEN exE]) apply (auto simp add: sign_def) done text{*A variant of @{text M_verifies_Signed_PReq} with explicit PI information. Even here we cannot be certain about what C sent to M, since a bad PG could have replaced the two key fields. (NOT USED)*} lemma Signed_PReq_imp_Says_Cardholder: "[| MsgDualSign = {|Hash PIData, Hash OIData|}; OIData = {|Number LID_M, Number XID, Nonce Chall_C, HOD, etc|}; PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M, TransStain|}; PIData = {|PIHead, PANData|}; Crypt (priSK C) (Hash MsgDualSign) ∈ parts (knows Spy evs); M = Merchant i; C = Cardholder k; C ∉ bad; evs ∈ set_pur|] ==> ∃KC EKj. Says C M {|{|sign (priSK C) MsgDualSign, EXcrypt KC EKj {|PIHead, Hash OIData|} PANData|}, OIData, Hash PIData|} ∈ set evs" apply clarify apply (erule rev_mp) apply (erule rev_mp) apply (erule set_pur.induct, simp_all, auto) done text{*When P receives an AuthReq and a dual signature, he knows that C and M agree on the essential details. PurchAmt however is never sent by M to P; instead C and M both send @{term "HOD = Hash{|Number OrderDesc, Number PurchAmt|}"} and P compares the two copies of HOD. Agreement can't be proved for some things, including the symmetric keys used in the digital envelopes. On the other hand, M knows the true identity of PG (namely j'), and sends AReq there; he can't, however, check that the EXcrypt involves the correct PG's key. *} theorem P_sees_CM_agreement: "[| AuthReqData = {|Number LID_M, Number XID, HOIData, HOD|}; KC ∈ symKeys; Gets (PG j) (EncB (priSK M) KM (pubEK (PG j)) AuthReqData P_I) ∈ set evs; C = Cardholder k; PI_sign = sign (priSK C) {|Hash PIData, HOIData|}; P_I = {|PI_sign, EXcrypt KC (pubEK (PG j)) {|PIHead, HOIData|} PANData|}; PANData = {|Pan (pan C), Nonce (PANSecret k)|}; PIData = {|PIHead, PANData|}; PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M, TransStain|}; evs ∈ set_pur; C ∉ bad; M ∉ bad|] ==> ∃OIData OrderDesc KM' trans j' KC' KC'' P_I' P_I''. HOD = Hash{|Number OrderDesc, Number PurchAmt|} & HOIData = Hash OIData & Notes M {|Number LID_M, Agent (PG j'), trans|} ∈ set evs & Says C M {|P_I', OIData, Hash PIData|} ∈ set evs & Says M (PG j') (EncB (priSK M) KM' (pubEK (PG j')) AuthReqData P_I'') ∈ set evs & P_I' = {|PI_sign, EXcrypt KC' (pubEK (PG j')) {|PIHead, Hash OIData|} PANData|} & P_I'' = {|PI_sign, EXcrypt KC'' (pubEK (PG j)) {|PIHead, Hash OIData|} PANData|}" apply clarify apply (rule exE) apply (rule P_verifies_Signed_PReq [OF refl refl refl]) apply (simp (no_asm_use) add: sign_def EncB_def, blast) apply (assumption+, clarify, simp) apply (drule Gets_imp_knows_Spy [THEN parts.Inj], assumption) apply (blast elim: EncB_partsE dest: refl [THEN M_Says_AuthReq] unique_LID_M2) done end
lemma Says_to_Gets:
Says A B X # evs ∈ set_pur ==> Gets B X # Says A B X # evs ∈ set_pur
lemma possibility_Uns:
[| CardSecret k = 0; C = Cardholder k; M = Merchant i; Key KC ∉ used []; Key KM ∉ used []; Key KP ∉ used []; KC ∈ symKeys; KM ∈ symKeys; KP ∈ symKeys; KC < KM; KM < KP; Nonce Chall_C ∉ used []; Chall_C ∉ range CardSecret ∪ range PANSecret; Nonce Chall_M ∉ used []; Chall_M ∉ range CardSecret ∪ range PANSecret; Chall_C < Chall_M; Number LID_M ∉ used []; LID_M ∉ range CardSecret ∪ range PANSecret; Number XID ∉ used []; XID ∉ range CardSecret ∪ range PANSecret; LID_M < XID; XID < OrderDesc; OrderDesc < PurchAmt |] ==> ∃evs∈set_pur. Says M C (sign (priSK M) {|Number LID_M, Number XID, Nonce Chall_C, Hash (Number PurchAmt)|}) ∈ set evs
lemma possibility_S:
[| CardSecret k ≠ 0; C = Cardholder k; M = Merchant i; Key KC ∉ used []; Key KM ∉ used []; Key KP ∉ used []; KC ∈ symKeys; KM ∈ symKeys; KP ∈ symKeys; KC < KM; KM < KP; Nonce Chall_C ∉ used []; Chall_C ∉ range CardSecret ∪ range PANSecret; Nonce Chall_M ∉ used []; Chall_M ∉ range CardSecret ∪ range PANSecret; Chall_C < Chall_M; Number LID_M ∉ used []; LID_M ∉ range CardSecret ∪ range PANSecret; Number XID ∉ used []; XID ∉ range CardSecret ∪ range PANSecret; LID_M < XID; XID < OrderDesc; OrderDesc < PurchAmt |] ==> ∃evs∈set_pur. Says M C (sign (priSK M) {|Number LID_M, Number XID, Nonce Chall_C, Hash (Number PurchAmt)|}) ∈ set evs
lemma Gets_imp_Says:
[| Gets B X ∈ set evs; evs ∈ set_pur |] ==> ∃A. Says A B X ∈ set evs
lemma Gets_imp_knows_Spy:
[| Gets B X ∈ set evs; evs ∈ set_pur |] ==> X ∈ knows Spy evs
lemma AuthReq_msg_in_parts_spies:
[| Gets M {|P_I, OIData, HPIData|} ∈ set evs; evs ∈ set_pur |] ==> P_I ∈ parts (knows Spy evs)
lemma AuthReq_msg_in_analz_spies:
[| Gets M {|P_I, OIData, HPIData|} ∈ set evs; evs ∈ set_pur |] ==> P_I ∈ analz (knows Spy evs)
lemma Spy_see_private_Key:
evs ∈ set_pur ==> (Key (invKey (publicKey b A)) ∈ parts (knows Spy evs)) = (A ∈ bad)
lemma Spy_analz_private_Key:
evs ∈ set_pur ==> (Key (invKey (publicKey b A)) ∈ analz (knows Spy evs)) = (A ∈ bad)
lemma parts_image_priEK:
[| Key (priEK C) ∈ parts (Key ` KK ∪ knows Spy evs); evs ∈ set_pur |] ==> priEK C ∈ KK ∨ C ∈ bad
lemma analz_image_priEK:
evs ∈ set_pur ==> (Key (priEK C) ∈ analz (Key ` KK ∪ knows Spy evs)) = (priEK C ∈ KK ∨ C ∈ bad)
lemma Crypt_valid_pubEK:
[| Crypt (priSK RCA) {|Agent C, Key EKi, onlyEnc|} ∈ parts (knows Spy evs); evs ∈ set_pur |] ==> EKi = pubEK C
lemma Crypt_valid_pubSK:
[| Crypt (priSK RCA) {|Agent C, Key SKi, onlySig|} ∈ parts (knows Spy evs); evs ∈ set_pur |] ==> SKi = pubSK C
lemma certificate_valid_pubEK:
[| cert C EKi onlyEnc (priSK RCA) ∈ parts (knows Spy evs); evs ∈ set_pur |] ==> EKi = pubEK C
lemma certificate_valid_pubSK:
[| cert C SKi onlySig (priSK RCA) ∈ parts (knows Spy evs); evs ∈ set_pur |] ==> SKi = pubSK C
lemma Says_certificate_valid:
[| Says A B (sign SK {|lid, xid, cc, cm, cert C EK onlyEnc (priSK RCA)|}) ∈ set evs; evs ∈ set_pur |] ==> EK = pubEK C
lemma Gets_certificate_valid:
[| Gets A (sign SK {|lid, xid, cc, cm, cert C EK onlyEnc (priSK RCA)|}) ∈ set evs; evs ∈ set_pur |] ==> EK = pubEK C
lemma new_keys_not_used:
[| evs ∈ set_pur; Key K ∉ used evs; K ∈ symKeys |] ==> K ∉ keysFor (parts (knows Spy evs))
lemma new_keys_not_analzd:
[| Key K ∉ used evs; K ∈ symKeys; evs ∈ set_pur |] ==> K ∉ keysFor (analz (knows Spy evs))
lemma Crypt_parts_imp_used:
[| Crypt K X ∈ parts (knows Spy evs); K ∈ symKeys; evs ∈ set_pur |] ==> Key K ∈ used evs
lemma Crypt_analz_imp_used:
[| Crypt K X ∈ analz (knows Spy evs); K ∈ symKeys; evs ∈ set_pur |] ==> Key K ∈ used evs
lemma gen_new_keys_not_used:
[| Key K ∉ used evs; K ∈ symKeys; evs ∈ set_pur |] ==> 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_pur |] ==> K ∉ keysFor (analz (Key ` KK ∪ knows Spy evs))
lemma analz_Key_image_insert_eq:
[| Key K ∉ used evs; K ∈ symKeys; evs ∈ set_pur |] ==> analz (Key ` insert K KK ∪ knows Spy evs) = insert (Key K) (analz (Key ` KK ∪ knows Spy evs))
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_pur ==> ∀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 Nonce_analz_image_Key_lemma:
P --> Nonce N ∈ analz (Key ` KK ∪ H) --> Nonce N ∈ analz H ==> P --> (Nonce N ∈ analz (Key ` KK ∪ H)) = (Nonce N ∈ analz H)
lemma Nonce_compromise:
[| evs ∈ set_pur; ∀K∈KK. K ∉ range (%C. priEK C) |] ==> (Nonce N ∈ analz (Key ` KK ∪ knows Spy evs)) = (Nonce N ∈ analz (knows Spy evs))
lemma PANSecret_notin_spies:
[| Nonce (PANSecret k) ∈ analz (knows Spy evs); evs ∈ set_pur |] ==> ∃V W X Y KC2 M. ∃P∈bad. Says (Cardholder k) M {|{|W, EXcrypt KC2 (pubEK P) X {|Y, Nonce (PANSecret k)|}|}, V|} ∈ set evs
lemma CardSecret_notin_spies:
evs ∈ set_pur ==> Nonce (CardSecret i) ∉ parts (knows Spy evs)
lemma analz_image_pan_lemma:
Pan P ∈ analz (Key ` nE ∪ H) --> Pan P ∈ analz H ==> (Pan P ∈ analz (Key ` nE ∪ H)) = (Pan P ∈ analz H)
lemma analz_image_pan:
[| evs ∈ set_pur; ∀K∈KK. K ∉ range (%C. priEK C) |] ==> (Pan P ∈ analz (Key ` KK ∪ knows Spy evs)) = (Pan P ∈ analz (knows Spy evs))
lemma analz_insert_pan:
[| evs ∈ set_pur; K ∉ range (%C. priEK C) |] ==> (Pan P ∈ analz (insert (Key K) (knows Spy evs))) = (Pan P ∈ analz (knows Spy evs))
theorem pan_confidentiality_unsigned:
[| Pan (pan C) ∈ analz (knows Spy evs); C = Cardholder k; CardSecret k = 0; evs ∈ set_pur |] ==> ∃P M KC1 K X Y. Says C M {|EXHcrypt KC1 (pubEK P) X (Pan (pan C)), Y|} ∈ set evs ∧ P ∈ bad
theorem pan_confidentiality_signed:
[| Pan (pan C) ∈ analz (knows Spy evs); C = Cardholder k; CardSecret k ≠ 0; evs ∈ set_pur |] ==> ∃P M KC2 PIDualSign_1 PIDualSign_2 other OIDualSign. Says C M {|{|PIDualSign_1, EXcrypt KC2 (pubEK P) PIDualSign_2 {|Pan (pan C), other|}|}, OIDualSign|} ∈ set evs ∧ P ∈ bad
lemma M_Notes_PG:
[| Notes M {|Number LID_M, Agent P, Agent M, Agent C, etc|} ∈ set evs; evs ∈ set_pur |] ==> ∃j. P = PG j
lemma goodM_gives_correct_PG:
[| MsgPInitRes = {|Number LID_M, xid, cc, cm, cert P EKj onlyEnc (priSK RCA)|}; Crypt (priSK M) (Hash MsgPInitRes) ∈ parts (knows Spy evs); evs ∈ set_pur; M ∉ bad |] ==> ∃j trans. P = PG j ∧ Notes M {|Number LID_M, Agent P, trans|} ∈ set evs
lemma C_gets_correct_PG:
[| Gets A (sign (priSK M) {|Number LID_M, xid, cc, cm, cert P EKj onlyEnc (priSK RCA)|}) ∈ set evs; evs ∈ set_pur; M ∉ bad |] ==> ∃j trans. P = PG j ∧ Notes M {|Number LID_M, Agent P, trans|} ∈ set evs ∧ EKj = pubEK P
lemma C_verifies_PInitRes:
[| MsgPInitRes = {|Number LID_M, Number XID, Nonce Chall_C, Nonce Chall_M, cert P EKj onlyEnc (priSK RCA)|}; Crypt (priSK M) (Hash MsgPInitRes) ∈ parts (knows Spy evs); evs ∈ set_pur; M ∉ bad |] ==> ∃j trans. Notes M {|Number LID_M, Agent P, trans|} ∈ set evs ∧ P = PG j ∧ EKj = pubEK P
lemma Says_C_PInitRes:
[| Says A C (sign (priSK M) {|Number LID_M, Number XID, Nonce Chall_C, Nonce Chall_M, cert P EKj onlyEnc (priSK RCA)|}) ∈ set evs; M ∉ bad; evs ∈ set_pur |] ==> ∃j trans. Notes M {|Number LID_M, Agent P, trans|} ∈ set evs ∧ P = PG j ∧ EKj = pubEK (PG j)
lemma P_verifies_AuthReq:
[| AuthReqData = {|Number LID_M, Number XID, HOIData, HOD|}; Crypt (priSK M) (Hash {|AuthReqData, Hash P_I|}) ∈ parts (knows Spy evs); evs ∈ set_pur; M ∉ bad |] ==> ∃j trans KM OIData HPIData. Notes M {|Number LID_M, Agent (PG j), trans|} ∈ set evs ∧ Gets M {|P_I, OIData, HPIData|} ∈ set evs ∧ Says M (PG j) (EncB (priSK M) KM (pubEK (PG j)) AuthReqData P_I) ∈ set evs
theorem M_verifies_AuthRes:
[| MsgAuthRes = {|{|Number LID_M, Number XID, Number PurchAmt|}, Hash authCode|}; Crypt (priSK (PG j)) (Hash MsgAuthRes) ∈ parts (knows Spy evs); PG j ∉ bad; evs ∈ set_pur |] ==> ∃M KM KP HOIData HOD P_I. Gets (PG j) (EncB (priSK M) KM (pubEK (PG j)) {|Number LID_M, Number XID, HOIData, HOD|} P_I) ∈ set evs ∧ Says (PG j) M (EncB (priSK (PG j)) KP (pubEK M) {|Number LID_M, Number XID, Number PurchAmt|} authCode) ∈ set evs
lemma C_determines_EKj:
[| Says C M {|EXHcrypt KC1.0 EKj {|PIHead, Hash OIData|} (Pan (pan C)), OIData, Hash {|PIHead, Pan (pan C)|}|} ∈ set evs; PIHead = {|Number LID_M, Trans_details|}; evs ∈ set_pur; C = Cardholder k; M ∉ bad |] ==> ∃trans j. Notes M {|Number LID_M, Agent (PG j), trans|} ∈ set evs ∧ EKj = pubEK (PG j)
lemma unique_LID_M:
[| Notes (Merchant i) {|Number LID_M, Agent P, Trans|} ∈ set evs; Notes C {|Number LID_M, Agent M, Agent C, Number OD, Number PA|} ∈ set evs; evs ∈ set_pur |] ==> M = Merchant i ∧ Trans = {|Agent M, Agent C, Number OD, Number PA|}
lemma unique_LID_M2:
[| Notes M {|Number LID_M, Trans|} ∈ set evs; Notes M {|Number LID_M, Trans'|} ∈ set evs; evs ∈ set_pur |] ==> Trans' = Trans
lemma signed_imp_used:
[| Crypt (priSK M) (Hash X) ∈ parts (knows Spy evs); M ∉ bad; evs ∈ set_pur |] ==> parts {X} ⊆ used evs
lemma signed_Hash_imp_used:
[| Crypt (priSK C) (Hash {|H, Hash X|}) ∈ parts (knows Spy evs); C ∉ bad; evs ∈ set_pur |] ==> parts {X} ⊆ used evs
lemma PRes_imp_LID_used:
[| Crypt (priSK M) (Hash {|N, X|}) ∈ parts (knows Spy evs); M ∉ bad; evs ∈ set_pur |] ==> N ∈ used evs
lemma C_verifies_PRes_lemma:
[| Crypt (priSK M) (Hash MsgPRes) ∈ parts (knows Spy evs); Notes C {|Number LID_M, Trans|} ∈ set evs; Trans = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|}; MsgPRes = {|Number LID_M, Number XID, Nonce Chall_C, Hash (Number PurchAmt)|}; evs ∈ set_pur; M ∉ bad |] ==> ∃j KP. Notes M {|Number LID_M, Agent (PG j), Trans|} ∈ set evs ∧ Gets M (EncB (priSK (PG j)) KP (pubEK M) {|Number LID_M, Number XID, Number PurchAmt|} authCode) ∈ set evs ∧ Says M C (sign (priSK M) MsgPRes) ∈ set evs
theorem C_verifies_PRes:
[| MsgPRes = {|Number LID_M, Number XID, Nonce Chall_C, Hash (Number PurchAmt)|}; Gets C (sign (priSK M) MsgPRes) ∈ set evs; Notes C {|Number LID_M, Agent M, Agent C, Number OrderDesc, Number PurchAmt|} ∈ set evs; evs ∈ set_pur; M ∉ bad |] ==> ∃P KP trans. Notes M {|Number LID_M, Agent P, trans|} ∈ set evs ∧ Gets M (EncB (priSK P) KP (pubEK M) {|Number LID_M, Number XID, Number PurchAmt|} authCode) ∈ set evs ∧ Says M C (sign (priSK M) MsgPRes) ∈ set evs
lemma Crypt_imp_Says_Cardholder:
[| Crypt K {|{|{|Number LID_M, others|}, Hash OIData|}, Hash PANData|} ∈ parts (knows Spy evs); PANData = {|Pan (pan (Cardholder k)), Nonce (PANSecret k)|}; Key K ∉ analz (knows Spy evs); evs ∈ set_pur |] ==> ∃M shash EK HPIData. Says (Cardholder k) M {|{|shash, Crypt K {|{|{|Number LID_M, others|}, Hash OIData|}, Hash PANData|}, Crypt EK {|Key K, PANData|}|}, OIData, HPIData|} ∈ set evs
lemma Says_PReqS_imp_trans_details_C:
[| MsgPReqS = {|{|shash, Crypt K {|{|{|Number LID_M, PIrest|}, Hash OIData|}, hashpd|}, cryptek|}, data|}; Says (Cardholder k) M MsgPReqS ∈ set evs; evs ∈ set_pur |] ==> ∃trans. Notes (Cardholder k) {|Number LID_M, Agent M, Agent (Cardholder k), trans|} ∈ set evs
lemma Notes_Cardholder_self_False:
[| Notes (Cardholder k) {|Number n, Agent P, Agent (Cardholder k), Agent C, etc|} ∈ set evs; evs ∈ set_pur |] ==> False
theorem M_verifies_Signed_PReq:
[| MsgDualSign = {|HPIData, Hash OIData|}; OIData = {|Number LID_M, etc|}; Crypt (priSK C) (Hash MsgDualSign) ∈ parts (knows Spy evs); Notes M {|Number LID_M, Agent P, extras|} ∈ set evs; M = Merchant i; C = Cardholder k; C ∉ bad; evs ∈ set_pur |] ==> ∃PIData PICrypt. HPIData = Hash PIData ∧ Says C M {|{|sign (priSK C) MsgDualSign, PICrypt|}, OIData, Hash PIData|} ∈ set evs
theorem P_verifies_Signed_PReq:
[| MsgDualSign = {|Hash PIData, HOIData|}; PIData = {|PIHead, PANData|}; PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M, TransStain|}; Crypt (priSK C) (Hash MsgDualSign) ∈ parts (knows Spy evs); evs ∈ set_pur; C ∉ bad; M ∉ bad |] ==> ∃OIData OrderDesc K j trans. HOD = Hash {|Number OrderDesc, Number PurchAmt|} ∧ HOIData = Hash OIData ∧ Notes M {|Number LID_M, Agent (PG j), trans|} ∈ set evs ∧ Says C M {|{|sign (priSK C) MsgDualSign, EXcrypt K (pubEK (PG j)) {|PIHead, Hash OIData|} PANData|}, OIData, Hash PIData|} ∈ set evs
lemma C_determines_EKj_signed:
[| Says C M {|{|sign (priSK C) text, EXcrypt K EKj {|PIHead, X|} Y|}, Z|} ∈ set evs; PIHead = {|Number LID_M, Number XID, W|}; C = Cardholder k; evs ∈ set_pur; M ∉ bad |] ==> ∃trans j. Notes M {|Number LID_M, Agent (PG j), trans|} ∈ set evs ∧ EKj = pubEK (PG j)
lemma M_Says_AuthReq:
[| AuthReqData = {|Number LID_M, Number XID, HOIData, HOD|}; sign (priSK M) {|AuthReqData, Hash P_I|} ∈ parts (knows Spy evs); evs ∈ set_pur; M ∉ bad |] ==> ∃j trans KM. Notes M {|Number LID_M, Agent (PG j), trans|} ∈ set evs ∧ Says M (PG j) (EncB (priSK M) KM (pubEK (PG j)) AuthReqData P_I) ∈ set evs
lemma Signed_PReq_imp_Says_Cardholder:
[| MsgDualSign = {|Hash PIData, Hash OIData|}; OIData = {|Number LID_M, Number XID, Nonce Chall_C, HOD, etc|}; PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M, TransStain|}; PIData = {|PIHead, PANData|}; Crypt (priSK C) (Hash MsgDualSign) ∈ parts (knows Spy evs); M = Merchant i; C = Cardholder k; C ∉ bad; evs ∈ set_pur |] ==> ∃KC EKj. Says C M {|{|sign (priSK C) MsgDualSign, EXcrypt KC EKj {|PIHead, Hash OIData|} PANData|}, OIData, Hash PIData|} ∈ set evs
theorem P_sees_CM_agreement:
[| AuthReqData = {|Number LID_M, Number XID, HOIData, HOD|}; KC ∈ symKeys; Gets (PG j) (EncB (priSK M) KM (pubEK (PG j)) AuthReqData P_I) ∈ set evs; C = Cardholder k; PI_sign = sign (priSK C) {|Hash PIData, HOIData|}; P_I = {|PI_sign, EXcrypt KC (pubEK (PG j)) {|PIHead, HOIData|} PANData|}; PANData = {|Pan (pan C), Nonce (PANSecret k)|}; PIData = {|PIHead, PANData|}; PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M, TransStain|}; evs ∈ set_pur; C ∉ bad; M ∉ bad |] ==> ∃OIData OrderDesc KM' trans j' KC' KC'' P_I' P_I''. HOD = Hash {|Number OrderDesc, Number PurchAmt|} ∧ HOIData = Hash OIData ∧ Notes M {|Number LID_M, Agent (PG j'), trans|} ∈ set evs ∧ Says C M {|P_I', OIData, Hash PIData|} ∈ set evs ∧ Says M (PG j') (EncB (priSK M) KM' (pubEK (PG j')) AuthReqData P_I'') ∈ set evs ∧ P_I' = {|PI_sign, EXcrypt KC' (pubEK (PG j')) {|PIHead, Hash OIData|} PANData|} ∧ P_I'' = {|PI_sign, EXcrypt KC'' (pubEK (PG j)) {|PIHead, Hash OIData|} PANData|}