Introduction

With the rapid development of network and communication technologies, in order to monitor and analyze patients’ health, the integrated EPR information system is widely used to share patients’ medical histories and help medical institutions to make correct clinical decisions rapidly. The registered user can on-line access various medical information and healthcare services from remote medical server. The ultimate aim of integrated EPR information system is to allow the sharing of patients’ medical information and histories scattered among all medical institutions, doctors, and patients through the Internet. Hence, all the medical participants, who could be from hospitals or from clinics and even an individual patient can be free to access all of services within the integrated EPR information systems. Due to the openness of the Internet, the public network communication between remote user and medical server is always a subject of information security and privacy risk in integrated EPR information system as a malicious attacker is considered to be powerful ability to launch various attacks. With the increase of security attacks [4, 6, 8, 9, 13, 15, 16, 19–21, 23, 25, 29] such as message replaying, participant masquerading and privacy exposing, many smart card based password authentication and key agreement schemes for the integrated EPR information system have been proposed [3, 7, 12, 17, 18, 26, 27].

In 2012, Wu et al. proposed a password based solution to build an efficient and patient-safety-centric scheme [27] for the integrated EPR information system. Wu et al.’s scheme requires only lightweight hashing functions and multiplication computations to be implemented under the medical application environments. However, in 2013, Lee et al. pointed out that Wu et al.’s solution is still vulnerable to lost smart card and stolen verifier attacks. After getting the secrets stored in the smart card by launching power analysis attacks [11, 22], the attacker can easily derives user’s password and masquerade as a legitimate user [14]. Lee et al. further proposed an improved version of authentication scheme [12] for the integrated EPR information system and their scheme can provide medical server and remote users with a secure and efficient practical environment. Unfortunately, in 2014, Wen [26] found that Lee et al.’s solution was insecure against off-line password guessing attack if the secrets stored in the user’s smart card are compromised and this problem also renders that their scheme fails to prevent user impersonation attack. In order to remedy this security problem found in Lee et al.’s scheme, Wen further proposed an improvement of Lee et al.’s scheme based on quadratic residues [2, 30]. However, in 2015, Das [3] showed that Lee et al.’s scheme and Wen’s scheme are still vulnerable to three disadvantages: 1) two schemes have design flaws in password change phase and this irrecoverable error enforces the user to re-register another new smart card issued by the server, 2) two schemes fail to protect privileged insider attack, 3) two schemes does not provide formal security verification. In order to remedy these design flaws in two schemes, Das propose a secure password-based remote user authentication scheme using smart cards for the integrated EPR information system and Das’s scheme is also efficient as compared to Lee et al.’s scheme and Wen’s scheme.

Although Das’s authentication scheme enhanced the security and efficiency of Lee et al.’s scheme and Wen’s scheme. However, we found that Das’s scheme has two security flaws: 1) the scheme fails to provide synchronized secret by launching modification attacks, 2) the scheme has user duplication attacks in password change phase. In order to solve these security weaknesses, we further propose a more secure user authentication scheme, while retaining the original merits of Das’s scheme. Through the formal security proof using the widely-accepted Burrows-Abadi-Needham (BAN) logic analysis [1] and show that our new scheme is surely more suitable than existing ones for use in assisting remote medical services to safeguard patient privacy.

The remainder of the paper is organized as follows. Section “Review of Das’s scheme” provides overview of Das’s authentication scheme in brief and shows its security weaknesses in Section “Two weaknesses on Das’s scheme”. Section “The proposed scheme” presents our improved scheme and proves the security of our scheme by using widely-accepted BAN logic analysis in Section “Security proof of our scheme using BAN logic”. In Section “Comparison of our scheme with related schemes”, we give a detailed comparison between our scheme and other related schemes. Finally, we draw our conclusions in Section “Conclusions”.

Review of Das’s scheme

In this section, Das’s scheme [3] will be briefly reviewed. There are four phases in Das’s scheme and Fig. 1 shows the entire flowchart of Das’s scheme. For convenience of description, terminology and notations used in the paper are summarized as follows:

  • S j : The trustworthy integrated EPR information system server.

  • U i : The user.

  • I D i : The identity of user U i .

  • P W i : The password of user U i .

  • h(⋅): A secure collision-free one-way hash function, such as HMAC [24].

  • K: The secret key of S j , where K is considered as a 1024-bit number.

  • H: The constant secret value of S j , where H is considered as a 1024-bit number.

  • X u : The secret number of U i , where X u is considered as a 1024-bit number.

  • ||: The concatenation operation.

  • ⊕: The bitwise XOR operation.

Fig. 1
figure 1

The flowchart of Das’s scheme

Full size image

Registration phase

In this phase, the user U i registers with the remote server S j through a secure channel to be a legal user. The details of registration phase are as follows:

  • Step R1:  U i chooses his/her identity I D i and password P W i .

  • Step R2:  U i generates a random secret number X u and it is kept secret to the user U i only.

  • Step R3:  U i computes R P W i = h(X u ||P W i ) and sends the registration request { I D i , R P W i } to S j via a secure channel.

  • Step R4:  S j validates the identity I D i of U i and computes v = h(K⊕I D i ) if I D i is valid.

  • Step R5:  S j computes s 1 = h(R P W i ||K), s 2 = h(R P W i ||s 1) and N = v⊕s 2 ⊕ H.

  • Step R6:  S j issues a medical smart card containing the information { I D i , h(⋅),N, s 1} to the user U i via a secure channel.

After receiving the smart card from S j , U i stores X u in its memory.

Login phase

If U i wants to access the integrated EPR information system server S j , the following steps need to be executed:

  • Step L1:  U i inserts his/her smart card into card reader and inputs identity I D i and password P W i . Then smart card computes R P W i = h(X u ||P W i ).

  • Step L2: The smart card generates a random number r 1 and computes h(r 1), s 2 = h(R P W i ||s 1) and C 1 = r 1 ⊕ s 2.

  • Step L3: Finally, U i sends the login request message { N, I D i , C 1, h(r 1)} to S j via a public channel.

Verification phase

When the server S j receives U i ’s login request message, S j and U i perform the following steps:

  • Step V1:  S j verifies the validity of U i ’s identity I D i . If it is valid, S j goes to Step V2. Otherwise, S j rejects U i ’s login request.

  • Step V2:  S j computes v = h(K⊕I D i ), s2′ = H⊕N⊕v and r1′ = s2′⊕C 1 and checks whether h(r1′) = h(r 1). If it holds, S j stores the pair (I D i , r1′) in its database and executes Step V3. Otherwise, S j rejects this login request.

  • Step V3:  S j computes a = r 2 ⊕ h(r1′||s2′) and b = h(s2′||r 2||r1′) and sends the authentication request message { a, b} to U i via a public channel, where r 2 is a random number generated by S j

  • Step V4: After receiving the message from S j , U i computes h(r 1||s 2), r2′ = a⊕h(r 1||s 2) and h(s 2||r2′||r 1) and checks whether b = h(s 2||r2′||r 1). If it holds, U i successfully authenticates S j and execute Step V5.

  • Step V5:  U i computes \(C_{2}=h(r_{2N||s_{2}})\oplus h(RPW_{i}||s_{1})\) and sends the acknowledgement message { C 2} to S j via a public channel.

  • Step V6: After receiving the message from U i , S j computes u = h(r 2||s 2N )⊕C 2 and checks whether s2′ = h(u). If it holds, S j successfully authenticates U i .

  • Step V7: Finally, S j and U i can compute a secret session key S K = h(r1′||r 2||a||b||N||I D i ) = h(r 1||r2′||a||b||N||I D i ) shared between them.

Password change phase

When the user U i wants to change his/her old password P W i to a new password \(PW_{i}^{new}\), U i must notify the remote server S j to update the old masked password R P W i = h(X u ||P W i ) to a new masked password \(RPW_{i}^{new}=h(X_{u}||PW_{i}^{new})\).

  • Step P1:  U i inserts his/her smart card into card reader and inputs identity I D i , old password P W i and new password \(PW_{i}^{new}\). Then smart card computes old masked password R P W i = h(X u ||P W i ) and new masked password \(RPW_{i}^{new}=h(X_{u}||PW_{i}^{new})\) and sends the password change request message {\(ID_{i}, RPW_{i}, RPW_{i}^{new}, N\)} to S j via a secure channel.

  • Step P2: After receiving the request from U i , S j computes v = h(K⊕I D i ), \(s_{1}^{*}=h(RPW_{i}||K)\), s 2 = N⊕v⊕H and \(s_{2}^{*}=h(RPW_{i}||s_{1}^{*})\) and checks whether \(s_{2}=s_{2}^{*}\). If it holds, S j goes to Step P3. Otherwise, S j terminates this phase.

  • Step P3:  S j computes \(s_{1}^{\prime \prime }=h(RPW_{i}^{new}||K)\), \(s_{2}^{\prime \prime }=h(RPW_{i}^{new}||s_{1}^{\prime \prime })\) and N ″ = v⊕s2″⊕H and sends { s1″,N ″} to U i via a secure channel.

  • Step P4: Finally, U i replaces s 1 with s1″ and N with N ” on his/her medical smart card.

Two weaknesses on Das’s scheme

In this section, we show that Das’s scheme has two weaknesses, which are discussed in the following subsections.

Modification attacks

In Step V2 of verification phase of Das’s scheme, in order to prevent replay attacks and man-in-the-middle attacks, the server stores latest login pair \((ID_{i}, r_{1}^{\prime })\) in its database, where r1′ = r 1. Whenever the server S j receives the next login request message {\(N^{\prime }, ID_{i}^{\prime }, C_{1}^{\prime }, h(r_{1}^{\prime \prime })\)} with new random number \(r_{1}^{\prime \prime }\) from the user U i , S j further computes \(v^{\prime }=h(K\oplus ID_{i}^{\prime })\), \(s_{2}^{\prime \prime \prime }=H\oplus N^{\prime }\oplus v^{\prime }\) and \(r_{1}^{\prime \prime \prime }=s_{2}^{\prime \prime \prime }\oplus C_{1}^{\prime }\) and checks whether the stored r1′ matches with the computed \(r_{1}^{\prime \prime \prime }\). If there is a match, S j discovers that the login request message is a replay message and S j will reject this request. Otherwise, S j convinces that the login request is not a replay message and it will replace r1′ with the computed \(r_{1}^{\prime \prime \prime }\) in its maintained database.

However, if an attacker U a intentionally collects previous login request messages over the public channel and replays the previous login request message to S j , U a is able to fool server S j to store wrong pair in its database. To launch modification attack, U a first collects latest login message {\(N^{\prime }, ID_{i}^{\prime }, C_{1}^{\prime }, h(r_{1}^{\prime \prime })\)} and previous login message { N, I D i , C 1, h(r 1)} from the public channel between U i and S j . Note that in previous login session, S j stores (I D i , r i ) in its maintained database and S j will replace previous random number r i with latest random number \(r_{1}^{\prime \prime }\) in latest login session.

Afterwards, U a can make a fool of medical remote server by replaying the previous login request message { N, I D i , C 1, h(r 1)} to S j . Since previous login request message { N, I D i , C 1, h(r 1)} is a legal message and \(r_{1} \neq r_{1}^{\prime \prime }\), S j will remissly replace \(r_{1}^{\prime \prime }\) with r 1 in Step V2 of verification phase. Moreover, S j generates a random number \(r_{2}^{\prime \prime \prime }\), computes the pair (a, b) and sends the authentication request message {a, b} to the attacker U a in Step V3 of verification phase. However, without knowing \(r_{2}^{\prime \prime \prime }\), s 2 and h(R P W i ||s 1), the attacker U a cannot reply the correct acknowledgement message { C 2} to S j in Step V5 of verification phase. As a result, U a cannot pass the verification of S j in Step V6 of verification phase and S j will reject U a ’s login request. Although U a ’s login request was fail, U a successfully fooled S j into believing him/her to store wrong pair in its maintained database. Thus, Das’s scheme is vulnerable to the modification attacks.

User duplication attacks

In Das’s scheme, we observe that a legitimate user may intentionally duplicate his/her account to multiple non-registered users by using the same identity with different masked passwords and the medical server S j is not aware of having caused problem. The detailed attacks are described as follows.

  1. (1)

    In password change of Das’s scheme, a registered user U i can freely change his/her old password P W i to a new password \(PW_{i}^{new}\) by sending the password change request message {\(ID_{i}, RPW_{i}, RPW_{i}^{new}, N\)} to remote server S j via a secure channel, where R P W i = h(X u ||P W i ) and \(RPW_{i}^{new}=h(X_{u}||PW_{i}^{new})\).

  2. (2)

    After verifying this request message, S j will compute \(s_{1}^{\prime \prime }=h(RPW_{i}^{new}||K)\) and N ″ = h(K⊕I D i )⊕s2″⊕H and send { s1″,N ″} to U i , where \(s_{2}^{\prime \prime }=h(RPW_{i}^{new}||s_{1}^{\prime \prime })\).

  3. (3)

    Finally, a registered user can successfully duplicate his/her medical account with new information { I D i , h(⋅),N ″,s1″,X u }.

Afterwards, U i has two accounts { I D i , h(⋅),N, s 1, X u } and { I D i , h(⋅),N ″,s1″,X u } with same identity and any duplicated account can intentionally expose to other non-registered users. Hence, Das’s scheme cannot prevent user duplication attacks.

The proposed scheme

In this section, we propose a simple improvement on Das’s authentication scheme, which keeps the merits of original scheme. In order to withstand the user duplication attack that is discussed in Section “User duplication attacks”, we use a parameter R to record the number of times U i re-registers to S j , where R = 0 if it is U i ’s initial registration. Fig. 2 shows the entire flowchart of our enhanced scheme for the integrated EPR information system.

Fig. 2
figure 2

The flowchart of our proposed scheme

Full size image

Registration phase

In this phase, the user U i registers with the remote server S j through a secure channel to be a legal user. The details of registration phase are as follows:

  • Step R1:  U i chooses his/her identity I D i and password P W i .

  • Step R2:  U i generates a random secret number X u and it is kept secret to the user U i only.

  • Step R3:  U i computes R P W i = h(X u ||P W i ) and sends the registration request { I D i , R P W i } to S j via a secure channel.

  • Step R4:  S j validates the identity I D i of U i and computes v = h(K⊕I D i ⊕ R) if I D i is valid, where R means the number of times U i re-registers to S j .

  • Step R5:  S j computes s 1 = h(R P W i ||K), s 2 = h(R P W i ||s 1) and N = v⊕s 2 ⊕ H.

  • Step R6:  S j issues a medical smart card containing the information { I D i , h(⋅),N, s 1} to the user U i via a secure channel. Moreover, S j maintains the access control table for a registration service and the format of access control table is shown in Table 1. Note that the first field records U i ’s identity, the second field records null if it is U i ’s initial registration, and the third field records R = 0 if it is U i ’s initial registration, otherwise, S j sets R = R + 1 in the existing field for U i .

  • Step R7: After receiving the smart card from S j , U i stores X u in its memory.

Table 1 Access control table of S j after finishing the registration phase
Full size table

Login phase

In this phase, the executed steps are the same as Das’s scheme.

Verification phase

When the server S j receives U i ’s login request message, S j and U i perform the following steps:

  • Step V1:  S j verifies the validity of U i ’s identity I D i . If it is valid, S j goes to Step V2. Otherwise, S j rejects U i ’s login request.

  • Step V2:  S j retrieves the stored R in the access control table and computes v = h(K⊕I D i ⊕ R), s2′ = H⊕N⊕v and r1′ = s2′⊕C 1. Then, S j checks whether h(r1′) = h(r 1). If it holds, S j executes Step V3. Otherwise, S j rejects this login request. Note that S j does not store r1′ into the access control table in this step.

  • Step V3, Step V4, Step V5: These three steps are the same as Das’s scheme.

  • Step V6:After receiving the message from U i , S j computes u = h(r 2||s2′)⊕C 2 and checks whether s2′ = h(u). If it holds, S j successfully authenticates U i and stores r1′ in its access control table. After finishing this step, the current format of access control table is shown in Table 2.

  • Step V7: This step is the same as Das’s scheme.

Table 2 Access control table of S j after finishing the verification phase
Full size table

In order to resist modification attacks, in Step V6 of verification phase, the server S j will store the latest random number r1′ in its access control table after verifying U i ’s acknowledgement message C 2. For such design of our scheme, an attacker U a cannot simply replay the previous login request messages to S j to launch modification attacks due to U a cannot compute the correct acknowledgement message C 2 without knowing \(r_{2}^{\prime }\), s 2, R P W i and s 1. In this way, the server confirms that the login request message is certainly a replay message and S j will discard that message. Thus, our proposed scheme has the ability to prevent the modification attacks.

Password change phase

When the user U i wants to change his/her old password P W i to a new password \(PW_{i}^{new}\), U i must notify the remote server S j to update the old masked password R P W i = h(X u ||P W i ) to a new masked password \(RPW_{i}^{new}=h(X_{u}||PW_{i}^{new})\).

  • Step P1:  U i inserts his/her smart card into card reader and inputs identity I D i , old password P W i and new password \(PW_{i}^{new}\). Then smart card computes old masked password R P W i = h(X u ||P W i ) and new masked password \(RPW_{i}^{new}=h(X_{u}||PW_{i}^{new})\) and sends the password change request message {\(ID_{i}, RPW_{i}, RPW_{i}^{new}, N\)} to S j via a secure channel.

  • Step P2: After receiving the request from U i , S j retrieves the stored R in the access control table and computes v = h(K⊕I D i ⊕ R), \(s_{1}^{*}=h(RPW_{i}||K)\), s 2 = N⊕v⊕H and \(s_{2}^{*}=h(RPW_{i}||s_{1}^{*})\). Then, S j checks whether \(s_{2}=s_{2}^{*}\). If it holds, S j goes to Step P3. Otherwise, S j terminates this phase.

  • Step P3:  S j computes v ′ = h(K⊕I D i ⊕ R + 1), \(s_{1}^{\prime \prime }=h(RPW_{i}^{new}||K)\), \(s_{2}^{\prime \prime }=h(RPW_{i}^{new}||s_{1}^{\prime \prime })\) and N ″ = v ′⊕s 2 ”⊕H and sends { s1″,N ″} to U i via a secure channel. After finishing this step, the current format of access control table is shown in Table 3.

  • Step P4: Finally, U i replaces s 1 with s1″ and N with N ” on his/her medical smart card.

Table 3 Access control table of S j after finishing the password change phase
Full size table

In order to prevent user duplication attacks, in Step P3 of password change phase, the value of R is incremented by one and it is updated in S j ’s access control table. It is noted that the new parameter v ′ = h(K⊕I D i ⊕ R + 1) and it is integrated with new login parameter N ″ = v ′⊕s2″⊕H. Although U i has two accounts { I D i , h(⋅),N, s 1, X u } and { I D i , h(⋅),N ″,s1″,X u } with same identity, S j will compute new parameter v ′ = h(K⊕I D i ⊕ R + 1) and verify the validity of N ″. In this way, U i cannot use this account { I D i , h(⋅),N, s 1, X u } to login to S j due to the previous login parameter N = h(K⊕I D i ⊕ R)⊕s 2 ⊕ H is illegal. Finally, any legitimate user cannot launch user duplication attacks in our proposed scheme.

Security proof of our scheme using BAN logic

In this section, we use the BAN logic [1] to analyze the security of the session key between user U i and medical server S j . Some notations used in BAN logic analysis are described as follows:

  • A| ≡ X: It means that A believes the formula X is true.

  • \(A \vartriangleleft X\): It means that A sees the formula X.

  • A| ⇒ X: It means that A has complete control over the formula X.

  • A| ∼ X: It means that A has once said the formula X.

  • ♯(X): It means that X is fresh. The formula X has not been used before or X is a nonce.

  • \(A \begin {array}{c} K \\ \longleftrightarrow \\ \end {array} B\): It means that principals A and B may use the shared key K to communicate. Note that K will never be discovered by any principals except A and B.

  • <X > Y : It means that formula X is combined with a secret parameter Y.

  • (X) K : It means that formula X is hashed with a key K.

  • \(\frac {Rule 1}{Rule 2}\): It can infer R u l e2 from R u l e1. For example, \(\frac {A creats random X}{A |\equiv \sharp (X)}\) means that principal A creates X, so A believes X is fresh.

  • SK: A session key established in each session.

In order to describe logical postulates of BAN logic in formal terms, we list four rules as follows:

  • (Rule 1) Message meaning rule:  \(\frac {A |\equiv A \begin {array}{c} K \\ \longleftrightarrow \\ \end {array} B, A \vartriangleleft (X)_{K}}{A |\equiv B |\sim X}\) If A believes that K is shared with B and sees X hashed with K, then A believes that B once said X.

  • (Rule 2) Nonce verification rule:  \(\frac {A |\equiv \sharp (X), A |\equiv B |\sim X}{A |\equiv B |\equiv X}\) If A believes that X has been uttered recently (freshness) and A believes that B once said X, and then A believes that B believes X.

  • (Rule 3) The jurisdiction rule:  \(\frac {A |\equiv B |\equiv X, A |\equiv B |\Rightarrow X}{A |\equiv X}\) If A believes that B has jurisdiction over X, and A believes that B believes a message X, then A believes X.

  • (Rule 4) The freshness conjuncatenation rule:  \(\frac {A |\equiv \sharp (X)}{A |\equiv \sharp (X, Y)}\) If one part known to be fresh, then the entire formula is fresh.

According to the analytic procedures of BAN logic, two participators U i and S j cooperatively run the proposed scheme and we list the verification goals of our scheme as follows:

  • (G.1):  \(U_{i} |\equiv U_{i} \begin {array}{c} SK \\ \longleftrightarrow \\ \end {array} S_{j}\)

  • (G.2):  \(S_{j} |\equiv U_{i} \begin {array}{c} SK \\ \longleftrightarrow \\ \end {array} S_{j}\)

Next, we use BAN logic to transform our scheme, illustrated in Fig. 2 into the idealized form. The scheme generic types are shown in the following:

  • Message 1.  U i → S j : N, I D i , C 1, h(r 1)

  • Message 2.  S j → U i : a, b

  • Message 3.  U i → S j : C 2

Idealize form of the proposed scheme:

  • Message 1.  \(U_{i} \rightarrow S_{j}: (s_{2})_{v, H}, ID_{i}, <r_{1}>_{s_{2}}, h(r_{1})\)

  • Message 2.  \(S_{j} \rightarrow U_{i}: <r_{2}>_{(r_{1})_{s_{2}}}, (r_{1}, r_{2})_{s_{2}}\)

  • Message 3.  \(U_{i} \rightarrow S_{j}: <s_{2}>_{(r_{2})_{s_{2}}}\)

To analyze the proposed scheme, the following assumptions are also required:

  • (A.1):  U i | ≡ ♯(r 1)

  • (A.2):  S j | ≡ ♯(r 2)

  • (A.3):  \(U_{i} |\equiv \left (U_{i} \begin {array}{c} v \\ \longleftrightarrow \\ \end {array} S_{j}\right )\)

  • (A.4):  \(S_{j} |\equiv \left (U_{i} \begin {array}{c} v \\ \longleftrightarrow \\ \end {array} S_{j}\right )\)

  • (A.5):  \(U_{i} |\equiv \left (U_{i} \begin {array}{c} H \\ \longleftrightarrow \\ \end {array} S_{j}\right )\)

  • (A.6):  \(S_{j} |\equiv \left (U_{i} \begin {array}{c} H \\ \longleftrightarrow \\ \end {array} S_{j}\right )\)

  • (A.7):  \(U_{i} |\equiv S_{j} |\equiv \left (U_{i} \begin {array}{c} v \\ \longleftrightarrow \\ \end {array} S_{j}\right )\)

  • (A.8):  \(S_{j} |\equiv U_{i} |\equiv \left (U_{i} \begin {array}{c} v \\ \longleftrightarrow \\ \end {array} S_{j}\right )\)

  • (A.9):  \(U_{i} |\equiv S_{j} |\equiv \left (U_{i} \begin {array}{c} H \\ \longleftrightarrow \\ \end {array} S_{j}\right )\)

  • (A.10):  \(S_{j} |\equiv U_{i} |\equiv \left (U_{i} \begin {array}{c} H \\ \longleftrightarrow \\ \end {array} S_{j}\right )\)

Based on the above-mentioned assumptions, the preliminary procedures of BAN logic are well prepared and we show the main steps of the verification proof as follows:

According to the Message 1, we could obtain:

  • (V.1):  \(S_{j} \vartriangleleft (s_{2})_{v, H}, ID_{i}, <r_{1}>_{s_{2}}, h(r_{1})\)

According to the assumption (A.4) and (A.6), we apply the message meaning rule to obtain:

  • (V.2):  S j | ≡ U i | ∼ v, H

According to the assumption (V.2), we apply the message meaning rule to obtain:

  • (V.3):  S j | ≡ U i | ∼ s 2

According to the assumption (V.3), we apply the message meaning rule to obtain:

  • (V.4):  S j | ≡ U i | ∼ r 1

According to the assumption (A.1) and (V.4), we apply the freshness conjuncatenation rule to obtain:

  • (V.5):  \(S_{j} \sharp <r_{1}>_{s_{2}}\)

According to (V.4) and (V.5), we apply the nonce verification rule to obtain:

  • (V.6):  \(S_{j}|\equiv U_{i}|\equiv <r_{1}>_{s_{2}}\)

According to (V.3) and (V.6), we apply the jurisdiction rule to obtain:

  • (V.7):  S j | ≡ r 1

According to the Message 2, we could obtain:

  • (V.8):  \(U_{i} \vartriangleleft <r_{2}>_{(r_{1})_{s_{2}}}, (r_{1}, r_{2})_{s_{2}}\)

According to the assumption (V.3) and (A.2), we apply the message meaning rule to obtain:

  • (V.9):  U i | ≡ S j | ∼ r 2

According to the assumption (A.2), we apply the freshness conjuncatenation rule to obtain:

  • (V.10):  \(U_{i} \sharp <r_{2}>_{(r_{1})_{s_{2}}}\)

According to (V.9) and (V.10), we apply the nonce verification rule to obtain:

  • (V.11):  \(U_{i}|\equiv S_{j}|\equiv <r_{2}>_{(r_{1})_{s_{2}}}\)

According to (V.9) and (V.11), we apply the jurisdiction rule to obtain:

  • (V.12):  U i | ≡ r 2

According to \(SK=h(r_{1}, r_{2}, <r_{2}>_{(r_{1})_{s_{2}}}, (r_{1}, r_{2})_{s_{2}}, (s_{2})_{v, H}, ID_{i})\), (V.12), and (A.1), we could obtain:

  • (V.13):  U i | ≡ U i S K ↔ S j (G.1)

According to the Message 3, we could obtain:

  • (V.14):  \(S_{j} \vartriangleleft <s_{2}>_{(r_{2})_{s_{2}}}\)

According to \(SK=h(r_{1}, r_{2}, <r_{2}>_{(r_{1})_{s_{2}}}, (r_{1}, r_{2})_{s_{2}}, (s_{2})_{v, H}, ID_{i})\), (V.3), (V.7) and (A.2), we could obtain:

  • (V.15):  S j | ≡ U i S K ↔ S j (G.2)

Finally, inferring from formulas V.13 and V.15, we have proven the proposed scheme achieves the verification goals as well as establishes a common session key SK between U i and S j .

Comparison of our scheme with related schemes

In this section, we compare our proposed scheme with some smart card based authentication schemes [3, 5, 10] in terms of computation overhead and security properties. For example in the experiment environment (CPU: 3.2 GHz, RAM: 3.0 G), we have followed the experimental results perform in [28]. The result reported that the average time of executing one hash function, one symmetric en/decryption operation and one chaotic maps operation are 0.2 ms, 0.45 ms and 32.2 ms, respectively. Comparison is done only for login and verification phases because these phases are used frequently. Note that exclusive-or operation is negligible and we omit the cost of exclusive-or operation. For convenience to evaluate the computational costs and functional features, we define some notations as follows.

  • T h : The time of executing a one-way hash function.

  • T s : The time of executing a symmetric en/decryption operation.

  • T c : The time of executing a Chebyshev chaotic maps operation.

  • F1: Computation cost of the user U i .

  • F2: Computation cost of the server S j .

  • F3: Execution time in user side.

  • F4: Execution time in server side.

  • F5: Total execution time.

  • F6: Provision of session key agreement.

  • F7: Provision of formal security proof.

  • F8: Prevention of modification attack.

  • F9: Prevention of user duplication attack.

  • F10: Without using synchronized timestamp.

Table 4 shows the comparisons of proposed scheme with related schemes in terms of computation overhead and security properties. As can be seen in Table 4, our scheme and Das’s scheme have better performance than other schemes. With respect to the security properties, while Das’s scheme is vulnerable to modification attack, Hao et al.’s scheme and Jiang et al.’s scheme are resistant to the attack. However, the security of Hao et al.’s scheme and Jiang et al.’s scheme were not proved in a formal model, while our proposed scheme not only satisfies all the security attributes but also provides the rigorous proof of the security. From an implementation point of view, our scheme requires less computational power and achieves more security criteria compared with related schemes and these features make our solution quite suitable to resource-constrained environments such as telecare medicine information systems and the integrated EPR information systems.

Table 4 Performance comparisons of our enhanced scheme with some authentication schemes for the integrated EPR information systems
Full size table

Conclusions

In this paper, we have analyzed that a smart card based authenticated key agreement scheme for the integrated EPR information system proposed by Das in 2015. Although the security of this scheme was proved through AVISPA tool, we have demonstrated that any legitimate but malicious user was able to launched user duplication attack. Moreover, Das’s scheme is vulnerable to modification attack and the malicious attacker can replay the previous login messages to fool medical server into maintaining wrong information in its database. To address these problems, an improved smart card based user authentication and key agreement scheme was presented in this paper. According to the formal verification, the proposed scheme has protected system security during the healthcare delivery session, and is more efficient and practical for the real life healthcare applications.