A Multi-server Environment with Secure and Efficient Remote User Authentication Scheme Based on Dynamic ID Using Smart Cards

Abstract

The growth of the Internet and telecommunication technology has facilitated remote access. During the last decade, numerous remote user authentication schemes based on dynamic ID have been proposed for the multi-server environment using smart cards. Recently, Shunmuganathan et al. pointed out that Li et al.’s scheme is defenseless in resisting the password guessing attack, stolen smart card attack and forgery attack. Furthermore, they showed the poor repairability and no two-factor security in Li et al.’s scheme. To surmount these security disadvantages, Shunmuganathan et al. proposed a remote user authentication scheme using smart card for multi-server environment and claimed that their scheme is secure and efficient. In this paper, we show that Shunmuganathan et al.’s scheme is also defenseless in resisting the password guessing attack, stolen smart card attack, user impersonation attack, forgery attack, forward secrecy and session key secrecy. Moreover, the two-factor security is also not preserved in their scheme. In our proposed scheme, a user is free to choose his/her login credentials such as user id and password. And also a user can regenerate the password any time. Simultaneously the proposed scheme preserves the merits of Shunmuganathan et al.’s scheme and also provides better functionality and security features, such as mutual authentication, session key agreement and perfect forward secrecy. The security analysis using the widely accepted Burrows–Abadi–Needham logic shows that the proposed scheme provides the mutual authentication proof between a user and a server. Through the rigorous formal and informal security analysis, we show that the proposed scheme is secure against possible known attacks. In addition, we carry out the simulation of the proposed scheme using the most-widely accepted and used Automated Validation of Internet Security Protocols and Applications tool and the simulation results clearly indicate that our scheme is secure.

1 Introduction

The advances in network technologies make the remote intersection easier. It provides a scalable platform for numerous services over the public network such as e-learning, e-commerce, e-governance and e-medicine. Most of the services and applications are being provided over the public channels. The rapid development of the network and information technology have greatly improved the social production of the online services. The panoptic recurrence of the network applications fundamentally advances the improvement of multi-server architecture, in which the remote users have access to various distributed servers on the internet. The multi-server system consists of three participants, including the remote users, the servers and the registration center. The registration center (RC) acts as the trusted third party and it administrates all the registered servers and users. Service providing servers have complete control of the information services and the registered users are able to get these services. According to the number of participants in mutual authentication phase, there are two types of multi-server authentication protocols: one is implemented by two parties such as user and server, and the other is implemented by three parties such as user, registration center and server [27, 42].

The rapid development of the technology also given enough room for the information security problems. So, secure communication and data transfer between the participants has become essential requirement. In the process of providing secure communication many user authentication schemes based on identity have been proposed in the literature. To initiate the authentication process, at first the legitimacy of the user is verified by providing the login credentials.

In order to provide access to a user for any service, the service provider needs to verify the remote user’s identity before giving access to the opted services. So, the identity authentication is needed and it is handy during verifying the validity of the user. Providing security for various types of online applications and services is the foremost barrier, which can restrict the unauthorized users from approaching service provider at various application systems. In recent days, a numerous number of identity based authentication schemes using smart card have been presented [8, 11–15, 17, 20–25, 39, 42, 47].

Keeping in view of basic cryptographic algorithms, the authentication schemes based on smart cards can be partitioned into two classifications, such as the hash based and the public key based authentication schemes. As per utilization of the methodology, the identity authentication schemes can be secluded into two: the single-server environment which can be relevant in user authentication mechanisms and the multi-server environment which can be suitable in user confirmation schemes, where the multi-server approval determines the issue existing in single-server accepts that the user needs to recollect various distinctive identities and passwords when he/she utilizes the single-server validation scheme to login and get to diverse remote servers. Subsequently, in recent years, several smart card and identity based authentication schemes have been proposed [8, 11, 12, 17, 19, 23, 24, 39, 47, 49], and all of them have their own strengths and weaknesses. If the established password based authentication systems are employed in a multi-servers environment, a user does not just require to login to different remote servers. Additionally, for accessing various servers a remote user can avoid remembering various identities and passwords as it is not efficient and effectively arouses the compromise his/her personal identities and passwords. Note that one-time registration is an important problem in a multi-server environment as it significantly reduces the computational overhead and communication overhead caused by repeated registrations in order to access multiple servers.

In multi-server authentication schemes, the following criteria are considered to be important. Our proposed scheme has the ability to accomplish the following [3]:

• C1: Select and modify the password at will

  The user is free to select the password and modify their password whenever they wish in such a way that password can be memorized easily and remember by the user. This is essential in making the process flexible to the user and more user-friendly.

• C2: Single registration

  Earlier different remote servers offer various pairs of identities (IDs) and passwords (PWs) which confuses the user, while he/she registers at the remote system. On the other hand, memorizing all the identities and the corresponding passwords is not an easy task. In order to provide the best convenience, first the remote user needs to get register just only once at the registration center and thus, the legal user will be allowed to access the authorized servers.

• C3: Security

  The most important requirement in any authentication scheme is always considered to be secure. In real world, every authentication scheme should be able to restrict or prevent all kinds of attacks which are malicious.

• C4: Mutual authentication

  The authentication scheme should be able to provide mutual authentication and restrict any malicious attack.

• C5: Session key agreement

  Session key agreement is a very important in authentication schemes. The user and server should be able to handle and protect the session key for future secure communications.

• C6: Low computation

  Smart card has limited computational power. Thus, for more efficient and practical use, the user and the server should use lower computation load such that it can help in improving the efficiency.

Fig. 1

The proposed multi-server environment

1.1 Multi-server Environment

Figure 1 shows our proposed multi-server environment. The multi-server system consists of three participants: remote users, servers and the registration center. The registration center (the trusted third party) administrates all the registered servers and users. Service providing servers have complete control on the information services and the registered users are able to get these services. According to the number of participant in mutual authentication phase, there are two types of multi-server authentication protocols. One is implemented by two parties: user and server, and the other is implemented by three parties: user, registration center and server [27, 42] . In this multi-server environment, each user should perform the registration procedure to register. The registered users can enjoy the services of the servers by logging to the servers. If the traditional authentication schemes are applied to this environment, the remote user needs to register with each and every server, and remembers the login credentials. Memorizing the login credentials of various servers is very much inconvenient and troublesome to the users. So, to overcome such trouble and facilitate the user with better login mechanism, several multi-server authentication proposals have been developed and presented [8, 13, 17, 20, 23, 24, 38, 39, 42, 47]. Each registered user gets the smart card from the registration center using which he/she can perform the login and authentication procedure to enjoy the services from the registered servers.

1.2 One-Way Collision-Resistant Hash Function

A one-way hash function h: $\{0,1\}^* \rightarrow \{0,1\}^k$ is considered as cryptographically secure and deterministic algorithm [5, 27, 36, 37, 41], which prefers input as an arbitrary length binary string $l \in \{0,1\}^*$ and produces an output as a binary string $h(l) \in \{0,1\}^k$ of a fixed-length k. The one way hash function may take the input in the form of a file, a message, or other blocks of data and also posses the listed properties, which are as follows [40]:

• The hash function $h(\cdot )$ can be performed on a data block of all sizes.

• The message digest h(l) is easy to perform on any given input l.

• The output h(l) produced by the hash function $h(\cdot )$ is fixed in length.

• Pre-image resistant: For a given hash value p, it is hard to find any l such that $p=$ h(l).

• Second Pre-image resistant: For a given $l_1$, it is computationally infeasible to find any $l_2$ with $l_1 \ne l_2$ such that $h(l_1) =$ $h(l_2)$.

• Collision resistant: It is computationally infeasible to find any pair $(l_1, l_2)$ with $l_1 \ne l_2$ such that $h(l_1) =$ $h(l_2)$.

1.3 Threat Model

In this paper, we use the following threat model considering the assumptions as follows [9, 10, 16, 26, 48]:

• An adversary can extract the information from the smart card by examining the power consumption or leaked information.

• An adversary is able to eavesdrop all the communications between the parties involved such as a user and a server over a public channel.

• An adversary has the potential to modify, delete, redirect and resend the eavesdropped transmitted messages.

• An adversary can be a legal user or an outsider in any system.

1.4 Our Contributions

The contributions are listed below:

• We have analyzed the recently proposed Shunmuganathan et al.’s scheme and pointed out that their scheme suffers from several attacks such as stolen smart card attack, password guessing attack, impersonation attack, replay attack, forgery attack and forward secrecy attack.

• To overcome the security weaknesses of Shunmuganathan et al.’s scheme, we have proposed an efficient and more secure multi-server authentication scheme that can preserve all the original merits of Shunmuganathan et al.’s scheme and withstands the possible known attacks.

• To strengthen our proposed scheme, the security analysis using the BAN Logic has been presented. Using the informal security analysis, we have also shown our scheme can resist numerous security attacks which include the attacks found in Shunmuganathan et al.’s scheme.

• In addition, we have performed the simulation of the proposed scheme using the most-widely accepted and used Automated Validation of Internet Security Protocols and Applications (AVISPA) tool and the simulation results clearly indicate that our scheme is secure.

• Furthermore, our scheme is computationally efficient as compared to Shunmuganathan et al.’s scheme and other related existing schemes.

1.5 Notations

In Table 1, we have listed the notations which are used throughout the paper.

Table 1 Notations and their meanings

1.6 Organization of the Paper

The rest of this paper is arranged as follows. In Sect. 2, we present the related work in the literature. In Sect. 3, we present briefly Shunmuganathan et al.’s scheme. Subsequently, we demonstrate the weaknesses of Shunmuganathan et al.’s scheme in Sect. 4. In Sect. 5, we propose our scheme based on dynamic identity. To strengthen our proposed scheme, the security analysis using BAN Logic, and informal security analysis are provided in Sect. 6. We perform the simulation of the proposed scheme using the most-widely accepted and used AVISPA tool for the formal security verification in Sect. 7. In Sect. 8, the security and performance comparisons of our scheme with various relevant schemes are shown. Finally, Sect. 9 concludes the paper.

2 Related Work

Lamport [18] was the first one who proposed password authentication concept to address the security issues over insecure public channels. Nevertheless, Lamport’s scheme needs to store the user passwords. In 2000, based on the ElGamal’s public key cryptosystem, Hwang and Li [25] proposed a user authentication scheme using smart cards, where the server does not need any storage of the password tables for authentication. Since then numerous researchers have focused on design and improvement of authentication schemes using one-way hash function for the single-server architecture [47]. However, when the single server architectures are connected to multi-server environment, the user faces various troubles such as repetitive registration to login to different remote servers and also he/she additionally needs to recollect different identities and passwords.

In 2004, based on symmetric key cryptosystem and hash function, Juang [14] proposed a multi-server authentication scheme, in which the public parameters require large storage memory. However, Chang and Lee [3] figured out that Juang’s scheme is defenseless against dictionary attack as the secret values of the smart card can be extracted, and also demonstrated that Juang’s scheme is inefficient. To overcome these pitfalls, Chang and Lee additionally proposed their enhanced remote user authentication scheme. But, later it was shown that their scheme is insecure against insider attack. In 2004, utilizing the Lagrange interpolation polynomial and RSA cryptosystem, Tsaur et al. [44] proposed a multi-server authentication scheme. Unfortunately, Tsaur et al.’s scheme is inefficient. In 2008, based on random nonce and hash function, Tsai [43] presented a multi-server authentication scheme. Their scheme takes the creditability as their scheme is designed without any verification table. Therefore, it is very much suitable for the distributed network environment with least computation expenses.

Regardless, these all displayed authentication schemes for multi-server environments have given a chance to aggressor to trace the legitimate user as the ID used by the user is static to the remote server during the login for every interaction session. Liao and Wang [24] proposed a multi-server authentication scheme based on dynamic identity, where a user presents his/her identity during the login phase to access the services from a remote server, which changes dynamically for each session. They claimed that their scheme can oppose numerous assaults and can accomplish mutual authentication. However, Hsiang and Shih [12] demonstrated that Liao and Wang’s scheme is vulnerable to masquerade attack, insider attack, server and registration center spoofing attack. Further, they also proved that Liao and Wang’s scheme does not facilitate mutual authentication. To beat these security pitfalls, Hsiang and Shih [12] presented an enhancement of Liao and Wang’s authentication protocol for multi-server environment. Hsiang and Shih’s scheme is also insecure against stolen smart card attack, impersonation attack and replay attack. Additionally, the password change phase is erroneous in their scheme. To resolve the security pitfalls in Hsiang and Shih’s authentication scheme, Sood et al. [39] and Lee et al. [20] came up with authentication protocols using smart cards, which are based on dynamic identity for multi-server architecture.

Li et al. [23] encountered that Sood et al.’s scheme is helpless against leak-of-verifier attack, stolen smart card attack and impersonation attack. As a remedy, they proposed an efficient authentication protocol based on dynamic identity for multi-server architecture, which removes the aforementioned weaknesses of Sood et al.’s scheme [39]. Lee et al. [20] showed that Hsiang and Shih’s scheme is suspectable to server spoofing attack and masquerade attack. Further, they showed that Hsiang and Shih’s scheme does not provide mutual authentication. To avoid the security flaws of Hsiang and Shih’s scheme, in 2011, Lee et al. [20] demonstrated an authentication scheme based on dynamic ID. Although they claimed that their scheme can withstand various attacks, Li et al. [23] showed that Lee et al.’s scheme can not furnish correct authentication and is also insecure against server spoofing attack and forgery attack. To overcome the shortcomings of Lee et al.’s scheme, Li et al. also demonstrated an authentication scheme, which is a dynamic ID based for multi-sever environment using smart cards.

Shunmuganathan et al. [38] pointed out the security flaws in Li et al.’s scheme and showed their scheme is inefficient to off-line password guessing attack, forgery attack and stolen smart card attack. And they also showed that Li et al.’s scheme faces poor reparability. To surmount these security disadvantages, Shunmuganathan et al. [38] proposed a scheme using smart card for multi-server environment and claims their scheme is secure and efficient. In this paper, we show that Shunmuganathan et al.’s scheme is also defenseless in resisting the off-line password guessing attack, stolen smart card attack, user impersonation attack, forgery attack, forward secrecy and session key secrecy. Their scheme does not also preserve the two-factor security. In our proposed scheme, a user is free to choose his/her login credentials such as user id and password and regenerate the password any time. In the meantime, the proposed scheme provides more functionality and security features such as session key agreement, perfect forward secrecy and mutual authentication.

3 Review of Shunmuganathan et al.’s Scheme

In this section, for a detailed investigation we review Shunmuganathan et al.’s remote user authentication scheme for multi-server environment based on dynamic ID using smart cards. In Shunmuganathan et al.’s scheme, we have three participants: the user ($U_i$), the server ($S_j$), and the registration center (RC). The registration center (RC), selects x as the master secret key and y as a secret number to compute $h(x\Vert y)$ and h(y), and then shares them with $S_j$ over a secure channel. Their scheme consists of four phases: registration phase, login phase, verification phase, and password change phase. The detailed description of their scheme are described phase-wise below.

3.1 Registration Phase

The RC generates x as a master secret key and y as a secret number. The RC then computes h(y) and $h(x\Vert y)$, and securely share them with $S_j$ through a secure channel, when $S_j$ is registered with RC. In order to enjoy the services of $S_j$, a new $U_i$ must first register with the RC, where $S_j$ has already been registered. This registration is a one-time activity, which can then be used to access all the servers $S_j$. $U_i$ undergoes the registration procedure using the following steps:

• R1: $U_i$ creates an account in the multi-server system by freely choosing his/her identity $ID_i$, a random number b and password $PW_i$. Then, $U_i$ computes $A_i = h(b\Vert PW_i)$ to hide the password $PW_i$. $U_i$ sends $ID_i$ and $A_i$ to the RC via a secure channel for registration.

• R2: After receiving $ID_i$ and $A_i$ from the user $U_i$ securely, the RC computes $B_i = h(ID_i\Vert x)$, $C_i = h(ID_i\Vert h(y)\Vert A_i)$, $D_i = h(B_i\Vert h(x\Vert y))\oplus A_i$ and $E_i = B_i\oplus h(x\Vert y)$.

• R3: The RC issues a smart card containing the information $\{C_i, D_i, E_i, h(y), h(\cdot )\}$. The RC hands over the smart card to $U_i$ through a secure channel.

• R4: $U_i$ keys b into his/her smart card. Finally, the smart card contains the information $\{C_i, D_i, E_i, b, h(y), h(\cdot )\}$.

3.2 Login Phase

The smart card received from the RC through the registration phase is used to access $S_j$ by a user $U_i$. Whenever $U_i$ wants to login to $S_j$, $U_i$ must generate a login request message using the following steps:

• L1: $U_i$ first places his/her smart card into the smart card reader and keys in $ID_i$ and $PW_i$. The smart card computes $A_i = h(b\Vert PW_i)$ and $C_i^* = h(ID_i\Vert h(y)\Vert A_i)$ using the input values and the data into its memory. Then, it checks if the computed $C_i^*$ is equal to $C_i$, which is stored in smart card. The equality lets the smart card validate the user $U_i$ and proceed with the next step. Otherwise, the smart card aborts the session.

• L2: The user’s smart card generates two random nonces $N_i$ and $N_k$, and computes $P_{ij}=E_i \oplus h(h(SID_j\Vert h(y))\Vert N_i)$, $F_i =D_i \oplus A_i$, $A1_i =h(A_i\Vert N_k)$, $CID_i =A1_i\oplus h(F_i \Vert SID_j\Vert N_i)$, $M_1=h(P_{ij}\Vert CID_i\Vert F_i\Vert N_i)$.

• L3: Finally, $U_i$’s smart card sends $\{P_{ij}, CID_i, M_1, N_i \}$ as a login request message to $S_j$ through a public channel.

3.3 Verification Phase

Once $S_j$ receives the login request message $\{P_{ij}, CID_i, M_1, N_i \}$ from $U_i$, it performs the following steps to validate the legitimacy of the user $U_i$ and complete mutual authentication:

• V1: $S_j$ computes the following using the login request message $\{P_{ij}, CID_i, M_1, N_i \}$ received from $U_i$, and $h(SID_j\Vert h(y))$ and $h(x\Vert y)$, which are known to $S_j$:

  $E_i = P_{ij}\oplus h(h(SID_j\Vert h(y))\Vert N_i)$, $B_i = E_i\oplus h(x\Vert y)$, $F_i = h(B_i\Vert h(x\Vert y))$, $A1_i = CID_i\oplus h(F_i \Vert SID_j\Vert N_i)$.

• V2: $S_j$ computes $h(P_{ij}\Vert CID_i\Vert F_i\Vert N_i)$ and checks whether this value is equal to $M_1$. If they are not equal, the request is not valid. $S_j$ then declines the login request and terminates this session. Otherwise, it is a valid login request and $S_j$ accepts the login request message and generates a nonce $N_j$, and computes $M_2 = h(F_i \Vert A1_i\Vert N_j\Vert SID_j)$, $M_3 = A1_i \oplus N_i \oplus N_j$. $S_j$ sends the message $\{M_2, M_3\}$ to $U_i$ through a public channel for mutual authentication.

• V3: $U_i$ extracts $N_j$ from the received message $\{M_2, M_3\}$ as $N_j = A1_i\oplus N_i \oplus M_3$ and computes $h(F_i \Vert A1_i\Vert N_j\Vert SID_j)$ to check the equality with the received message $M_2$. If the condition is not satisfied, $U_i$ declines further process and terminates the session. Otherwise, $U_i$ successfully authenticates $S_j$, and computes the mutual authentication message $M_4 = h(F_i \Vert A1_i\Vert N_i\Vert SID_j)$ and sends $\{M_4\}$ to the server $S_j$ through a public channel.

• V4: Upon receiving the message $\{M_4\}$ from $U_i$, $S_j$ computes $h(F_i \Vert A1_i\Vert N_i\Vert SID_j)$ and compares it with $M_4$. If the verification does not hold, $S_j$ terminates the session. Otherwise, $S_j$ is successful in authenticating $U_i$ and thereby, the mutual authentication process is completed. Once the mutual authentication succeeds, $U_i$ and $S_j$ compute the session key for their future secure communication as $SK = h(F_i \Vert A1_i\Vert N_i\Vert N_j\Vert SID_j)$.

The login and verification phases of Shunmuganathan et al.’s scheme is summarized in Table 2.

Table 2 Login and verification phases of Shunmuganathan et al.’s scheme

3.4 Password Change Phase

$U_i$ invokes this phase to change/modify the password $PW_i$ to a new password $PW_i^{new}$. This phase does not require any secure channel or any interaction with the RC. The steps involved in this phase are as follows.

• P1: $U_i$ places the smart card into the smart card reader and keys in $ID_i$ and $PW_i$.

• P2: The smart card computes $A_i = h(b\Vert PW_i)$ and $C_i^* = h(ID_i\Vert h(y)\Vert A_i)$. It then checks whether the computed $C_i^*$ is equal to $C_i$. If the verification does not hold, the smart card declines the password change request. Otherwise, $U_i$ is allowed to input a new password $PW_i^{new}$ and a new random number $b^{new}$.

• P3: The smart card computes $A_i^{new} =$ $h(b^{new}\Vert$ $PW_i^{new})$, $C_i^{new} =$ $h(ID_i\Vert$ $h(y)\Vert$ $A_1^{new})$ and $D_i^{new}=$ $D_i\oplus$ $A_i \oplus$ $A_i^{new}$.

• P4: Finally, the smart card replaces $C_i$ with $C_i^{new}$ and $D_i$ with $D_i^{new}$ to complete the password change phase.

4 Cryptanalysis on Shunmuganathan et al.’s Scheme

In this section, we analyze the security of the recently proposed Shunmuganathan et al.’s scheme and show that their scheme is vulnerable to the following attacks.

4.1 Password Guessing Attack

We assume that the user $U_i$’s smart card is lost or stolen. An attacker can then extract the information $\{C_i, D_i, b, E_i, h(y), h(\cdot )\}$, which are stored in the smart card according to the threat model provided in Sect. 1.3. In this attack, an attacker tries to guess the password $PW_i$ by computing $A_i^*= h(b\Vert PW_i')$, $F_i^* = A_i^* \oplus D_i$, $M_1^*=h(P_{ij}\Vert CID_i\Vert F_i^*\Vert N_i)$, and then checking $M_1^* \overset{?}{=}M_1$. If the verification is successful, the attacker guesses the correct password. Otherwise, the attacker repeats this process until he/she obtains the correct password. This shows that Shunmuganathan et al.’s scheme is insecure against the password guessing attack.

4.2 User Impersonation Attack

If $F_i$ is known, the user impersonation attack is possible in Shunmuganathan et al.’s scheme. This is achieved while the password guessing attack is successful. The attacker computes $F_i^* = A_i^* \oplus D_i$, and $M_1^*=h(P_{ij}\Vert CID_i^*\Vert F_i^*\Vert N_i)$ and then transmits the message $\{P_{ij}, CID_i^*, M_1^*, N_i \}$ to $S_j$. $S_j$ verifies $M_1^*$ by computing $E_i = P_{ij} \oplus h(h(SID_j\Vert h(y))\Vert N_i)$, $B_i = E_i\oplus h(x\Vert y)$, $F_i = h(B_i\Vert h(x\Vert y))$, $A1_i = CID_i^*\oplus h(F_i \Vert SID_j\Vert N_i)$, and then checking the condition $h(P_{ij}\Vert CID_i^*\Vert F_i\Vert N_i)\overset{?}{=}M_1^*$. This verification gets successful. Hence, the attacker can successfully impersonate the user.

4.3 Stolen Smartcard Attack

An adversary can successfully login into the system with the extracted information $\{C_i, D_i, E_i, b, h(y), h()\}$ from the smart card and guessing a correct password $PW_i^*$ as explained in Sect. 4.1. Furthermore, in Sect. 4.2, we have shown using the stolen smart card, an adversary can easily impersonate a legitimate user $U_i$ even without knowing the valid $ID_i$, and secret keys x and y. Thus, Shunmuganathan et al.’s scheme is insecure against the stolen smart card attack.

4.4 No Two-Factor Security

Shunmuganathan et al.’s scheme scheme completely violates the two-factor security due to the following reason. First, our analysis under the off-line password guessing attack proves that their scheme does not provide two-factor authentication. Next, our analysis under stolen smart card attack shows that once the data in the smart card are extracted, a valid login message can be created even without knowing $ID_i$ of the user $U_i$. An adversary can also login any number of times without being detected by $S_j$. $S_j$ cannot prevent the further misuse of the smart card as it has no provision to securely revoke the stolen smart card.

4.5 Forgery Attack

The discussed stolen smart card attack (Sect. 4.3) proves that an adversary can forge as a legal user to login to the remote server $S_j$. The adversary can forge a valid login request $\{P_{ij}, CID_i^*, M_1^*, N_i \}$ using the data stored in the stolen smart card to fool $S_j$. The adversary can also manipulate the login request just with the data stored in the smart card without even knowing $ID_i$ as explained in the stolen smart card and user impersonation attacks. This is clear that Shunmuganathan et al.’s scheme cannot withstand the forgery attack.

4.6 Good Repairability

A good login and authentication mechanism should be able to revoke lost or stolen smart card with good repairability. The registration center RC should be able to revoke the smart card, if at all it is lost or stolen. Although, Shunmuganathan et al. claims that their scheme provides good repairability, we have shown that their scheme is insecure against stolen smart card and password guessing attack (Sects. 4.1 and 4.3). Therefore, Shunmuganathan et al.’s scheme does not provide good repairability.

4.7 Replay Attack

In this type of attack, an adversary tries to eavesdrop a valid login message $\{P_{ij}, CID_i^*, M_1^*, N_i \}$ between $U_i$ and $S_j$. Then the adversary replays it back to $S_j$ and tries to gain access to the service provided by $S_j$. After receiving a mutual authentication challenge response message $\{ M_2, M_3 \}$ from $S_j$, the adversary tries to generate a response message $\{ M_4 \}$ by extracting $N_j$ from $M_3$. As we have already shown that the adversary can successfully compute $M_4$ and get $F_i, A1_i, N_i$. Therefore, the adversary can successfully generate $M_4$ and send it to $S_j$. Hence, Shunmuganathan et al.’s scheme cannot resist replay attack.

4.8 Forward Secrecy

From the above discussions in Sects. 4.5 and 4.7, an adversary can compute $F_i, A1_i,$ and $N_i$. Also, from the transmitted message $\{M_2, M_3\}$ from $S_j$, the adversary can compute $N_j = A1_i\oplus N_i\oplus M3$. In order to compute a session key $SK = h(F_i\Vert A1_i\Vert N_i\Vert N_j\Vert SID_j)$, the adversary has all the required credentials. Hence, the adversary can easily compute the session key. As a result, Shunmuganathan et al.’s scheme does not preserve forward secrecy property.

5 Our Proposed Scheme

In this section, we present our proposed scheme, which has three participants, such as the registration center RC, the user $U_i$, and the server $S_j$. Our scheme possesses four phases, namely registration, login, authentication and key agreement, and password change phase. We use the notations listed in Table 1 for describing our scheme.

5.1 Registration Phase

The registration of $U_i$ with the RC is a one-time activity. This phase consists of the following steps:

• R1: $U_i$ freely chooses his/her identity $ID_i$, password $PW_i$, and generates a random number b to compute $A_i =$ $h(ID_i\oplus b\oplus PW_i)$. $U_i$ then transmits $ID_i$ and $A_i$ to the RC for the registration purpose via a secure channel.

• R2: The RC computes $B_i =$ $h(A_i\Vert x)$, $C_i =$ $h(ID_i\Vert h(y)\Vert A_i)$, $D_i =$ $h(B_i\Vert h(x\Vert y))$, and $E_i =$ $B_i\oplus h(x\Vert y)$. The RC stores $\{C_i, D_i, E_i, h(y), h(\cdot )\}$ on the user $U_i$’s smart card and sends it to $U_i$ via a secure channel.

• R3: After receiving the smart card from the RC, $U_i$ computes $L_i =$ $b \oplus h(ID_i\Vert PW_i)$ and keys $L_i$ into the smart card. Finally, the smart card contains the information $\{C_i, D_i, E_i, L_i, h(y), h(\cdot )\}$. Note that in our scheme, the random secret number b is not stored directly as compared to Shunmuganathan et al.’s scheme and instead of storing b the smart card stores $L_i$. This helps to prevent the privileged-insider attack in our scheme.

The user registration phase of our scheme is summarized in Table 3.

Table 3 User registration phase of our scheme

5.2 Login Phase

This phase helps $U_i$ to send a login request message to $S_j$ with the following steps:

• L1: $U_i$ places the smart card into the smart card reader, and inputs $ID_i$ and $PW_i$.

• L2: The smart card performs computations $b =$ $L_i \oplus h(ID_i\Vert PW_i)$, $A_i =$ $h(ID_i\oplus b \oplus PW_i)$ and $C_i^* =$ $h(ID_i\Vert h(y)\Vert A_i)$ and then checks if the computed $C_i^*$ is equal to $C_i$, which is available in the smart card. If there is a match, the smart card proceeds with the next step. Otherwise, the smart card aborts the session.

• L3: The smart card generates a nonce $N_i$. The smart card then computes $CID_i =$ $A_i\oplus h(D_i \Vert SID_j\Vert N_i)$, $P_{ij} =$ $E_i \oplus h(h(SID_j\Vert h(y))\Vert N_i)$, $M_1 =$ $h(P_{ij}\Vert CID_i\Vert A_i\Vert N_i)$, and $M_2 =$ $h(SID_j\Vert h(y))\oplus N_i$.

• L4: $U_i$ finally sends the login request message $\{ CID_i, P_{ij}, M_1 , M_2\}$ to $S_j$ via a public channel.

5.3 Authentication and Key Agreement Phase

In this phase, $S_j$ and $U_i$ execute the following steps to verify the login request and complete challenge response message for mutual authentication. At the end of this phase, both $U_i$ and $S_j$ agree on a secret session key $SKey_{ij}$ for their future secure communication.

• V1: $S_j$ computes $N_i =$ $h(SID_j\Vert h(y))\oplus M_2$, $E_i=$ $P_{ij}\oplus h(h(SID_j\Vert h(y))\Vert N_i)$, $B_i =$ $E_i\oplus h(x\Vert y)$, $D_i =$ $h(B_i\Vert h(x\Vert y))$, $A_i =$ $CID_i\oplus h(D_i \Vert SID_j\Vert N_i)$ using the transmitted message credentials {$P_{ij}$, $CID_i$, $M_1$, $M_2$} and known credentials $h(x\Vert y), h(y)$.

• V2: $S_j$ computes $h(P_{ij}\Vert CID_i\Vert A_i\Vert N_i)$ and checks whether it matches with $M_1$. If it does not hold, $S_j$ declines the login request and terminates the session. Otherwise, $S_j$ accepts the login request message and generates a nonce $N_j$. $S_j$ then computes $SK_{ij} =$ $h(h(B_i\Vert h(x\Vert y))\Vert A_i)$, $M_3 =$ $h(SK_{ij}\Vert A_i\Vert SID_j\Vert N_j)$ and $M_4 =$ $SK_{ij} \oplus N_j$. $S_j$ sends the message $\{M_3, M_4\}$ to $U_i$ via a public channel.

• V3: Upon receiving the message $\{M_3, M_4\}$ from $S_j$, $U_i$ computes $SK_{ij} =$ $h(D_i\Vert A_i)$, extracts $N_j$ by computing $N_j =$ $SK_{ij} \oplus M_4$, and checks whether $h(SK_{ij} \Vert A_i\Vert SID_j\Vert N_j)$ is equal to $M_3$. If they are equal, $U_i$ successfully authenticates $S_j$. $U_i$ further computes $M_5 =$ $h(SK_{ij} \Vert A_i\Vert SID_j\Vert N_i\Vert N_j)$ and sends the message $\{M_5\}$ to $S_j$ via a public channel. Otherwise, the session is terminated.

• V4: $S_j$ computes $h(SK_{ij} \Vert A_i\Vert SID_j\Vert N_i\Vert N_j)$ and compares it with the received $M_5$. If they are equal, $S_j$ successfully authenticates $U_i$ and the mutual authentication is complete. Otherwise, the session is terminated. Then, both $U_i$ and $S_j$ compute a common session key $SKey_{ij} =$ $h(SK_{ij} \Vert A_i\Vert SID_j\Vert N_i\Vert D_i\Vert N_j)$ for their secure future communication.

The login, and authentication and key agreement phases of our scheme are summarized in Table 4.

Table 4 Login, and authentication and key agreement phases of our scheme

5.4 Password Change Phase

To change the old password $PW_i$ to a new password $PW_i^{new}$, a user $U_i$ needs to invoke this phase. There is no need to communicate with the RC further for the password change. This phase has the following steps:

• P1: $U_i$ places his/her smart card into the smart card reader, and then inputs $ID_i$ and $PW_i$.

• P2: The smart card computes $b^* =$ $L_i \oplus h(ID_i\Vert PW_i)$, $A_i^* =$ $h(ID_i\oplus b^* \oplus PW_i)$ and $C_i^* =$ $h(ID_i\Vert h(y)\Vert A_i^*)$. The smart card then checks if the computed $C_i^*$ is equal to $C_i$. If the equality does not hold, the smart card declines the request for password change. Otherwise, $U_i$ keys in a new password $PW_i^{new}$.

• P3: The smart card computes $A_i^{new} =$ $h(ID_i\oplus b^* \oplus PW_i^{new})$ and $C_i^{new}=h(ID_i\Vert A_i^{new}\Vert h(y))$, and then replaces $C_i$ with $C_i^{new}$ .

• P4: Finally, the smart card computes $L_i^{new} =$ $b^* \oplus h(ID_i\Vert PW_i^{new})$ and replaces $L_i$ with $L_i^{new}$.

6 Security Analysis of the Proposed Scheme

In this section, we show that the proposed scheme provides secure mutual authentication between a user $U_i$ and a server $S_j$ through the formal protocol analysis using the well-known widely-accepted BAN logic [2]. In addition, we simulate the proposed scheme for the formal security verification using the widely-accepted Automated Validation of Internet Security Protocols and Applications (AVISPA) tool [1] in Sect. 7 to show that it is secure against the replay and man-in-the-middle attacks. Wang et al. [46] pointed out that anyone of the formal security analysis, informal security analysis and AVISPA simulation analysis can not capture all the attacks. Hence, it is necessary for the proposed scheme to show that it is secure against possible known attacks using all possible security analysis. For this purpose, we also perform the informal security analysis to show that our scheme is also secure against other possible known attacks.

6.1 Authentication Proof Based on BAN Logic

The BAN logic [2] is widely being used to verify the correctness of the authentication protocol with key agreement. The protocol correctness refers to the communication parties $U_i$ and $S_j$, who share a fresh shared session key with each other after the protocol is executed. We first provide some notations of the BAN logic as follows:

• The principal P believes the announcement X.

• $P \triangleleft X$: P considers X, which means that a message containing X is received by P where X can be read by P.

• P sometime stated X, which means that as P once stated it in sometime.

• P commands X, P has complete authority on X, and P considers X as trusted (Jurisdiction over X).

• $\sharp (X)$: The message X is fresh, which means that no any entity sent a message containing X at whenever ahead of current round.

• P and Q use SK (shared key) to communicate with each other.

• $P \overset{SK}{\longleftrightarrow } Q:$ P and Q use SK as a shared secret between them.

• $\{X\}_k$: The formula X is encrypted under the key k.

• $<X>_Y$:  The formula X is combined with the formula Y.

• $(X)_k$:  The formula X is hashed with the key k.

In order to describe logical postulates of BAN logic in formal terms[2], we present the following rules:

Rule (1). Message meaning rule: For shared secret keys:

(1)

P is said to believe Q, if P believes that k is shared with Q and P sees X encrypted under k.

Rule (2). Nonce verification rule:

(2)

If P believes that X is expressed recently (freshness) and P believes that Q once said X, P believes that Q believes X.

Rule (3). Jurisdiction rule:

(3)

If P believes that Q has jurisdiction over X, and P believes that Q believes a message X, P believes X.

Rule (4). Freshness rule:

(4)

If one part known to be fresh, the entire formula must be fresh.

Rule (5). Belief rule:

(5)

If P believes Q believes the message set (X, Y), P also believes Q believes the message X.

According to the analytic procedures of the BAN logic, our proposed protocol should satisfy the following goals:

Goal 1.

Goal 2.

Goal 3.

Goal 4.

Prior to the formal analysis, we first idealize the communicated messages of our proposed protocol to alleviate the analysis between $U_i$ and $S_j$, which are as follows:

Message 1: $U_i \rightarrow S_j :$ $\langle P_{iJ}, CID_i,$ $E_i, U_i\overset{{ h(SID_j\Vert h(y)) }}{\longleftrightarrow }$ $S_j, D_i,$ $N_i,$ $M_1,$ $M_2 \rangle _{U_i\overset{{\ A_i \ }}{\longleftrightarrow }S_j}$.

Message 2: $S_j \rightarrow U_i: <SID_j, N_j, U_i\overset{{\ A_i \ }}{\longleftrightarrow }S_j >_{U_i\overset{{\ SK_{ij}\ }}{\longleftrightarrow }S_j}$.

Message 3: $U_i \rightarrow S_J: <SID_j, U_i\overset{{\ A_i \ }}{\longleftrightarrow }S_j, N_i, N_j>_{U_i\overset{\ {SK_{ij}\ }}{\longleftrightarrow }S_j}$.

Based on our proposed protocol, we make some initial state assumptions, which are listed as follows:

$A_1$:

$A_2$:

$A_3$:

$A_4$:

$A_5$:

$A_6$:

$A_1$ and $A_2$ believe that both $U_i$ and $S_j$ generate the fresh random numbers $N_i$ and $N_j$ respectively. Therefore, they assure their freshness, respectively. $A_3$ and $A_4$ are valid because the shared secret key $A_i$ can be computed by both user $U_i$, and server $S_j$ from the credentials issued by the RC as the master secret key. The assumption $A_5$ $(A_6)$ holds because once $U_i$ $(S_j)$ shared the same shared session key $SKey_{ij}$.

Further, we demonstrate our proposed protocol based on the rules of the BAN logic that our protocol can achieve the intended goals using the initial assumptions, and the inside information descriptions are as follows:

According to the message 1, we could obtain:

Step 1: $S_j \triangleleft ( CID_i, P_{ij}, U_i\overset{{h(SID_j\Vert h(y))}}{\longleftrightarrow }S_j, E_i, D_i, N_i,M_1, M_2)_{U_i\overset{{A_i}}{\longleftrightarrow }S_j}$.

From Step 1 and assumption $A_3$, we apply the message meaning rule to get:

Step 2:

From Step 2 and assumption $A_1$, we apply the freshness conjuncatenation rule to get:

Step 3:

According to Steps 2 and 3, we apply the nonce-verification rule to obtain:

Step 4:

According to Step 4, we apply the belief rule to obtain:

Step 5:

According to Step 5 and $A_4$, we apply the jurisdiction rule to get:

Step 6:

According to message 2, we obtain:

Step 7: $U_i \triangleleft (N_j, U_i\overset{{A_i}}{\longleftrightarrow }S_j, SID_j)_{U_i\overset{{SK_{ij}}}{\longleftrightarrow }S_j}$.

According to Step 7, we apply seeing rule and get:

Step 8: $U_i \triangleleft (M_3, M_4)$, where $M_4 = SK_{ij} \oplus N_j$ and $M_3= h(SK_{ij}\Vert A_i\Vert SIDj\Vert N_j)$.

According to Step 8 and $A_5$, we apply the message meaning rule to get:

Step 9:

From Step 9 and assumption $A_2$, we apply the freshness conjuncatenation rule to get:

Step 10:

According to Steps 9 and 10, we apply the nonce verification rule to obtain:

Step 11:

According to Step 11, we apply the belief rule to get:

Step 12: (Goal 2)

According to $A_5$ and the Step 12, we apply the jurisdiction rule to obtain:

Step 13: (Goal 1)

According to message 3, we can obtain

Step 14: $S_j \triangleleft ( N_i, U_i\overset{{A_i}}{\longleftrightarrow }S_j, N_j, SID_j)_{U_i\overset{{SK_{ij}}}{\longleftrightarrow }S_j}$.

According to Step 14 and assumption $A_3$, we apply the message meaning rule to get:

Step 15:

According to Step 15 and assumption $A_2$, we apply the freshness conjuncatenation rule to get:

Step 16:

According to Step 16, we apply the belief rule to get:

Step 17: (Goal 4)

According to assumption $A_4$ and Step 17, we apply the jurisdiction rule to get:

Step 18: (Goal 3)

According to Steps 12, 13, 17, and 18, it is clear that our protocol successfully achieves all the goals (Goals 1-4). Both user $U_i$ and server $S_j$ believe that they share a secure session key $h(SK_{ij}\Vert SID_j\Vert A_i\Vert N_i\Vert N_j\Vert D_i)$ with each other.

6.2 Discussion and Informal Security Analysis

In this section, we show that our scheme has the ability to support the important functionality properties and also to defend various known attacks.

6.2.1 Efficient Password Verification Mechanism

In our proposed scheme, during the login phase, the smart card can verify whether the user $U_i$ inputs a correct password by checking if $C_i^*$ is equal to $C_i$. If the user $U_i$ inputs a wrong password $PW_i' (\ne PW_i)$, the smart card computes $b =$ $L_i \oplus h(ID_i\Vert PW_i)$, $A_i=$ $h(ID_i\oplus b\oplus PW_i')$ and $C_i^*=$ $h(ID_i\Vert h(y)\Vert A_i)$ and gets $C_i^* \ne C_i$. Thus, the session is rejected by the smart card. Therefore, the proposed scheme is efficient in the wrong password detection and improves the user friendliness.

6.2.2 User Anonymity

In our scheme, the anonymity of the user $U_i$ is preserved by transmitting a session variant ID. The login request message $\{ CID_i, P_{ij}, M_1 , M_2 \}$ sent to the server $S_j$, which does not contain ID in plain text. Each parameter in the login message is associated with nonce and secured through one-way hashing that provides dynamic to the message. This dynamic property helps in providing user anonymity.

6.2.3 Stolen Smartcard Attack

We assume that the user $U_i$’s smart card has been lost or stolen. The attacker can extract the stored data $\{C_i, D_i, E_i, L_i, h(y), h(\cdot )\}$ from the smart card. Though the attacker can extract the stored information on the smart card, he/she cannot make use of the information. In order to login to the system, the attacker needs to know $ID_i$ and $PW_i$ correctly, which are not possible to guess both $ID_i$ and password $PW_i$ exactly at the same time as they are protected using a one-way cryptographic hash function. In addition, the master secret key x is unknown to the attacker. Therefore, the proposed scheme can resist stolen smart card attack.

6.2.4 Password Guessing Attack

In the login and authentication phases, the user $U_i$ inputs $ID_i$ and $PW_i$ into the smart card. The computed values of b, $A_i$ and $C_i^*$ are securely protected using the one-way hash function and as discussed above the attacker needs to know $ID_i$ and $PW_i$ correctly, which are not possible. Therefore, our proposed scheme withstands password guessing attack.

6.2.5 Replay and Man-in-the-Middle Attacks

In our scheme, two random nonces $N_i$ and $N_j$ are generated by the user $U_i$ and the server $S_j$, respectively, which make all messages dynamic and valid for that session only. An attacker can access the service by eavesdropping the previous login request $\{CID_i, P_{ij}, M_1 , M_2 \}$ from the user $U_i$, and may replay the same message to $S_j$. From the server $S_j$, the attacker gets an acknowledge message $\{M3, M4\}$. Despite of extracting all the transmitted messages, the attacker is not successful in computing the message $\{M_5\}$ to respond to the server $S_j$ without knowing $D_i, A_i$ and $N_i$. Similarly, if the attacker replies a previous message $\{M_3, M_4\}$ to $U_i$, due to the difference of the two random numbers $N_i$ of these two different sessions, the previous computed random number $N_j$ will not be equal to the random number $N_j$ of this session that was chosen by $S_j$. Moreover, the computation of $h(D_i\Vert A_i\Vert N_j\Vert SID_j)$ will not be equal to $M_3$ due to which the authentication will fail. Therefore, our proposed scheme can resist replay and man-in-the-middle attack attack.

6.2.6 Forgery Attack

To forge as a legal user to login to the remote server $S_j$, an attacker must be able to eavesdrop a valid login request $\{CID_i, P_{ij}, M_1, M_2 \}$ to fool $S_j$. However, the adversary cannot compute a valid login request message without knowing $E_i,$ $D_i,$ $A_i$ and $N_i$. In addition, if the adversary is a legal user of the system, he/she also cannot masquerade as another legal user to login to the remote server $S_j$ as he/she cannot compute $D_i$ and $A_i$ from his/her smart card and the intercepted login request $\{ CID_i, P_{ij}, M_1, M_2 \}$ without knowing x,  $h(x\Vert y),$ b and $PW_i$. Beside, if the adversary gets $U_i$’s smart card and extracts the parameters $\{C_i, D_i,$ $E_i, L_i,$ $h(y), h(\cdot )\}$ stored in the smart card, he/she cannot also forge a login request to fool $S_j$, because he/she cannot use these parameters to compute the correct value of $A_i$ without knowing the password $PW_i$. Therefore, our proposed scheme can withstand forgery attack.

6.2.7 Server and Registration Center Spoofing Attacks

An attacker being either legal but malicious user or legal but malicious server may try to perform the server spoofing attack and registration center spoofing attack in our proposed scheme. On the server spoofing attack, if the attacker is a legal user of the system, he/she must be able to forge a valid response message $\{M_3, M_4\}$ to $U_i$. However, the attacker cannot compute $D_i$ and $A_i$ from his/her smart card and the intercepted login request $\{CID_i, P_{ij}, M_1, M_2 \}$ without the knowledge of $h(x\Vert y)$. Therefore, the attacker cannot compute the valid $M_3$ and $M_4$. Even if the attacker is a legal server of the system, he/she cannot also masquerade as another server to fool any legal user since he/she does not have the other server’s secret information $h(SID_j\Vert h(y))$ to check the login request and cannot compute the valid response message $\{M_3, M_4\}$. Therefore, our proposed scheme can withstand the server spoofing attack.

On the registration center spoofing attack, the legal user and the legal server cannot get the master secret key x and secret number y, which are held by the registration center (RC) only. Therefore, any attacker cannot masquerade as the registration center, and our scheme can withstand this type of attack.

6.2.8 Known-Key Secrecy

Known-key secrecy means that compromise of one session key should not compromise other session keys. In our scheme, the session key $SKey_{ij} =$ $h(SK_{ij}\Vert A_i\Vert SID_j\Vert N_i\Vert D_i\Vert N_j)$ between a user $U_i$ and a server $S_j$ is associated with $D_i,$ $A_i,$ $N_i,$ $N_j$ and $SK_{ij}$. If an attacker knows a past session key $SKey_{ij}$, he/she cannot obtain $SK_{ij}$, $D_i$ and $A_i$ from the session key since they are protected by the one-way hash function $h(\cdot )$. As a result, the attacker cannot get the other session keys. Thus, our scheme provides the known-key secrecy property.

6.2.9 Forward Secrecy

Forward secrecy means that if the master secret key x of the system is compromised, the secrecy of previously established session keys should not be affected. If the master secret key x is compromised for some reason, the attacker cannot compute any previous session key $SKey_{ij}$ between a user $U_i$ and a server $S_j$ without knowing $PW_i,$ b,  $ID_i$ and y. Therefore, the proposed scheme can ensure forward secrecy property.

6.2.10 Denial-of-Service Attack

In our proposed scheme, $U_i$ sends the login message $\{CID_i,$ $P_{ij},$ $M_1,$ $M_2\}$ to the opted server $S_j$ to get the services. Upon receiving the login message, $S_j$ performs some computations and also verifies the legitimacy of $U_i$. Here, in our proposed scheme, $S_j$ performs the computations as shown in Step V1 and verifies the login request as shown in Step V2 in Sect. 5.3. If the verification fails, $S_j$ terminates the session. But, once the legitimacy of the user is verified, $S_j$ agrees to provide the necessary services to $U_i$. Therefore, our proposed scheme is secure against this attack.

6.2.11 Good Repairability

A good login and authentication mechanism should be able to revoke lost or stolen smart card with good repairability. The registration center RC should be able to revoke the smart card, if at all it is lost or stolen. In our scheme, if a legitimate user $U_i$’s smart card is lost or stolen, he/she has to request the RC to issue the new smart card with the same user identity $ID_i$ for his/her future communications. In order to launch the login request with the help of stolen smart card, $U_i$ needs to have valid login credentials $ID_i$ and $PW_i$. We have already shown that our scheme preserves user anonymity, resists stolen smart card attack and off-line password guessing attack. Therefore, it is not possible to get valid $ID_i$ and $PW_i$. Hence, our scheme provides good repairability property.

6.2.12 Proper Mutual Authentication

The proposed scheme provides proper mutual authentication due to the following reason. The user $U_i$ sends the message $\{CID_i, P_{ij}, M_1, M_2 \}$ to the server $S_j$ to access the service. After receiving the message, $S_j$ computes $N_i,$ $E_i,$ $B_i,$ $D_i,$ $A_i$ and then checks if $h(P_{ij} \Vert CID_i \Vert A_i \Vert N_i) = M_1$. If it holds, $U_i$ is a valid user and the login request is accepted by the server $S_j$. Otherwise, $S_j$ rejects the login request. Since the authentication equation relies on the one-way hash function, any fabricated message $\{CID_i', P_{ij}', M_1', M_2' \}$ cannot pass the verification. Then, $S_j$ computes the message $\{M_3, M_4\}$ and sends it to $U_i$. $U_i$ computes $SK_{ij} =$ $h(D_i\Vert A_i)$ and $N_j$, and checks whether $h(SK_{ij} \Vert A_i\Vert SID_j\Vert N_j)$ is equal to $M_3$. If they are not equal, $U_i$ terminates the scheme. Otherwise, $S_j$ is authenticated by $U_i$. Since it protected by a one-way hash function, any fabricated message $\{M_3', M_4'\}$ cannot pass the authentication. With the same reason, any fabricated mutual authentication message $\{M_5'\}$ cannot pass the mutual authentication. Therefore, our proposed scheme provides proper mutual authentication.

Fig. 2

Role specification in HLPSL for a user $U_i$

Fig. 3

Role specification in HLPSL for the RC

7 Simulation for Formal Security Verification using AVISPA Tool

In this section, we simulate our scheme for the formal security verification using the widely-accepted AVISPA (Automated Validation of Internet Security Protocols and Applications) tool.

AVISPA is a modular and expressive formal language for specifying protocols and their security properties. It integrates different back-ends that implement a variety of state-of-the-art automatic analysis techniques [1]. It is a push-button tool for the automated validation of Internet security-sensitive protocols and applications, which becomes a widely-accepted tool for our formal security verification in recent years, [4, 6, 7, 28–35]. AVISPA contains four back-ends: On-the-fly Model-Checker (OFMC), Constraint Logic based Attack Searcher (CL-AtSe), SAT-based Model-Checker (SATMC) and Tree Automata based on Automatic Approximations for the Analysis of Security Protocols (TA4SP). The detailed descriptions of these back-ends are available in [1].

The protocols to be analyzed under the AVISPA tool need to be specified in the HLPSL (High Level Protocols Specification Language), which is a role-oriented language [1]. HLPSL is based on roles: the basic roles represent each participant role, and composition roles represent the scenarios of basic roles. Each role is independent from the others, which gets some initial information by parameters, and then communicates with the other roles by channels. In HLPSL, an intruder is always denoted by i, which is always modeled using the Dolev–Yao model [9]. Thus, it is possible for the intruder to assume a legitimate role in a protocol run. The role system also defines a number of sessions, and a number of principals and some basic roles. HLPSL is first translated using HLPSL2IF translator to the intermediate format (IF). IF is then fed to one of the backends to produce the output format (OF). It contains the following sections [45]:

• SUMMARY section tells that whether the tested protocol is safe, unsafe, or whether the analysis is inconclusive.

• DETAILS section either explains under what condition the tested protocol is declared safe, or what conditions have been used for finding an attack, or finally why the analysis was inconclusive.

• PROTOCOL, GOAL and BACKEND sections denote the name of the protocol, the goal of the analysis and the name of the back-end used, respectively.

• Finally, after some comments and statistics, the trace of an attack (if any) is also printed in the standard Alice-Bob format.

Several basic types are supported in HLPSL, which are given below for better understanding of the specifications of various roles described in Sect. 7.1 [1]:

• agent: It is for the principal name. The intruder is always assumed to have the special identifier i.

• public_key: It indicates agents’ public keys in a public-key cryptosystem. For example, given a public (respectively private) key K, its inverse private (respectively public) key is obtained by $inv\_K$.

• symmetric_key: It represents the keys for a symmetric-key cryptosystem.

• text: It is often used as nonces. These values can be also used for messages. For example, if Ni is of type text (fresh), then $Ni'$ will be a fresh value which the intruder cannot guess easily.

• nat: It represents the natural numbers in non-message contexts.

• const: It denotes the constants.

• hash_func: It represents cryptographic hash functions.

For a given message msg and encryption key k, $\{msg\}\_k$ denotes the symmetric/public-key encryption. In HLPSL, the associative “$\cdot$” operator is always used for concatenation.

Fig. 4

Role specification in HLPSL for the server $S_j$

7.1 Specifying the Protocol

This section describes the specifications of the roles in HLPSL for our scheme. Three basic roles for a user $U_i$, the RC and a server $S_j$ are implemented in HLPSL for our scheme. Apart from these roles, the roles for the session, goal and environment in HLPSL must be specified for our scheme. We have implemented our scheme for the formal security verification during the registration phase, login phase as well as authentication and session key agreement phase.

The role of the initiator, user $U_i$ is shown in Fig. 2. $U_i$ first receives the start signal, changes its state from 0 to 1 maintained by the variable State, and then sends the registration request message $\{ ID_i, A_i \}$ securely to the RC during the registration phase with the help of $SEND(\, )$ operation. $U_i$ also receives a smart card with the information $\{C_i, D_i, E_i, h(y), h(\cdot ) \}$ securely from the RC with the help of $RECV(\, )$ operation. During the login, and authentication and key agreement phases, $U_i$ sends the login request message $\{ CID_i, P_{ij}, M_1 , M_2\}$ to $S_j$ via a public channel. $U_i$ then receives the message $\{M_3, M_4\}$ from $S_j$ via a public channel. Finally, $U_i$ sends the message $\{M_5\}$ to $S_j$ via a public channel.

The type declaration $channel \,(dy)$ declares that the channel is for the Dolev–Yao threat model [9], which means that the intruder (i) has the ability to intercept, analyze, and/or modify messages transmitted over a insecure public channel.The “played_by A” declaration indicates that the agent named in variable A plays in the role. A knowledge declaration (generally in the top-level Environment role) is used to specify the intruder’s initial knowledge. Immediate reaction transitions are of the form $X =|> Y$, which relate an event X and an action Y. Note that the declaration witness(A, B, id, E) declares for a (weak) authentication property of A by B on E, declares that agent A is witness for the information E; this goal will be identified by the constant id in the goal section [1]. The declaration request (B, A, id, E) hints for a strong authentication property of A by B on E, declares that agent B requests a check of the value E; this goal will be identified by the constant id in the goal section [1]. For examples, witness(Ui, Sj, user_server_ni, Ni’) means that $U_i$ has freshly generated the value $N_i$ for $S_j$. request(Sj, Ui, server_user_nj, Nj’) tells that $U_i$’s acceptance of the value $N_j$ generated for $U_i$ by $S_j$. The declaration type secret(PWi,B, sub1, Ui) means that the information $PW_i$ and b are kept secret to the user $U_i$ only, which are characterized by the protocol id sub1. If a variable V is kept permanently secret, it is expressed by the goal secrecy_of V. As a result, if V is ever obtained or derived by the intruder, a security violation will result. In a similar way, the roles of the RC and a server $S_j$ are given in Figs. 3 and 4, respectively.

Fig. 5

Role specification in HLPSL for the session, and goal and environment

The roles for the session, and the goal and environment of our scheme are given in Fig. 5. All the basic roles, such as user, rc and server are the instances with concrete arguments in the role of the session. The top-level role (environment) is always defined in HLPSL specification. The intruder (i) also participates in the execution of protocol as a concrete session as shown in Fig. 5. We have three secrecy goals and two authentication goals in our implementation. For example, the secrecy goal: secrecy_of sub1 tells that the information $PW_i$ and b are kept secret to the user $U_i$ only. The authentication goal: authentication_on user_server_ni indicates that $U_i$ generates a random nonce $N_i$, where $N_i$ is only known to $U_i$. When the server $S_j$ will receive $N_i$ from other messages from $U_i$, it performs a strong authentication for $U_i$ based on $N_i$.

7.2 Simulation Results

We have simulated our scheme under the OFMC and CL-AtSe backends using the Security Protocol ANimator for AVISPA (SPAN) [1]. The following verifications are executed in our scheme [6, 7, 28–32]:

• Executability check on non-trivial HLPSL specifications: Due to some modeling mistakes, the protocol model can not sometimes execute to completion. It may be possible that the AVISPA backends can not find an attack, if the protocol model can not reach to a state where that attack can happen. An executability test becomes extremely essential [45]. Our scheme shows that the protocol description is well matched with the designed goals as specified in Figs. 2, 3, 4 and 5 for the executability test.

• Replay attack check: For the replay attack check, the OFMC and Cl-AtSe back-ends verify if the legitimate agents can execute the specified protocol by performing a search of a passive intruder. These back-ends provide the intruder the knowledge of some normal sessions between the legitimate agents. The test results shown in Figs. 6 and 7 indicate that our scheme is secure against the replay attack.

• Dolev–Yao model check: For the Dolev–Yao model check, the OFMC and Cl-AtSe back-ends also verifies whether there is any man-in-the-middle attack possible by an intruder. It is evident from the results reported in Figs. 6 and 7 that our scheme fulfills the design properties and is also secure under these backends.

Fig. 6

The result of the analysis using OFMC backend

Fig. 7

The result of the analysis using CL-AtSe backend

8 Performance Comparison with Related Schemes

In this section, we compare the performance and functionality features of our proposed scheme with the related existing authentication schemes proposed for the multi-server environment. This evaluation gives an insight into the effectiveness of the proposed scheme.

In Table 5, we have shown the security features provided and protected by our scheme as compared to those for the existing related schemes, such as Hsiang-Shih’s scheme [12], Lee et al.’s scheme [19], Li et al.’s scheme [21] and Shunmuganathan et al.’s scheme [38]. It is noted that password guessing attack is possible all other existing schemes. Moreover, proper mutual authentication, good repairability and two-factor security are not provided in the existing schemes. In addition, existing schemes are vulnerable to impersonation attack and forgery attack. We also see that the stolen smart card attack is not protected by the existing schemes [19, 21, 38]. On the other hand, our scheme protects known attacks shown in this table, and also supports good features mentioned in the table.

Table 5 Comparison of security features

In Table 6, we have compared the communication overhead of our scheme with the existing related schemes, such as Hsiang-Shih’s scheme [12], Lee et al.’s scheme [19], Li et al.’s scheme [21] and Shunmuganathan et al.’s scheme [38] during the login and authentication phases in terms of the number of transmitted messages and the number of bits required for these messages. For the communication cost analysis, we assume that each of the identity $ID_i$ of the user $U_i$ and the identity $SID_j$ of the server$S_j$ is 160 bits. The random nonce is assumed to be 160 bits. The hash output or message digest is taken as 160 bits (if we use SHA-1 as the secure one-way hash function [37]). In our scheme, we need three messages to be transmitted between $U_i$ and $S_j$. During the login phase, the message $\{CID_i, P_{ij}, M_1, M_2\}$ requires $4\,\times \,160 = 640$ bits. During the authentication and key agreement phase, the messages $\{M_3, M_4\}$ and $\{M_5\}$ require $2\,\times \,160 = 320$ bits and 160 bits, respectively. As a result, total communication overhead of our scheme during the login and authentication phases becomes $(640 + 320 + 160)$ $= 1120$ bits for three transmitted messages. On the other hand, the communication overheads for Hsiang-Shih’s scheme, Lee et al.’s scheme, Li et al.’s scheme and Shunmuganathan et al’s scheme are 2720, 1280, 1120 and 1120 bits, respectively. Note that our scheme performs better than Hsiang-Shih’s scheme and Lee et al.’s scheme, whereas the communication costs required for Li et al.’s scheme and Shunmuganathan et al.’s scheme are same as that for our scheme. However, our scheme is more secure and provides more functionality features as compared to other schemes as shown in Table 5.

Table 6 Communication overhead comparison during the login and authentication phases

Finally, in Table 7, we have compared the computation overhead of our scheme with the existing Hsiang-Shih’s scheme, Lee et al.’s scheme, Li et al.’s scheme and Shunmuganathan et al’s scheme. Let $T_h$ and $T_x$ refer to the execution time of the one way hash function operation and bitwise XOR operation, respectively. In our scheme, during the login phase, the computational cost is $8 T_h + 6 T_x$. During the authentication and key agreement phase, our scheme requires the computation cost $17 T_h + 6 T_x$. As a result, total computation overhead becomes $25 T_h + 12 T_x$. On the other hand, the computation overheads for Hsiang-Shih’s scheme, Lee et al.’s scheme, Li et al.’s scheme and Shunmuganathan et al’s scheme are $26 T_h + 23 T_x$, $20 T_h + 10 T_x$, $19 T_h + 12 T_x$ and $20 T_h + 10 T_x$, respectively. Due to efficient one-way hash function and bitwise XOR operations, the computation overhead of our scheme is also comparable with that for Hsiang-Shih’s scheme, Lee et al.’s scheme, Li et al.’s scheme and Shunmuganathan et al’s scheme.

Table 7 Computation overhead comparison during the login and authentication phases

9 Conclusion

In this paper, we have first reviewed Shunmuganathan et al.’s remote user authentication scheme for multi-server environment, and then shown that Shunmuganathan et al.’s scheme is vulnerable to password guessing attack, user impersonation attack, stolen smart card’s attack, replay attack, forgery attack. In addition, Shunmuganathan et al.’s scheme fails to provide forward secrecy and two-factor security. To overcome the shortcomings of these security weaknesses, we have proposed a more secure and effective multi-server authentication scheme based on the dynamic ID. We have demonstrated that our scheme can resist and sustain to the essential requirements for multi-server environment. In comparison with Shunmuganathan et al.’s scheme and other related schemes, our proposed scheme is more secure. Furthermore, we have simulated our scheme for the formal security verification using the most-widely accepted and used AVISPA tool and the simulation results clearly show that our scheme is secure. Through the widely-accepted BAN logic, we have also proved that our scheme provides mutual authentication between a user and a server. In addition, our scheme is comparable in both communication and computation as compared to Shunmuganathan et al.’s scheme and other schemes. High security along with low communication and computation overheads make our proposed scheme more suitable for practical applications in wireless communications.