PROTOCOL:
SET Purchase Request, and Payment Authorization

VARIANT:
Original

PURPOSE:

The Secure Electronic Transactions (SET) Protocol Suite is designed to allow for a secure e-commerce. The key feature is to hide the customer's credit card details from the merchant, and the customer's purchase details from the bank. Rather, by the construction of the protocol, both merchant and bank see only what they need to see in order to complete the transaction. Following [BMP:SET:Purchase:TR] we focus here on the main part of the protocol, purchase request and payment authorization, leaving out the initial registration protocols and assuming already registered participants. Note that we do allow dishonest participants.  

REFERENCE:

[BMP:SET:Purchase:TR], [SET]  

MODELER:

Sebastian Mödersheim, ETH Zürich  

ALICE_BOB:

The protocol involves three parties: Cardholder C, Merchant M, and Payment Gateway P. The cryptographic constructions of this protocol are quite complex and for readability we thus use the following macros: Further, for the communicated data, we use the following abbreviations (in accordance with the business specification of SET and the model of [BMP:SET:Purchase:TR]): Purchase Request Protocol:
 % Purchase Initiate Request
 1. C->M: P_Init_Req
 % Purchase Initiate Response
 2. M->C: Sign_M(P_Init_Resp).SignCert(M).EncCert(P)
 % Purchase Request
 3. C->M: OI.DualSig_C(OI,PI).
           Encrypt_P(AI,K1,DualSig_C(OI,PI).PI).
           SignCert(C)
 % Purchase Response
 4. M->C: Sign_M(Purch_Res).SignCert(M)
 
Payment Authorization Protocol:
 % Payment Authorization Request
 1. M->P: Encrypt_P(_,K2,Sign_M(AuthReq)).
           Encrypt_P(AI,K1,DualSig_C(OI,PI).PI).
          SignCert(C).SignCert(M).EncCert(M)
 % Payment Authorization Response
 2. P->M: Encrypt_M(K3,Sign_P(Auth_Res)).
          Encrypt_P(AI,K4,Sign_P(Cap_Token)).
          SignCert(P)
 
Following [BMP:SET:Purchase:TR], we simplify this into one protocol, omitting certificates (we assume that all agents initially have each other's public-keys) and remove the sub-message that in the payment authorization response step which the payment gateway encrypts to itself:
 % Purchase Initiate Request
 1. C->M: P_Init_Req
 % Purchase Initiate Response
 2. M->C: Sign_M(P_Init_Resp)
 % Purchase Request
 3. C->M: OI.DualSig_C(OI,PI).
           Encrypt_P(AI,K1,DualSig_C(OI,PI).PI)
 % Payment Authorization Request
 4. M->P: Encrypt_P(_,K2,Sign_M(AuthReq)).
           Encrypt_P(AI,K1,DualSig_C(OI,PI).PI)
 % Payment Authorization Response
 5. P->M: Encrypt_M(K3,SignK_P(Auth_Res))
 % Purchase Response
 6. M->C: Sign_M(Purch_Res)
 
We consider the following goals: the parties shall authenticate each other on (the hash of) the order and payment information. Moreover, the order information shall remain secret between cardholder and merchant, and the payment information, in particular the credit card details, shall remain secret between cardholder and payment gateway.  

LIMITATIONS:

We have abstracted from the following details:  

PROBLEMS:
4
 

ATTACKS:

The first attack is that a dishonest payment gateway p can forward a payment authorization request to any other payment gateway p'. In a nutshell, the attack trace has the form
  ... 
  m     -> p:  Encrypt_p (_,K2,Sign_M(AuthReq)).
               Encrypt_p (AI,K1,DualSig_C(OI,PI).PI)
  p(m)  -> p': Encrypt_p'(_,K2,Sign_M(AuthReq)).
               Encrypt_p'(AI,K1,DualSig_C(OI,PI).PI)
  ...
  
This is due to the fact that the part of the message signed by the cardholder (as well as the one signed by the merchant) does not contain the name of the desired payment gateway. Rather, the payment gateway is only determined by the public-key encryption for the desired gateway. Though only a dishonest payment gateway can ``forward'' the payment requests, this may lead to the situation that two payment gateways charge the account of the cardholder and both posses messages that seem to prove that the cardholder authorized the transaction. The vulnerability is limited by the fact that the payment gateway actually chosen by the cardholder must be dishonest in the first place. In our opinion, one should definitely include the name of the payment gateway also in the dual signature to prevent this situation.

We also found a second, albeit quite artificial, attack. For the simplicity of the presentation, we do not display here the complete attack trace. Let c be an honest cardholder, m and m' be an honest and a dishonest merchant, and p and p' be an honest and a dishonest payment gateway. (All dishonest parties cooperate and are thus merged into one intruder.) Consider a session between c, m and p', and a session between c, m', and p, which all run according to the protocol. Let lid, xid, orderdesc, purchamt be the data of the session between c, m', and p. Let finally ai be the account information of c. Then the intruder (i.e. m' and p' together) can construct the message

    lid.xid.h(orderdesc.purchamt).purchamt.m'.h(xid.ai_c)
 
which is the payment information that only the honest participants c and p are supposed to see. It is thus possible that the secrecy of the payment information between an honest cardholder and an honest payment gateway is violated, if a dishonest merchant and a dishonest payment gateway cooperate. However, the relevance of this attack is questionable. It is standard to check protocols under the assumption of dishonest players, and it is clear that in such sessions secrecy guarantees, for instance, are void (as the intruder knows the secrets). The question is rather whether such a session can also compromise the security goals of other sessions (as it is the case for instance in the well-known attack against the Needham-Schroeder Public Key Protocol). For the SET protocol, however, it is clear that, once an honest cardholder runs a session with a dishonest payment gateway, the account-information of the cardholder is compromised in all sessions; it is thus not surprizing that the payment information from a session with an honest payment gateway can also be reconstructed in such a case. Note that this attack is not possible without a dishonest merchant, i.e. even though a dishonest payment gateway knows the account details, it cannot obtain order information of sessions with an honest merchant.

 

NOTES:

 


HLPSL:

role cardholder(C,M,P: agent,
                AI : text,
                PurchAmt : nat,
                OrderDesc : text,
                EncK_C, SignK_C, 
                EncK_M, SignK_M, 
                EncK_P, SignK_P : public_key
               ) played_by C def=

 local S : nat,
       LID_M, Chall_C : text,
       XID, Chall_M : text,
       OI,PI,DualSig : message,
       K1 : symmetric_key,
       SND, RCV: channel (dy)

 init S := 0

 transition

 % =|> Purchase Initiate Request
 1. S = 0 /\ 
    RCV(start) 
    =|>
    S' := 1 /\
    LID_M' := new() /\
    Chall_C' := new() /\
    SND(LID_M'.Chall_C')

 % Purchase Initiate Response =|> Purchase Request
 2. S = 1 /\ 
    RCV(LID_M.Chall_C.XID'.Chall_M'.
        {h(LID_M.Chall_C.XID'.Chall_M')}_inv(SignK_M))
    =|> 
    S' := 2 /\
    OI' := XID'.Chall_C.h(OrderDesc.PurchAmt).Chall_M' /\
    PI' := LID_M.XID'.h(OrderDesc.PurchAmt).PurchAmt.M.h(XID'.AI) /\
    DualSig' := h(OI').h(PI').{h(h(OI').h(PI'))}_inv(SignK_C) /\
    K1' := new() /\
    SND(OI'.DualSig'.
        {DualSig'.PI'}_K1'.{AI.K1'}_EncK_P) /\
    witness(C,M,deal,OI'.h(PI')) /\
    witness(C,P,deal,OI'.PI') /\
    secret(OrderDesc,order,{C,M}) /\
    secret(PurchAmt,order,{C,M,P}) /\
    secret(PI',payment,{C,P})

 % Purchase Response =|>
 3. S = 2 /\
    RCV(LID_M.XID.Chall_C.h(PurchAmt).
        {h(LID_M.XID.Chall_C.h(PurchAmt))}_inv(SignK_M))
    =|>
    S' := 3 /\
    request(C,M,deal,OI.h(PI))
    % /\ request(C,P,deal,OI.PI) %% cannot be done; see notes, item 2

end role


role merchant (C,M,P: agent, PurchAmt : nat, OrderDesc : text, EncK_C, SignK_C, EncK_M, SignK_M, EncK_P, SignK_P : public_key ) played_by M def= local S : nat, LID_M, Chall_C : text , XID, Chall_M : text, OI,HPI,DualSig,Paymentpart,AuthReq : message, K2 : symmetric_key, K3 : symmetric_key, SND, RCV: channel (dy) init S := 0 transition % Purchase Initiate Request =|> Purchase Initiate Response 1. S = 0 /\ RCV(LID_M'.Chall_C') =|> S' := 1 /\ XID' := new() /\ Chall_M' := new() /\ SND(LID_M'.Chall_C'.XID'.Chall_M'. {h(LID_M'.Chall_C'.XID'.Chall_M')}_inv(SignK_M)) % Purchase Request =|> Payment Authorization Request 2. S = 1 /\ RCV(XID.Chall_C.h(OrderDesc.PurchAmt).Chall_M. h(OI').HPI'.{h(h(OI').HPI')}_inv(SignK_C). Paymentpart') /\ OI' = XID.Chall_C.h(OrderDesc.PurchAmt).Chall_M =|> S' := 2 /\ DualSig' := h(OI').HPI'.{h(h(OI').HPI')}_inv(SignK_C) /\ K2' := new() /\ AuthReq' := LID_M.XID.h(OI').h(OrderDesc.PurchAmt). DualSig' /\ SND({AuthReq'.{h(AuthReq')}_inv(SignK_M)}_K2'.{K2'}_EncK_P. Paymentpart') /\ witness(M,C,deal,OI'.HPI') /\ witness(M,P,deal,OI'.HPI') % Payment Authorization Response =|> Purchase Response 3. S = 2 /\ RCV({LID_M.XID.PurchAmt. {h(LID_M.XID.PurchAmt)}_inv(SignK_P)}_K3'.{K3'}_EncK_M) =|> S' := 3 /\ SND(LID_M.XID.Chall_C.h(PurchAmt). {h(LID_M.XID.Chall_C.h(PurchAmt))}_inv(SignK_M)) /\ request(M,C,deal,OI.HPI) /\ request(M,P,deal,OI.HPI) end role
role paymentgateway(C,M,P: agent, AI : text, EncK_C, SignK_C, EncK_M, SignK_M, EncK_P, SignK_P : public_key ) played_by P def= local S : nat, XID, Chall_M, LID_M, Chall_C : text , AuthReq,Paymentpart,OI,PI,DualSig : message, K1,K2 : symmetric_key, K3 : symmetric_key, PurchAmt : nat, OrderDesc : text, SND, RCV: channel (dy) init S := 0 transition % Payment Authorization Request =|> Payment Authorization Response 1. S = 0 /\ RCV({AuthReq'.{h(AuthReq')}_inv(SignK_M)}_K2'.{K2'}_EncK_P. {DualSig'.PI'}_K1'.{AI.K1'}_EncK_P ) /\ AuthReq' = LID_M'.XID'.h(OI').h(OrderDesc'.PurchAmt').DualSig' /\ OI' = XID'.Chall_C'.h(OrderDesc'.PurchAmt').Chall_M' /\ DualSig' = h(OI').h(PI').{h(h(OI').h(PI'))}_inv(SignK_C) /\ PI' = LID_M'.XID'.h(OrderDesc'.PurchAmt').PurchAmt'.M.h(XID'.AI) =|> S' := 1 /\ K3' := new() /\ SND({LID_M'.XID'.PurchAmt'. {h(LID_M'.XID'.PurchAmt')}_inv(SignK_P)}_K3'.{K3'}_EncK_M) /\ wrequest(P,C,deal,OI'.PI') /\ wrequest(P,M,deal,OI'.h(PI')) /\ witness(P,C,deal,OI'.PI') /\ witness(P,M,deal,OI'.h(PI')) end role
role session(C,M,P: agent, AI : text, PurchAmt : nat, OrderDesc : text, EncK_C, SignK_C, EncK_M, SignK_M, EncK_P, SignK_P : public_key ) def= % local SI, RI, SR, RR: channel(dy) composition cardholder(C,M,P,AI,PurchAmt,OrderDesc, EncK_C,SignK_C,EncK_M,SignK_M,EncK_P,SignK_P) /\ merchant (C,M,P, PurchAmt,OrderDesc, EncK_C,SignK_C,EncK_M,SignK_M,EncK_P,SignK_P) /\ paymentgateway(C,M,P,AI, EncK_C,SignK_C,EncK_M,SignK_M,EncK_P,SignK_P) end role
role environment() def= local AList, RList: (message.message) set, S2, R2, S3, R3: channel (dy) const h: hash_func, deal,order,payment : protocol_id, c,m,p: agent, enc_c,sign_c,enc_m,sign_m,enc_p,sign_p,enc_i,sign_i: public_key, ai_c,ai_i,od1,od2,od3,od4,od5: text, pa1,pa2,pa3,pa4,pa5 : nat intruder_knowledge = {c,m,p,enc_c,sign_c,enc_m,sign_m,enc_p,sign_p, enc_i,sign_i,inv(enc_i),inv(sign_i),ai_i,pa3,od3,pa4,od4,h } composition session(c,m,p,ai_c,pa2,od2,enc_c,sign_c,enc_m,sign_m,enc_p,sign_p) /\ % session(i,m,p,ai_i,pa3,od3,enc_i,sign_i,enc_m,sign_m,enc_p,sign_p) /\ session(c,i,p,ai_c,pa4,od4,enc_c,sign_c,enc_i,sign_i,enc_p,sign_p) /\ session(c,m,i,ai_c,pa5,od5,enc_c,sign_c,enc_m,sign_m,enc_i,sign_i) end role
goal % Entity authentication (G1) % Message authentication (G2) % Replay protection (G3) % Accountability (G17) % Proof of Origin (G18) % Proof of Delivery (G19) authentication_on deal weak_authentication_on deal % ID protection (Eavesdr.) (G13) % Conifidentiality (G12) --- Missing in table of D6.1 secrecy_of order secrecy_of payment end goal environment()