Design of electronic payment system based on authenticated key exchange

Abstract

This paper proposes an electronic payment system based on authenticated key exchange protocol. In this scheme, an effective owner tracing mechanism is introduced to identify a malicious customer. Moreover, every participant can mutually authenticate each other. The security of the scheme is mainly based on the hardness assumption of computational Diffie–Hellman and discrete logarithm problems. Furthermore, the security of our scheme is simulated in the automated validation of Internet security protocols and applications tool and proved that the scheme is secure against replay and man-in-the-middle attacks.

1 Introduction

Electronic commerce has equipped as a suitable alternative for financial transactions over the web. A typical electronic payment (e-payment) system comprises of three parties, namely, a customer, a bank, and a merchant. The bank plays a major role in distributing e-cash among each registered user, and the customer can withdraw e-cash for online merchandise. The amount is credited into merchant’s account after a successful transaction. The life-cycle of e-payment framework incorporates three unique phases: withdrawal phase, payment phase, and deposit phase. The major challenges in an e-payment system are the loss of anonymity, double spending, forgeability, and re-usability. Loss of anonymity lead to breach of privacy due to identity theft. A preventive measure is necessary to identify the user who tries to double spend the already used e-coin. Forgeability signifies that an illegitimate user can counterfeit as a legitimate one, whereas, reusability defines, as an e-coin holds sensitive information of user and bank, therefore, each user must be allotted a unique e-coin for preserving confidentiality.

Chaum has proposed the primitive online e-payment system using the properties of blind signature to prevent double spending [1]. In his scheme, a customer is allowed to choose a random e-coin which is then blinded, and signed by the bank. However, the signer must ensure that the message contains precise information. In 1996, Tygar and Yee have shown that the protocol lacks atomicity during transaction failure [2] also lacks scalability [3] as the number of e-coin spent needs to be recorded further it tracks double spending and therefore, the coins database increases over time. Hence, to overcome the above issue Chaum [4] proposed an offline electronic payment system using cut and choose methodology where the e-coin stays anonymous when spent for the first time but the user’s identity is revealed when attempted to spend for the second time. However, the system is inefficient due to weak check system where a user can pass forged coin detection by claiming data error [5]. As the e-coin is derived from k sets of two-element of numbers, a user can possibly try to forge by producing two different sets of numbers, therefore, matching 2k set from records is inefficient. Brand introduced a restrictive blind signature scheme where a client provides zero-knowledge proof along with his identity in the resulting blind signature [6, 7]. The scheme is inadequate to prevent double spending of e-coin if a malicious user can construct a forged identity and can spend the e-coin multiple times [8]. Fujisaki and Okamoto introduced a partially blind signature to overcome the downsides of carrying public and private keys where bank needs to maintain a huge database of every client [9, 10]. Shi et al. proposed a conditional e-payment system where the digital cash is not bound to client’s identity, therefore it achieves anonymity [11]. However, the scheme is inefficient due to expensive cut-and-choose along with secret sharing mechanism [12]. Popescu et al. and Wang et al. introduced trustee based e-cash systems using bilinear pairing [13, 14]. Popescu’s scheme fails to deliver a legitimate e-coin from withdrawal phase to payment phase [15] and also lacks anonymity [16]. In Wang’s scheme, a malicious user can use a de-registered certificate to withdraw an e-coin from bank [15]. Later, Issac and Zeadally introduced an anonymous secure gateway centric payment model, where a client and merchant communicate with one another with respect to payment gateway [17]. The protocol uses MAC and symmetric key cryptosystem, however, fails to provide fairness¹ and non-repudiation [18]. Lin et al. has proposed a bilinear pairing based e-payment system which is more efficient and practical [19]. However, the scheme suffers from heavy computation overhead and fails to provide security on a transaction as the same symmetric key is used to encrypt the payment information in each transaction [20]. Eslami et al.’s scheme attaches an expiration date to e-cash by applying a challenge-and-response ElGamal signatures to reveal a user’s identity if double spending occurs [21]. The method has a flaw as a customer can easily evade such double-spending tracking by just choosing a meaningless signing key and generating the corresponding verifying key [16]. Also they introduced a certificate issuing authority to manage license. The scheme is found to be incapable of preventing double spending by Li et al. where a merchant can misuse a user’s e-cash easily without being traced by the trustee [22]. Rather, the legitimate user’s identity will be traced since the customer’s identity is embedded in the e-cash and mutual authentication is not assured in payment phase . Chen et al. proposed an online payment system for digital content that adopts the concept of subliminal channel to protect customer’s ownership [23]. However, from literature it is clear that subliminal channel suffer’s from low transmission efficiency also causes high computation and communication cost [24, 25]. Recently, Yang et al. proposed an authenticated encryption scheme where the sender uses his private key along with receiver’s public key to develop symmetric key [26]. To lessen the computational cost, the scheme has eradicated digital signature. Yang claimed to achieve authenticity, privacy and prevention from double spending, but his protocol is found to be vulnerable to impersonation attack [27]. An adversary simply having the knowledge of public parameters which includes full control over the communication channel and access to identities as well as public keys can impersonate the legitimate user by forging into buying phase. An attacker can forward a message imitating as an authentic customer to the bank. The bank may successfully verify the purchase request. Hence, failing to achieve privacy and security.

From the literature it is observed that to fulfil all the requirements of an e-payment system, the existing protocols have introduced high computational overhead. To alleviate these limitations, we have suggested an authenticated key exchange protocol for electronic payment system with following characteristics:

• The model achieves anonymity with traceable owner tracking mechanism.

• The protocol is secure under the hardness of solving discrete logarithm problem (DLP) and computational Diffie–Hellman problem (CDHP). A low cost authenticated channel is designed to achieve mutual authentication between each protocol using XOR and one-way hash function.

• A formal and informal security verification is achieved using AVISPA software and valid assumptions to support the design.

The remainder of the paper is organized as follows. Section 2 introduces techniques applied in our scheme. Section 3 presents an authenticated key exchange protocol for electronic payment based on efficient one-way hash function and exclusive-or (XOR) operation while the security issues are analyzed in Sect. 4. Section 5 provides the simulation of formal security verification using AVISPA to show that our scheme is secure against passive and active attacks. Section 6 offers a comparison of proposed scheme with existing protocols along with performance evaluation. Finally, we conclude in Sect. 7.

2 Preliminaries

This section introduces three cryptographic techniques used in our proposed scheme: DLP [28], computational Diffie–Hellman (CDH) [29], and one-way hash function [30].

2.1 Discrete logarithm problem

Let G be a cyclic group of order q with a generator g for every h which belongs to G, there is a unique $x \in Z_p^{*}$ such that $g^x=h$ mod p, where it is hard to compute x.

2.2 Computational Diffie–Hellman problem

Given $(g, g^a, g^b)$ where a, b are selected randomly from $Z_p^*$. The CDH assumption states that for a generator g and values a and b that are all randomly selected, it is computationally intractable to compute the value $g^{ab}$ mod p.

2.3 One-way hash function

A cryptographic one-way hash function maps a string of arbitrary length to a string of fixed length called the hashed value. Let H(.) is taking an input x and returning a fixed-size string y. The basic requirements for a cryptographic one-way hash function includes:

• Given x, it is comparatively easy to compute H(x).

• Given y, it is unfeasible to deduce x such that $y=H(x)$.

3 Our proposed scheme

In this section, we briefly demonstrate our electronic payment system. The scheme is designed for mobile commerce or wireless wide area network (WWAN) enabled hand-held devices which includes three participants namely, customer, bank, and merchant. An effective owner tracing mechanism is applied in case the customer tries to spend the e-cash twice. The scheme includes five distinct phases: initialization phase, registration phase, withdrawal phase, payment phase, and deposit phase. Authenticity is achieved by ensuring key management, user identification, and message integrity. It is assumed that the transactions happen using secure socket layer (SSL), which is a standard security mechanism for secure communication between server and customer. It ensures secure transmission of sensitive information containing credit card numbers, social security numbers and login information. Table 1 demonstrates the useful notations used in our paper. The architecture of our scheme is illustrated in Fig. 1, with description about every stage.

Fig. 1

Architecture of E-payment system. 1 The customer registers himself by opening an account with the bank; 2 the bank generates a unique token ID to identify each customer’s account during the transaction; 3 the customer withdraws an e-coin from bank before transaction; 4 the customer places a purchase request to the merchant; 5 the merchant sends a withdrawal message to the bank for customer’s account verification; 6 the bank responds to the request and provides a message of a successful transaction; 7 the merchant responds to the customer’s purchase request

3.1 Initialization phase

This phase is carried out by the bank where a large prime p and a primitive root g mod p is chosen. Both p and g are made public.

3.2 Registration phase

Initially, every client (customer or merchant) has to open an account with the bank by registering his personal details. The details include permanent account number (PAN), address, phone number, international mobile station equipment identity (IMEI), etc. In our scheme we have chosen 15 digit unique IMEI number to identify the user. The general purpose of IMEI is to identify a device that uses terrestrial mobile networks. It is used in devices such as 3G/4G tablets, laptops with PCMCIA wireless Internet cards etc. Here, the user initially registers his IMEI number based on the total number of subscriber identity module (SIM) slots on his mobile device which is independent of its transceiver. However, if a user changes his device, he needs to update his IMEI number with the bank. In a case of mismatch on IMEI number, the bank has the right to suspend the transaction at redemption phase. A method called tokenization is introduced by the bank to prevent the storage of customer’s credit/debit card details at merchant’s site [31]. In this paper, a cryptographic function is used to generate a token ID for each account holder. The process of registration can be achieved either online or off-line as demonstrated in Fig. 2. The steps are illustrated as follows:

• Step 1: The participant $P_i$ where $i \in$ {customer or merchant} compute his identity $(ID_i)$, which is a unique string consists of IMEI number and phone number defined as,

  $$ ID_i=H(IMEI) \oplus Phone\_no $$

  (1)

  Then each participant chooses a random secret key ($x_i$) to compute his respective public key ($Pub_i$) as,

  $$ Pub_i=g^{x_i}\ mod \ p $$

  (2)

  and subsequently send a pair of $(ID_i, Pub_i)$ to the bank.

  $$ P_i \rightarrow B: \{ID_i, Pub_i\} $$

• Step 2: Upon receiving $P_i's$ initiation message {$Pub_i$,$ID_i$}, the bank randomly selects its master secret key (msk) followed by a random nonce ($N_b$) to compute its corresponding public key (mpk) as,

  $$ mpk=g^{msk}\ mod \ p $$

  (3)

  then send (mpk, $N_b$) along with banks ID ($ID_b$) to each participant $P_i$.

  $$ B \rightarrow P_i: \{ID_b, N_b, mpk\} $$

• Step 3: After receiving $\{ID_b, N_b, mpk\}$ from the bank, each participant computes following operations as,

  $$W_i=H(IMEI_i)\oplus Acc\_no $$

  (4)
  $$ V_i=H(x_i||ID_i) $$

  (5)
  $$ D_i=H(x_i||ID_i) \oplus H(IMEI_i) $$

  (6)
  $$ K_i=H(IMEI_i||Pub_i||x_i) $$

  (7)

  then send following parameters $\{ID_i,ID_b,D_i,K_i,W_i,N_b\}$ to the bank.

  $$ P_i \rightarrow B: \{ID_i,ID_b,D_i,K_i,W_i,N_b\} $$

• Step 4: The bank uses the concept of tokenization to shroud the customer’s personal account details from merchant as follows,

  $$ TD_i=ID_i \oplus Acc\_no \oplus H(msk) $$

  (8)

• Step 5: Using participant’s public key, the bank computes a shared session key ($SK_i$) and a symmetric encryption key ($Key_i$) as mentioned below,

  $$ SK_i=(Pub_i)^{msk}\ mod \ p $$

  (9)
  $$ Key_i=H(SK_i||D_i||K_i) $$

  (10)

  the bank stores ($ID_i$, $TD_i$, $Pub_i$, $W_i$) in its database, and send a pair of $\{ID_i,TD_i\}$ encrypted with symmetric key ($Key_i$) to each participants.

  $$ B \rightarrow P_i: E_{Key_{i}}\{TD_i,ID_i\} $$

Table 1 Notations

Fig. 2

Overview of user registration

3.3 Withdrawal phase

This phase is run between C and B. Before processing the transaction, customer C requests the bank for withdrawing ecash. The bank responses with a series of authentication requests to verify user’s identity. Finally, the customer stores the response for payment phase. The overview of this phase is depicted in Fig. 3. The steps are illustrated as follows:

• Step 1: The customer C chooses two random numbers (n, u) where n provides randomness to the message digest, u is generated for digital signatures, and a time-stamp ($T_s$) to provide a timing on a signed document. To withstand replay and man-in-the-middle attack following operations are carried out to generate ($v_c$, e, A, $Rv_c$, $Rw_c$, $\sigma _c$, $K_1$, $K_{cb}$, Z, $\alpha$) where the values are defined as,

  $$ v_c=H(W_c||x_c||V_c) $$

  (11)
  $$ e=H(v_c||n) $$

  (12)
  $$ A=g^u \ mod \ p $$

  (13)
  $$ Rw_c=H(n||H(Amt)||SK_c) $$

  (14)
  $$ Rv_c=A \oplus Rw_c $$

  (15)
  $$ K_1=g^{e*x_c}\ mod \ p $$

  (16)
  $$ K_{cb}=H(K_1||mpk||T_s||ID_c||ID_b) $$

  (17)
  $$ sigma _c=(e*x_c-u*Rw_c)\ mod \ (p-1) $$

  (18)
  $$ Z=H(K_c||\sigma _c)\oplus H(u) $$

  (19)
  $$ \alpha =H(K_1||Rw_c||K_{cb})$$

  (20)

  Here, $K_c$, $W_c$, and $V_c$ are referred to $K_i$, $W_i$, and $V_i$ computed by each participant during registration phase. A signature ($\sigma _c$) is generated then encrypted with symmetric key $Key_{cb}$ referred as $Key_i$. Then the customer sends H(Amt) to be withdrawn along with parameter $A,\sigma _c, Rv_c,\alpha$ and time-stamp $(T_s).$

  $$ C \rightarrow B: \{D_c, E_{Key_{cb}}\{ H(Amt),A,\sigma _c,T_s, Rv_c,\alpha \},E_{K_{cb}} \{Amt,TD_c,Z\}\} $$

• Step 2: Upon receiving the message from customer, the bank performs an authentication check in order to converts Amt into e-coins (CNO). Initially, the bank applies the pre-shared symmetric key $Key_{cb}$ to obtain $H(Amt),A,\sigma _c,$ $T_s, Rv_c,\alpha ,$ $E_{K_{cb}} \{Amt,TD_c,Z\}.$Then computes,

  $$ Rw_c'=Rv_c \oplus A $$

  (21)

  and subsequently, the signature is verified by computing $K_1'$ from ($\sigma _c$), A, and $Rw_c'$ which is a string converted into BigInteger as,

  $$ K_1'=(g^{\sigma _c})*(A^{Rw_c'})\ mod \ p $$

  (22)

  Thereafter, the symmetric key $(K_{cb}')$ is deduced using Eq. (22) as follows,

  $$ K_{cb}'=H(K_1'||mpk||T_s||ID_c||ID_b) $$

  (23)

  The time-stamp ($T_s$) is verified to check whether ($T'-T_s$) is less than ($\triangle T$), where ($T'$) is the current system time, and ($\triangle T$) is the amount of time tolerated for a transmission delay. If fails, the bank rejects the request else verifies by checking whether α ≟ $H(K_1'||Rw_c'||K_{cb}')$.

• Step 3: Upon successful verification the bank selects a random number (r) and assigns the e-coin (CNO) to the requested amount. Then it computes (L, $M_1$, $M_2$) and performs a hash function on the respective e-coin H(CNO). After which, it generates $M_3$ along with signature ($\sigma _b$) as follows,

  $$ L=H(r) $$

  (24)
  $$ M_1=Z\oplus L $$

  (25)
  $$ M_2=g^{r*H(CNO)}\ mod \ p $$

  (26)
  $$ \sigma _b=(r*H(CNO)-M_1*msk)\ mod \ (p-1) $$

  (27)
  $$ M_3=H(K_c||\sigma _c) \oplus M_2 $$

  (28)

  the bank stores $L,M_2,CNO$ then sends the coin number along with computed parameters to the customer.

  $$ B \rightarrow C: E_{K_{bc}}\{ID_b,CNO,M_1,M_3,\sigma _b,H(CNO),TD_c\} $$

• Step 4: Once the customer receives a message he undergoes a series of verification process as follows,

  $$ L'=Z\oplus M_1 $$

  (29)
  $$ M_2'= (g^{\sigma _b})*(mpk^{M_1}) $$

  (30)

  The customer checks whether the following equation matches with H(u) as,

  $$ H(u){\mathop {=}\limits ^{?}}M_3 \oplus Z \oplus M_2' $$

  (31)

  Once the customer is confirmed, he knows that the coin is valid. Therefore, he stores $\{CNO,H(CNO),L',M_2'\}$ in his database, else rejects it.

Fig. 3

Overview of withdrawal phase

3.4 Payment phase

This phase is initiated when a customer wishes to purchase a digital content after visiting the merchant’s website where, he spends his ecash $\{H(CNO),L',M_2'\}$ during checkout session by sending a purchase request with invoice number to the merchant. Once, the merchant receives the message, he re-confirms the request from the customer, then forwards the payment details to the bank. The payment phase is discussed in Fig. 4. The steps are explained as follows:

• Step 1: Customer initializes a purchase request by sending invoice number ($Inv\_no$) and product details ($Prod\_det$) with a random nonce ($N_c$). Also, computes a one-time key $H(D_c||Pub_c||$ $N_c)$ to encrypt the message consisting of $(D_c,Pub_c,Inv\_no,Prod\_det)$ that are sent to the merchant.

  $$ C \rightarrow M: D_c,Pub_c,N_c,\{Pub_c,D_c,Inv\_no,Prod\_det\}_{H(D_c,Pub_c,N_c)} $$

• Step 2: Similarly, the merchant responses to the purchase request by sending his identity, public key, a request of confirmation, a random nonce ($N_m$) and an encrypted message with one-time key $H(D_m||Pub_m||N_m)$ to the customer.

  $$ M \rightarrow C: ID_m,Pub_m,N_m,\{Pub_m,ID_m,Req\_conf,N_c\}_{H(ID_m,Pub_m,N_m)} $$

• Step 3: Once the customer has received a response he randomly selects a secret key (k), a new time-stamp ($T_{new}$) and compute (Y, d, $K_2$, $R_1$) as follows,

  $$ Y=g^k\ mod \ p $$

  (32)
  $$ d=H(v_c||k) $$

  (33)
  $$ K_2=g^{d*x_c}\ mod \ p $$

  (34)
  $$ R_1=H(D_c||Inv\_no||H(CNO)) $$

  (35)

  and subsequently computes the signature $(\delta _c)$ and ecash as,

  $$ \delta _c=(d*x_c-R_1*T_{new}*k)\ mod \ (p-1) $$

  (36)
  $$ ecash=H(H(CNO)||L'||M_2'||N_m||N_c||T_{new}) $$

  (37)

  The customer then computes a shared session key ($SK_{cm}$), a symmetric en/decryption key ($K_{cm}$) followed by $(\beta )$ to authenticate and pay the merchant with ecash as,

  $$ SK_{cm}=(Pub_m)^{x_c}\ mod \ p $$

  (38)
  $$ K_{cm}=H(SK_{cm}||ID_m||ID_c||N_c||N_m) $$

  (39)
  $$ \beta =H(K_2||K_{cm}||R_1) $$

  (40)

  $C \rightarrow M:$ $ID_c,ID_m,T_{new},E_{K_{cm}}\{CNO,\delta _c,R_1,Y,E_{K_2}[ ecash,H(CNO),\beta , E_{K_{cb}} (ecash,TD_c,N_c, T_{new})]\}$

• Step 4: Upon receiving the message from customer, the merchant first checks the freshness of the time-stamp received as $T'-T_{new}'<? \triangle T$. If it is not fresh, the merchant rejects the request and send an error message $\bot$. If satisfied, then computes $SK_{cm}',K_{cm}'$ as shown below,

  $$ SK_{cm}'=(Pub_c)^{x_m}\ mod \ p $$

  (41)
  $$ K_{cm}'=H(SK_{cm}'||ID_m||D_c||N_c||N_m) $$

  (42)

  Using $K_{cm}'$ the merchant applies a decryption algorithm to obtain the message $\{CNO,\delta _c,$ $T_{new},R_1,$ $Y,E_{K_2}[ ecash,H(CNO),\beta , E_{K_{cb}} (ecash,TD_c,N_c, T_{new})]\}$. Then uses the signature $\delta _c$ to compute $K_2'$ as,

  $$ K_2'=(g^{\delta _c})*(Y^{R_1*T_{new}}) mod (p-1) $$

  (43)

  and a symmetric decryption key algorithm is applied on the message $\{ecash,H(CNO),$ $E_{K_{cb}} (ecash,$ $TD_c,N_c, T_{new})\}$. The merchant here, verifies by checking whether α ≟ $H(K_2'||K_{cm}'||R_1)$. If the authentication is successful then M forwards the payment information $\{ecash,H(CNO),E_{K_{cb}}$ $(ecash,TD_c,N_c, T_{new})\}$ to the bank for redemption. Otherwise, aborts the transaction.

Fig. 4

Overview of payment phase

3.5 Deposit phase

At the deposit phase the merchant forwards a transaction detail including CNO and ecash to the bank for redemption. The deposit phase is discussed in Fig. 5. The steps are explained as follows:

• Step 1: The merchant selects a random secret (q), a new time-stamp $(T_n)$ then computes these parameters ($V_1$, $V_m$, $F_1$, $V_z$, $K_3$) followed by a signature ($\sigma _m$) to prevent repudiation as shown below,

  $$ V_1=H(ID_m||x_m) $$

  (44)
  $$ V_m=H(V_1||q) $$

  (45)
  $$ F_1=H(CNO||H(q)) $$

  (46)
  $$ V_z=F_1 \oplus V_m $$

  (47)
  $$ K_3=g^{ecash}\ mod \ p $$

  (48)
  $$ \sigma _m=(ecash-V_m*x_m)\ mod \ (p-1) $$

  (49)

  A session key ($SK_{mb}$), a symmetric key ($K_{mb}$) is generated to forward the redemption request along with (ecash, CNO) followed by $(\gamma )$ to verify the authenticity of merchant. Here, $D_m$ and $K_m$ represent $D_i$, $K_i$ respectively from registration phase for all participants. The process is described as follows,

  $$ SK_{mb}=mpk^{x_m}\ mod \ p $$

  (50)
  $$ K_{mb}=H(SK_{mb}||D_m||K_m||ID_m||ID_b) $$

  (51)
  $$ \gamma =H(K_3||V_m||ID_m||ID_c||ID_b) $$

  (52)

  $M \rightarrow B:$ $ID_m,ID_c,T_n,E_{K_{mb}} \{Pub_m,H(q),V_z,\sigma _m,H(CNO),N_m,E_{K{cb}} [ecash,TD_c,N_c, T_{new}]\}.$

• Step 2: The bank checks the legitimacy of merchant by primitively verifying the freshness of time-stamp as $T'-T_{n}'<? \triangle T$, then responds either by sending a successful message or abort the entire session. Initially, the bank computes ($F_1'$) and a shared session key ($SK_{mb}'$) followed by a symmetric decryption key ($K_{mb}'$) as follows,

  $$ F_1'=H(H(CNO)||H(q)) $$

  (53)
  $$ SK_{bm}'=(Pub_m)^{msk}\ {\rm mod} \ p $$

  (54)
  $$ K_{mb}'=H(SK_{mb}'||D_m||K_m||ID_m||ID_b) $$

  (55)

  and subsequently computes $V_m'$ and $K_3'$ using the signature $\sigma _m$ to prove merchant’s authenticity as,

  $$ V_m'=V_z\oplus F_1' $$

  (56)
  $$ K_3'=(g^{\sigma _m})*(Pub_m^{V_m}) $$

  (57)

  Using the computed parameters $V_m'$ and $K_3'$, bank computes $\gamma '=H(K_3'||V_m'||$ $ID_m||ID_c||$ $ID_b)$ then verifies if γ ≟ $\gamma'$. If this holds then computes $K_{cb}'$ and decrypt the message $(ecash,TD_c,$ $N_c,T_{new})$ which was sent by C via M, else abort the session. Upon successful decryption, B searches for $ID_c$ and H(CNO) stored in the database. If it exist then perform a step 2 of Sect. 3.6 then, sends a success (Succ) message and bill (Bill) to the customer. Later, deducts the (CNO) from customer’s account in the form of a digital cash.

  $$ B \rightarrow M: E_{K_m}\{Succ,Bill,ID_b\} $$

• Step 3: The merchant then sends ($Bill, Inv\_no$) message to customer along with product delivery $Prod_{delivery}$ details upon successful transaction.

  $$ M \rightarrow C: E_{K_{cm}}\{Succ,Bill,Inv\_no, Prod_{delivery}\} $$

Fig. 5

Overview of deposit phase

3.6 E-cash owner tracing phase

This phase prevents an ecash to be spent twice. Initially, upon receiving the message from merchant, the bank verifies the ecash requested for redemption using following steps:

• Step 1: The merchant sends following message $ID_m,ID_c,Pub_m,H(q),V_z,\sigma _m,H(CNO),$ $T_n,N_m,$ $E_{K_{cb}}[ecash,TD_c,$ $N_c,T_{new}]$ to the bank, then the bank takes payer’s identity $ID_c$ to match with its database to retrieve respective public key, thereby applies a symmetric decryption algorithm on $K_{cb}'=H(K_1'||mpk||T_s)$.

• Step 2: Upon decryption, the bank obtains $\{ecash,TD_c,N_c,T_{new}\}$, from which it computes the $(ecash)'$ and then verifies with the received one as follows,

  • (i) B first applies a one-way hash function on CNO to obtain $H(CNO)'$ in order to match with the stored H(CNO) from the database of customer with identity $ID_c.$ Thereafter, checks whether the obtained H(CNO)′ ≟ H(CNO).

  • (ii) If the above equation holds then computes an ecash from $H(CNO)',L',$ $M_2',N_m,N_c,$ $T_{new}$ and compares with stored value as ecash ≟ $H(H(CNO)'||L'||M_2'||N_m||N_c$ $||T_{new})$. If this equation satisfies, then the bank searches for redundant log of ecash from database, if the log $count=1$ it accepts the cash, else rejects entire transaction sending an error message $\bot$.

  • (iii) Upon acceptance, the bank verifies the customer’s account to debit amount as follows,

    $$ Acc\_{no^{\prime}} = {TD_{c}} \oplus H(msk) \oplus {ID_{c}} = {ID_{c}} \oplus Acc\_{no} \oplus H(msk) \oplus H(msk) \oplus {ID_{c}} = Acc\_no $$

    if the account is successfully derived, then it is confirmed that the customer is legitimate. Otherwise, abort the session.

    $$ \begin{aligned} Usr\_det=\, & {} W_c \oplus Acc\_no^{\prime}\\= \,& {} H(IMEI_c) \oplus Acc\_no \oplus Acc\_no^{\prime}\\=\, & {} H(IMEI_c) \\ Phone\_no=\, & {} Usr\_det\oplus ID_c\\=\, & {} H(IMEI_c)\oplus H(IMEI_c) \oplus Phone\_no\\=\, & {} Phone\_no \end{aligned}$$

  Hence, through $H(IMEI_c), Phone\_no$ the owner can be traced successfully.

4 Security analysis

This section illustrates the formal and informal security properties of the proposed scheme. The informal security analysis includes mutual authentication, prevention from double spending, anonymity revocation, unforgeability, key-compromise impersonation attack, unknown key-share attack, and non-repudiation. Whereas, the formal security analysis is presented to prove that the proposed authenticated key exchange protocol is secure or SAFE against active and passive attacks such as, man-in-the-middle attack and replay attack. The participants and bank can identify each other through $ID_i$, where $i \in \{C,B,M\}$. Here, bank is a trusted party who can only have the authority to view every detail of registered user’s but can not modify it. For instance, if the bank acts maliciously and tries to forge the messages sent over the transaction between C and M. It fails to weaken the integrity as each time the transaction amount and its respective parameters pass through a secure one-way hash algorithm which produces a message digest. In order to preserve anonymity every participant in communication can only view the identity $ID_i$ along with the public keys $Pub_i$ of other members (the merchant/customer can have access to only the publicly displayed parameters). At malicious owner tracing phase the bank undergoes a series of computations to get the original identity of payer through $(IMEI_i,Phone\_no)$. As, the entire transaction is encrypted and signed to achieve confidentiality and integrity no outsider can gather secret information except the publicly available values. Therefore, to sustain anonymity the bank may reveal the illegitimate user at malicious owner tracing phase to the participants in communication.

4.1 Mutual authentication

Mutual authentication refers that in a communication between two parties, each participant must authenticate itself to another by providing its effective identity [32]. In our scheme, not only a bank can authenticate customer/merchant but also the customer/merchant can authenticate bank vice versa. Similarly, a customer can authenticate the bank/merchant vice versa. For instance, in the withdrawal phase, the bank authenticates the customer C by computing $K_{1}'$ from Eq. 22 followed by comparing whether $K_{cb}$ ≟ $K_{cb}'$. Also, by examining whether α ≟ $\alpha '$. This implies that, both customer and bank computed same value.

Similarly, in payment phase, the merchant authenticates customer by verifying whether $K_{cm}$ ≟ $H(SK_{mc}'||ID_m||D_c||N_c||N_m)$ as in Eqs. 39 and 42. Along with comparing whether β ≟ $\beta'$. Finally, at the deposit phase, the bank authenticates the merchant using Eqs. 50 and 54 in order to compute symmetric key $K_{mb}'=H(SK_{mb}'||D_m||K_m||ID_m||ID_b)$ followed by verifying whether γ ≟ $\gamma'$. Thus, the scheme satisfies mutual authentication property to combat man-in-the-middle attack.

4.2 Prevention from double spending

When the merchant sends a redemption message $T_n,E_{K_{mb}} \{Pub_m,H(q),V_z,\sigma _m,H(CNO,N_m,$ $E_{K{cb}} [ecash,TD_c,N_c,T_{new}]\}$ to the bank, the bank decrypts the encrypted customer’s message embedded with the merchant’s request, i.e., $E_{K_{cb}} [ecash,$ $TD_c,N_c,T_{new}]$ to checks whether the ecash is already spent as the transaction is stored in the database. Suppose a malicious customer wants to use previous transaction message for requesting e-coin withdrawal from the bank. The bank checks the signature $\sigma _c$ on the requested amount if it already exist in the bank’s database, then the session is rejected. Thus, our scheme can thwart double spending issue.

4.3 Anonymity revocation

Anonymity revocation ensures that a customer’s identity is revealed successfully from an ecash without allowing double spending. The ecash owner tracing mechanism in Sect. 3.6 illustrates the protocol.

4.4 Unforgeability

In case, the customer and the merchant try to forge bank’s signature for illegal benefits in the withdrawal phase. The signature ($\sigma _b$) of e-coin (CNO) is signed by the bank. In the proposed scheme, the customer and merchant cannot generate a valid bank’s signature because they do not know the bank’s secret key (msk) and also the random secret (r) which are preserved under DLP and CDHP.

4.5 Man-in-the-middle attack

Since the customer and merchant communicates with the bank under a secure channel, and all the transferred messages are encrypted followed by valid signature between each communicating parties, it is impossible to modify the message during transaction. Suppose an adversary A learns the symmetric keys exchanged at withdrawal, payment, and deposit phase by performing man-in-the-middle attack, following description satisfies our claim.

In our scheme, at withdrawal phase, an adversary A cannot compute ($K_1$) in Eq. 16 without knowing the random secret (n) and user’s private key ($x_c$). Hence, A selects a random secret ($r_a' \in Z_p*$) and computes $v_c=H(W_c||x_a'||V_c)$ where ($x_a'$) is private key of adversary. Similarly, computes $e=H(v_c||r_a')$ and ($K_1$). Further, A intercepts the message $(E_{K_{cb}}(Amt,TD_c,Z))$ transmitted from C to B. Now B performs the validity check on the received message for which B computes ($K_1'$) in Eq. 22 from which ($K_{cb}$’) is computed and verified $K_{cb}$ ≟ $K_{cb}'$. If it does not match i.e., $K_{cb} \ne K_{cb}'$ then bank sends an authentication failed message to C.

Similarly, in the payment phase, an adversary cannot guess the nonce ($N_c, N_m$), also he cannot extract $SK_{cm}$ in Eq. 38, as this would be equivalent of solving the CDH problem which is assumed to be computationally hard. At deposit phase, an adversary A cannot compute $F_1$ in Eq. 46 without having the knowledge of the random secret q. Adversary A cannot extract $SK_{mb}$ in Eq. 50 as this would be equivalent of solving the CDH problem which is assumed to be computationally hard along with one-way property of hash function. Thus, the attack is not possible, as we have also verified using AVISPA toolkit which is depicted in Figs. 7 and 8.

4.6 Key-compromise impersonation attack

This attack refers that if the private key of a customer and merchant is compromised and is known to an adversary A, then he can impersonate as a legitimate user by performing any number of the transaction [33]. However, our scheme does not allow A to impersonate as either C or M. Assume that the private key $x_c$ of C is compromised by A, therefore, it is possible that he may impersonate M to C and try to obtain the correct session key computed between them. A uses C’s private key $x_c$ and M’s public key to compute $SK_{cm}$ in Eq. 38. Then compute $K_{cm}=H(SK_{cm}||ID_m||ID_c||N_c||N_m$ in order to send M, similarly to compute $SK_{cm}'$ in Eq. 41, A must require the knowledge of $M's$ private key $x_m$. Since due to the difficulty of solving discrete logarithm problem it is impossible to derive the private key of M from its public key $Pub_m=g^{x_m}$, also the accurate session key cannot be computed by A.

Similarly, it is infeasible to derive the session key between B and C, B and M by an adversary A. Thus, the proposed scheme can withstand key-compromise impersonation attack. In case a customer tries to impersonate another participant, suppose C tries to impersonate B he can randomly pick his secret key but it is infeasible to derive B’s secret key mpk from its public key due to the difficulty of solving DLP.

4.7 Unknown key-share attack

This attack indicates that after the completion of a protocol session, A believes that he has shared a session key with M or B, whereas M and B, unfortunately, believed that they shared session key with C. In our protocol, the identities are included in Eqs. 17, 39, and 51. Also, these are validated by C, M, and B in Eqs. 23, 42, and 55 separately. Therefore, each communicating group either C and B, C and M, and M and B gets confirmation that they share secure session key with legitimate user not with an adversary A.

4.8 Replay attack

If an adversary A wants to replay messages $Pub_m,N_m,\{ID_m,Pub_m, Req\_conf\}$ $_{H(ID_m||Pub_m||N_m)}$ which is a response sent by the M to C in the payment phase and $ID_c,ID_m,T_{new},CNO,\delta _c, R_1,Y,$ $E_{K_2},[ecash,H(CNO),\beta ,$ $E_{K_{cb}}(ecash,TD_c, T_{new})]$ is sent by C to M, the merchant/the bank can detect this attempt. The attack could be illustrated as:

A generates a time-stamp $T_{new}'$ then replay the message in $\{CNO,\delta _c,T_{new}',R_1,Y,E_{K_2}$ [ecash,  $H(CNO),\beta , E_{K_{cb}}(ecash,TD_c, T_{new})] \}$ it cannot pass the verification $T'-T_{new}'<? \triangle T$.

If the replaying message pass the verification $T'-T_{new}'<? \triangle T$, then the merchant verifies the signature computed using time-stamp $T_{new}'$ to verify $\delta _c'=(d*x_a-R_1'*T_{new}'*k')$ where $x_a$ is the private key of adversary which will not match $\delta _c$ as per Eq. 43.

4.9 Non-repudiation

It determines that every party in communication can not deny the authenticity of their signature embedded on the document. This is described at every phase of transaction as follows:

• 1. At the withdrawal phase, the customer sends his request for e-coin through its signature $\sigma _c$ which is evaluated by the bank as follows.

  $$\begin{aligned} K_1'=\, & {} (g^{\sigma _c})*(A^{Rw_c'}) \hbox {mod}\, p\\=\, & {} (g^{\{e*x_c-u*Rw_c\}})*(g^{u*Rw_c'}) \hbox {mod}\, p\\=\, & {} (g^{e*x_c-u*Rw_c+{u*Rw_c'}}) \hbox {mod}\, p\\=\, & {} (g^{e*x_c}) \hbox {mod}\, p\\ \end{aligned}$$

• 2. The customer receives the e-coin signed with bank’s authentic signature $\sigma _b$ at the withdrawal phase.

  $$\begin{aligned} M_2'=\, & {} (g^{\sigma _b})*(mpk^{M_1}) \hbox {mod}\, p\\=\, & {} (g^{\{r*H(CNO)-M_1*msk\}})*(g^{msk*M_1}) \hbox {mod}\, p\\=\, & {} g^{(r*H(CNO)-M_1*msk+msk*M_1)} \hbox {mod}\, p\\=\, & {} g^{(r*H(CNO))} \hbox {mod}\, p \end{aligned}$$

• 3. At the payment phase, the merchant verifies the legitimacy of order placed by customer for purchase by first checking the time-stamp $T_{new}$ and by validating signature $\delta _c.$

  $$\begin{aligned} K_2'=\, & {} (g^{\delta _c})*(Y^{R_1*T_{new}}) \hbox {mod}\, p\\=\, & {} g^{\{d*x_c-R_1*T_{new}*k\}}*g^{\{k*R_1*T_{new}\}} \hbox {mod}\, p\\=\, & {} g^{(d*x_c-R_1*T_{new}*k+k*R_1*T_{new})} \hbox {mod}\, p\\=\, & {} g^{d*x_c} \hbox {mod}\, p\\ \end{aligned}$$

• 4. At the deposit phase, the bank validates the request by merchant for redemption of e-coin into his account through his signature $\sigma _m.$

  $$\begin{aligned} K_3'=\,& {} (g^{\sigma _m})*(Pub_m^{V_m}) \hbox {mod} p\\=\, & {} g^{\{ecash-V_m*x_m\}}*g^{\{V_m*x_m\}} \hbox {mod} p\\=\, & {} g^{\{ecash-V_m*x_m+V_m*x_m\}} \hbox {mod} p\\=\, & {} g^{ecash} \hbox {mod} p \end{aligned}$$

5 Simulation for formal security verification of our scheme using AVISPA tool

In this section, we present a formal security verification module using the widely acknowledged AVISPA tool to ensure that the scheme is secure against the active and passive attacks [34, 35]. Followed by an illustration of the concept and knowledge about AVISPA simulator tool and then present a High-Level Protocols Specification Language (HLPSL) code description along with simulation results of proposed scheme.

Fig. 6

Architecture of AVISPA

5.1 AVISPA

AVISPA is a push-button tool for the automated validation of the Internet security-sensitive protocols and applications. It is considered as a widely accepted simulation tool for formal security verification by Internet engineering task force (IETF) [34], which measures whether the security protocol is SAFE or UNSAFE. It uses a special language called High-Level Protocol Specification Language and integrates the different back-ends that implement a variety of state-of-the-art automatic analysis techniques [36]. The architecture of AVISPA is demonstrated in Fig. 6. This language is based on roles where the AVISPA tool mechanically translates the HLPSL into a lower level specification using a HLPSL2IF translator. Afterward, it generates an intermediate format (IF). The present version integrates four back-ends namely, on-the-fly model-checker (OFMC), CL-based attack searcher (CL-AtSe), SAT-based model-checker (SATMC), and tree- automata-based protocol analyzer (TA4SP). The OFMC is responsible for symbolic techniques for exploring the state place in a demand driven way. CL-AtSe provides a translation from any security protocol wrote into an intermediate format (IF) into a set of constraints mainly used to find whether there are attacks on protocols. SAT generates a propositional form then input into a SAT solver and any model found is translated back into an attack. Finally, TA4SP is responsible for approximating the intruder knowledge using regular tree languages.

The AVISPA tool is mainly designed for IT professionals, engineers, and protocol analysts working in industry or standardized organizations. All the mentioned back-ends analyze the protocols under the assumptions of perfect cryptography where messages exchanged over a network are assumed to be under the control of a Dolev–Yao intruder [37]. AVISPA is role specific therefore each role is independent of others, by getting some initial information and communicating with other roles in the channel. Our authenticated key exchange protocol for electronic payment system is simulated using security protocol animator (SPAN) for AVISPA. Based on the four back-ends, OUTPUTFORMAT (OF) is generated after successful execution describing whether the protocol is safe or unsafe.

5.2 Specifying the protocol

We have implemented our scheme using the HLPSL language where, we assign three primary roles including a client, a bank, and a merchant represented as C, B,  and M respectively. The role specification of a spender, as the client C, the trusted arbitrator, as the bank B, and the specification for the role of the vendor, as the merchant M is given in Appendix A.

5.3 Analysis of results

The simulation results of our scheme on the back-ends OFMC and CL-AtSe is depicted using SPAN for AVISPA in Figs. 7 and 8. The results ensure that our scheme can withstand popular active attacks, such as the masquerading, replay, and man-in-the-middle attacks, and passive attacks. The summary of the results under OFMC and CL-AtSe prove that the protocol is safe against replay and man-in-the-middle attacks.

Fig. 7

Simulation result of OFMC

Fig. 8

Simulation result of CL-AtSe

6 Performance evaluation

In this section, we compare the proposed scheme with some existing systems already discussed in the literature with respect to features and communication efficiency. The properties considered in comparisons include anonymity, unforgeability, double spending, malicious owner tracing, off-line /on-line, non-repudiation, and mutual authentication. Among, which anonymity, unforgeability, double spending, and malicious owner tracing are the four essential features related to privacy and security, our scheme achieves all the essential features as mentioned in Sect. 4. Table 2 shows the comparison with existing schemes.

Table 2 Comparison of features of our scheme with existing schemes

Next, we compare the communication overhead which represents the number of interactions /rounds in each phase of our scheme with existing ones. Each phase is evaluated based on round complexity where our scheme provides an extra phase for efficient owner tracing which could be excluded while comparing with the above-mentioned schemes. Table 3 illustrates the performance evaluation.

Table 3 Comparison of required number of rounds for each protocol

We summarize the communication complexity of related ecash in Table 4. To make the DLP and CDH assumption intractable, we assume as in that p is 1024 bits as the scheme is designed for mobile commerce therefore increasing the key size may increase cost of computation and complexity. Assume that the output size of secure one-way hash functions is 512 bits. The following notations are utilized to mention the computation cost in each phase of transaction between bank, customer, and merchant. The computation time of one-way hashing operation is $T_{h}$, $T_{m}$ depicts the computation time of one modular multiplication, $T_{e}$ presents the computation time of one modular exponential operation, and $T_{i}$ represents inverse operation.

In fact, the magnitude of these computation costs can be denoted as $T_i>T_e>T_m>T_h$.

Table 4 Comparison of communication cost in each protocol

We discuss the comparison of existing schemes with respect to four phases in transaction that includes, registration/open account phase, withdrawal phase, payment phase, and deposit phase.

Table 4 indicates that our proposed scheme has low computational cost as compared to Chen et al. and Eslami’s scheme. Hence, our proposed model stands complete with all necessary features and is proved to be safe against active and passive attacks by satisfying properties of authenticated key exchange.

7 Conclusion

This paper proposes an authenticated key exchange protocol for the electronic payment system. The scheme achieves mutual authentication and introduces an effective malicious owner tracing mechanism. The performance evaluation shows that our scheme has low round complexity and computationally efficient as compared with existing protocols. Furthermore, the scheme also meets the essential features of an e-payment system. Additionally, the simulation results on AVISPA software confirmed that the proposed scheme is secure under OFMC and CL-AtSe back-ends and proves that the scheme can withstand active and passive attacks.

Appendices

Appendices

Appendix A In this appendix, we discussed the HLPSL verification code using AVISPA toolkit for the proposed electronic payment scheme. The HLPSL specifications are currently outlined or standardized by organizations like the IETF. The role specification of customer, bank and merchant is represented using given codes as follows.

1.1 Role specification of customer

role client(C,B,M:agent,

SKc,Key,Kcb,SKcm,Kcm,Km,SKm:symmetric_key,

Mul,Sub,H:hash_func,

Pubc,Mpk,Pubm:public_key,

Snd,Rcv:channel(dy))

played_by C

def=

local State:nat,

Xc,G,IDc,IDb,Msk,Nb,IMEI,W,V,Dc,Kc,K1,N,Ts,Vc,Rvc,Rwc,Rc,E,R,M1,M2,M3,Z,Alpha,CNO,C1,TDc,Amt,A,U,S,K2,K3,K,Y,D,K4,K5,R1,Invno,Proddet,Nm,IDm,Nc,Reqconf,Ecash,Beta,Tnew,Q,Xm,V1,Vm, Vz,K6,K7,F1,Gamma,Succ,Bill,Phoneno,Accno,L,Dm :text

const client_xc,bank_msk, merchant_xm,subs1,subs2,subs3,subs4,subs5,subs6,subs7,subs8:protocol_id

init State := 0

transition

1. State =0 /$\backslash$Rcv(start)$=|>$

State’:=1/$\backslash$IMEI’:=new()

/$\backslash$IDc’:=xor(H(IMEI),Phoneno)

/$\backslash$Xc’:=new()

/$\backslash$Pubc’:=exp(G,Xc)

/$\backslash$Snd(IDc.Pubc)

/$\backslash$secret(Xc,subs1,C,B)

/$\backslash$secret(Xc,subs2,C,M)

2. State=1/$\backslash$Rcv(IDb.Mpk.Nb)$=|>$

State’:=2/$\backslash$W’:=xor(H(IMEI),Accno)

/$\backslash$V’:=H(Xc.IDc)

/$\backslash$Dc’:=xor(H(Xc.IDc),H(IMEI))

/$\backslash$Kc’:=H(IMEI.Pubc.Xc)

/$\backslash$Snd(IDc.IDb.Dc.K1.W.Nb)

/$\backslash$secret(IMEI,subs3,C,B)

3. State=2/$\backslash$Rcv(IDc.TDc_Key)$=|>$

State’:=3/$\backslash$SKc’:=exp(Mpk,Xc)

/$\backslash$Key’:=H(SKc’.Dc.Kc)

/$\backslash$N’:=new()

/$\backslash$U’:=new()

/$\backslash$Ts’:=new()

/$\backslash$Vc’:=H(W.Xc.V)

/$\backslash$E’:=H(Vc.N)

/$\backslash$A’:=exp(G,U)

/$\backslash$Rwc’:=H(N.H(Amt).SKc)

/$\backslash$Rvc’:=xor(A,Rwc)

/$\backslash$K1’:=exp(G,Mul(E,Xc))

/$\backslash$K2’:=Sub(Mul(E,Xc),Mul(U,Rwc))

/$\backslash$Z’:=xor(H(K1.K3),H(U))

/$\backslash$Alpha’:=H(K1.Rwc.Kcb)

/$\backslash$Kcb’:=H(K2.Ts.Mpk)

/$\backslash$Snd(Dc.H(Amt).A.K2.Rvc.Alpha.Ts_Key.Amt.TDc.Z_Kcb)

/$\backslash$secret(Vc,subs4,C,B)

4. State=3/$\backslash$Rcv(IDb.M1.M3.H(CNO).CNO.TDc.K3_Kcb)$=|>$

State’:=4/$\backslash$L’:=xor(Z,M1)

/$\backslash$M2’:=Mul(exp(G,K3),exp(Pubc,M1))

/$\backslash$Nc’:=new()

/$\backslash$Snd(Dc.Pubc.Nc.Pubc.Dc.Invno.Proddet_H(Dc.Pubc.Nc))

5. State=4/$\backslash$Rcv(IDm.Pubm.Nm.Pubm.IDm.Reqconf_H(IDm.Pubm.Nm))$=|>$

State’:=5/$\backslash$K’:=new()

/$\backslash$Tnew’:=new()

/$\backslash$Y’:=exp(G,K)

/$\backslash$Ecash’:=H(CNO.L.M2.Nm.Nc.Tnew)

/$\backslash$D’:=H(Vc.K)

/$\backslash$K4’:=exp(G,Mul(D.Xc))

/$\backslash$K5’:=Sub(Mul(D,Xc),Mul(R1,Tnew,K))

/$\backslash$R1’:=H(Dc.Invno.H(CNO))

/$\backslash$SKcm’:=exp(Pubm,Xc)

/$\backslash$Kcm’:=H(SKcm.IDm.IDc.Nc.Nm)

/$\backslash$Beta’:=H(K4.Kcm.R1)

/$\backslash$Snd(IDc.IDm.Tnew.CNO.K5.R1.Y.Ecash.H(CNO).Beta.Ecash.TDc.Nm.Tnew_Kcb_K4_Kcm)

6. State =5/$\backslash$Rcv(Succ.Bill.Invno_Kcm)$=|>$

State’:=6/$\backslash$request(C,M,client_xc,Xc’)

end role

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

1.2 Role specification of bank

role bank(C,B,M:agent,

SKc,Key,Kcb,SKcm,Kcm,Km,SKm:symmetric_key,

Mul,Sub,H:hash_func,

Pubc,Mpk,Pubm:public_key,

Snd,Rcv:channel(dy))

played_by B

def=

local State:nat,

Xc,G,IDc,IDb,Msk,Nb,IMEI,W,V,Dc,Kc,K1,N,Ts,Vc,Rvc,Rwc,Rc,E,R,M1,M2,M3,Z,Alpha,CNO,C1,TDc,Amt,A,U,S,K2,K3,K,Y,D,K4,K5,R1,Invno,Proddet,Nm,IDm,Nc,Reqconf,Ecash,Beta,Tnew,Q,Xm,V1,Vm,Vz,K6,K7,F1,Gamma,Succ,Bill,Phoneno,Accno,L,Dm :text

const client_xc,bank_msk, merchant_xm,subs1,subs2,subs3,subs4,subs5,subs6,subs7,subs8:protocol_id

init State := 0

transition

1. State =0 /$\backslash$Rcv(IDc,Pubc)$=|>$ State’:=1/$\backslash$IDb’:=new()

/$\backslash$Msk’:=new()

/$\backslash$Nb’:=new()

/$\backslash$Mpk’:=exp(G,Msk)

/$\backslash$Snd(IDb.Mpk.Nb)

/$\backslash$secret(Msk,subs3,B,C)

/$\backslash$secret(Msk,subs4,B,M)

2. State=1 /$\backslash$Rcv(IDc.IDb.Dc.Kc.W.Nb)$=|>$

State’:=2/$\backslash$TDc’:=xor(IDc,xor(Accno,H(Msk)))

/$\backslash$SKc’:=exp(Pubc,Msk)

/$\backslash$Key’:=H(SKc.Dc.Kc)

/$\backslash$Snd(IDc.TDc_Kc)

3. State=2/$\backslash$Rcv(Dc.H(Amt).A.K2.Rvc.Ts_Key.Amt.TDc.Z_Kcb)$=|>$

State’:=3/$\backslash$Rwc’:=xor(Rvc,A)

/$\backslash$K1’:=Mul(exp(G,K3),exp(A,Rwc’))

/$\backslash$Kcb’:=H(K1’.Mpk.Ts)

/$\backslash$Alpha’:=H(K1’.Rwc’.Kcb’)

/$\backslash$R’:=new()

/$\backslash$CNO’:=new()

/$\backslash$L’:=H(R)

/$\backslash$M1’:=xor(Z,L’)

/$\backslash$M2’:=exp(G,Mul(R,H(CNO)))

/$\backslash$K3’:=Sub(Mul(R,H(CNO)),Mul(M1,Msk))

/$\backslash$M3’:=xor(H(Kc.K2),M2)

/$\backslash$Snd(IDb.M1.M3.H(CNO).CNO.TDc.K3_Kcb)

4. State=3/$\backslash$Rcv(IDm.IDc.Pubm.H(Q).H(CNO).Gamma.Vz.K7.Nm.Ecash.TDc.Nc.Tnew_Kcb_Km)$=|>$

State’:=4/$\backslash$ F1’:=H(CNO.H(Q))

/$\backslash$SKm’:=exp(Pubm,Msk)

/$\backslash$Km’:=(SKm’.F1’.IDm)

/$\backslash$Vm’:=xor(Vz,F1’)

/$\backslash$K6’:=Mul(exp(G,K7),exp(Pubm,Vm))

/$\backslash$Gamma:=H(K6’.Vm’.IDm.IDc.IDb)

/$\backslash$Succ’:=new()

/$\backslash$Bill’:=new()

/$\backslash$Snd(Succ.Bill.IDb_Km)

end role

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

1.3 Role specification of merchant

role merchant(C,B,M:agent,

SKc,Key,Kcb,SKcm,Kcm,Km,SKm:symmetric_key,

Mul,Sub,H:hash_func,

Pubc,Mpk,Pubm:public_key,

Snd,Rcv:channel(dy))

played_by M

def=

local State:nat,

Xc,G,IDc,IDb,Msk,Nb,IMEI,W,V,Dc,Kc,K1,N,Ts,Vc,Rvc,Rwc,Rc,E,R,M1,M2,M3,Z,Alpha,CNO,C1,TDc,Amt,A,U,S,K2,K3,K,Y,D,K4,K5,R1,Invno,Proddet,Nm,IDm,Nc,Reqconf,Ecash,Beta,Tnew,Q,Xm,V1,Vm,Vz,K6,K7,F1,Gamma,Succ,Bill,Phoneno,Accno,L,Dm :text

const client_xc,bank_msk, merchant_xm,subs1,subs2,subs3,subs4,subs5,subs6,subs7,subs8:protocol_id

init State := 0

transition

1.State =0 /$\backslash$Rcv(Dc.Pubc.Nc.Pubc.Dc.Invno.Proddet_H(Dc.Pubc.Nc))$=|>$

State’:=1/$\backslash$Xm’:=new()

/$\backslash$Pubm’:=exp(G,Xm)

/$\backslash$IDm’:=xor(H(IMEI),Phoneno)

/$\backslash$Nm’:=new()

/$\backslash$Snd(IDm.Pubm.Nm.Pubm.IDm.Reqconf_H(IDm.Pubm.Nm))

/$\backslash$secret(Xm,subs5,M,C)

/$\backslash$secret(Xm,subs6,M,B)

2. State =1/$\backslash$Rcv(IDc.IDm.Tnew.CNO.K5.R1.Y.Ecash.H(CNO).Beta.Ecash.TDc_Kcb_K4_Kcm)$=|>$

State’:=2/$\backslash$SKcm’:=exp(Pubc,Xm)

/$\backslash$Kcm’:=H(SKcm.IDm.Dc.Nc.Nm)

/$\backslash$K4’:=Mul(exp(G,K5),exp(Y,Mul(R1,Tnew)))

/$\backslash$Beta’:=HH(K4’.Kcm’.R1)

/$\backslash$Q’:=new()

/$\backslash$V1’:=H(IDm.Xm)

/$\backslash$Vm’:=H(V1.Q)

/$\backslash$F1’:=H(CNO.H(Q))

/$\backslash$Vz’:=xor(F1,Vm)

/$\backslash$K6’:=exp(G,Ecash)

/$\backslash$K7’:=Sub(Ecash,Mul(Vm,Xm))

/$\backslash$SKmb’:=exp(Mpk,Xm)

/$\backslash$Kmb’:=H(SKm.Dm.Km)

/$\backslash$Gamma’:=H(K6.Vm.IDm.IDc.IDb)

/$\backslash$Snd(IDm.IDc.Pubm.H(Q).H(CNO).Gamma.Vz.K7.Nm.Ecash.TDc.Nm.Tnew_Kcb_Km)

3. State=2/$\backslash$Rcv(Succ.Bill.IDb_Km)$=|>$

State’:=3/$\backslash$Snd(Succ.Bill.Invno_Kcm)

end role

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%