VARIANT:

Instantiation with only honest payment gateways

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 assume 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(A)={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) 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:

None

NOTES:

In this variant the payment gateway role is played only
by honest participants to avoid the attacks of found in the case with dishonest payment gateways.

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 the 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}) /\
    secret(AI,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) 

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