Secure Authentication Protocol for Wireless Sensor Networks in Vehicular Communications

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.

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. 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
$RA$	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
$TI{D}_i$	Unique temporary identity of user
$h(·)$	One-way hash function
⊕	Bitwise XOR operation
$\left|\right|$	Concatenation operation

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 $HI{D}_i=h(I{D}_i\left|\right|R{N}_i)$, $HP{W}_i=h(P{W}_i\left|\right|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(HI{D}_i\left|\right|R{G}_i)$, $B_i=h(HI{D}_i\left|\right|HP{W}_i\left|\right|R{G}_i)$, $C_i=q_i\oplus HP{W}_i$, and $D_i=C_i\oplus h\left(K_s\right)$. 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\left|\right|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\left|\right|P{W}_i)\oplus H{N}_i$, $HI{D}_i=h(I{D}_i\left|\right|R{N}_i)$, $HP{W}_i=h(P{W}_i\left|\right|R{N}_i)$, and $B_i^{*}=h(HI{D}_i\left|\right|HP{W}_i\left|\right|R{G}_i)$. Then, the smartcard checks whether $B_i^{*}\stackrel{?}{=}{B}_i$. If it is equal, the smartcard computes $q_i=C_i\oplus HP{W}_i$ and generates a random nonce $N{U}_i$. The smartcard also computes $M_{TS}=h(q_i\left|\right|B_i\left|\right|N{U}_i)$, $p_1=N{U}_i\oplus q_i$, $p_2=I{D}_k\oplus h(p_1\left|\right|q_i)$ and $E_i=D_i\oplus HP{W}_i$. Finally, the smartcard sends the login request message $\{M_{TS},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\left(K_s\right),N{U}_i=p_1\oplus q_i$ and $I{D}_k=p_2\oplus h(p_1\left|\right|q_i)$. Then, $S{N}_j$ computes $M_{TS}^{*}=h(q_i\left|\right|B_i\left|\right|N{U}_i)$ and checks whether $M_{TS}^{*}$ is equal to $M_{TS}$. Then, $S{N}_j$ generates a random nonce $N{S}_j$ and computes $X_k=h(I{D}_k\left|\right|K_s)$, $M_{SV}=h(I{D}_k\left|\right|N{S}_j\left|\right|X_k\left|\right|I{D}_j)$, $d_1=N{S}_j\oplus h\left(I{D}_k\right),d_2=I{D}_j\oplus I{D}_k$. Finally, $S{N}_j$ sends $\{M_{SV},d_1,d_2\}$ to the vehicle sensor.

Step 3:

Upon receiving the message $\{M_{SV},d_1,d_2\}$, the vehicle sensor $V{S}_k$ retrieves $N{S}_j=d_1\oplus h\left(I{D}_k\right)$ 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 $RA$. After receiving $X_k$ from $RA$ through a secure channel, $V{S}_k$ computes $M_{SV}^{*}=h(I{D}_k\left|\right|N{S}_j\left|\right|X_k\left|\right|I{D}_j)$ and checks whether $M_{SV}^{*}\stackrel{?}{=}{M}_{SV}$. If it is verified, $V{S}_k$ chooses a random nonce $N{V}_k$ and computes $v=h\left(I{D}_k\right|\left|N{S}_j\right|\left|N{V}_k\right)$, $M_{VS}=h(X_k\left|\right|N{S}_j\left|\right|v)$, and $t=N{S}_j\oplus N{V}_k$. Finally, $V{S}_k$ sends $\{M_{VS},t\}$ to $S{N}_j$.

Step 4:

After receiving the message $\{M_{VS},t\}$, $S{N}_j$ retrieves $N{V}_k=t\oplus N{S}_j$ and computes $v=h(I{D}_k\left|\right|N{S}_j\left|\right|N{V}_k),M_{VS}^{*}=h(X_k\left|\right|N{S}_j\left|\right|v)$. Then, $S{N}_j$ checks whether $M_{VS}^{*}\stackrel{?}{=}{M}_{VS}$ is correct. If it is correct, $S{N}_j$ computes $w=N{S}_j\oplus N{U}_i$, $M_{ST}=h(q_i\left|\right|N{U}_i\left|\right|N{S}_j\left|\right|I{D}_i\left|\right|I{D}_k)$ and sends $\{M_{ST},w\}$ to $U_i$.

Step 5:

Upon receiving the message $\{M_{ST},w\}$ from $S{N}_j$, $U_i$ retrieves $N{S}_j=w\oplus N{U}_i$ and computes $M_{ST}^{*}=h(q_i\left|\right|N{U}_i\left|\right|N{S}_j\left|\right|I{D}_i\left|\right|I{D}_k)$, and then $U_i$ checks whether $M_{ST}^{*}\stackrel{?}{=}h(q_i\left|\right|N{U}_i\left|\right|N{S}_j\left|\right|I{D}_i\left|\right|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^{*}\left|\right|P{W}_i^{*})$, $HI{D}_i^{*}=h(I{D}_i^{*}\left|\right|P{W}_i^{*})$, $HP{W}_i^{*}=h(P{W}_i^{*}\left|\right|R{N}_i)$, and $B_i^{*}=h(HI{D}_i^{*}\left|\right|HP{W}_i^{*}\left|\right|R{G}_i)$. It checks whether $B_i^{*}\stackrel{?}{=}{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^{new}$.

Step 3:

The smartcard calculates $HP{W}_i^{new}=h(P{W}_i^{new}\left|\right|R{N}_i^{*})$, $H{N}_i^{new}=R{N}_i\oplus h(I{D}_i^{*}\left|\right|P{W}_i^{new})$, $B_i^{new}=h(HI{D}_i^{*}\left|\right|HP{W}_i^{new}\left|\right|R{G}_i)$, $C_i^{new}=q_i\oplus HP{W}_i^{new}$, and $D_i^{new}=D_i\oplus C_i\oplus C_i^{new}$ by using the new password of $U_i$. Finally, smartcard replaces $\{H{N}_i,B_i,C_i,D_i\}$ with $\{H{N}_i^{new},B_i^{new},C_i^{new},D_i^{new}\}$.

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_{TS},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 $HP{W}_i=D_i\oplus E_i$, $q_i=C_i\oplus HP{W}_i$, $N{U}_i=p_1\oplus q_i$, $I{D}_k=p_2\oplus h(p_1\left|\right|q_i)$, and $M_{TS}=h(q_i\left|\right|B_i\left|\right|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 $HP{W}_i$ and a random nonce $N{U}_i$. $U_a$ then chooses a random nonce $R{U}_a$ and computes $M_{TSa}=h(q_i\left|\right|B_i\left|\right|N{U}_a)$, $p_{1a}=N{U}_a\oplus q_i$, and $p_{2a}=I{D}_k\oplus h(p_{1a}\left|\right|q_i)$. Finally, $U_a$ generates the login request message $\{M_{TSa},p_{1a},p_{2a},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\left(K_s\right),N{U}_a=p_{1a}\oplus p{2}_{2a}$, and $I{D}_k=p_{2a}\oplus h(p_{1a}\left|\right|q_i)$. $S{N}_j$ then computes $M_{TS}^{*}=h(q_i\left|\right|B_i\left|\right|N{U}_a)$ and checks whether $M_{TS}^{*}$ is equal to $M_{TSa}$. Then, $S{N}_j$ generates a random nonce $N{S}_{j2}$ and computes $X_k=h(I{D}_k\left|\right|K_s)$, $M_{SV2}=h(I{D}_k\left|\right|N{S}_{j2}\left|\right|X_k\left|\right|I{D}_j)$, $d_1=N{S}_{j2}\oplus h\left(I{D}_k\right)$, and $d_2=I{D}_{j2}\oplus I{D}_k$. Finally, $S{N}_j$ sends $\{M_{SV2},d_1,d_2\}$ to the vehicle sensor.

Step 4:

Upon receiving the message $\{M_{SV2},d_1,d_2\}$, the vehicle sensor $V{S}_k$ retrieves $N{S}_{j2}=d_1\oplus h\left(I{D}_k\right)$ and $I{D}_j=d_2\oplus I{D}_k$, and then $V{S}_k$ checks the freshness of $N{S}_{j2}$. If it is fresh, $V{S}_k$ sends $I{D}_k$ and requests the sink node’s master key $X_k$ from $RA$. After receiving $X_k$ from $RA$ through a secure channel, $V{S}_k$ computes $M_{SV2}^{*}=h(I{D}_k\left|\right|N{S}_{j2}\left|\right|X_k\left|\right|I{D}_j)$ and checks whether $M_{SV2}^{*}\stackrel{?}{=}{M}_{SV2}$. If it is verified, $V{S}_k$ chooses a random nonce $N{V}_{k2}$ and computes $v=h\left(I{D}_k\right|\left|N{S}_{j2}\right|\left|N{V}_{k2}\right)$, $M_{VS2}=h(X_k\left|\right|N{S}_{j2}\left|\right|v)$, and $t=N{S}_{j2}\oplus N{V}_{k2}$. Finally, $V{S}_k$ sends $\{M_{VS2},t\}$ to $S{N}_j$.

Step 5:

After receiving the message $\{M_{VS2},t\}$, $S{N}_j$ retrieves $N{V}_{k2}=t\oplus N{S}_{j2}$ and computes $v=h\left(I{D}_k\right|\left|N{S}_{j2}\right|\left|N{V}_{k2}\right)$ and $M_{VS2}^{*}=h(X_k\left|\right|N{S}_{j2}\left|\right|v)$. Then, $S{N}_j$ checks whether $M_{VS2}^{*}\stackrel{?}{=}{M}_{SV2}$ is correct. If it is correct, $S{N}_j$ computes $w=N{S}_{j2}\oplus N{U}_a$ and $M_{ST2}=h(q_i\left|\right|N{U}_a\left|\right|N{S}_{j2}\left|\right|I{D}_i\left|\right|I{D}_k)$ and sends $\{M_{ST2},w\}$ to $U_a$.

Step 6:

Upon receiving the message $\{M_{ST2},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\left|\right|q_i)$ and then computes $N{S}_j=d_1\oplus h\left(I{D}_k\right)$. 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_{TS},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_{ST}=h(q_i\left|\right|N{U}_i\left|\right|N{S}_j\left|\right|I{D}_i\left|\right|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_{TS}=h(q_i\left|\right|B_i\left|\right|N{U}_i)$. However, we demonstrate that an adversary can compute the value $M_{TS}$ 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 $HP{W}_i=h(P{W}_i\left|\right|a_i)$. Then, $U_i$ sends $\{I{D}_i,HP{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 $TI{D}_i$ for $U_i$ and computes $X_i=h(I{D}_i\left|\right|K_S),A_i=X_i\oplus h(I{D}_i\left|\right|HP{W}_i),B_i=h(HP{W}_i\left|\right|X_i)$, and $C_i=X_i\oplus h(TI{D}_i\left|\right|K_s)$. After that, $S{N}_j$ stores $\{A_i,B_i,TI{D}_i\}$ in a smartcard, which it issues to $U_i$ through a secure channel. Finally, $S{N}_j$ stores $\{TI{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\left|\right|P{W}_i)\oplus a_i$ and stores $\left\{Q_i\right\}$ in the smartcard. Consequently, $S{N}_j$ stores $\{A_i,B_i,TI{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\left|\right|P{W}_i)\oplus Q_i,HP{W}_i=h(P{W}_i\left|\right|a_i),X_i=h(I{D}_i\left|\right|HP{W}_i)\oplus A_i$, and $B_i^{*}=h(HP{W}_i\left|\right|X_i)$ and checks whether $B_i^{*}\stackrel{?}{=}{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\left|\right|R{U}_i),CI{D}_i=I{D}_i\oplus h(TI{D}_i\left|\right|X_i\left|\right|R{U}_i)$, and $M_{TS}=h(I{D}_i\left|\right|X_i\left|\right|R{U}_i)$. $U_i$ sends the login request message $\{M_{TS},M_1,M_2,CI{D}_i,TI{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 $TI{D}_i$ in a database. Then, $S{N}_j$ computes $X_i=C_i\oplus h(TI{D}_i\left|\right|K_S),R{U}_i=M_1\oplus X_i,I{D}_i=CI{D}_i\oplus h(TI{D}_i\left|\right|X_i\left|\right|R{U}_i),I{D}_k=M_2\oplus h(X_i\left|\right|R{U}_i)$, and $M_{TS}^{*}=h(I{D}_i\left|\right|X_i\left|\right|R{U}_i)$ and checks whether $M_{TS}^{*}\stackrel{?}{=}{M}_{TS}$. If it is correct, $S{N}_j$ generates a random nonce $R{S}_j$ and computes $X_k=h(I{D}_k\left|\right|K_S),M_{SV}=h(I{D}_k\left|\right|I{D}_j\left|\right|X_k\left|\right|R{S}_j),M_3=R{S}_j\oplus h(I{D}_j\left|\right|X_k)$, and $M_4=I{D}_k\oplus I{D}_j$. $S{N}_j$ also sends the authentication request message $\{M_{SV},M_3,M_4\}$ to $V{S}_k$ via a public channel.

Step 3:

Upon receiving the message $\{M_{SV},M_3,M_4\}$, $V{S}_k$ computes $I{D}_j=M_4\oplus I{D}_k$ and receives $X_k$ from $RA$. Then, $V{S}_k$ computes $R{S}_j=M_3\oplus h(I{D}_j\left|\right|X_k)$ and $M_{SV}^{*}=h(I{D}_k\left|\right|I{D}_j\left|\right|X_k\left|\right|R{S}_j)$ and checks whether $M_{SV}^{*}\stackrel{?}{=}{M}_{SV}$. If they are equal, $V{S}_k$ generates a random nonce $R{V}_k$ and computes $v_i=h(I{D}_k\left|\right|R{S}_j\left|\right|R{V}_K),M_{VS}=h(X_k\left|\right|R{S}_j\left|\right|v_i)$, and $t=R{S}_j\oplus R{V}_k$. Finally, $V{S}_k$ sends $\{M_{VS},t\}$ to $S{N}_j$ through a public channel.

Step 4:

After receiving the message $\{M_{VS},t\}$ from $V{S}_k$, $S{N}_j$ computes $R{V}_k=t\oplus R{S}_j,v_i=h(I{D}_k\left|\right|R{S}_j\left|\right|R{V}_k)$ and $M_{VS}^{*}=h(X_k\left|\right|R{S}_j\left|\right|v_i)$. Then, $S{N}_j$ checks whether $M_{VS}^{*}\stackrel{?}{=}{M}_{VS}$. 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 $TI{D}_i^{new}$ and computes $M_5=TI{D}_i^{new}\oplus h(R{S}_j\left|\right|R{V}_k)$ and $M_{ST}=h(R{U}_i\left|\right|R{S}_j\left|\right|R{V}_k\left|\right|I{D}_k\left|\right|I{D}_i)$. $S{N}_j$ also sends the message $\{M_{ST},M_5,n,m\}$ to $U_i$ via an open channel.

Step 5:

Upon receiving the message $\{M_{ST},M_5,n,m\}$, $U_i$ computes $R{S}_j=n\oplus R{U}_i,R{V}_k=m\oplus R{U}_i,TI{D}_i^{new}=M_5\oplus h(R{S}_j\left|\right|R{V}_k)$, and $M_{ST}^{*}=h(R{U}_i\left|\right|R{S}_j\left|\right|R{V}_k\left|\right|I{D}_k\left|\right|I{D}_i)$. Then, $U_i$ checks whether $M_{ST}^{*}\stackrel{?}{=}{M}_{ST}$. If it is equal, $U_i$ updates $TI{D}_i$ to $TI{D}_i^{new}$. Finally, $U_i$ computes $M_6=h(I{D}_i\left|\right|R{U}_i\left|\right|R{S}_j)$ and sends the confirmation message $\left\{M_6\right\}$ to $S{N}_j$.

Step 6:

After receiving the message $\left\{M_6\right\}$ from $U_i$, $S{N}_j$ computes $M_6^{*}=h(I{D}_i\left|\right|R{U}_i\left|\right|R{S}_j)$ and $C_i^{*}=X_i\oplus h(TI{D}_i^{new}\left|\right|K_S)$. Then, $S{N}_j$ checks whether $M_6^{*}\stackrel{?}{=}{M}_6$. If it is valid, $S{N}_j$ replaces $\{TI{D}_i,C_i\}$ with $\{TI{D}_i^{new},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:

$SC$ computes $a_i^{*}=h(I{D}_i^{*}\left|\right|P{W}_i^{*})\oplus Q_i,HP{W}_i^{*}=h(P{W}_i^{*}\left|\right|a_i^{*}),X_i^{*}=h(I{D}_i^{*}\left|\right|HP{W}_i^{*})\oplus A_i$, and $B_i^{*}=h(HP{W}_i^{*}\left|\right|X_i^{*})$. Then, $SC$ compares the computed $B_i^{*}$ with the stored $B_i$ in its memory. If it is valid, $SC$ 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^{new}$ in the smartcard.

Step 4:

Using the new password $P{W}_i^{new}$, $SC$ computes $Q_i^{new}=h(I{D}_i^{*}\left|\right|P{W}_i^{new})\oplus a_i^{*},HP{W}_i^{new}=h(P{W}_i^{new}\left|\right|a_i^{*}),A_i^{new}=X_i^{*}\oplus h(I{D}_i^{*}\left|\right|HP{W}_i^{new}),B_i^{new}=h(HP{W}_i^{new}\left|\right|X_i^{*})$, and $C_i^{new}=X_i^{*}\oplus h(TI{D}_i\left|\right|K_s)$. Finally, the smartcard replaces the old information with $\{A_i^{new},B_i^{new},C_i^{new},Q_i^{new}\}$.

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_{TS},M_1,M_2,CI{D}_i,TI{D}_i\}$ and response message $\left\{M_6\right\}$ 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 $CI{D}_i=I{D}_i\oplus h(TI{D}_i\left|\right|X_i\left|\right|R{U}_i)$ and $TI{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,TI{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\left|\right|K_S)$, $A_i=X_i\oplus h(I{D}_i\left|\right|HP{W}_i)$, $B_i=h(HP{W}_i\left|\right|X_i)$, $C_i=X_i\oplus h(TI{D}_i\left|\right|K_S)$, and $Q_i=h(I{D}_i\left|\right|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_{TS},M_1,M_2,CI{D}_i,TI{D}_i\}$ and confirmation message $\left\{M_6\right\}$ from $U_i$, the sink node $S{N}_j$ checks whether $M_{TS}$ and $M_6$ are correct. In addition, $S{N}_j$ retrieves $X_i$ from a database to validate $M_{TS}$. If this is correct, $S{N}_j$ authenticates $U_i$. After receiving $\{M_{VS},t\}$ from $V{S}_k$, the sink node checks whether $M_{SV}=h(I{D}_k\left|\right|R{S}_j\left|\right|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_{ST}=h(R{U}_i\left|\right|R{S}_j\left|\right|R{V}_k\left|\right|I{D}_k\left|\right|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. 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
${\left\{X\right\}}_K$	Formula X is encrypted by the key K
$P\stackrel{K}{\leftrightarrow }Q$	P and Q communicate using K as the shared key
$SK$	Session key used in the current authentication session

. 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\stackrel{K}{\leftrightarrow }Q,P⊲{\left\{X\right\}}_K}{P\left|\equiv Q\right|\sim X},$$

2. 

Nonce verification rule :

$$\frac{P\left|\equiv \#\left(X\right),P\right|\equiv Q|\sim X}{P\left|\equiv Q\right|\equiv X},$$

3. 

Jurisdiction rule :

$$\frac{P\left|\equiv Q\right|⟹X,P\left|\equiv Q\right|\equiv X}{P|\equiv X},$$

4. 

Freshness rule :

$$\frac{P|\equiv \#(X)}{P|\equiv \#\left(X,Y\right)},$$

5. 

Belief rule :

$$\frac{P|\equiv \left(X,Y\right)}{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\mid \equiv (R{S}_j,R{V}_k),$

Goal 2:

$U_i\mid \equiv S{N}_j\mid \equiv (R{S}_j,R{V}_k),$

Goal 3:

$S{N}_j\mid \equiv \left(R{U}_i\right),$

Goal 4:

$S{N}_j\mid \equiv U_i\mid \equiv \left(R{U}_i\right),$

Goal 5:

$S{N}_j\mid \equiv \left(R{V}_k\right),$

Goal 6:

$S{N}_j\mid \equiv V{S}_k\mid \equiv \left(R{V}_k\right).$

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,TI{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,TI{D}_i^{new},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\mid \equiv (U_i\stackrel{X_i}{⟷}S{N}_j),$

A₂:

$S{N}_j\mid \equiv (U_i\stackrel{X_i}{⟷}S{N}_j),$

A₃:

$V{S}_k\mid \equiv (V{S}_k\stackrel{X_k}{⟷}S{N}_j),$

A₄:

$S{N}_j\mid \equiv (V{S}_k\stackrel{X_k}{⟷}S{N}_j),$

A₅:

$S{N}_j\mid \equiv \#\left(R{U}_i\right),$

A₆:

$V{S}_k\mid \equiv \#\left(R{S}_j\right),$

A₇:

$S{N}_j\mid \equiv \#\left(R{V}_k\right),$

A₈:

$U_i\mid \equiv \#\left(R{S}_j\right),$

A₉:

$U_i\mid \equiv (U_i\stackrel{I{D}_i}{⟷}S{N}_j),$

A₁₀:

$U_i\mid \equiv S{N}_j\Rightarrow (R{S}_j,R{V}_k),$

A₁₁:

$S{N}_j\mid \equiv U_i\Rightarrow \left(R{U}_i\right),$

A₁₂:

$S{N}_j\mid \equiv V{S}_k\Rightarrow \left(R{V}_k\right).$

6.2.5. Proof Using BAN Logic

The detailed steps of the main proof are as follows:

Step 1:

According to $Ms{g}_1$, we can obtain

$$S_1:S{N}_j⊲{(I{D}_i,I{D}_k,TI{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\mid \equiv U_i\sim {(I{D}_i,I{D}_k,TI{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\mid \equiv \#{(I{D}_i,I{D}_k,TI{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\mid \equiv U_i\mid \equiv {(I{D}_i,I{D}_k,TI{D}_i,R{U}_i)}_{X_i}.$$

Step 5:

According to $Ms{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\mid \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\mid \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\mid \equiv S{N}_j\mid \equiv {(I{D}_i,I{D}_k,R{U}_i)}_{X_k}.$$

Step 9:

According to $Ms{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\mid \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\mid \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\mid \equiv V{S}_k\mid \equiv {(I{D}_k,R{S}_j,R{V}_k)}_{X_k}.$$

Step 13:

According to $Ms{g}_4$, we can obtain

$$S_{13}:U_i⊲({I{D}_k,TI{D}_i^{new},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\mid \equiv S{N}_j\sim ({I{D}_k,TI{D}_i^{new},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\mid \equiv \#({I{D}_k,TI{D}_i^{new},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\mid \equiv S{N}_j\mid \equiv ({I{D}_k,TI{D}_i^{new},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\mid \equiv S{N}_j\mid \equiv (R{S}_j,R{V}_k).\left(\mathbf{Goal}\mathbf{2}\right)$$

Step 18:

In conformity with the jurisdiction rule with $S_{17}$ and $A_{10}$, we can obtain

$$S_{18}:U_i\mid \equiv (R{S}_j,R{V}_k).\left(\mathbf{Goal}\mathbf{1}\right)$$

Step 19:

In conformity with the belief rule with $S_4$, we can get

$$S_{19}:S{N}_j\mid \equiv U_i\mid \equiv \left(R{U}_i\right).\left(\mathbf{Goal}\mathbf{4}\right)$$

Step 20:

According the jurisdiction rule with $S_{19}$ and $A_{11}$, we can obtain

$$S_{20}:S{N}_j\mid \equiv \left(R{U}_i\right).\left(\mathbf{Goal}\mathbf{3}\right)$$

Step 21:

In conformity with the belief rule with $S_{12}$, we can get

$$S_{21}:S{N}_j\mid \equiv V{S}_k\mid \equiv \left(R{V}_k\right).\left(\mathbf{Goal}\mathbf{6}\right)$$

Step 22:

According the jurisdiction rule with $S_{19}$ and $A_{11}$, we can obtain

$$S_{20}:S{N}_j\mid \equiv \left(R{V}_k\right).\left(\mathbf{Goal}\mathbf{5}\right)$$

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 $role$: $user$ denotes a user $UA$, $sinknode$ denotes a sink node $SN$, and $vehiclesense$ denotes a vehicle sense $VS$. The $session$ and $environment$ 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, $UA$ changes the state value 0 to 1. Then, $UA$ sends the registration request $\{I{D}_i,HP{W}_i\}$ to $SN$ via a secure channel and receives the smartcard from $SN$. After that, $UA$ updates the state from 1 to 2. During the login and authentication phase, $UA$ sends the login message $\{M_{ts},M_1,M_2,CI{D}_i,TI{D}_i\}$ to $SN$ via a public channel. Then, $UA$ declares $witness(UA,SN,ua\_sn\_rui,R{U}_i^{\prime })$, which means that it generates a random nonce $R{U}_i$. After generating $R{U}_i$, $UA$ receives the message $\{M_{st},M_5,n,m\}$ from $SN$ and updates the state from 2 to 3. Finally, $UA$ sends $\left\{M_6\right\}$ to $SN$ through a public channel and $SN$ authenticates $UA$ by using a random nonce $R{U}_i$. Similarly, the simulated results of $SN$ and $VS$ 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. Computation cost of our proposed scheme with other related schemes.

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

$T_h$: One-way hash operation, $T_s$: Symmetric key cryptographic operation, $T_M$: Elliptic curve scalar point multiplication operation.

.

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 $8T_h$ for the user, $13T_h$ for the sink node, and $4T_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. 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.

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_{TS},M_1,M_2,CI{D}_i,TI{D}_i\},\{M_{SV},M_3,M_4\},\{M_{VS},t\},\{M_{ST},M_5,n,m,\},and\left\{M_6\right\}$ 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. 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

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.