Open AccessArticle

Secure Authentication Protocol for Wireless Sensor Networks in Vehicular Communications

SungJin Yu

JoonYoung Lee

¹,

KyungKeun Lee

²,

KiSung Park

^1,*

and

YoungHo Park

^1,*

School of Electronics Engineering, Kyungpook National University, Daegu 41566, Korea

Samsung Electronics, Suwon 16677, Korea

Authors to whom correspondence should be addressed.

Sensors 2018, 18(10), 3191; https://doi.org/10.3390/s18103191

Submission received: 27 July 2018 / Revised: 18 September 2018 / Accepted: 18 September 2018 / Published: 21 September 2018

(This article belongs to the Special Issue Advances on Vehicular Networks: From Sensing to Autonomous Driving)

Download

Browse Figures

Figure 1
Vehicular communications system model. "> Figure 2
User registration phase of the Mohit et al.’s scheme. "> Figure 3
User login and authentication phase of the Mohit et al.’s scheme. "> Figure 4
Password change phase of the Mohit et al.’s scheme. "> Figure 5
User registration phase of the proposed scheme. "> Figure 6
User login and authentication phase of the proposed scheme. "> Figure 7
Password change phase of the proposed scheme. "> Figure 8
Role specification for session and environment. "> Figure 9
Role specification for user <math display="inline"><semantics> <mrow> <mi>U</mi> <mi>A</mi> </mrow> </semantics></math>. "> Figure 10
Role specification for <math display="inline"><semantics> <mrow> <mi>V</mi> <mi>S</mi> </mrow> </semantics></math>. "> Figure 11
Role specification for <math display="inline"><semantics> <mrow> <mi>S</mi> <mi>N</mi> </mrow> </semantics></math>. "> Figure 12
The result of analysis using OFMC and CL-AtSe ">

Versions Notes

Abstract

With wireless sensor networks (WSNs), a driver can access various useful information for convenient driving, such as traffic congestion, emergence, vehicle accidents, and speed. However, a driver and traffic manager can be vulnerable to various attacks because such information is transmitted through a public channel. Therefore, secure mutual authentication has become an important security issue, and many authentication schemes have been proposed. In 2017, Mohit et al. proposed an authentication protocol for WSNs in vehicular communications to ensure secure mutual authentication. However, their scheme cannot resist various attacks such as impersonation and trace attacks, and their scheme cannot provide secure mutual authentication, session key security, and anonymity. In this paper, we propose a secure authentication protocol for WSNs in vehicular communications to resolve the security weaknesses of Mohit et al.’s scheme. Our authentication protocol prevents various attacks and achieves secure mutual authentication and anonymity by using dynamic parameters that are changed every session. We prove that our protocol provides secure mutual authentication by using the Burrows–Abadi–Needham logic, which is a widely accepted formal security analysis. We perform a formal security verification by using the well-known Automated Validation of Internet Security Protocols and Applications tool, which shows that the proposed protocol is safe against replay and man-in-the-middle attacks. We compare the performance and security properties of our protocol with other related schemes. Overall, the proposed protocol provides better security features and a comparable computation cost. Therefore, the proposed protocol can be applied to practical WSNs-based vehicular communications.

Keywords:

authentication; wireless sensor network; vehicular communications; formal security analysis; BAN logic; AVISPA

1. Introduction

Wireless sensor networks (WSNs), in conjunction with intelligent transport systems (ITS) and embedded technology, have advanced to such an extent that drivers can make full use of various information such as traffic congestion, vehicle accidents, and speed. To provide these useful services, a sensor in the vehicle collects data on the vehicle and surrounding area and sends it to the traffic manager through a sink node. The traffic manager in the traffic management office receives data from vehicle sensors and can monitor a vehicle and the surrounding area to provide useful data to the driver in real time. However, a malicious adversary can easily obtain and modify the data because it is transmitted via a public network. Therefore, the authentication protocol between the vehicle and user in vehicular communications has become a very important security issue. In the last few decades, numerous authentication schemes for WSNs have been proposed to ensure secure communications and user privacy [1,2,3,4,5,6,7,8]. In 2006, Wong et al. [9] proposed a dynamic ID-based user authentication scheme for WSNs. However, Das et al. [10] showed that Wong et al.’s [9] scheme is vulnerable to the stolen verifier attack and proposed an improved two-factor authentication scheme to overcome these security problems. In 2010, Chen et al. [11] demonstrated that Das et al.’s scheme [10] cannot provide secure mutual authentication and cannot resist parallel session attacks. To resolve this problem, they proposed a robust mutual authentication scheme for WSNs. Khan et al. [12] also showed that Das et al.’s scheme [10] cannot prevent the privileged insider and bypassing attacks, nor can it provide mutual authentication and the password changing phase. To overcome these security weaknesses, they proposed a two-factor user authentication protocol that uses secret parameters. In 2011, Yeh et al. [13] found that Das et al.’s scheme cannot resist the insider attack and provide mutual authentication, which are essential security requirements for the WSNs. They proposed a secured authentication protocol for WSNs that uses elliptic curve cryptography (ECC). Unfortunately, Han [14] pointed out that Yeh et al.’s scheme cannot provide mutual authentication, perfect forward secrecy, and key agreement. To resolve the security weaknesses of Yeh et al.’s scheme, Shi et al. [15] proposed a new user authentication protocol for WSNs using ECC. However, Choi et al. [16] showed that Shi et al.’s [15] scheme is vulnerable to a smartcard being stolen, sensor energy exhaustion, and session key attacks. They proposed a new user authentication protocol based on ECC.

In the last few decades, numerous protocols for secure vehicle communications have been proposed [17,18,19,20,21,22,23,24,25]. In 2008, Zhang et al. [17] proposed an efficient roadside unit (RSU)-aided message authentication scheme that uses a hash message authentication code (HMAC) for vehicular communications networks. Zhang et al. also proposed [18] an efficient message authentication scheme for vehicular communications. Lu et al. [19] proposed an efficient conditional privacy preservation protocol for secure vehicular communications that uses bilinear pairing. However, their protocol is not efficient in resource-constrained vehicular ad hoc networks (VANETs) because it has used multiple anonymous key and has high latency for generating of pseudo-random keys [20]. In 2014, Chuang and Lee [21] proposed an authentication mechanism for vehicle to vehicle communications in VANETs. However, in 2016, Kumari et al. [22] showed that Chuang and Lee’s authentication protocol is vulnerable to insider and impersonation attacks, and they proposed an enhanced authentication protocol for VANETs. In 2017, Mohit et al. [23] also proposed an authentication protocol for WSNs in vehicle communications. Mohit et al. claimed that their proposed scheme can resist various attacks such as smartcard stolen, impersonation, and untraceable attacks. In this paper, however, we demonstrate that their scheme cannot resist impersonation and trace attacks. In addition, we show that Mohit et al.’s scheme cannot provide anonymity, session key security, and mutual authentication. We propose a secure authentication protocol for WSNs in vehicle communications that overcomes these security weaknesses.

1.1. Threat Model

To analyze the security of our proposed scheme, we introduce the Dolev–Yao (DY) threat model, which is widely used to evaluate the security of a protocol. The detailed assumptions of the DY threat model are as follows:

An adversary can modify, eavesdrop, insert or delete the transmitted messages over a public channel.
An adversary can obtain a lost or smartcard stolen, and he/she can also extract the information stored in the smartcard [26,27].
An adversary can perform various attacks such as impersonation, trace, smartcard stolen, and replay attacks.

1.2. Our Contributions

The main contributions of this paper are as follows:

We demonstrate that Mohit et al.’s scheme is vulnerable to various attacks such as impersonation and trace attacks. In addition, we point out that their scheme cannot provide mutual authentication, session key security and anonymity.
We propose a secure authentication protocol for WSNs in vehicular communications to resolve these security weaknesses. Our proposed protocol prevents impersonation and trace attacks, and also achieves anonymity, session key security and secure mutual authentication. In addition, the proposed scheme is efficient because it utilizes only hash function and XOR operation in authentication phase.
We prove that our protocol provides secure mutual authentication by using the broadly accepted Burrows–Abadi–Needham (BAN) logic [28]. We also perform an informal analysis to demonstrate the security of the proposed protocol against various attacks such as impersonation and trace attacks.
We compare the performance of our scheme against those of related existing schemes and perform a formal security verification by using the widespread Automated Validation of Internet Security Protocols and Applications (AVISPA) simulation software tool.

1.3. Paper Outline

The remainder of this paper is organized as follows. In Section 2, we introduce the vehicular communications system model. In Section 3 and Section 4, we review Mohit et al.’s authentication scheme and analyze its security weaknesses. In Section 5, we propose a secure authentication protocol for WSNs in vehicular communications to resolve the security problems of their scheme. In Section 6, we present an informal analysis on the security of our protocol and prove that it achieves secure mutual authentication by using BAN logic. In Section 7 and Section 8, we present the formal security verification with the AVISPA simulation tool and compare the performance of our protocol with that of related protocols. Finally, we present our conclusions in Section 9.

2. System Model

In this section, we introduce a vehicular communication system using WSNs and essential security requirements. There are three entities involved in the vehicular communications system: the vehicle sensor, sink node, and user. The vehicular communications system model is shown in Figure 1.

The vehicular communications system consists of two parts: the WSNs and vehicle and the user and sink node. The vehicle sensor is deployed in the vehicle and collects data on the traffic and surrounding area in real time, which it then sends to the sink node. After receiving the data from the vehicle sensor, the sink node stores it for the user. The user can control the response to traffic jams, speed, and emergency situations based on the data collected by the sink node.

The numerous authentication protocols [29,30,31] have defined security requirements in order to explain their security goals. Therefore, we also define the essential security requirements to explain and ensure our security goals.

Untraceability and anonymity. In a modern vehicular communication system, user’s real identity and location data are very sensitive information. For these reason, an adversary cannot trace a user’s location and know the user’s real identity to guarantee a privacy of user.
Secure mutual authentication. A secure mutual authentication is known for a essential security requirement in VANETs in order to guarantee that only the legitimate users should access the services and communicate securely with each other [32].
Confidentiality. In our system, the user, sink node, and vehicle sense can freely communicate among themselves through a internet. However, an adversary can try to obtain various pieces of information from users such as traffic congestion, speed, and vehicle accident because it is transmitted in a public channel. Therefore, a confidentiality must be guaranteed and the transmitted data is only known to legitimate user in order to ensure a security.

3. Review of Mohit et al.’s Scheme

In this section, we review Mohit et al.’s authentication protocol for WSNs, which consists of three phases: system setup, user registration, and user login and authentication. Table 1 presents the notations used in this paper.

3.1. System Setup Phase

When a driver wants to deploy a sensor in a vehicle, the registration authority (RA) registers the vehicle sensor in the network. In addition, RA stores various data on the vehicle such as the vehicle number, engine, battery, and insurance in a database.

3.2. User Registration Phase

If a new traffic manager

U_{i}

wants to register him or herself,

U_{i}

must send the registration request message to the sink node

S N_{j}

first. The user registration phase of Mohit et al.’s scheme is shown in Figure 2, and the detailed steps are described as follows.

Step 1:: $U_{i}$ chooses an identity $I D_{i}$ , password $P W_{i}$ , and random nonce $R N_{i}$ . $U_{i}$ then computes $H I D_{i} = h (I D_{i} | | R N_{i})$ , $H P W_{i} = h (P W_{i} | | R N_{i})$ and sends them to the sink node via a secure channel.
Step 2:: $S N_{j}$ selects a random nonce $R G_{i}$ and random number $q_{i}$ , and then $S N_{j}$ computes $A_{i} = h (H I D_{i} | | R G_{i})$ , $B_{i} = h (H I D_{i} | | H P W_{i} | | R G_{i})$ , $C_{i} = q_{i} \oplus H P W_{i}$ , and $D_{i} = C_{i} \oplus h (K_{s})$ . After that, $S N_{j}$ stores ${A_{i}, B_{i}, C_{i}, D_{i}, R G_{i}}$ in the smartcard and issues the smartcard to $U_{i}$ through a secure channel.
Step 3:: Upon receiving the smartcard, $U_{i}$ computes $H N_{i} = h (I D_{i} | | P W_{i}) \oplus R N_{i}$ and stores it in the smartcard. Ultimately, the smartcard contains ${A_{i}, B_{i}, C_{i}, D_{i}, R G_{i}, H N_{i}}$ .

3.3. User Login and Authentication Phase

If a user

U_{i}

wants to access the system,

U_{i}

must send the login request message to the sink node

S N_{j}

. After receiving the login request message from

U_{i}

S N_{j}

checks whether it is legitimate. If it is valid,

S N_{j}

performs the authentication phase. The user login and authentication phase of Mohit et al.’s scheme is shown in Figure 3. The detailed steps of this phase are described as follows.

Step 1:: $U_{i}$ inserts the smartcard into a card reader and inputs $I D_{i}$ and $P W_{i}$ . The smartcard then computes $R N_{i} = h (I D_{i} | | P W_{i}) \oplus H N_{i}$ , $H I D_{i} = h (I D_{i} | | R N_{i})$ , $H P W_{i} = h (P W_{i} | | R N_{i})$ , and $B_{i}^{*} = h (H I D_{i} | | H P W_{i} | | R G_{i})$ . Then, the smartcard checks whether $B_{i}^{*} \overset{?}{=} B_{i}$ . If it is equal, the smartcard computes $q_{i} = C_{i} \oplus H P W_{i}$ and generates a random nonce $N U_{i}$ . The smartcard also computes $M_{T S} = h (q_{i} | | B_{i} | | N U_{i})$ , $p_{1} = N U_{i} \oplus q_{i}$ , $p_{2} = I D_{k} \oplus h (p_{1} | | q_{i})$ and $E_{i} = D_{i} \oplus H P W_{i}$ . Finally, the smartcard sends the login request message ${M_{T S}, p_{1}, p_{2}, E_{i}}$ to $S N_{j}$ via a public channel.
Step 2:: After receiving the login request message from $U_{i}$ , $S N_{j}$ retrieves $q_{i} = E_{i} \oplus h (K_{s}), N U_{i} = p_{1} \oplus q_{i}$ and $I D_{k} = p_{2} \oplus h (p_{1} | | q_{i})$ . Then, $S N_{j}$ computes $M_{T S}^{*} = h (q_{i} | | B_{i} | | N U_{i})$ and checks whether $M_{T S}^{*}$ is equal to $M_{T S}$ . Then, $S N_{j}$ generates a random nonce $N S_{j}$ and computes $X_{k} = h (I D_{k} | | K_{s})$ , $M_{S V} = h (I D_{k} | | N S_{j} | | X_{k} | | I D_{j})$ , $d_{1} = N S_{j} \oplus h (I D_{k}), d_{2} = I D_{j} \oplus I D_{k}$ . Finally, $S N_{j}$ sends ${M_{S V}, d_{1}, d_{2}}$ to the vehicle sensor.
Step 3:: Upon receiving the message ${M_{S V}, d_{1}, d_{2}}$ , the vehicle sensor $V S_{k}$ retrieves $N S_{j} = d_{1} \oplus h (I D_{k})$ and $I D_{j} = d_{2} \oplus I D_{k}$ . Then, $V S_{k}$ checks the freshness of $N S_{j}$ . If it is fresh, $V S_{k}$ sends $I D_{k}$ and requests the sink node’s master key $X_{k}$ from $R A$ . After receiving $X_{k}$ from $R A$ through a secure channel, $V S_{k}$ computes $M_{S V}^{*} = h (I D_{k} | | N S_{j} | | X_{k} | | I D_{j})$ and checks whether $M_{S V}^{*} \overset{?}{=} M_{S V}$ . If it is verified, $V S_{k}$ chooses a random nonce $N V_{k}$ and computes $v = h (I D_{k} | | N S_{j} | | N V_{k})$ , $M_{V S} = h (X_{k} | | N S_{j} | | v)$ , and $t = N S_{j} \oplus N V_{k}$ . Finally, $V S_{k}$ sends ${M_{V S}, t}$ to $S N_{j}$ .
Step 4:: After receiving the message ${M_{V S}, t}$ , $S N_{j}$ retrieves $N V_{k} = t \oplus N S_{j}$ and computes $v = h (I D_{k} | | N S_{j} | | N V_{k}), M_{V S}^{*} = h (X_{k} | | N S_{j} | | v)$ . Then, $S N_{j}$ checks whether $M_{V S}^{*} \overset{?}{=} M_{V S}$ is correct. If it is correct, $S N_{j}$ computes $w = N S_{j} \oplus N U_{i}$ , $M_{S T} = h (q_{i} | | N U_{i} | | N S_{j} | | I D_{i} | | I D_{k})$ and sends ${M_{S T}, w}$ to $U_{i}$ .
Step 5:: Upon receiving the message ${M_{S T}, w}$ from $S N_{j}$ , $U_{i}$ retrieves $N S_{j} = w \oplus N U_{i}$ and computes $M_{S T}^{*} = h (q_{i} | | N U_{i} | | N S_{j} | | I D_{i} | | I D_{k})$ , and then $U_{i}$ checks whether $M_{S T}^{*} \overset{?}{=} h (q_{i} | | N U_{i} | | N S_{j} | | I D_{i} | | I D_{k})$ is correct. If they are equal, mutual authentication has been successfully achieved.

3.4. Password Change Phase

U_{i}

can freely update his or her password when desired. The password change phase is described in Figure 4 and the detailed steps of this phase are as follows.

Step 1:: $U_{i}$ inserts smartcard in the card reader and inputs the identity $I D_{i}^{*}$ and password $P W_{i}^{*}$ , and then $U_{i}$ submits ${I D_{i}^{*}, P W_{i}^{*}}$ to the card reader via a secure channel.
Step 2:: After receiving ${I D_{i}^{*}, P W_{i}^{*}}$ , the smartcard computes $R N_{i} = H N_{i} \oplus h (I D_{i}^{*} | | P W_{i}^{*})$ , $H I D_{i}^{*} = h (I D_{i}^{*} | | P W_{i}^{*})$ , $H P W_{i}^{*} = h (P W_{i}^{*} | | R N_{i})$ , and $B_{i}^{*} = h (H I D_{i}^{*} | | H P W_{i}^{*} | | R G_{i})$ . It checks whether $B_{i}^{*} \overset{?}{=} B_{i}$ . If this is verified, the smartcard sends the authentication message and requests a new password from $U_{i}$ . After receiving the authentication message from smartcard, $U_{i}$ inputs the new password $P W_{i}^{n e w}$ .
Step 3:: The smartcard calculates $H P W_{i}^{n e w} = h (P W_{i}^{n e w} | | R N_{i}^{*})$ , $H N_{i}^{n e w} = R N_{i} \oplus h (I D_{i}^{*} | | P W_{i}^{n e w})$ , $B_{i}^{n e w} = h (H I D_{i}^{*} | | H P W_{i}^{n e w} | | R G_{i})$ , $C_{i}^{n e w} = q_{i} \oplus H P W_{i}^{n e w}$ , and $D_{i}^{n e w} = D_{i} \oplus C_{i} \oplus C_{i}^{n e w}$ by using the new password of $U_{i}$ . Finally, smartcard replaces ${H N_{i}, B_{i}, C_{i}, D_{i}}$ with ${H N_{i}^{n e w}, B_{i}^{n e w}, C_{i}^{n e w}, D_{i}^{n e w}}$ .

4. Cryptanalysis of Mohit et al.’s Scheme

In this section, we discuss the security weaknesses of Mohit et al.’s scheme. They asserted that their scheme is secure against trace and impersonation attack, and they showed that their scheme can provide anonymity, session key security and secure mutual authentication. However, here we demonstrate that Mohit et al.’s scheme does not resist the following attacks.

4.1. Impersonation Attack

If an adversary

U_{a}

tries to impersonate a legitimate user,

U_{a}

can successfully generate a login request message of legitimate user

{M_{T S}, p_{1}, p_{2}, E_{i}}

. According to Section 1.1, we can assume that

U_{a}

obtains the smartcard of the legitimate user

U_{i}

and extracts the values

{B_{i}, C_{i}, D_{i}}

stored in smartcard and that

U_{a}

has the messages transmitted in the previous session. Here, we show that Mohit et al.’s scheme does not prevent an impersonation attack.

Step 1:: $U_{a}$ computes $H P W_{i} = D_{i} \oplus E_{i}$ , $q_{i} = C_{i} \oplus H P W_{i}$ , $N U_{i} = p_{1} \oplus q_{i}$ , $I D_{k} = p_{2} \oplus h (p_{1} | | q_{i})$ , and $M_{T S} = h (q_{i} | | B_{i} | | N U_{i})$ , where $E_{i}$ , $p_{1}$ , and $p_{2}$ are messages of the previous session.
Step 2:: $U_{a}$ can obtain the secret parameters $q_{i}$ , $B_{i}$ , and $H P W_{i}$ and a random nonce $N U_{i}$ . $U_{a}$ then chooses a random nonce $R U_{a}$ and computes $M_{T S a} = h (q_{i} | | B_{i} | | N U_{a})$ , $p_{1 a} = N U_{a} \oplus q_{i}$ , and $p_{2 a} = I D_{k} \oplus h (p_{1 a} | | q_{i})$ . Finally, $U_{a}$ generates the login request message ${M_{T S a}, p_{1 a}, p_{2 a}, E_{i}}$ and sends it to the sink node $S N_{j}$ .
Step 3:: After receiving the login request message from $U_{a}$ , $S N_{j}$ retrieves $q_{i} = E_{i} \oplus h (K_{s}), N U_{a} = p_{1 a} \oplus p 2_{2 a}$ , and $I D_{k} = p_{2 a} \oplus h (p_{1 a} | | q_{i})$ . $S N_{j}$ then computes $M_{T S}^{*} = h (q_{i} | | B_{i} | | N U_{a})$ and checks whether $M_{T S}^{*}$ is equal to $M_{T S a}$ . Then, $S N_{j}$ generates a random nonce $N S_{j 2}$ and computes $X_{k} = h (I D_{k} | | K_{s})$ , $M_{S V 2} = h (I D_{k} | | N S_{j 2} | | X_{k} | | I D_{j})$ , $d_{1} = N S_{j 2} \oplus h (I D_{k})$ , and $d_{2} = I D_{j 2} \oplus I D_{k}$ . Finally, $S N_{j}$ sends ${M_{S V 2}, d_{1}, d_{2}}$ to the vehicle sensor.
Step 4:: Upon receiving the message ${M_{S V 2}, d_{1}, d_{2}}$ , the vehicle sensor $V S_{k}$ retrieves $N S_{j 2} = d_{1} \oplus h (I D_{k})$ and $I D_{j} = d_{2} \oplus I D_{k}$ , and then $V S_{k}$ checks the freshness of $N S_{j 2}$ . If it is fresh, $V S_{k}$ sends $I D_{k}$ and requests the sink node’s master key $X_{k}$ from $R A$ . After receiving $X_{k}$ from $R A$ through a secure channel, $V S_{k}$ computes $M_{S V 2}^{*} = h (I D_{k} | | N S_{j 2} | | X_{k} | | I D_{j})$ and checks whether $M_{S V 2}^{*} \overset{?}{=} M_{S V 2}$ . If it is verified, $V S_{k}$ chooses a random nonce $N V_{k 2}$ and computes $v = h (I D_{k} | | N S_{j 2} | | N V_{k 2})$ , $M_{V S 2} = h (X_{k} | | N S_{j 2} | | v)$ , and $t = N S_{j 2} \oplus N V_{k 2}$ . Finally, $V S_{k}$ sends ${M_{V S 2}, t}$ to $S N_{j}$ .
Step 5:: After receiving the message ${M_{V S 2}, t}$ , $S N_{j}$ retrieves $N V_{k 2} = t \oplus N S_{j 2}$ and computes $v = h (I D_{k} | | N S_{j 2} | | N V_{k 2})$ and $M_{V S 2}^{*} = h (X_{k} | | N S_{j 2} | | v)$ . Then, $S N_{j}$ checks whether $M_{V S 2}^{*} \overset{?}{=} M_{S V 2}$ is correct. If it is correct, $S N_{j}$ computes $w = N S_{j 2} \oplus N U_{a}$ and $M_{S T 2} = h (q_{i} | | N U_{a} | | N S_{j 2} | | I D_{i} | | I D_{k})$ and sends ${M_{S T 2}, w}$ to $U_{a}$ .
Step 6:: Upon receiving the message ${M_{S T 2}, w}$ from $S N_{j}$ , $U_{a}$ successfully achieves mutual authentication.

Therefore, Mohit et al.’s scheme is vulnerable to impersonation attacks.

4.2. Trace Attack and Anonymity Preservation

According to Section 4.1, an adversary

U_{a}

can obtain the real identities of the vehicle sensor and sink node. First,

U_{a}

retrieves the vehicle sensor’s real identity

I D_{k} = p_{2} \oplus h (p_{1} | | q_{i})

and then computes

N S_{j} = d_{1} \oplus h (I D_{k})

. Finally,

U_{a}

retrieves the sink node’s real identity

I D_{j} = d_{2} \oplus I D_{k}

. For this reason, Mohit et al.’s scheme does not prevent trace attack or provide anonymity.

4.3. Mutual Authentication

In Section 4.1, we demonstrate that Mohit et al.’s scheme does not resist impersonation attacks. An adversary

U_{a}

can compute the login request message

{M_{T S}, p_{1}, p_{2}, E_{i}}

and successfully achieve mutual authentication with

V S_{k}

. In addition, the sink node

S N_{j}

cannot compute the authentication message

M_{S T} = h (q_{i} | | N U_{i} | | N S_{j} | | I D_{i} | | I D_{k})

in the login and authentication phase because

S N_{j}

does not know the real identity of

U_{i}

. Therefore, Mohit et al.’s scheme does not provide secure mutual authentication.

4.4. Session Key Security

Mohit et al. claimed that their scheme can provide session key security because an adversary cannot compute

M_{T S} = h (q_{i} | | B_{i} | | N U_{i})

. However, we demonstrate that an adversary can compute the value

M_{T S}

in Section 4.1. Therefore, Mohit et al.’s scheme cannot achieve session key security.

5. Proposed Protocol

In this section, we propose a secure authentication protocol for WSNs in vehicle communications to resolve the security problems of Mohit et al.’s scheme [23]. Our proposed scheme consists of four phases: system setup, user registration, login and authentication and password change. In our protocol, the system setup phase is equivalent to that of Mohit et al.’s scheme. The details of the other three phases are presented below.

5.1. User Registration Phase

When a new user

U_{i}

wants to first access the sink node as a traffic manager, he or she must first register with the sink node. The user registration phase of the proposed protocol is shown in Figure 5 and the detailed steps are as follows:

Step 1:: The user $U_{i}$ selects the identity $I D_{i}$ and password $P W_{i}$ and then generates a random number $a_{i}$ to computes $H P W_{i} = h (P W_{i} | | a_{i})$ . Then, $U_{i}$ sends ${I D_{i}, H P W_{i}}$ to the sink node $S N_{j}$ via a secure channel.
Step 2:: After receiving the registration request message from $U_{i}$ , $S N_{j}$ generates a random unique identity $T I D_{i}$ for $U_{i}$ and computes $X_{i} = h (I D_{i} | | K_{S}), A_{i} = X_{i} \oplus h (I D_{i} | | H P W_{i}), B_{i} = h (H P W_{i} | | X_{i})$ , and $C_{i} = X_{i} \oplus h (T I D_{i} | | K_{s})$ . After that, $S N_{j}$ stores ${A_{i}, B_{i}, T I D_{i}}$ in a smartcard, which it issues to $U_{i}$ through a secure channel. Finally, $S N_{j}$ stores ${T I D_{i}, C_{i}}$ in a database.
Step 3:: Upon receiving the smartcard from $S N_{j}$ , $U_{i}$ calculates $Q_{i} = h (I D_{i} | | P W_{i}) \oplus a_{i}$ and stores ${Q_{i}}$ in the smartcard. Consequently, $S N_{j}$ stores ${A_{i}, B_{i}, T I D_{i}, Q_{i}}$ in the smartcard.

5.2. Login and Authentication Phase

If a user

U_{i}

wants to access the sink node

S N_{j}

U_{i}

must send a login request message. The login and authentication phase of our scheme is shown in Figure 6 and the details of this phase are as follows.

Step 1:: $U_{i}$ inserts the smartcard and inputs the identity $I D_{i}$ and password $P W_{i}$ into a smartcard reader. Then, $U_{i}$ computes $a_{i} = h (I D_{i} | | P W_{i}) \oplus Q_{i}, H P W_{i} = h (P W_{i} | | a_{i}), X_{i} = h (I D_{i} | | H P W_{i}) \oplus A_{i}$ , and $B_{i}^{*} = h (H P W_{i} | | X_{i})$ and checks whether $B_{i}^{*} \overset{?}{=} B_{i}$ . If it is equal, $U_{i}$ generates a random nonce $R U_{i}$ and computes $M_{1} = R U_{i} \oplus X_{i}, M_{2} = I D_{k} \oplus h (X_{i} | | R U_{i}), C I D_{i} = I D_{i} \oplus h (T I D_{i} | | X_{i} | | R U_{i})$ , and $M_{T S} = h (I D_{i} | | X_{i} | | R U_{i})$ . $U_{i}$ sends the login request message ${M_{T S}, M_{1}, M_{2}, C I D_{i}, T I D_{i}}$ to $S N_{j}$ through a public channel.
Step 2:: After receiving the login request message from $U_{i}$ , $S N_{j}$ retrieves $C_{i}$ matched with $T I D_{i}$ in a database. Then, $S N_{j}$ computes $X_{i} = C_{i} \oplus h (T I D_{i} | | K_{S}), R U_{i} = M_{1} \oplus X_{i}, I D_{i} = C I D_{i} \oplus h (T I D_{i} | | X_{i} | | R U_{i}), I D_{k} = M_{2} \oplus h (X_{i} | | R U_{i})$ , and $M_{T S}^{*} = h (I D_{i} | | X_{i} | | R U_{i})$ and checks whether $M_{T S}^{*} \overset{?}{=} M_{T S}$ . If it is correct, $S N_{j}$ generates a random nonce $R S_{j}$ and computes $X_{k} = h (I D_{k} | | K_{S}), M_{S V} = h (I D_{k} | | I D_{j} | | X_{k} | | R S_{j}), M_{3} = R S_{j} \oplus h (I D_{j} | | X_{k})$ , and $M_{4} = I D_{k} \oplus I D_{j}$ . $S N_{j}$ also sends the authentication request message ${M_{S V}, M_{3}, M_{4}}$ to $V S_{k}$ via a public channel.
Step 3:: Upon receiving the message ${M_{S V}, M_{3}, M_{4}}$ , $V S_{k}$ computes $I D_{j} = M_{4} \oplus I D_{k}$ and receives $X_{k}$ from $R A$ . Then, $V S_{k}$ computes $R S_{j} = M_{3} \oplus h (I D_{j} | | X_{k})$ and $M_{S V}^{*} = h (I D_{k} | | I D_{j} | | X_{k} | | R S_{j})$ and checks whether $M_{S V}^{*} \overset{?}{=} M_{S V}$ . If they are equal, $V S_{k}$ generates a random nonce $R V_{k}$ and computes $v_{i} = h (I D_{k} | | R S_{j} | | R V_{K}), M_{V S} = h (X_{k} | | R S_{j} | | v_{i})$ , and $t = R S_{j} \oplus R V_{k}$ . Finally, $V S_{k}$ sends ${M_{V S}, t}$ to $S N_{j}$ through a public channel.
Step 4:: After receiving the message ${M_{V S}, t}$ from $V S_{k}$ , $S N_{j}$ computes $R V_{k} = t \oplus R S_{j}, v_{i} = h (I D_{k} | | R S_{j} | | R V_{k})$ and $M_{V S}^{*} = h (X_{k} | | R S_{j} | | v_{i})$ . Then, $S N_{j}$ checks whether $M_{V S}^{*} \overset{?}{=} M_{V S}$ . If it is equal, $S N_{j}$ computes $n = R S_{j} \oplus R U_{i}$ and $m = R V_{k} \oplus R U_{i}$ . After that, $S N_{j}$ generates a new random unique identity $T I D_{i}^{n e w}$ and computes $M_{5} = T I D_{i}^{n e w} \oplus h (R S_{j} | | R V_{k})$ and $M_{S T} = h (R U_{i} | | R S_{j} | | R V_{k} | | I D_{k} | | I D_{i})$ . $S N_{j}$ also sends the message ${M_{S T}, M_{5}, n, m}$ to $U_{i}$ via an open channel.
Step 5:: Upon receiving the message ${M_{S T}, M_{5}, n, m}$ , $U_{i}$ computes $R S_{j} = n \oplus R U_{i}, R V_{k} = m \oplus R U_{i}, T I D_{i}^{n e w} = M_{5} \oplus h (R S_{j} | | R V_{k})$ , and $M_{S T}^{*} = h (R U_{i} | | R S_{j} | | R V_{k} | | I D_{k} | | I D_{i})$ . Then, $U_{i}$ checks whether $M_{S T}^{*} \overset{?}{=} M_{S T}$ . If it is equal, $U_{i}$ updates $T I D_{i}$ to $T I D_{i}^{n e w}$ . Finally, $U_{i}$ computes $M_{6} = h (I D_{i} | | R U_{i} | | R S_{j})$ and sends the confirmation message ${M_{6}}$ to $S N_{j}$ .
Step 6:: After receiving the message ${M_{6}}$ from $U_{i}$ , $S N_{j}$ computes $M_{6}^{*} = h (I D_{i} | | R U_{i} | | R S_{j})$ and $C_{i}^{*} = X_{i} \oplus h (T I D_{i}^{n e w} | | K_{S})$ . Then, $S N_{j}$ checks whether $M_{6}^{*} \overset{?}{=} M_{6}$ . If it is valid, $S N_{j}$ replaces ${T I D_{i}, C_{i}}$ with ${T I D_{i}^{n e w}, C_{i}^{*}}$ .

5.3. Password Change Phase

In our proposed protocol,

U_{i}

can change the password when desired without the help of the sink node

S N_{j}

. The password change phase is shown in Figure 7 and the detailed steps of this phase are presented below:

Step 1:: $U_{i}$ inserts his or her smartcard into a card reader and inputs the identity $I D_{i}$ and old password $P W_{i}^{*}$ .
Step 2:: $S C$ computes $a_{i}^{*} = h (I D_{i}^{*} | | P W_{i}^{*}) \oplus Q_{i}, H P W_{i}^{*} = h (P W_{i}^{*} | | a_{i}^{*}), X_{i}^{*} = h (I D_{i}^{*} | | H P W_{i}^{*}) \oplus A_{i}$ , and $B_{i}^{*} = h (H P W_{i}^{*} | | X_{i}^{*})$ . Then, $S C$ compares the computed $B_{i}^{*}$ with the stored $B_{i}$ in its memory. If it is valid, $S C$ sends an authentication message to $U_{i}$ .
Step 3:: On receiving the message from the smartcard, $U_{i}$ inserts the new password $P W_{i}^{n e w}$ in the smartcard.
Step 4:: Using the new password $P W_{i}^{n e w}$ , $S C$ computes $Q_{i}^{n e w} = h (I D_{i}^{*} | | P W_{i}^{n e w}) \oplus a_{i}^{*}, H P W_{i}^{n e w} = h (P W_{i}^{n e w} | | a_{i}^{*}), A_{i}^{n e w} = X_{i}^{*} \oplus h (I D_{i}^{*} | | H P W_{i}^{n e w}), B_{i}^{n e w} = h (H P W_{i}^{n e w} | | X_{i}^{*})$ , and $C_{i}^{n e w} = X_{i}^{*} \oplus h (T I D_{i} | | K_{s})$ . Finally, the smartcard replaces the old information with ${A_{i}^{n e w}, B_{i}^{n e w}, C_{i}^{n e w}, Q_{i}^{n e w}}$ .

6. Security Analysis

In this section, we use the Burrow–Abadi–Needham (BAN) logic [28], which is a broadly accepted formal security model, to carry out an analysis and prove that our protocol can provide secure mutual authentication. We also demonstrate that our proposed protocol can resist various attacks through an informal security analysis, which is based on Section 1.1.

6.1. Informal Security Analysis

We present an informal security analysis of our proposed scheme to show that it prevents trace, impersonation, and replay attacks. In addition, we demonstrate that our protocol can achieve mutual authentication and anonymity.

6.1.1. Impersonation Attack

If an adversary

U_{a}

tries to impersonate a legitimate user

U_{i}

U_{a}

must generate a login request message

{M_{T S}, M_{1}, M_{2}, C I D_{i}, T I D_{i}}

and response message

{M_{6}}

successfully. However,

U_{a}

cannot generate these because

U_{a}

cannot know the real identity of

U_{i}

and secret parameters

X_{i}, R U_{i}

, and

K_{S}

. In addition,

U_{a}

does not retrieve a random nonce

R U_{i}

from

M_{1}

. Therefore, our protocol resists impersonation attacks because

U_{a}

cannot generate valid messages.

6.1.2. Trace Attack and Anonymity

In the login and authentication phase of our protocol, an adversary

U_{a}

cannot trace a legitimate user

U_{i}

or vehicle

V S_{k}

because all transmitted messages are changed every session. In addition,

U_{i}

sends the dynamic identity

C I D_{i} = I D_{i} \oplus h (T I D_{i} | | X_{i} | | R U_{i})

and

T I D_{i}

to the sink node, and the identity of

V S_{k}

is also included in

M_{4} = I D_{k} \oplus I D_{j}

. In other words, to obtain the record of a user’s movement and real identity, an adversary must know the user’s real identity

I D_{i}

, secret parameter

X_{i}

, and random nonces

R U_{i}

R S_{j}

, and

R V_{k}

. For these reasons, our protocol provides the anonymity and is secure against trace attacks.

6.1.3. Smartcard Stolen Attack

According to Section 1.1, we assume that an adversary

U_{a}

can obtain a smartcard and extract the parameters

{A_{i}, B_{i}, T I D_{i}, Q_{i}}

. However,

U_{a}

cannot obtain any sensitive user information without

I D_{i}

and

P W_{i}

because the parameters stored in smartcards are masked in

X_{i} = h (I D_{i} | | K_{S})

A_{i} = X_{i} \oplus h (I D_{i} | | H P W_{i})

B_{i} = h (H P W_{i} | | X_{i})

C_{i} = X_{i} \oplus h (T I D_{i} | | K_{S})

, and

Q_{i} = h (I D_{i} | | P W_{i}) \oplus a_{i}

by the hash function and XOR operation. Consequently, our proposed protocol prevents smartcard stolen attack.

6.1.4. Replay Attack

According to Section 1.1, we suppose that adversary

U_{a}

tries to impersonate a legitimate user

U_{i}

by resending messages transmitted in the previous session,

U_{a}

cannot impersonate

U_{i}

successfully. In our scheme, the sink node

S N_{j}

checks whether a random nonce is fresh or not. If a random nonce value

R U_{i}

is not fresh,

S N_{j}

rejects the login request message. In addition,

U_{a}

cannot generate the confirmation message

M_{6}

successfully because

U_{a}

cannot obtain the random nonce

R S_{j}

generated by

S N_{j}

. Therefore, the proposed protocol is secure against replay attacks.

6.1.5. Secure Mutual Authentication

When receiving the login message

{M_{T S}, M_{1}, M_{2}, C I D_{i}, T I D_{i}}

and confirmation message

{M_{6}}

from

U_{i}

, the sink node

S N_{j}

checks whether

M_{T S}

and

M_{6}

are correct. In addition,

S N_{j}

retrieves

X_{i}

from a database to validate

M_{T S}

. If this is correct,

S N_{j}

authenticates

U_{i}

. After receiving

{M_{V S}, t}

from

V S_{k}

, the sink node checks whether

M_{S V} = h (I D_{k} | | R S_{j} | | R V_{k})

is valid. If it is valid,

S N_{j}

authenticates

V S_{k}

. Finally, the user

U_{i}

checks whether the received value

M_{S T} = h (R U_{i} | | R S_{j} | | R V_{k} | | I D_{k} | | I D_{i})

is correct. If it is correct,

U_{i}

authenticates

S N_{j}

. Therefore, all entities authenticate each other successfully because an adversary cannot know the important parameters discussed in Section 6.1.1 and Section 6.1.2.

According to Section 6.1.2 and Section 6.1.5, all transmitted messages are changed every session and an adversary cannot obtain user’s sensitive information. Therefore, we achieve essential security requirement into untraceability, anonymity, secure mutual authentication and confidentiality. Furthermore, secure mutual authentication is proved in Section 6.2 using BAN logic.

6.2. Security Analysis Using BAN Logic

To prove the secure mutual authentication of our protocol, we perform an analysis with the BAN logic [28], which is a widely accepted formal security model. First, we define the notation of the BAN logic in Table 2. Then, we describe the logical postulates of the BAN logic in Section 6.2.1. Next, we present the goals, idealized form, and initial assumptions of our protocol. Finally, we demonstrate that our protocol achieves secure mutual authentication between

U_{i}

and

V K_{k}

by using the BAN logic.

6.2.1. Postulates of BAN Logic

The postulates of the BAN logic are given below:

1.: Message meaning rule :

$\frac{P | \equiv P \overset{K}{\leftrightarrow} Q, P ⊲ {\{X\}}_{K}}{P |\equiv Q| \sim X},$
2.: Nonce verification rule :

$\frac{P |\equiv # (X), P| \equiv Q | \sim X}{P |\equiv Q| \equiv X},$
3.: Jurisdiction rule :

$\frac{P |\equiv Q| ⟹ X, P |\equiv Q| \equiv X}{P | \equiv X},$
4.: Freshness rule :

$\frac{P | \equiv # (X)}{P | \equiv # (X, Y)},$
5.: Belief rule :

$\frac{P | \equiv (X, Y)}{P | \equiv X} .$

6.2.2. Goals

We have the following goals to prove the secure mutual authentication of our proposed protocol:

Goal 1:: $U_{i} ∣ \equiv (R S_{j}, R V_{k}),$
Goal 2:: $U_{i} ∣ \equiv S N_{j} ∣ \equiv (R S_{j}, R V_{k}),$
Goal 3:: $S N_{j} ∣ \equiv (R U_{i}),$
Goal 4:: $S N_{j} ∣ \equiv U_{i} ∣ \equiv (R U_{i}),$
Goal 5:: $S N_{j} ∣ \equiv (R V_{k}),$
Goal 6:: $S N_{j} ∣ \equiv V S_{k} ∣ \equiv (R V_{k}) .$

6.2.3. Idealized Forms

The idealized forms of the transmitted messages are given below:

Msg₁:: $U_{i} \to S N_{j}$ : ${(I D_{i}, I D_{k}, T I D_{i}, R U_{i})}_{X_{i}},$
Msg₂:: $S N_{j} \to V S_{k}$ : ${(I D_{i}, I D_{k}, R U_{i})}_{X_{k}},$
Msg₃:: $V S_{k} \to S N_{j}$ : ${(I D_{k}, R S_{j}, R V_{k})}_{X_{k}},$
Msg₄:: $S N_{j} \to U_{i}$ : $({I D_{k}, T I D_{i}^{n e w}, R U_{i}, R S_{j}, R V_{k})}_{I D_{i}},$
Msg₅:: $U_{i} \to S N_{j}$ : $({R U_{i}, R S_{j})}_{I D_{i}} .$

6.2.4. Assumptions

We make the following initial assumptions to perform the BAN logic proof:

A₁:: $U_{i} ∣ \equiv (U_{i} \overset{X_{i}}{⟷} S N_{j}),$
A₂:: $S N_{j} ∣ \equiv (U_{i} \overset{X_{i}}{⟷} S N_{j}),$
A₃:: $V S_{k} ∣ \equiv (V S_{k} \overset{X_{k}}{⟷} S N_{j}),$
A₄:: $S N_{j} ∣ \equiv (V S_{k} \overset{X_{k}}{⟷} S N_{j}),$
A₅:: $S N_{j} ∣ \equiv # (R U_{i}),$
A₆:: $V S_{k} ∣ \equiv # (R S_{j}),$
A₇:: $S N_{j} ∣ \equiv # (R V_{k}),$
A₈:: $U_{i} ∣ \equiv # (R S_{j}),$
A₉:: $U_{i} ∣ \equiv (U_{i} \overset{I D_{i}}{⟷} S N_{j}),$
A₁₀:: $U_{i} ∣ \equiv S N_{j} \Rightarrow (R S_{j}, R V_{k}),$
A₁₁:: $S N_{j} ∣ \equiv U_{i} \Rightarrow (R U_{i}),$
A₁₂:: $S N_{j} ∣ \equiv V S_{k} \Rightarrow (R V_{k}) .$

6.2.5. Proof Using BAN Logic

The detailed steps of the main proof are as follows:

Step 1:: According to $M s g_{1}$ , we can obtain

$S_{1} : S N_{j} ⊲ {(I D_{i}, I D_{k}, T I D_{i}, R U_{i})}_{X_{i}} .$
Step 2:: In conformity with the message meaning rule with $S_{1}$ and $A_{2}$ , we can get

$S_{2} : S N_{j} ∣ \equiv U_{i} \sim {(I D_{i}, I D_{k}, T I D_{i}, R U_{i})}_{X_{i}} .$
Step 3:: According to the freshness rule with $A_{5}$ , we can get

$S_{3} : S N_{j} ∣ \equiv # {(I D_{i}, I D_{k}, T I D_{i}, R U_{i})}_{X_{i}} .$
Step 4:: According to the nonce verification rule with $S_{2}$ and $S_{3}$ , we can obtain

$S_{4} : S N_{j} ∣ \equiv U_{i} ∣ \equiv {(I D_{i}, I D_{k}, T I D_{i}, R U_{i})}_{X_{i}} .$
Step 5:: According to $M s g_{2}$ , we can get

$S_{5} : V S_{k} ⊲ {(I D_{i}, I D_{k}, R U_{i})}_{X_{k}} .$
Step 6:: In conformity with the message meaning rule with $S_{5}$ and $A_{3}$ , we can get

$S_{6} : V S_{k} ∣ \equiv S N_{j} \sim {(I D_{i}, I D_{k}, R U_{i})}_{X_{k}} .$
Step 7:: According to the freshness rule with $A_{6}$ , we can obtain

$S_{7} : V S_{k} ∣ \equiv # {(I D_{i}, I D_{k}, R U_{i})}_{X_{k}} .$
Step 8:: According to the nonce verification rule with $S_{6}$ and $S_{7}$ , we can get

$S_{8} : V S_{k} ∣ \equiv S N_{j} ∣ \equiv {(I D_{i}, I D_{k}, R U_{i})}_{X_{k}} .$
Step 9:: According to $M s g_{3}$ , we can obtain

$S_{9} : S N_{j} ⊲ {(I D_{k}, R S_{j}, R V_{k})}_{X_{k}} .$
Step 10:: In conformity with the message meaning rule with $S_{9}$ and $A_{4}$ , we can obtain

$S_{10} : S N_{j} ∣ \equiv V S_{k} \sim {(I D_{k}, R S_{j}, R V_{k})}_{X_{k}} .$
Step 11:: According to the freshness rule with $A_{7}$ , we can get

$S_{11} : S N_{j} ∣ \equiv # {(I D_{k}, R S_{j}, R V_{k})}_{X_{k}} .$
Step 12:: According to the nonce verification rule with $S_{10}$ and $S_{11}$ , we can get

$S_{12} : S N_{j} ∣ \equiv V S_{k} ∣ \equiv {(I D_{k}, R S_{j}, R V_{k})}_{X_{k}} .$
Step 13:: According to $M s g_{4}$ , we can obtain

$S_{13} : U_{i} ⊲ ({I D_{k}, T I D_{i}^{n e w}, R U_{i}, R S_{j}, R V_{k})}_{I D_{i}} .$
Step 14:: In conformity with the message meaning rule with $S_{13}$ and $A_{9}$ , we can get

$S_{14} : U_{i} ∣ \equiv S N_{j} \sim ({I D_{k}, T I D_{i}^{n e w}, R U_{i}, R S_{j}, R V_{k})}_{I D_{i}} .$
Step 15:: According to the freshness rule with $A_{8}$ , we can get

$S_{15} : U_{i} ∣ \equiv # ({I D_{k}, T I D_{i}^{n e w}, R U_{i}, R S_{j}, R V_{k})}_{I D_{i}} .$
Step 16:: According to the nonce verification rule with $S_{14}$ and $S_{15}$ , we can get

$S_{16} : I D_{i} ∣ \equiv S N_{j} ∣ \equiv ({I D_{k}, T I D_{i}^{n e w}, R U_{i}, R S_{j}, R V_{k})}_{I D_{i}} .$
Step 17:: According to the belief rule with $S_{16}$ , we can get

$S_{17} : U_{i} ∣ \equiv S N_{j} ∣ \equiv (R S_{j}, R V_{k}) . (Goal 2)$
Step 18:: In conformity with the jurisdiction rule with $S_{17}$ and $A_{10}$ , we can obtain

$S_{18} : U_{i} ∣ \equiv (R S_{j}, R V_{k}) . (Goal 1)$
Step 19:: In conformity with the belief rule with $S_{4}$ , we can get

$S_{19} : S N_{j} ∣ \equiv U_{i} ∣ \equiv (R U_{i}) . (Goal 4)$
Step 20:: According the jurisdiction rule with $S_{19}$ and $A_{11}$ , we can obtain

$S_{20} : S N_{j} ∣ \equiv (R U_{i}) . (Goal 3)$
Step 21:: In conformity with the belief rule with $S_{12}$ , we can get

$S_{21} : S N_{j} ∣ \equiv V S_{k} ∣ \equiv (R V_{k}) . (Goal 6)$
Step 22:: According the jurisdiction rule with $S_{19}$ and $A_{11}$ , we can obtain

$S_{20} : S N_{j} ∣ \equiv (R V_{k}) . (Goal 5)$

Based on goals 1–6, we prove that our proposed protocol achieves secure mutual authentication between

U_{i}

and

V S_{k}

7. Security Analysis Using the AVISPA Tool

In this section, we perform a formal security verification of our protocol with the widely accepted Automated Validation of Internet Security Protocols and Applications (AVISPA) simulation tool [33,34]. Formal security verification with this tool has received much attention and has been used in numerous studies to demonstrate that various authentication protocols are secure against replay and man-in-the-middle attacks [35,36,37,38,39].

With AVISPA, the security protocol must be implemented by using the High Level Protocols Specification Language (HLPSL) [40]. The HLPSL specifications of the security protocol are translated to an intermediate format (IF) by the HLPSLIF translator. Finally, it is converted to the output format (OF) with the On-the-fly Model-Checker (OFMC) [41], the CL-based Attack Searcher (AtSe) [42], SAT-based Model-Checker (SATMC), or Tree Automata-based Protocol Analyzer (TA4SP).

7.1. HLPSL Specifications

According to HLPSL, the proposed protocol has three entities, which are called

r o l e

u s e r

denotes a user

U A

s i n k n o d e

denotes a sink node

S N

, and

v e h i c l e s e n s e

denotes a vehicle sense

V S

. The

s e s s i o n

and

e n v i r o n m e n t

also contain the security goals, as shown in Figure 8. The role specifications of

U_{i}

are shown in Figure 9 and the details are as follows.

When

U_{i}

receives the start message,

U A

changes the state value 0 to 1. Then,

U A

sends the registration request

{I D_{i}, H P W_{i}}

S N

via a secure channel and receives the smartcard from

S N

. After that,

U A

updates the state from 1 to 2. During the login and authentication phase,

U A

sends the login message

{M_{t s}, M_{1}, M_{2}, C I D_{i}, T I D_{i}}

S N

via a public channel. Then,

U A

declares

w i t n e s s (U A, S N, u a_s n_r u i, R U_{i}^{'})

, which means that it generates a random nonce

R U_{i}

. After generating

R U_{i}

U A

receives the message

{M_{s t}, M_{5}, n, m}

from

S N

and updates the state from 2 to 3. Finally,

U A

sends

{M_{6}}

S N

through a public channel and

S N

authenticates

U A

by using a random nonce

R U_{i}

. Similarly, the simulated results of

S N

and

V S

are defined as shown in Figure 10 and Figure 11.

7.2. Analysis of Simulation Results

In this section, we present the results of the AVISPA analysis using OFMC and CL-AtSe back-ends to ensure the security of our protocol, as shown in Figure 12. To estimate the security against replay attack, the OFMC and CL-AtSe back-ends check whether a legitimate entity can execute the protocol by searching for a passive adversary. Moreover, the OFMC and CL-AtSe back-ends also check whether the proposed protocol is secure against the man-in-the-middle attack for the DY model checking.

The OFMC back-end has a search time of 1.17 seconds to visit 130 nodes, and the CL-AtSe back-end analyzes two states with a translation time of 0.12 seconds. Because the replay attack and Dolev–Yao model checking are performed successfully, the proposed protocol is safe against replay and man-in-the-middle attacks.

8. Performance Analysis

In this section, we compare the computation and communication costs of our proposed protocol with those of related protocols [3,15,16,23,43,44] and discuss the security properties.

8.1. Computation Cost

We compare the computation overheads of our protocol with those of related protocols [3,15,16,23,43,44]. For the comparison of computation cost, we define the notations as follows.

T_{h}

T_{S}

, and

T_{M}

denote the times for hash operation (≈0.0005 s), symmetric key cryptographic operation (≈0.0087 s) and elliptic curve scalar point multiplication operation (≈0.0630 s), respectively. The analysis results are presented in Table 3.

We use the existing computation analysis results of Mohit et al. [23] for a rough evaluation. We do not include the XOR operation because it is negligible compared with the other operations. The results show that our protocol needs

8 T_{h}

for the user,

13 T_{h}

for the sink node, and

4 T_{h}

for the sensor. Thus, total cost of our protocol is 0.0125 seconds. Even though this is slightly higher than the cost for Mohit et al.’s protocol, the difference is negligible, and the proposed protocol provides better security than other protocols. Therefore, our protocol is secure and suitable for practical WSNs environments.

8.2. Security Properties

Table 4 compares the security properties of our proposed protocol compared with other related protocols. The existing related schemes clearly cannot resist various attacks, and their protocols cannot achieve anonymity and mutual authentication. For these reasons, our protocol provides better security features than the other protocols [3,15,16,23,43,44].

8.3. Communication Cost

Finally, we analyze the communication cost of our scheme with related protocols. For the communication analysis, we assume that a random nonce (number) and timestamp are 64 bits, a pseudo-identity is 160 bits, the SHA-1 hash digest [45] is 160 bits, elliptic curve scalar multiplication is 512 bits, and symmetric key cryptographic operation is 256 bits. In the login and authentication phase of our protocol, the transmitted messages

{M_{T S}, M_{1}, M_{2}, C I D_{i}, T I D_{i}}, {M_{S V}, M_{3}, M_{4}}, {M_{V S}, t}, {M_{S T}, M_{5}, n, m,}, a n d {M_{6}}

require

(160 + 64 + 64 + 160 + 160 = 608

bits),

(160 + 64 + 64 = 288

bits),

(160 + 64 = 224

bits),

(160 + 160 + 64 + 64 = 448

bits) and 160 bits, respectively. Consequently, the total communication cost is

(608 + 288 + 224 + 448 + 160 = 1728

bits). Table 5 presents the results of this analysis. Even though our protocol has a higher communication cost than Mohit et al.’s scheme, the vehicle sense sends only 224 bits, which is similar to that of their scheme. Therefore, from the perspective of limited resources, the proposed scheme is sufficiently applicable to WSN environments.

9. Conclusions

In this paper, we demonstrate that Mohit et al.’s scheme does not resist the impersonation and trace attacks. We also show that it does not achieve secure mutual authentication, session key security, and anonymity. We propose a secure authentication protocol for WSNs in vehicular communications to resolve the security problems of their scheme. The proposed protocol is secure against impersonation, replay, smartcard stolen and trace attacks and can achieve secure mutual authentication and anonymity by using dynamic values for the transmitted messages that change every session. We also prove that our protocol can provide secure mutual authentication between

U_{i}

S N_{j}

and

V S_{k}

by using BAN logic and we present a formal security verification using the AVISPA tool. Furthermore, we compare the performance and security functionalities with those of other related protocols. Therefore, the proposed protocol can be efficiently applied to practical vehicle communications systems.

Author Contributions

Conceptualization, S.Y.; Formal Analysis, K.P.; Project Administration, Y.P.; Software, J.L.; Supervision, Y.P.; Writing—Original Draft, S.Y.; Writing—Review and Editing, K.L., K.P. and Y.P.

Funding

This work was supported by the Basic Science Research Program through the National Research Foundation of Korea funded by the Ministry of Science, ICT and Future Planning under Grant 2017R1A2B1002147 and in part by the BK21 Plus project funded by the Ministry of Education, Korea under Grant 21A20131600011.

Acknowledgments

The authors would like to thank the anonymous reviewers and the Associate Editor for their valuable feedback on the paper, which helped us to improve its quality and presentation.

Conflicts of Interest

The authors declare no conflict of interest.

References

Chatterjee, K.; De, A.; Gupta, D. A secure and efficient authentication protocol in wireless sensor network. Wirel. Pers. Commun. 2015, 81, 17–37. [Google Scholar] [CrossRef]
Kim, J.; Lee, D.; Jeon, D.; Lee, Y.; Won, D. Security anaylsis and improvements two-factor mutual authentication with key agreement in wireless sensor networks. Sensors 2014, 14, 6443–6462. [Google Scholar] [CrossRef] [PubMed]
Kumari, S.; Om, H. Authentication protocol for wireless sensor networks applications like safety monitoring in coal mines. Comput. Netw. 2016, 104, 137–154. [Google Scholar] [CrossRef]
Wang, D.; Wang, P. On the anonymity of two-factor authentication schemes for wireless sensor networks. Comput. Netw. 2014, 73, 41–57. [Google Scholar] [CrossRef]
Park, Y.; Park, Y. Three-factor user authentication and key agreement using elliptic curve cryptosystem in wireless sensor networks. Sensors 2016, 16, 2123. [Google Scholar] [CrossRef] [PubMed]
Jiang, Q.; MA, P.F.; Lu, X.; Tian, Y.L. An efficient two-factor user authentication scheme with unlinkability for wireless sensor networks. Peer-to-Peer Netw. Appl. 2015, 8, 1070–1081. [Google Scholar] [CrossRef]
Amin, R.; Biswas, G.P. A secure light weight scheme for user authentication and key agreement in multi-gateway based wireless sensor networks. Ad Hoc Netw. 2016, 36, 58–80. [Google Scholar] [CrossRef]
Amin, R.; Hafizul Islam, S.K.; Biswas, G.P.; Khan, M.K.; Leng, L.; Kumar, N. Design of an anonymity preserving three-factor authenticated key exchange protocol for wireless sensor networks. Comput. Netw. 2016, 101, 42–62. [Google Scholar] [CrossRef]
Wong, K.H.; Zheng, Y.; Cao, J.; Wang, S. A dynamic user authentication scheme for wireless sensor networks. In Proceedings of the 2006 IEEE International Conference on Sensor Networks, Ubiquitous, and Trustworthy Computing (SUTC’06), Taichung, Taiwan, 5–7 June 2006; Volume 1, pp. 1–8. [Google Scholar]
Das, M.L. Two-factor user authentication in wireless sensor networks. IEEE Trans. Wirel. Commun. 2009, 8, 1086–1090. [Google Scholar] [CrossRef]
Chen, T.H.; Shih, W.K. A robust mutual authentication protocol for wireless sensor networks. ETRI J. 2010, 32, 704–712. [Google Scholar] [CrossRef]
Khan, M.K.; Alghathbar, K. Cryptanalysis and security improvements of two-factor user authentication in wireless sensor networks. Sensors 2010, 10, 2450–2459. [Google Scholar] [CrossRef] [PubMed]
Yeh, H.L.; Chen, T.H.; Liu, P.C.; Kim, T.H.; Wei, H.W. A secured authentication protocol for wireless sensor networks using elliptic curves cryptography. Sensors 2011, 11, 4767–4779. [Google Scholar] [CrossRef] [PubMed]
Han, W. Weakness of a Secured Authentication Protocol for Wireless Sensor Networks Using Elliptic Curves Cryptography. IACR Cryptol. ePrint Arch. 2011, 2011, 293. [Google Scholar]
Shi, W.; Gong, P. A new user authentication protocol for wireless sensor networks using elliptic curves cryptography. Int. J. Sens. Netw. 2013, 2013, 730831. [Google Scholar] [CrossRef]
Choi, Y.; Lee, D.; Kim, J.; Nam, J.; Won, D. Security enhanced user authentication protocol for wireless sensor networks using elliptic curves cryptography. Sensors 2014, 14, 10081–10106. [Google Scholar] [CrossRef] [PubMed]
Zhang, C.; Lin, X.; Lu, R.; Ho, P.H. RAISE: An efficient RSU-aided message authentication scheme in vehicular communication networks. In Proceedings of the 2008 IEEE International Conference on Communications, Beijing, China, 19–23 May 2008; pp. 1–7. [Google Scholar]
Zhang, C.; Lin, X.; Lu, R.; Ho, P.H.; Shen, S. An Efficient Message Authentication Scheme for Vehicular Communications. IEEE Trans. Veh. Technol. 2008, 57, 3357–3368. [Google Scholar] [CrossRef] [Green Version]
Lu, R.; Lin, X.; Zhu, H.; Ho, P.H.; Shen, X. ECPP: Efficient conditional privacy preservation protocol for secure vehicular communications. In Proceedings of the 2008 IEEE INFOCOM Conference on Computer Communications, Phoenix, AZ, USA, 13–18 April 2008; pp. 1–9. [Google Scholar]
Huang, D.; Misra, S.; Verma, M.; Xue, G. PACP: An efficient pseudonymous authentication-based conditional privacy protocol for VANETs. IEEE Trans. Intell. Transp. Syst. 2011, 12, 736–746. [Google Scholar] [CrossRef]
Chuang, M.C.; Lee, J.F. Team: Trust-extended authentication mechanism for vehicular ad hoc networks. IEEE Syst. J. 2014, 8, 749–758. [Google Scholar] [CrossRef]
Kumari, S.; Karuppiah, M.; Li, X.; Wu, F.; Das, A.K.; Odelu, V. An enhanced and secure trust-extended authentication mechanism for vehicular ad-hoc networks. Secur. Commun. Netw. 2016, 9, 4255–4271. [Google Scholar] [CrossRef]
Mohit, P.; Amin, R.; Biswas, G. Design of authentication protocol for wireless sensor network-based smart vehicular system. Veh. Commun. 2017, 9, 64–71. [Google Scholar] [CrossRef]
Alshaer, H.; Elmirghani, J.M. Road safety based on efficient vehicular broadcast communications. In Proceedings of the 2009 IEEE Intelligent Vehicles Symposium, Xian, China, 3–5 June 2009; pp. 1155–1160. [Google Scholar]
Alshaer, H. Securing vehicular ad-hoc networks connectivity with roadside units support. In Proceedings of the 2015 IEEE 8th GCC Conference & Exhibition, Muscat, Oman, 1–4 February 2015; pp. 1–6. [Google Scholar]
Dolev, D.; Yao, A.C. On the security of public key protocols. IEEE Trans. Inf. Theory 1983, 29, 198–208. [Google Scholar] [CrossRef] [Green Version]
Kocher, P.; Jaffe, J.; Jun, B. Differential power analysis. In Advances in Cryptology; Springer Science+Business Media: Berlin, Germany; New York, NY, USA, 1999; pp. 388–397. [Google Scholar]
Burrows, M.; Abadi, M.; Needham, R. A logic of authentication. ACM Trans. Comput. Syst. 1990, 8, 18–36. [Google Scholar] [CrossRef]
Zhang, L.; Wu, Q.; Domingo-Ferrer, J.; Qin, B.; Hu, C. Distributed Aggregate Privacy-Preserving Authentication in VANETs. IEEE Trans. Intell. Transp. Syst. 2016, 18, 516–526. [Google Scholar] [CrossRef]
Zhang, L.; Wu, Q.; Solanas, A.; Domingo-Ferrer, J. A Scalable Robust Authentication Protocol for Secure Vehicular Communications. IEEE Trans. Veh. Technol. 2009, 59, 1606–1617. [Google Scholar] [CrossRef]
Liu, J.; Li, J.; Zhang, L.; Dai, F.; Zhang, Y.; Meng, X.; Shen, J. Secure intelligent traffic light control using fog computing. Future Gener. Comput. Syst. 2018, 78, 817–824. [Google Scholar] [CrossRef]
Riley, M.; Akkaya, K.; Fong, K. A survey of authentication schemes for vehicular ad hoc networks. Secur. Commun. Netw. 2011, 4, 1137–1152. [Google Scholar] [CrossRef]
AVISPA. Automated Validation of Internet Security Protocols and Applications. Available online: http://www.avispa-project.org/ (accessed on 4 July 2018).
SPAN: A Security Protocol Animator for AVISPA. Available online: http://www.avispa-project.org/ (accessed on 4 July 2018).
Park, K.S.; Park, Y.H.; Park, Y.H.; Reddy, A.G.; Das, A.K. Provably secure and efficient authentication protocol for roaming service in global mobility networks. IEEE Access 2017, 5, 25110–25125. [Google Scholar] [CrossRef]
Odelu, V.; Das, A.K.; Choo, K.R.; Kumar, N.; Park, Y.H. Efficient and secure time-key based single sign-on authentication for mobile devices. IEEE Access 2017, 5, 27707–27721. [Google Scholar] [CrossRef]
Odelu, V.; Das, A.K.; Kumari, S.; Huang, X.; Wazid, M. Provably secure authenticated key agreement scheme for distributed mobile cloud computing services. Futuer Generat. Comput. Syst. 2017, 68, 74–88. [Google Scholar] [CrossRef]
Park, K.S.; Park, Y.H.; Park, Y.H.; Das, A.K. 2PAKEP: Provably Secure and Efficient Two-Party Authenticated Key Exchange Protocol for Mobile Environment. IEEE Access 2018, 6, 30225–30241. [Google Scholar] [CrossRef]
Banerjee, S.; Odelu, V.; Das, A.K.; Chattopadhyay, S.; Kumar, N.; Park, Y.H.; Tanwar, S. Design of an Anonymity-Preserving Group Formation Based Authentication Protocol in Global Mobility Networks. IEEE Access 2018, 6, 20673–20693. [Google Scholar] [CrossRef]
Von Oheimb, D. The high-level protocol specification language HLPSL developed in the EU project avispa. In Proceedings of the APPSEM 2005 Workshop, Tallinn, Finland, 13–15 September 2005; pp. 1–2. [Google Scholar]
Basin, D.; Modersheim, S.; Vigano, L. OFMC: A symbolic model checker for security protocols. Int. J. Inf. Secur. 2005, 4, 181–208. [Google Scholar] [CrossRef] [Green Version]
Turuani, M. The CL-Atse porotocol analyser. In Proceedings of the International Coneference on Rewriting Techniques and Applications (RTA), Seattle, WA, USA, 12–14 August 2006; pp. 227–286. [Google Scholar]
He, D.; Kumar, N.; Chen, J.; Lee, C.C.; Chilamkurti, N.; Yeo, S.S. Robust anonymous authentication protocol for health-care applications using wireless medical sensor networks. Multimed. Syst. 2015, 21, 49–60. [Google Scholar] [CrossRef]
Xue, K.; Ma, C.; Hong, P.; Ding, R. A temporal credential based mutual authentication and key agreement scheme for wireless sensor networks. J. Netw. Comput. Appl. 2013, 36, 316–323. [Google Scholar] [CrossRef]
FIPS PUB 180-4: Secure Hash Standard (SHS). Available online: https://nvlpubs.nist.gov/nistpubs/FIPS/NIST.FIPS.180-4.pdf (accessd on 23 July 2018).

Figure 1. Vehicular communications system model.

Figure 2. User registration phase of the Mohit et al.’s scheme.

Figure 3. User login and authentication phase of the Mohit et al.’s scheme.

Figure 4. Password change phase of the Mohit et al.’s scheme.

Figure 5. User registration phase of the proposed scheme.

Figure 6. User login and authentication phase of the proposed scheme.

Figure 7. Password change phase of the proposed scheme.

Figure 8. Role specification for session and environment.

Figure 9. Role specification for user

U A

Figure 9. Role specification for user

U A

Figure 10. Role specification for

V S

Figure 10. Role specification for

V S

Figure 11. Role specification for

S N

Figure 11. Role specification for

S N

Figure 12. The result of analysis using OFMC and CL-AtSe

Table 1. Notations.

Notation	Description
$I D_{i}$	Identity of user
$I D_{j}$	Identity of sink node
$I D_{k}$	Identity of vehicle sensor
$P W_{i}$	Password of user
$R A$	Registration authority
$a_{i}$	Random number by user
$R U_{i}$	Random nonce by user
$R S_{j}$	Random nonce by sink node
$R V_{k}$	Random nonce by vehicle sensor
$K_{S}$	Master key of sink node
$T I D_{i}$	Unique temporary identity of user
$h (\cdot)$	One-way hash function
⊕	Bitwise XOR operation
$\| \|$	Concatenation operation

Table 2. Notations of the BAN logic.

Notation	Description
$P \| \equiv X$	Pbelieves the statement X
#X	The statement X is fresh
$P ⊲ X$	Psees the statement X
$P \| \sim X$	P once said X
$P \Rightarrow X$	Pcontrols the statement X
$< X >_{Y}$	Formula X is combined with the formula Y
${X}_{K}$	Formula X is encrypted by the key K
$P \overset{K}{\leftrightarrow} Q$	P and Q communicate using K as the shared key
$S K$	Session key used in the current authentication session

Table 3. Computation cost of our proposed scheme with other related schemes.

Schemes	User	Sink Node	Sensor	Total Cost	Total Cost (s)
Shi et al. [15]	$5 T_{h} + 3 T_{M}$	$3 T_{h} + 2 T_{M}$	$4 T_{h} + T_{M}$	$12 T_{h} + 6 T_{M}$	0.3840
Choi et al. [16]	$12 T_{h} + 3 T_{M}$	$5 T_{h} + T_{M}$	$7 T_{h} + 2 T_{M}$	$24 T_{h} + 6 T_{M}$	0.3900
He et al. [43]	$4 T_{h} + 2 T_{s}$	$2 T_{h} + 5 T_{s}$	$T_{h} + 2 T_{s}$	$7 T_{h} + 9 T_{s}$	0.0818
Xue et al. [44]	$10 T_{h}$	$14 T_{h}$	$6 T_{h}$	$30 T_{h}$	0.0150
Kumari and Om [3]	$10 T_{h}$	$8 T_{h}$	$6 T_{h}$	$24 T_{h}$	0.0120
Mohit et al. [23]	$7 T_{h}$	$9 T_{h}$	$4 T_{h}$	$20 T_{h}$	0.0100
Ours	$8 T_{h}$	$13 T_{h}$	$4 T_{h}$	$25 T_{h}$	0.0125

T_{h}

: One-way hash operation,

T_{s}

: Symmetric key cryptographic operation,

T_{M}

: Elliptic curve scalar point multiplication operation.

Table 4. Security properties of our proposed scheme with other related schemes.

Security Property	Shi et al. [15]	Choi et al. [16]	He et al. [43]	Xue et al. [44]	Kumari and Om [3]	Mohit et al. [23]	Ours
Impersonation attack	∘	∘	∘	∘	×	×	∘
Smartcard stolen attack	×	∘	∘	∘	∘	×	∘
Password change attack	∘	×	×	×	∘	∘	∘
Replay attack	∘	∘	∘	∘	∘	∘	∘
Trace attack	×	×	×	×	×	×	∘
Anonymity	×	×	∘	×	×	×	∘
Mutual authentication	∘	∘	∘	∘	×	×	∘

∘: preserves the security properties, ×: does not preserve the security properties.

Table 5. Communication cost of our proposed scheme with other related schemes.

Schemes	Communication Cost
Shi et al. [15]	3968 bits
Choi et al. [16]	3584 bits
He et al. [43]	1216 bits
Xue et al. [44]	1920 bits
Kumari and Om [3]	2048 bits
Mohit et al. [23]	1280 bits
Ours	1728 bits

© 2018 by the authors. Licensee MDPI, Basel, Switzerland. This article is an open access article distributed under the terms and conditions of the Creative Commons Attribution (CC BY) license (http://creativecommons.org/licenses/by/4.0/).

Share and Cite

MDPI and ACS Style

Yu, S.; Lee, J.; Lee, K.; Park, K.; Park, Y. Secure Authentication Protocol for Wireless Sensor Networks in Vehicular Communications. Sensors 2018, 18, 3191. https://doi.org/10.3390/s18103191

AMA Style

Yu S, Lee J, Lee K, Park K, Park Y. Secure Authentication Protocol for Wireless Sensor Networks in Vehicular Communications. Sensors. 2018; 18(10):3191. https://doi.org/10.3390/s18103191

Chicago/Turabian Style

Yu, SungJin, JoonYoung Lee, KyungKeun Lee, KiSung Park, and YoungHo Park. 2018. "Secure Authentication Protocol for Wireless Sensor Networks in Vehicular Communications" Sensors 18, no. 10: 3191. https://doi.org/10.3390/s18103191

APA Style

Yu, S., Lee, J., Lee, K., Park, K., & Park, Y. (2018). Secure Authentication Protocol for Wireless Sensor Networks in Vehicular Communications. Sensors, 18(10), 3191. https://doi.org/10.3390/s18103191

Note that from the first issue of 2016, this journal uses article numbers instead of page numbers. See further details here.

Article Menu

Secure Authentication Protocol for Wireless Sensor Networks in Vehicular Communications

Abstract

1. Introduction

1.1. Threat Model

1.2. Our Contributions

1.3. Paper Outline

2. System Model

3. Review of Mohit et al.’s Scheme

3.1. System Setup Phase

3.2. User Registration Phase

3.3. User Login and Authentication Phase

3.4. Password Change Phase

4. Cryptanalysis of Mohit et al.’s Scheme

4.1. Impersonation Attack

4.2. Trace Attack and Anonymity Preservation

4.3. Mutual Authentication

4.4. Session Key Security

5. Proposed Protocol

5.1. User Registration Phase

5.2. Login and Authentication Phase

5.3. Password Change Phase

6. Security Analysis

6.1. Informal Security Analysis

6.1.1. Impersonation Attack

6.1.2. Trace Attack and Anonymity

6.1.3. Smartcard Stolen Attack

6.1.4. Replay Attack

6.1.5. Secure Mutual Authentication

6.2. Security Analysis Using BAN Logic

6.2.1. Postulates of BAN Logic

6.2.2. Goals

6.2.3. Idealized Forms

6.2.4. Assumptions

6.2.5. Proof Using BAN Logic

7. Security Analysis Using the AVISPA Tool

7.1. HLPSL Specifications

7.2. Analysis of Simulation Results

8. Performance Analysis

8.1. Computation Cost

8.2. Security Properties

8.3. Communication Cost

9. Conclusions

Author Contributions

Funding

Acknowledgments

Conflicts of Interest

References

Share and Cite

Article Metrics

Article Access Statistics

Further Information

Guidelines

MDPI Initiatives

Follow MDPI