# A Two-Factor RSA-Based Robust Authentication System for Multiserver Environments

Authors: Ruhul Amin; SK Hafizul Islam; Muhammad Khurram Khan; Arijit Karati; Debasis Giri; Saru Kumari
Journal: Security and Communication Networks
 (2017)

---

## Abstract

The concept of two-factor multiserver authentication protocol was developed to avoid multiple number of registrations using multiple smart-cards and passwords. Recently, a variety of two-factor multiserver authentication protocols have been developed. It is observed that the existing RSA-based multiserver authentication protocols are not suitable in terms of computation complexities and security attacks. To provide lower complexities and security resilience against known attacks, this article proposes a two-factor (password and smart-card) user authentication protocol with the RSA cryptosystem for multiserver environments. The comprehensive security discussion proved that the known security attacks are eliminated in our protocol. Besides, our protocol supports session key agreement and mutual authentication between the application server and the user. We analyze the proof of correctness of the mutual authentication and freshness of session key using the BAN logic model. The experimental outcomes obtained through simulation of the Automated Validation of Internet Security Protocols and Applications (AVISPA) S/W show that our protocol is secured. We consider the computation, communication, and storage costs and the comparative explanations show that our protocol is flexible and efficient compared with protocols. In addition, our protocol offers security resilience against known attacks and provides lower computation complexities than existing protocols. Additionally, the protocol offers password change facility to the authorized user.


---

## Body

## 1. Introduction

Nowadays, network technologies and the online applications are rapidly growing; the Internet users are accessing online services to make their life more comfortable over Internet. When accessing a remote server, a session key should be negotiated between user and remote server, which would be used to encrypt the confidential messages. In this regard, two-factor authentication protocols using smart-card and password are widely used and designing a robust and efficient two-factor authentication protocol is a critical task. The concept of client-server communication over insecure networks has been introduced for single server environment, and many researchers have proposed numerous authentication protocols [1–3] using hash function [4–6], RSA cryptosystem [7–9], elliptic curve [10], chaotic map [11, 12], and bilinear pairing [13]. However, these protocols are unsuitable for multiserver communications. For this purpose, lots of authentication protocols [13–17] have been put forward for multiserver architecture. In multiserver communications, there are three entities such as a user, a registration center, and a number of application servers. In this environment, all the application servers and users registered themselves to the registration center. All of these application servers are responsible for providing required services to the users. An architecture of the multiserver communication is given in Figure 1.Figure 1
Multiserver framework used in our protocol.User anonymity [18, 19] is one of the security issues in user authentication protocol, where user’s identity should be kept secret from the adversary. There are several application areas such as banking, medical system [7, 10], and wireless sensor network [20], where the authorized users want to keep their identity secret from an adversary; that is, the adversary is unable to extract or guess user’s original identity from the login and authentication messages. In addition to that, the mutual authentication is another important security aspect, where client and server both can verify each other to avoid man-in-the-middle attack. As the adversary can also act as server, so verifying at the server end is also important. Like mutual authentication, protection of low-entropy information such as identity and password from guessing attack is very imperative. Furthermore, the insider attack is also difficult to protect since a person who is managing the registration center may misuse users’ confidential information such as password. So, the protection of such kind of attack is also essential. As we know the public messages of any authentication protocol are transmitted via open channels, and thus an adversary may intercept, drop, modify, and reroute the captured messages. Thus, the adversary can try to impersonate either the user or the remote server. In this regard, mutual authentication [18, 19] between the participants is most important security aspect. Another objective of any client-server authentication protocol is to negotiate a session key between entities. Since both the participants negotiate their session key, whether the session keys computed by the both entities are equal or not should be checked. In order to perform this, a session key verification property [21] should be involved in the protocol.


### 1.1. Literature Reviews

In the literature, numerous multiserver authentication protocols are designed to achieve strong security as well as lower complexities. In 2009, Liao and wang [22] put forward a multiserver authentication protocol; however, Chen et al. [23] showed that the protocol in [22] suffers from forward secrecy problem. Further, Hsiang and Shih [24] demonstrated that the protocol in [22] cannot defy some common attacks [13], and then they enhanced it to remedy the identified weaknesses. Lee et al. [25] designed an enhanced and efficient multiserver authentication protocol after pointing out the security weakness of the protocol in [24]. Subsequently, Troung et al. [26] illustrated that the protocol in [24] cannot resist smart-card stolen and user impersonation attacks. To vanquish these loopholes, the authors put forward another multiserver authentication protocol and showed that it is secure against common attacks. Moreover, Sood et al. [15] observed different security weaknesses of the protocol in [24] and then designed a multiserver authentication protocol. In 2012, Li et al. [17] showed that the protocol in [15] cannot withstand smart-card stolen attack and subsequently put forward a new protocol. Currently, Pippal et al. [14] designed a secure smart-card based user authentication protocol and showed that their protocol is robust against known attacks. Unfortunately, He et al. [27] demonstrated that the protocol in [14] is not secure against impersonation attack, offline password guessing attack, insider attack, and server spoofing attack. Also, Yeh [16] demonstrated that the protocol in [14] is not secure against some common attacks. More recently, Hsieh and Leu [28] demonstrated that Liao and Hsiao’s protocol [29] could not give full security requirements and then devised an efficient protocol using bilinear pairing. In 2015, Amin and Biswas [13] showed that the protocol in [28] is insecure against offline password guessing attack, server masquerading attack, and user anonymity problem. Additionally, they described that the password change facility of this protocol is not user-friendly. To overcome these security vulnerabilities, Amin and Biswas [13] devised user authentication and session key agreement protocol using smart-card and bilinear pairing. In the same year, Giri et al. [8] proposed a robust authentication protocol using RSA and claimed that it is strongly protected against security vulnerabilities. But, Amin and Biswas [7] highlighted that the protocol in [8] is not secure against several security attacks. Further, they proposed a new protocol to overcome the security weaknesses. In 2016, Sutrala et al. [30] show that the protocol in [7] is not secure and also proposed an improved protocol. Similarly, the authors in [31] demonstrated security attacks of the protocol in [7] and proposed a new RSA-based authentication protocol.


### 1.2. Contributions

This article claims the following contributions.(i)
We have pointed out that all the existing RSA-based multiserver protocols include high computation cost and are insecure against known attacks.(ii)
The main contribution of this article is the design and analysis of a lightweight and robust authentication protocol for multiserver environments.(iii)
The proposed protocol is analyzed using the AVISPA S/W and its results showed that our protocol is secure.(iv)
We proved that our protocol is completely protected against known security threats. Further, it solves the problem of anonymity issue.(v)
We show that the performance of our protocol is better in terms of computation and communication overheads.


### 1.3. Organization of the Article

Section2 discusses our authentication protocol for multiserver architecture. The concrete security discussion of our protocol appears in Section 3. The authentication correctness of our protocol using BAN logic is shown in Section 4. The simulation results of our protocol using AVISPA S/W are discussed in Section 5. The comprehensive performance measurement of our protocol and comparative results with other protocols appear in Section 6. We have provided the conclusion with some remarks and future scope in Section 7.


## 1.1. Literature Reviews

In the literature, numerous multiserver authentication protocols are designed to achieve strong security as well as lower complexities. In 2009, Liao and wang [22] put forward a multiserver authentication protocol; however, Chen et al. [23] showed that the protocol in [22] suffers from forward secrecy problem. Further, Hsiang and Shih [24] demonstrated that the protocol in [22] cannot defy some common attacks [13], and then they enhanced it to remedy the identified weaknesses. Lee et al. [25] designed an enhanced and efficient multiserver authentication protocol after pointing out the security weakness of the protocol in [24]. Subsequently, Troung et al. [26] illustrated that the protocol in [24] cannot resist smart-card stolen and user impersonation attacks. To vanquish these loopholes, the authors put forward another multiserver authentication protocol and showed that it is secure against common attacks. Moreover, Sood et al. [15] observed different security weaknesses of the protocol in [24] and then designed a multiserver authentication protocol. In 2012, Li et al. [17] showed that the protocol in [15] cannot withstand smart-card stolen attack and subsequently put forward a new protocol. Currently, Pippal et al. [14] designed a secure smart-card based user authentication protocol and showed that their protocol is robust against known attacks. Unfortunately, He et al. [27] demonstrated that the protocol in [14] is not secure against impersonation attack, offline password guessing attack, insider attack, and server spoofing attack. Also, Yeh [16] demonstrated that the protocol in [14] is not secure against some common attacks. More recently, Hsieh and Leu [28] demonstrated that Liao and Hsiao’s protocol [29] could not give full security requirements and then devised an efficient protocol using bilinear pairing. In 2015, Amin and Biswas [13] showed that the protocol in [28] is insecure against offline password guessing attack, server masquerading attack, and user anonymity problem. Additionally, they described that the password change facility of this protocol is not user-friendly. To overcome these security vulnerabilities, Amin and Biswas [13] devised user authentication and session key agreement protocol using smart-card and bilinear pairing. In the same year, Giri et al. [8] proposed a robust authentication protocol using RSA and claimed that it is strongly protected against security vulnerabilities. But, Amin and Biswas [7] highlighted that the protocol in [8] is not secure against several security attacks. Further, they proposed a new protocol to overcome the security weaknesses. In 2016, Sutrala et al. [30] show that the protocol in [7] is not secure and also proposed an improved protocol. Similarly, the authors in [31] demonstrated security attacks of the protocol in [7] and proposed a new RSA-based authentication protocol.


## 1.2. Contributions

This article claims the following contributions.(i)
We have pointed out that all the existing RSA-based multiserver protocols include high computation cost and are insecure against known attacks.(ii)
The main contribution of this article is the design and analysis of a lightweight and robust authentication protocol for multiserver environments.(iii)
The proposed protocol is analyzed using the AVISPA S/W and its results showed that our protocol is secure.(iv)
We proved that our protocol is completely protected against known security threats. Further, it solves the problem of anonymity issue.(v)
We show that the performance of our protocol is better in terms of computation and communication overheads.


## 1.3. Organization of the Article

Section2 discusses our authentication protocol for multiserver architecture. The concrete security discussion of our protocol appears in Section 3. The authentication correctness of our protocol using BAN logic is shown in Section 4. The simulation results of our protocol using AVISPA S/W are discussed in Section 5. The comprehensive performance measurement of our protocol and comparative results with other protocols appear in Section 6. We have provided the conclusion with some remarks and future scope in Section 7.


## 2. Proposed Authentication Protocol

Based on RSA cryptosystem, this section introduces a two-factor multiserver authentication protocol using password and smart-card. Our authentication protocol includes initialization phase, registration phase for application serverASj and user Ui, login phase, verification phase, and password change phase. We present a list of symbols used throughout this article in the Notations.


### 2.1. Initialization Phase

This phase is executed by theRC to initialize the whole system. Accordingly, RC determines two large prime numbers p and q (each of them at least 1024 bits), computes n=p×q, and further determines a generator g∈Zn∗. RC keeps (p,q) as secrets and publishes n as public value. RC further selects a cryptographic hash function h(·): {0,1}∗→{0,1}l, where {0,1}∗ represents arbitrary binary string and {0,1}l is a fixed-length l binary string.


### 2.2. Application Server Registration Phase

The main objective ofASj is to provide remote services to Ui on demand through insecure communication. In order to provide remote services, all ASj must execute registration phase to the trusted RC. During registration, RC and ASj perform the operations as given below.Step 1.
A
S
j first selects his/her identity IDj and submits it to RC through a secure channel.Step 2.
After receiving the registration request,RC chooses a public key ej(1<ej<ϕ(n)) such that gcd(ϕ(n),ej)=1 and computes the corresponding private key dj≡ej-1modϕ(n), where ϕ(n)=(p-1)(q-1). RC further computes confidential information Yj=h(ej∥dj).Step 3.
R
C maintains a table RCT that includes IDj,ej,(Yj⊕x) and keeps it securely. Finally, RC sends dj to ASj securely.
We further depict the registration phase of application server of the proposed protocol in Figure2.Figure 2
Application server registration phase of our protocol.


### 2.3. User Registration Phase

To register withRC, Ui performs the tasks as explained below.Step 1.
U
i determines his/her identity IDi together with password PWi and sends 〈IDi,Ai〉 to RC over a secure channel, where Ai=h(IDi∥PWi).Step 2.
After receiving〈IDi,Ai〉, RC computes Bi=gx·IDimodn, Ci=IDiAimodn, Di=Bi⊕Ci, Ei=h(Ai∥Bi), and Fi=ENCx(IDi) and then embeds 〈Di,Ei,Fi,h(·),n〉 into an new and fresh smart-card.Step 3.
After preparing the smart-card,RC sends it to Ui over secure channel or in person.Further we demonstrate the user registration phase of our protocol in Figure3.Figure 3
User registration phase of our protocol.


### 2.4. Login Phase

At the time of enjoying remote services,Ui takes initiation and executes this phase. The following operations are performed in this phase.Step 1.
U
i inserts the smart-card and enters 〈IDi,PWi〉 to the terminal on request. Then, the terminal computes Ai∗=h(IDi∗∥PWi∗), Ci∗=IDiAi∗modn, Bi∗=Di⊕Ci∗, and Ei∗=h(Ai∗∥Bi∗) and checks the condition whether Ei∗ matches with Ei. If the condition holds, it implies that (IDi∗=IDi) and (PWi∗=PWi).Step 2.
The terminal now produces a random numberRi and calculates M1=h(Bi∗∥Ri) and M2=h(Bi∗)⊕Ri and then sends 〈M1,M2,Fi,IDj〉 to RC using an insecure channel.Further we provide description of login phase of the proposed protocol in Figure4.Figure 4
Login phase of our protocol.


### 2.5. Verification Phase

This phase achieves a session key agreement betweenUi and ASj with the help of RC over insecure communication. All the operations performed by RC, Ui, and ASj are discussed now.Step 1.
After getting login message〈M1,M2,Fi,IDj〉, RC first decrypts Fi using its own secret key x and then further computes Bi′=gx·IDimodn, Ri′=M2⊕h(Bi′), and M1′=h(Bi′∥Ri′). Then RC checks whether M1′ matches with M1. If the condition holds, Ui is verified by RC.Step 2.
R
C extracts Yj and the public key ej and then computes M3=Yj⊕IDi. Finally, RC sends 〈ej, M3〉 to Ui via insecure channel.Step 3.
After receiving〈ej,M3〉, Ui computes Yj′=M3⊕IDi, M4=h(IDi∥Ri∥Yj′∥IDj), and M5=(IDi∥Ri∥M4)ejmodn and then transmits M5 to ASj over insecure channel.Step 4.
After receivingM5, ASj first decrypts M5 using its private key dj and according to RSA cryptosystem, ASj obtains 〈IDi,Ri,M4〉. Then ASj computes Yj′′=h(ej∥dj) and M4′′=h(IDi∥Ri∥Yj′′∥IDj) and then checks whether M4′′ matches with M4. If such condition is incorrect, ASj terminates the connection or else authenticates Ui.Step 5.
After verifyingUi, ASj computes the session key SKj=h(IDi∥IDj∥Ri∥Rj) and further computes Rij=Ri⊕Rj and M6=h(SKj∥Rj∥IDj). ASj sends 〈M6,Rij〉 to Ui through any insecure channel.Step 6.
After receiving〈M6,Rij〉, Ui computes Rj′=Rij⊕Ri, SKi=h(IDi∥IDj∥Ri∥Rj′), and M6′=h(SKi∥Rj′∥IDj) and checks whether M6′=?M6 holds. If the condition holds, Ui authenticates ASj and session key generated by Ui and ASj is verified.Further we provide the description of verification phase of our protocol in Figure5.Figure 5
Verification phase of our protocol.


### 2.6. Password Change Phase

In password-based remote user authentication protocol, user’s password is one of the most sensitive information pieces and must be changed whenever required. Therefore, password change phase must be rendered to the registered user. This phase requires the following actions to change the password.Step 1.
U
i inserts the smart-card and enters old 〈IDi,PWi〉 to the terminal on request. Then, the terminal computes Ai∗=h(IDi∗∥PWi∗), Ci∗=IDiAi∗modn, Bi∗=Di⊕Ci∗, and Ei∗=h(Ai∗∥Bi∗) and checks whether Ei∗ matches with Ei. If the condition is correct, it implies that (IDi∗=IDi) and (PWi∗=PWi).Step 2.
After successfully verifying〈IDi,PWi〉, the smart-card made request to the Ui for a new password. Then Ui enters a fresh password PWin and then the smart-card computes Ain=h(IDi∥PWin), Cin=IDiAimodn, Din=Bi∗⊕Cin, and Ein=h(Ain∥Bi∗) and replaces 〈Di,Ei〉 with 〈Din,Ein〉.Further we explained the our password change phase in Figure6.Figure 6
Password update phase of our protocol.


## 2.1. Initialization Phase

This phase is executed by theRC to initialize the whole system. Accordingly, RC determines two large prime numbers p and q (each of them at least 1024 bits), computes n=p×q, and further determines a generator g∈Zn∗. RC keeps (p,q) as secrets and publishes n as public value. RC further selects a cryptographic hash function h(·): {0,1}∗→{0,1}l, where {0,1}∗ represents arbitrary binary string and {0,1}l is a fixed-length l binary string.


## 2.2. Application Server Registration Phase

The main objective ofASj is to provide remote services to Ui on demand through insecure communication. In order to provide remote services, all ASj must execute registration phase to the trusted RC. During registration, RC and ASj perform the operations as given below.Step 1.
A
S
j first selects his/her identity IDj and submits it to RC through a secure channel.Step 2.
After receiving the registration request,RC chooses a public key ej(1<ej<ϕ(n)) such that gcd(ϕ(n),ej)=1 and computes the corresponding private key dj≡ej-1modϕ(n), where ϕ(n)=(p-1)(q-1). RC further computes confidential information Yj=h(ej∥dj).Step 3.
R
C maintains a table RCT that includes IDj,ej,(Yj⊕x) and keeps it securely. Finally, RC sends dj to ASj securely.
We further depict the registration phase of application server of the proposed protocol in Figure2.Figure 2
Application server registration phase of our protocol.


## 2.3. User Registration Phase

To register withRC, Ui performs the tasks as explained below.Step 1.
U
i determines his/her identity IDi together with password PWi and sends 〈IDi,Ai〉 to RC over a secure channel, where Ai=h(IDi∥PWi).Step 2.
After receiving〈IDi,Ai〉, RC computes Bi=gx·IDimodn, Ci=IDiAimodn, Di=Bi⊕Ci, Ei=h(Ai∥Bi), and Fi=ENCx(IDi) and then embeds 〈Di,Ei,Fi,h(·),n〉 into an new and fresh smart-card.Step 3.
After preparing the smart-card,RC sends it to Ui over secure channel or in person.Further we demonstrate the user registration phase of our protocol in Figure3.Figure 3
User registration phase of our protocol.


## 2.4. Login Phase

At the time of enjoying remote services,Ui takes initiation and executes this phase. The following operations are performed in this phase.Step 1.
U
i inserts the smart-card and enters 〈IDi,PWi〉 to the terminal on request. Then, the terminal computes Ai∗=h(IDi∗∥PWi∗), Ci∗=IDiAi∗modn, Bi∗=Di⊕Ci∗, and Ei∗=h(Ai∗∥Bi∗) and checks the condition whether Ei∗ matches with Ei. If the condition holds, it implies that (IDi∗=IDi) and (PWi∗=PWi).Step 2.
The terminal now produces a random numberRi and calculates M1=h(Bi∗∥Ri) and M2=h(Bi∗)⊕Ri and then sends 〈M1,M2,Fi,IDj〉 to RC using an insecure channel.Further we provide description of login phase of the proposed protocol in Figure4.Figure 4
Login phase of our protocol.


## 2.5. Verification Phase

This phase achieves a session key agreement betweenUi and ASj with the help of RC over insecure communication. All the operations performed by RC, Ui, and ASj are discussed now.Step 1.
After getting login message〈M1,M2,Fi,IDj〉, RC first decrypts Fi using its own secret key x and then further computes Bi′=gx·IDimodn, Ri′=M2⊕h(Bi′), and M1′=h(Bi′∥Ri′). Then RC checks whether M1′ matches with M1. If the condition holds, Ui is verified by RC.Step 2.
R
C extracts Yj and the public key ej and then computes M3=Yj⊕IDi. Finally, RC sends 〈ej, M3〉 to Ui via insecure channel.Step 3.
After receiving〈ej,M3〉, Ui computes Yj′=M3⊕IDi, M4=h(IDi∥Ri∥Yj′∥IDj), and M5=(IDi∥Ri∥M4)ejmodn and then transmits M5 to ASj over insecure channel.Step 4.
After receivingM5, ASj first decrypts M5 using its private key dj and according to RSA cryptosystem, ASj obtains 〈IDi,Ri,M4〉. Then ASj computes Yj′′=h(ej∥dj) and M4′′=h(IDi∥Ri∥Yj′′∥IDj) and then checks whether M4′′ matches with M4. If such condition is incorrect, ASj terminates the connection or else authenticates Ui.Step 5.
After verifyingUi, ASj computes the session key SKj=h(IDi∥IDj∥Ri∥Rj) and further computes Rij=Ri⊕Rj and M6=h(SKj∥Rj∥IDj). ASj sends 〈M6,Rij〉 to Ui through any insecure channel.Step 6.
After receiving〈M6,Rij〉, Ui computes Rj′=Rij⊕Ri, SKi=h(IDi∥IDj∥Ri∥Rj′), and M6′=h(SKi∥Rj′∥IDj) and checks whether M6′=?M6 holds. If the condition holds, Ui authenticates ASj and session key generated by Ui and ASj is verified.Further we provide the description of verification phase of our protocol in Figure5.Figure 5
Verification phase of our protocol.


## 2.6. Password Change Phase

In password-based remote user authentication protocol, user’s password is one of the most sensitive information pieces and must be changed whenever required. Therefore, password change phase must be rendered to the registered user. This phase requires the following actions to change the password.Step 1.
U
i inserts the smart-card and enters old 〈IDi,PWi〉 to the terminal on request. Then, the terminal computes Ai∗=h(IDi∗∥PWi∗), Ci∗=IDiAi∗modn, Bi∗=Di⊕Ci∗, and Ei∗=h(Ai∗∥Bi∗) and checks whether Ei∗ matches with Ei. If the condition is correct, it implies that (IDi∗=IDi) and (PWi∗=PWi).Step 2.
After successfully verifying〈IDi,PWi〉, the smart-card made request to the Ui for a new password. Then Ui enters a fresh password PWin and then the smart-card computes Ain=h(IDi∥PWin), Cin=IDiAimodn, Din=Bi∗⊕Cin, and Ein=h(Ain∥Bi∗) and replaces 〈Di,Ei〉 with 〈Din,Ein〉.Further we explained the our password change phase in Figure6.Figure 6
Password update phase of our protocol.


## 3. Discussion about the Security

This section measures security strength of our protocol by analyzing several security attacks. Generally, password-based authentication protocol suffers from different attacks. The authentication protocol must resist the known attacks and achieve mutual authentication, session key verification along with login, and password change phase efficiently. Here, we analyze that our protocol can defy all the relevant security attacks. In this regard, we define some valid assumptions [2, 10, 20] as follows.Definition 1.
An adversaryA has the capabilities for retrieving smart-card information using power consumption monitoring method [34, 35]. For instance, if A gets the smart-card, he/she has the capability of finding the confidential data from it.Definition 2.
All messages produced by the protocol during execution are sent via insecure communication such as Internet. Therefore,A intercepts, deletes, modifies, reroutes, and resends the transmitted message. It is worth noting that A cannot intercept any information from the secure network [10].Definition 3.
A knows execution of the protocol; that is, the protocol is public. Additionally, A may behave like legitimate user or client.Definition 4.
We considered that the authorized user selects dictionary word as password and identity. It is noted thatA is unable to guess password and identity in polynomial time. If Ai=h(IDi∥PWi) is known to A, then it is hard to verify guessed password and identity using Ai in polynomial time [20].Definition 5.
We considered that the random nonce and secret key size are significantly large (parameter with high entropy). Therefore,A is unable to guess the information within polynomial time.Definition 6.
LetAi=Bi⊕Ci and only Ai is known to A. Then A cannot find Bi or Ci from Ai within polynomial time.Definition 7.
Assume length of identity or password isn characters. According to [36], the probability of guessing the password is approximately equal to 1/26n.Theorem 8.
Our multiserver authentication protocol resists smart-card stolen attack.Proof.
In smart-card stolen attack,A generally extracts all the smart-card information (see Definition 1) and then tries to login to ASj on behalf of Ui. Suppose A got smart-card of Ui and extracted the information 〈Di,Ei,Fi,h(·),n〉, where Bi=gx·IDimodn, Ci=IDiAimodn, Di=Bi⊕Ci, Ei=h(Ai∥Bi), and Fi=ENCx(IDi). Note that A cannot compute any confidential information of  Ui or ASj using Di. Further, Ei and Fi are protected by the hash function and symmetric key encryption algorithm, respectively. Therefore, the extraction of secure information by A is infeasible and the protocol resists smart-card stolen attack.Theorem 9.
Our multiserver authentication protocol can defy the offline identity guessing attack.Proof.
As per Theorem8, it is clear that A has no advantage to found confidential information from the lost/stolen smart-card of any legal user. In this attack, we further elaborated whether A can guess user’s identity using intercepted public messages. We supposed that A intercepts the login messages 〈M1,M2,Fi,IDj〉, 〈ej,M3〉, and 〈M5,M6,Rij〉, where M1=h(Bi∗∥Ri), M2=h(Bi∗)⊕Ri, M3=Yj⊕IDi, M4=h(IDi∥Ri⊕Yj′∥IDj), M5=(IDi∥Ri∥M4)ejmodn, Rij=Ri⊕Rj, and M6=h(SKj∥Rj∥IDj). Note that A cannot guess IDi using Bi without knowing the secret key d of RC. Further, A cannot guess IDi from M3 without Yj. If A wants to verify the guessed identity using Bi∗ and M3, the probability would be approximately 1/26n+1024 and 1/26n+128, respectively, where length of d is 1024 bits. The value of M5 is transmitted as ciphertext, and therefore, it is also infeasible to extract information without the private key dj of ASj. Hence, the proposed authentication protocol can defy this type of offline identity guessing attack.Theorem 10.
Our multiserver authentication protocol can defy the offline password guessing attack.Proof.
Similar to Theorem9, A may attempt to guess PWi of Ui in offline mode. We described in Theorem 8 that A cannot extract or guess Ui’s password PWi from the smart-card information. In addition, the public messages are also independent of Ui’s PWi. As a result, A has no way to guess Ui’s password in offline mode.Theorem 11.
Our multiserver authentication protocol can defy the insider attack.Proof.
As mentioned in [7, 10], if the insider person A of RC or ASj gets Ui’s password PWi by some means, she/he can attempt to login different accounts of Ui. Thus, the protection against the insider attack is also an important issue in password-based authentication system. When the registration phase of our protocol is executed, Ui delivers IDi and Ai to RC for issuing a smart-card, where Ai=h(IDi∥PWi). Since Ai is protected by hash function, A is unable to extract PWi due to one-way behavior of the hash function.Theorem 12.
Our multiserver authentication protocol can defy the user impersonation attack.Proof.
To impersonateUi, A has to generate a valid login message that must be authenticated by RC. During the login phase, Ui generates 〈M1,M2,Fi,IDj〉, where M1=h(Bi∗∥Ri) and M2=h(Bi∗)⊕Ri. Note that A can generate the random number Ri. However, it is very difficult to compute Bi=gx·IDimodn without knowing 〈x,IDi〉 from the known information. Therefore, the protocol resists user impersonation attack.Theorem 13.
Our multiserver authentication protocol can defy the server impersonation attack.Proof.
Resembling Theorem12, A may attempt to forge the authentication message to ASj. For that, A has to compute another genuine message 〈M6,Rij〉, which is to be authenticated by Ui, where Rij=Ri⊕Rj and M6=h(SKj∥Rj∥IDj). Now, A generates the random number Rj′(≠Rj) and tries to compute the valid Rij. But, it is infeasible to compute Rij without knowing Ri. On the other hand, A cannot compute correct M6 without knowing SKj. Hence, the adversary is unable to launch this attack.Theorem 14.
Our multiserver authentication protocol can defy the session key computation attack.Proof.
The protocol negotiates a session key betweenUi and ASj, which will be used to encrypt the confidential information transmitted over public channel. Our authentication protocol computes the session key SKj=SKi=h(IDi∥IDj∥Ri∥Rj) and its security depends on the hash function. Note that session key depends on the confidential information 〈IDi,Ri,Rj〉. We discussed earlier that A is unable to compute these pieces of information. Hence, A is unable to calculate the session key of our protocol.Theorem 15.
Our multiserver authentication protocol can defy the known session specific temporary information attack.Proof.
It is assumed that short-term information used in the protocol is known toA. However, A could not compute the session key in any session. We assume that A knows Ri and Rj tries to compute SKj. Then A needs IDi to compute SKj. We described earlier that the computation of IDi is not feasible by A. Therefore, A cannot launch this attack.Theorem 16.
Our multiserver authentication protocol can defy the stolen verifier attack.Proof.
At the time of application server registration,RC maintains a table called RCT, which includes 〈IDj,ej,(Yj⊕x)〉. Among these, Yj is the most confidential parameter used in the proposed protocol. We now supposed that A got RCT by some means and attempted to break the security of the proposed protocol. Note that Yj is not stored in plaintext form. It is stored as Yj⊕x in the table, where x is the secret key of RC. As a result, A cannot compute Yj without knowing x.


## 4. Authentication Proof Using BAN Logic

This section addresses the freshness of the exchanged message and the proof of the mutual authentication based on Burrows-Abadi-Needham (BAN) logic [9, 13]. Being a known security model, BAN logic is required to demonstrate the authentication and secure key distribution protocols. Now, some backgrounds and notations used in BAN logic are given below.(i)
Principals are agents involved in the protocol (usually people or programs).(ii)
Keys are required to encrypt messages symmetrically.(iii)
Public Keys are similar to Keys except they are used in pairs.(iv)
Nonces are message parts that are not repeated.(v)
Timestamps are similar to nonces where they are unlikely to be repeated.The BAN statements used in this paper that are required to analyze the security of our protocol are listed in the Notations.The logical postulates of the BAN logic are listed in Table1.Table 1
Logical postulates of BAN logic.
Rule
Notation
Description
Message meaning
P
∣
≡
P
⇌
K
Q
,
P
⊲
X
K
P
∣
≡
Q
∣
~
X
If principalP believes K is shared with Q and sees XK,
thenP believes Q once said X.
Freshness-conjuncatenation
P
∣
≡
♯
(
X
)
P
∣
≡
♯
(
X
,
Y
)
IfP believes X is fresh, then P believes
the freshness of (X,Y).
Belief
P
∣
≡
(
X
)
,
P
∣
≡
Y
P
∣
≡
(
X
,
Y
)
If principalP believes X and Y, then P believes (X,Y).
Nonce verification
P
∣
≡
♯
X
,
P
∣
≡
Q
∣
~
X
P
∣
≡
Q
∣
≡
X
IfP believes X is fresh and the principal
Q once sent X, then P believes that Q believes X.
Jurisdiction
P
∣
≡
Q
⇒
X
,
P
∣
≡
Q
∣
≡
X
P
∣
≡
X
If the principal believes thatQ has jurisdiction over X and Q believes X,
thenP believes that X is true.
Session key
P
∣
≡
♯
(
X
)
,
P
∣
≡
Q
∣
≡
X
P
∣
≡
P
↔
K
Q
IfP believes session key is fresh and P and Q believe X, which are the
necessary parameters of session key, thenP believes that (s)he shares
session keyK with Q.In order to prove the authentication protocol is valid, a list of the following things must be processed:(i)
In language of formal logic, idealize our protocol.(ii)
Find out assumptions about the initial state of our protocol.(iii)
In order to deduce new predicates, use production and rules of the logic.(iv)
Use logic to find out beliefs made by parties in our protocol.To show our protocol is secure, it must satisfy BAN logic based goals as discussed below.(i)
Goal 1: Ui∣≡Ui↔SKASj(ii)
Goal 2: Ui∣≡ASj∣≡Ui↔SKASj(iii)
Goal 3: ASj∣≡ASj↔SKUi(iv)
Goal 4: ASj∣≡Ui∣≡ASj↔SKUiOur protocol is transformed into the idealized form:M1: Ui→ASj:M5,〈Ri〉YjM2: ASj→Ui:M6,〈Rj〉IDiThe assumptions on initial state of the protocol are made to analyze the proposed protocol as follows: A1:Ui∣≡♯(Ri)A2:ASj∣≡♯(Rj)C1:Ui∣≡Ui↔YjASjC2:ASj∣≡ASj↔IDiUiB1:ASj∣≡Ui⇒RiB2:Ui∣≡ASj⇒RjIdealized form of the protocol is demonstrated under BAN logic with assumptions. The main proofs are as follows:M1: Ui→ASj:M5,〈Ri〉Yj.Based on seeing rule, we getS1:ASj⊲M5According toC2, S1, and message meaning rule, we knowS2:ASj∣≡Ui∣~Ri.According toA2, S2, and freshness-conjuncatenation rule and nonce verification rule, we knowS3:ASj∣≡Ui∣≡Ri, where Ri is the essential session key parameter of the proposed protocol.According toB1, S3, and the jurisdiction rule is applied, we knowS4: ASj∣≡Ri.According toA2, S3, and the session key rule is used, we getS5: ASj∣≡ASj↔SKUi (Goal 3).S5 with nonce verification rule according to A2 is used and we getS6: ASj∣≡Ui∣≡ASj↔SKUi (Goal 4).M2: ASj→Ui:M6,〈Rj〉IDi.Based on seeing rule it getsS7: Ui⊲M6.Based onC1, S7, and message meaning rules, it is known thatS8: Ui∣≡ASj∣~Rj.Based onA1, S8, and nonce verification and freshness-conjuncatenation rules, we getS9: Ui∣≡ASj∣≡Rj, where Rj is essential session key parameter of our protocol.Based onB2, S9, and jurisdiction rule, we getS10: Ui∣≡Rj.Based onA1, S9, and the session key rule, we getS11: Ui∣≡Ui↔SKASj (Goal 1).S11 and nonce verification rule are used according to A1 and getS12: Ui∣≡ASj∣≡Ui↔SKASj (Goal 2).The discussion made above proves that our protocol correctly achieves the mutual authentication property.


## 5. Simulation Results of the Scheme Using AVISPA

We first briefly discuss the concept of the AVISPA and then present simulation results followed by HLPSL code of our protocol. According to literature review, the AVISPA is one of the widely used simulation tools for verifying security correction of the authentication protocol. Many earlier protocols [7, 10, 20] have been simulated using AVISPA tool.


### 5.1. Description of the AVISPA Tool

It is well known that AVISPA [37] is known as a tool for formal security verification. AVISPA supports HLPSL (High Level Scheme Specification Language). A general description and pictorial representation of the AVISPA tool can be found in [20, 37, 38]. AVISPA tool supports four different back-ends (OFMC, CL-AtSe, SATMC, and TA4SP) and abstraction based methods that are integrated through HLPSL. We refer to [38] for more details of OFMC, CL-AtSe, SATMC, and TA4SP. During the execution of the tool, HLPSL specification is interpreted into intermediate form (IF) by hlpsl2if translator where IF is lower-level language and directly read by AVISPA back-ends.The HLPSL is a role-oriented language where every party plays a role during protocol execution. Every role is free from others, retrieving some initial information through parameters and communicating with other roles by the channels. Intruder is framed using the model [39] with a possibility for intruder as a legitimate role in protocol run. In addition, role system narrates principals, number of sessions, and roles. OUTPUT FORMAT (OF) using the four back-ends is produced, and (OF) after successful execution highlights the result whether our protocol is safe or not under which condition output is generated. Based on the HLPSL language, we have implemented the role specifications for the user, registration center, and application server in Algorithms 1, 2, and 3, respectively. The role specification for the session, goal, and environment in HLPSL is given in Algorithm 4.Algorithm 1:Role specification for the user of our protocol in HLPSL.
role user (Ui, RC, ASj: agent,
SKey1  : symmetric_key,
SKey2  : symmetric_key,
H, MUL, SUB: hash_func,
Snd, Rcv: channel(dy))
played_by Ui
def=
local State  :  nat,
IDi, PWi, IDj, N, Ej, Yj: text,
Di, Ei, Fi, Ai, Bi, Ci, Ri, M1, M2, M3, M4, M6, Rij, Rj, M5,
SKi: message,
Inc  :  hash_func
const user_rserver, rserver_aserver,
aserver_user, sec1, sec2, sec3, sec4, sec5, sec6: protocol_id
init State ≔0
transition
1. State = 0 ∧ Rcv(start)=∣>
State＇ ≔ 1 ∧ Ai＇ ≔ h(IDi.PWi)
∧ Snd({IDi.Ai＇}_SKey2)
2. State = 1 ∧ Rcv({Di＇.Ei＇.Fi＇.N＇}_SKey2) =∣>
State＇ ≔ 2 ∧ Ci＇ ≔ exp(IDi, Ai)
∧ Bi＇ ≔ xor(Di＇,Ci＇)
∧ Ri＇ ≔new()
∧ M1＇ ≔h(Bi＇.Ri＇)
∧ M2＇ ≔ xor(h(Bi＇), Ri＇)
∧ Snd(M1＇.M2＇.Fi.IDj)
∧ secret({PWi}, sec1, {Ui})
3. State = 2 ∧ Rcv(Ej＇.M3＇) =∣>
State＇ ≔ 3 ∧ Yj＇ ≔ xor(M3＇,IDi)
∧ M4＇ ≔ h(IDi. Ri. Yj＇.IDj)
∧ M5＇ ≔exp((IDi.Ri.M4＇), Ej)
∧ Snd(M5＇)
∧ secret({Yj＇}, sec2, {Ui,ASj,RC})
∧ witness(ASj, Ui, aserver_user, Ri)
4. State = 3 ∧ Rcv(M6＇,Rij＇) =∣>
State＇ ≔ 4 ∧ Rj＇ ≔ xor(Rij,Ri)
∧ SKi＇ ≔ h(IDi.IDj.Ri.Rj＇)
∧ secret({SKi}, sec3, {Ui,ASj})
end roleAlgorithm 2:Role specification for registration server of our protocol in HLPSL.
role rserver (RC, Ui, ASj: agent,
SKey1  :  symmetric_key,
SKey2  :  symmetric_key,
H, MUL, SUB: hash_func,
Snd, Rcv: channel(dy) )
played_by RC
def=
local State  : nat,
IDj, IDi, Ej, P, Q, N, W, Dj, G, Yj: text,
Ai, Bi, Ci, Di, Ei, Fi, X, M1, M2, M3: message,
Inc  : hash_func
const user_rserver, rserver_aserver,
aserver_user, sec1, sec2, sec3, sec4, sec5,
sec6  : protocol_id
init State ≔0
transition
1. State = 0∧ Rcv({IDj＇}_SKey1) =∣>
State＇ ≔ 1 ∧ Ej＇ ≔ new()
∧ Dj＇ ≔new()
∧ P＇ ≔new()
∧ Q＇ ≔new()
∧N＇ ≔ MUL(P＇,Q＇)
∧W＇ ≔ MUL(SUB(P＇,1), SUB(Q＇,1))
∧ Yj＇ ≔ h(Ej＇.Dj＇)
∧ Snd({Ej＇.Dj＇}_SKey1)
∧ secret({Dj＇}, sec4, {ASj,RC})
∧ secret({P＇,Q＇}, sec5, {RC})
2. State = 1∧ Rcv({IDi.Ai＇}_SKey2) =∣>
State＇ ≔ 2 ∧ Bi＇ ≔ exp(G,MUL(X,IDi))
∧ Ci＇ ≔ exp(IDi,Ai)
∧ Di＇ ≔ xor(Bi＇,Ci＇)
∧ Ei＇ ≔h(Ai.Bi＇)
∧ Fi＇ ≔{IDi}_X
∧ Snd({Di＇.Ei＇.Fi＇.N}_SKey2)
3. State = 2∧ Rcv(M1＇.M2＇.Fi.IDj) =∣>
State＇ ≔ 3 ∧ M3＇ ≔ xor(Yj,IDi)
∧ Snd(Ej.M3＇)
end roleAlgorithm 3:Role specification for the application-server of our protocol in HLPSL.
role aserver (ASj, Ui, RC: agent,
SKey1  : symmetric_key,
SKey2  : symmetric_key,
% H is hash function
H,MUL,SUB: hash_func,
Snd, Rcv: channel(dy) )
played_by ASj
def=
local State  : nat,
IDi, IDj, Ej, Dj, Yj: text,
M5, M9, Ri, M4, Rj, Rij, SKj, M6: message,
Inc  : hash_func
const user_rserver, rserver_aserver,
aserver_user, sec1, sec2, sec3, sec4, sec5,
sec6  : protocol_id
init State ≔0
transition
1. State = 0 ∧ Rcv(start)=∣>
State＇ ≔ 1 ∧ IDj＇ ≔new()
∧ Snd({IDj＇}_SKey1)
∧ Rcv({Ej.Dj}_SKey1)
2. State = 1 ∧ Rcv(M5＇) =∣>
State＇ ≔ 2 ∧ M9＇ ≔ exp(M5＇,Dj)
∧ M9＇ ≔ (IDi.Ri.M4)
∧ Yj＇ ≔ h(Ej.Dj)
∧ Rj＇ ≔ new()
∧ Rij＇ ≔ xor(Ri,Rj)
∧ SKj＇ ≔ h(IDi.IDj.Ri.Rj＇)
∧ M6＇ ≔ h(SKj＇.Rj＇.IDj)
∧ Snd(M6＇.Rij＇)
∧ secret({Ri,Rj＇}, sec6, {ASj,Ui})
∧ witness(Ui, ASj, aserver_user, Rj)
end roleAlgorithm 4:Role specification for the goal, session, and environment of our protocol in HLPSL.
role session(Ui, RC, ASj: agent,
SKey1  : symmetric_key,
SKey2  : symmetric_key,
H, MUL,SUB: hash_func)
def=
local SI, SJ, RI, RJ, PI, PJ: channel (dy)
composition
user(Ui, RC, ASj, SKey1, SKey2, H, MUL, SUB, SI, RI)
∧ rserver(Ui, RC, ASj, SKey1, SKey2, H, MUL, SUB, SJ, RJ)
∧ aserver(Ui, RC, ASj, SKey1, SKey2, H, MUL, SUB, PI, PJ)
end role
role environment()
def=
const ui, rc, asj: agent,
skey1  : symmetric_key,
skey2  : symmetric_key,
h,mul, sub: hash_func,
idi, pwi, idj, ai, bi, ci, di, ei, fi, m1, m2, m3, m4, m5, m6, ri, rj,
rij, ski, skj, n  : text,
user_aserver_Ri, aserver_user_Rj, sec1, sec2, sec3, sec4, sec5,
sec6: protocol_id
intruder_knowledge ={ui, rc, asj, h, mul, m6, rij, m5, m3, di,
ei, fi, n, m1, m2, idj}
composition
session(rc, ui, asj, skey1, skey2, h, mul, sub)
∧ session(ui, rc, asj, skey1, skey2, h, mul, sub)
∧ session(asj, ui, rc, skey1, skey2, h, mul, sub)
end role
goal
secrecy_of sec1
secrecy_of sec2
secrecy_of sec3
secrecy_of sec4
secrecy_of sec5
secrecy_of sec6
authentication_on user_aserver_Ri
authentication_on aserver_user_Rj
end goal
environment()


### 5.2. Simulation Results

Algorithms5 and 6 show the results on back-ends CL-AtSe and OFMC. Results for both the back-ends confirm that the protocol is SAFE which indicates that the protocol resists passive and active attacks. The proposed protocol achieves the following six properties and two authentication phases that are mentioned below.(1)
Secrecy_of sec 1:PWi is the confidential information and known to Ui only.(2)
Secrecy_of sec 2: the confidential informationYj is known to 〈Ui,ASj,RC〉 only.(3)
Secrecy_of sec 3: the session keySKi is shared only between Ui and ASj.(4)
Secrecy_of sec 4: the private keydj of ASj is shared between 〈ASj,RC〉.(5)
Secrecy_of sec 5: the confidential informationP and Q pieces are only known to RC.(6)
secrecy_of sec 6: the random numbers〈Ri,Rj〉 are known to 〈ASj,Ui〉 only.(7)
authentication_on alice_server_Ri:Ui produces a random nonce Ri, and if ASj gets it secretly, then ASj authenticates Ui.(8)
authentication_on server_alice_Rj:Ui authenticates ASj based on the random number Rj.Algorithm 5:OFMC back-end simulation result of our protocol.
% OFMC
% Version of 2006/02/13
SUMMARY
SAFE
DETAILS
BOUNDED_NUMBER_OF_SESSIONS
PROTOCOL
/home/avispa/web-interface-computation/./
tempdir/workfile8Y6LVt.if
GOAL
as_specified
BACKEND
OFMC
COMMENTS
STATISTICS
parseTime: 0.00 s
searchTime: 0.19 s
visitedNodes: 17 nodes
depth: 2 pliesAlgorithm 6:CL-AtSe back-end result of the proposed protocol.
SUMMARY
SAFE
DETAILS
BOUNDED_NUMBER_OF_SESSIONS
TYPED_MODEL
PROTOCOL
/home/avispa/web-interface-computation
/./tempdir/workfilegQjd7wqdOJ.if
GOAL
As Specified
BACKEND
CL-AtSe
STATISTICS
Analysed: 15 states
Reachable: 15 states
Translation: 0.32 seconds
Computation: 0.00 seconds


## 5.1. Description of the AVISPA Tool

It is well known that AVISPA [37] is known as a tool for formal security verification. AVISPA supports HLPSL (High Level Scheme Specification Language). A general description and pictorial representation of the AVISPA tool can be found in [20, 37, 38]. AVISPA tool supports four different back-ends (OFMC, CL-AtSe, SATMC, and TA4SP) and abstraction based methods that are integrated through HLPSL. We refer to [38] for more details of OFMC, CL-AtSe, SATMC, and TA4SP. During the execution of the tool, HLPSL specification is interpreted into intermediate form (IF) by hlpsl2if translator where IF is lower-level language and directly read by AVISPA back-ends.The HLPSL is a role-oriented language where every party plays a role during protocol execution. Every role is free from others, retrieving some initial information through parameters and communicating with other roles by the channels. Intruder is framed using the model [39] with a possibility for intruder as a legitimate role in protocol run. In addition, role system narrates principals, number of sessions, and roles. OUTPUT FORMAT (OF) using the four back-ends is produced, and (OF) after successful execution highlights the result whether our protocol is safe or not under which condition output is generated. Based on the HLPSL language, we have implemented the role specifications for the user, registration center, and application server in Algorithms 1, 2, and 3, respectively. The role specification for the session, goal, and environment in HLPSL is given in Algorithm 4.Algorithm 1:Role specification for the user of our protocol in HLPSL.
role user (Ui, RC, ASj: agent,
SKey1  : symmetric_key,
SKey2  : symmetric_key,
H, MUL, SUB: hash_func,
Snd, Rcv: channel(dy))
played_by Ui
def=
local State  :  nat,
IDi, PWi, IDj, N, Ej, Yj: text,
Di, Ei, Fi, Ai, Bi, Ci, Ri, M1, M2, M3, M4, M6, Rij, Rj, M5,
SKi: message,
Inc  :  hash_func
const user_rserver, rserver_aserver,
aserver_user, sec1, sec2, sec3, sec4, sec5, sec6: protocol_id
init State ≔0
transition
1. State = 0 ∧ Rcv(start)=∣>
State＇ ≔ 1 ∧ Ai＇ ≔ h(IDi.PWi)
∧ Snd({IDi.Ai＇}_SKey2)
2. State = 1 ∧ Rcv({Di＇.Ei＇.Fi＇.N＇}_SKey2) =∣>
State＇ ≔ 2 ∧ Ci＇ ≔ exp(IDi, Ai)
∧ Bi＇ ≔ xor(Di＇,Ci＇)
∧ Ri＇ ≔new()
∧ M1＇ ≔h(Bi＇.Ri＇)
∧ M2＇ ≔ xor(h(Bi＇), Ri＇)
∧ Snd(M1＇.M2＇.Fi.IDj)
∧ secret({PWi}, sec1, {Ui})
3. State = 2 ∧ Rcv(Ej＇.M3＇) =∣>
State＇ ≔ 3 ∧ Yj＇ ≔ xor(M3＇,IDi)
∧ M4＇ ≔ h(IDi. Ri. Yj＇.IDj)
∧ M5＇ ≔exp((IDi.Ri.M4＇), Ej)
∧ Snd(M5＇)
∧ secret({Yj＇}, sec2, {Ui,ASj,RC})
∧ witness(ASj, Ui, aserver_user, Ri)
4. State = 3 ∧ Rcv(M6＇,Rij＇) =∣>
State＇ ≔ 4 ∧ Rj＇ ≔ xor(Rij,Ri)
∧ SKi＇ ≔ h(IDi.IDj.Ri.Rj＇)
∧ secret({SKi}, sec3, {Ui,ASj})
end roleAlgorithm 2:Role specification for registration server of our protocol in HLPSL.
role rserver (RC, Ui, ASj: agent,
SKey1  :  symmetric_key,
SKey2  :  symmetric_key,
H, MUL, SUB: hash_func,
Snd, Rcv: channel(dy) )
played_by RC
def=
local State  : nat,
IDj, IDi, Ej, P, Q, N, W, Dj, G, Yj: text,
Ai, Bi, Ci, Di, Ei, Fi, X, M1, M2, M3: message,
Inc  : hash_func
const user_rserver, rserver_aserver,
aserver_user, sec1, sec2, sec3, sec4, sec5,
sec6  : protocol_id
init State ≔0
transition
1. State = 0∧ Rcv({IDj＇}_SKey1) =∣>
State＇ ≔ 1 ∧ Ej＇ ≔ new()
∧ Dj＇ ≔new()
∧ P＇ ≔new()
∧ Q＇ ≔new()
∧N＇ ≔ MUL(P＇,Q＇)
∧W＇ ≔ MUL(SUB(P＇,1), SUB(Q＇,1))
∧ Yj＇ ≔ h(Ej＇.Dj＇)
∧ Snd({Ej＇.Dj＇}_SKey1)
∧ secret({Dj＇}, sec4, {ASj,RC})
∧ secret({P＇,Q＇}, sec5, {RC})
2. State = 1∧ Rcv({IDi.Ai＇}_SKey2) =∣>
State＇ ≔ 2 ∧ Bi＇ ≔ exp(G,MUL(X,IDi))
∧ Ci＇ ≔ exp(IDi,Ai)
∧ Di＇ ≔ xor(Bi＇,Ci＇)
∧ Ei＇ ≔h(Ai.Bi＇)
∧ Fi＇ ≔{IDi}_X
∧ Snd({Di＇.Ei＇.Fi＇.N}_SKey2)
3. State = 2∧ Rcv(M1＇.M2＇.Fi.IDj) =∣>
State＇ ≔ 3 ∧ M3＇ ≔ xor(Yj,IDi)
∧ Snd(Ej.M3＇)
end roleAlgorithm 3:Role specification for the application-server of our protocol in HLPSL.
role aserver (ASj, Ui, RC: agent,
SKey1  : symmetric_key,
SKey2  : symmetric_key,
% H is hash function
H,MUL,SUB: hash_func,
Snd, Rcv: channel(dy) )
played_by ASj
def=
local State  : nat,
IDi, IDj, Ej, Dj, Yj: text,
M5, M9, Ri, M4, Rj, Rij, SKj, M6: message,
Inc  : hash_func
const user_rserver, rserver_aserver,
aserver_user, sec1, sec2, sec3, sec4, sec5,
sec6  : protocol_id
init State ≔0
transition
1. State = 0 ∧ Rcv(start)=∣>
State＇ ≔ 1 ∧ IDj＇ ≔new()
∧ Snd({IDj＇}_SKey1)
∧ Rcv({Ej.Dj}_SKey1)
2. State = 1 ∧ Rcv(M5＇) =∣>
State＇ ≔ 2 ∧ M9＇ ≔ exp(M5＇,Dj)
∧ M9＇ ≔ (IDi.Ri.M4)
∧ Yj＇ ≔ h(Ej.Dj)
∧ Rj＇ ≔ new()
∧ Rij＇ ≔ xor(Ri,Rj)
∧ SKj＇ ≔ h(IDi.IDj.Ri.Rj＇)
∧ M6＇ ≔ h(SKj＇.Rj＇.IDj)
∧ Snd(M6＇.Rij＇)
∧ secret({Ri,Rj＇}, sec6, {ASj,Ui})
∧ witness(Ui, ASj, aserver_user, Rj)
end roleAlgorithm 4:Role specification for the goal, session, and environment of our protocol in HLPSL.
role session(Ui, RC, ASj: agent,
SKey1  : symmetric_key,
SKey2  : symmetric_key,
H, MUL,SUB: hash_func)
def=
local SI, SJ, RI, RJ, PI, PJ: channel (dy)
composition
user(Ui, RC, ASj, SKey1, SKey2, H, MUL, SUB, SI, RI)
∧ rserver(Ui, RC, ASj, SKey1, SKey2, H, MUL, SUB, SJ, RJ)
∧ aserver(Ui, RC, ASj, SKey1, SKey2, H, MUL, SUB, PI, PJ)
end role
role environment()
def=
const ui, rc, asj: agent,
skey1  : symmetric_key,
skey2  : symmetric_key,
h,mul, sub: hash_func,
idi, pwi, idj, ai, bi, ci, di, ei, fi, m1, m2, m3, m4, m5, m6, ri, rj,
rij, ski, skj, n  : text,
user_aserver_Ri, aserver_user_Rj, sec1, sec2, sec3, sec4, sec5,
sec6: protocol_id
intruder_knowledge ={ui, rc, asj, h, mul, m6, rij, m5, m3, di,
ei, fi, n, m1, m2, idj}
composition
session(rc, ui, asj, skey1, skey2, h, mul, sub)
∧ session(ui, rc, asj, skey1, skey2, h, mul, sub)
∧ session(asj, ui, rc, skey1, skey2, h, mul, sub)
end role
goal
secrecy_of sec1
secrecy_of sec2
secrecy_of sec3
secrecy_of sec4
secrecy_of sec5
secrecy_of sec6
authentication_on user_aserver_Ri
authentication_on aserver_user_Rj
end goal
environment()


## 5.2. Simulation Results

Algorithms5 and 6 show the results on back-ends CL-AtSe and OFMC. Results for both the back-ends confirm that the protocol is SAFE which indicates that the protocol resists passive and active attacks. The proposed protocol achieves the following six properties and two authentication phases that are mentioned below.(1)
Secrecy_of sec 1:PWi is the confidential information and known to Ui only.(2)
Secrecy_of sec 2: the confidential informationYj is known to 〈Ui,ASj,RC〉 only.(3)
Secrecy_of sec 3: the session keySKi is shared only between Ui and ASj.(4)
Secrecy_of sec 4: the private keydj of ASj is shared between 〈ASj,RC〉.(5)
Secrecy_of sec 5: the confidential informationP and Q pieces are only known to RC.(6)
secrecy_of sec 6: the random numbers〈Ri,Rj〉 are known to 〈ASj,Ui〉 only.(7)
authentication_on alice_server_Ri:Ui produces a random nonce Ri, and if ASj gets it secretly, then ASj authenticates Ui.(8)
authentication_on server_alice_Rj:Ui authenticates ASj based on the random number Rj.Algorithm 5:OFMC back-end simulation result of our protocol.
% OFMC
% Version of 2006/02/13
SUMMARY
SAFE
DETAILS
BOUNDED_NUMBER_OF_SESSIONS
PROTOCOL
/home/avispa/web-interface-computation/./
tempdir/workfile8Y6LVt.if
GOAL
as_specified
BACKEND
OFMC
COMMENTS
STATISTICS
parseTime: 0.00 s
searchTime: 0.19 s
visitedNodes: 17 nodes
depth: 2 pliesAlgorithm 6:CL-AtSe back-end result of the proposed protocol.
SUMMARY
SAFE
DETAILS
BOUNDED_NUMBER_OF_SESSIONS
TYPED_MODEL
PROTOCOL
/home/avispa/web-interface-computation
/./tempdir/workfilegQjd7wqdOJ.if
GOAL
As Specified
BACKEND
CL-AtSe
STATISTICS
Analysed: 15 states
Reachable: 15 states
Translation: 0.32 seconds
Computation: 0.00 seconds


## 6. Performance Evaluation and Discussion

This section discusses the performance of the proposed protocol and then compares it with the recently published protocols [14, 16, 32, 33] in terms of computation, smart-card storage, and communication costs. Note that the login and authentication phases are necessary for performing secure communication in each authentication cycle. Therefore, we have considered these phases in comparison. To evaluate the computational cost, this article used the following time complexities.(i)
Th: cost for one-way hash operation(ii)
Tsym: cost for symmetric key encryption/decryption operation(iii)
Te: cost for exponentiation operation(iv)
Tm: cost for modular multiplication operationThe results obtained in [40] have executed various cryptographic operations using MIRACL C/C++ Library. It requires Windows 7 with 32-bit OS, Visual C++ 2008, 1024-bit cyclic group, 160-bit prime field Fp, AES for symmetric encryption/decryption, and SHA-1 operation. On these above configurations, execution time (in ms) of such different operations is as follows: Th≈0.0004ms, Tsym≈0.1303ms, Tm≈0.0147ms, and Te≈1.8269ms.In Tables2 and 3, we observed that computational cost and execution time of our protocol are lower than the protocols proposed in [14, 16] and nearly equal to the protocols in [32, 33]. Our protocol provides strong security protection against known attacks, such as mutual authentication, user anonymity, session key agreement, efficient login phase, and verification phase, and response time of the protocol is comparatively lesser than other protocols. For better understanding, we give execution cost (ms) comparison of the proposed protocol and the related ones [14, 16, 32, 33] in Figure 7.Table 2
Computation cost comparison of our protocol with other protocols.
Scheme
User
Server
Total
Pippal et al. [14]
4
T
h
+
3
T
e
+
T
m
3
T
h
+
4
T
e
+
T
m
7
T
h
+
7
T
e
+
2
T
m
Yeh [16]
4
T
h
+
2
T
e
+
T
m
5
T
h
+
4
T
e
+
T
m
9
T
h
+
6
T
e
+
2
T
m
Wei et al. [32]
7
T
h
+
2
T
e
6
T
h
+
2
T
e
13
T
h
+
4
T
e
Li et al. [33]
5
T
h
+
T
e
8
T
h
+
3
T
e
13
T
h
+
4
T
e
Proposed
6
T
h
+
2
T
e
6
T
h
+
2
T
e
+
T
s
y
m
12
T
h
+
4
T
e
+
T
s
y
mTable 3
Execution time (ms) comparison of our protocol with other protocols.
Scheme
User
Server
Total
Pippal et al. [14]
5.4966 ms
7.3235 ms
12.8200 ms
Yeh [16]
3.6701 ms
7.5621 ms
11.2322 ms
Wei et al. [32]
3.6566 ms
3.6562 ms
7.3128 ms
Li et al. [33]
1.8289 ms
5.4839 ms
7.3128 ms
Proposed
3.6562 ms
3.7865 ms
7.4427 msFigure 7
Execution time (ms) of different protocols.In Table4, smart-card storage cost, communication cost, and total number of message transmissions have been provided. The notation 160×Sj∗ indicates that smart-card storage capacity is dependent on the total number of application servers. Therefore, the limitation of the protocols [14, 16, 32] is that the number of application servers is restricted owing to low capacity of smart-card. Note that smart-card storage cost does not increase with the number of application servers in the protocol [33] and our protocol. The proposed protocol requires less storage costs for the smart-card compared to the protocols proposed in [14, 16, 32, 33]. In our protocol, we provide session key verification property and to achieve it, the protocol takes extra single message exchange in comparison with the protocols [14, 16, 32, 33]. Note that the protocols [14, 16, 32, 33] do not provide the session key verification property. In Table 4, we also noticed that the total number of bits transmission of our protocol is lesser than related protocols.Table 4
Communication and storage costs of our protocol and others.
Scheme
Smart-card cost (bits)
Communication cost (bits)
Number of messages
Pippal et al. [14]
4256
+
(
160
×
S
j
)
∗
2528
3
Yeh [16]
4256
+
(
160
×
S
j
)
∗
2528
3
Wei et al. [32]
2368
+
(
160
×
S
j
)
∗
3328
3
Li et al. [33]
3712
2688
3
Proposed
2528
2304
4


## 7. Conclusion and Future Scope

This article presents a flexible and cost-effective RSA-based multiserver authentication protocol to perform secure mutual authentication over any insecure channel with user and application server. We have then proved informally that our protocol can defy different cryptographic attacks. Moreover, the security of the mutual authentication and the freshness of the session key have been established based on BAN logic model, and AVISPA simulation results claim that proposed protocol is SAFE in CL-AtSe and OFMC models. We have then shown that the performance of our protocol is more effective than the existing protocols in terms of complexities. Our protocol is not only robust, but also flexible since it has user-friendly password change phase.In recent times, cloud computing is also applied to the environment of mobile communication. However, the computation and storage capabilities of mobile devices are very limited. Therefore an attempt can be made to design a provably secure and lightweight multiserver authentication protocol for mobile cloud computing environments.



---

*Source: 5989151-2017-08-21.xml*