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:

Sign_A(Msg)=Msg.{h(Msg)}_inv(SignK(A))
Encrypt_B(Msg1,K,Msg2)={Msg2}_K.{Msg1.K}EncK(B). Note that we explicitly give a symmetric key that is used in the encryption and that is transmitted in a digital envelope together with Msg1 that is most precious.
SignCert(M)={A.SignK(A)}_inv(SignK(CA))
EncCert(A)={A.EncK(A)}_inv(SignK(CA))
DualSig_A(M1,M2) = Sign_A(h(M1).h(M2))

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]):

P_Init_Req=LID_M.Chall_C
The purchase initiate request, which consists of an identifier and a challenge chosen by the cardholder, both modelled as nonces;
P_Init_Resp=LID_M.Chall_C.XID.Chall_M
The response to an initiate request, containing an identifier and a challenge from the merchant, modelled as nonces.
AI
Account Information, the details of the credit card of the cardholder. This is the most precious secret of the protocol.
OI=XID.Chall_C.h(OrderDesc.PurchAmt).Chall_M
Order Information, which contains a hash-value of the order description and the purchase amount. These data are negotiated out-of-band before the protocol and both cardholder and merchant initially share this information.
PI=LID_M.XID.h(OrderDesc.PurchAmt).PurchAmt.M.h(XID.AI)
Payment Information, containing a hash of the account information
AuthReq=LID_M.XID.h(OI).h(OrderDesc.PurchAmt).DualSign_C(PI,OI)
Auth_Res=LID_M.XID.PurchAmt
Purch_Res=LID_M.XID.Chall_C.h(PurchAmt)

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:

The shopping process itself, i.e. selection of goods and computing the price to pay.
The registration of the participants.
The public-key infrastructure and verification of certificates (assuming everybody already has each other's public key).
Omitting a special PAN and PANSecret (assuming AI data is sufficient for payment gateway).

PROBLEMS:

strong authentication on deal
weak authentication on deal
secrecy of order
secrecy of payment

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:

There is nothing in the messages that ensures freshness for the payment gateway. However it is unreasonable to assume a payment gateway would not log the payment requests it has received. So we can assume that it won't accept a second time a message with the same identifiers LID_M and XID, and thus check only for weak authentication from the gateways point-of-view.
The cardholder cannot be sure, upon receiving the final purchase response message from the merchant, that the payment gateway has actually seen the transaction. This is not very surprizing as this message can be sent by the merchant without first contacting the payment gateway (the merchant then looses the guarantee that he will receive the money).

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()