# A Novel Secure Authentication Protocol for IoT and Cloud Servers

Authors: Ummer Iqbal; Aditya Tandon; Sonali Gupta; Arvind R. Yadav; Rahul Neware; Fraol Waldamichael Gelana
Journal: Wireless Communications and Mobile Computing
 (2022)

---

## Abstract

The integration of IoT with the cloud infrastructure is essential for designing smart applications. However, such integration may lead to security issues. Authentication and session key establishment is an essential security requirement for secure communication between IoT devices and cloud servers. For evaluating authentication key agreement schemes, the extended Canetti–Krawczyk (eCK) adversary model is regarded to be a more strict and relevant adversary model. Many schemes for authenticated key exchange between IoT devices and cloud servers have been proposed in the literature but have been assessed under Dolev and Yoa (DY) adversary model. Recently, Rostampour et al. introduced an ECC-based approach for enabling authentication between IoT devices and cloud servers that is secure and robust to various attacks under the Dolev and Yoa adversary model. In this paper, a detailed review and the automated security verification of the Rostampour et al. scheme are carried out under the eCK adversary model using Scyther-Compromise. The validation indicates that the scheme is not secure and is susceptible to various attacks under the eCK adversary model. To overcome the limitation of the Rostampour et al. scheme, a design of an ECC-based scheme for authentication between IoT devices and cloud servers under the eCK adversary model is proposed. The Scyther verification indicates that the scheme is safe under the eCK adversary model. The soundness of the correctness of the proposed scheme has been analyzed using BAN logic. Comparative analysis indicates that the scheme is resilient under the eCK adversary model with an energy overhead of 278.16 mJ for a resource constraint IoT device and a communication overhead of 1,408 bits.


---

## Body

## 1. Introduction

The internet of things (IoT) is a new network that provides numerous embedded devices to the Internet to share data. It is based on information and communication technologies. Embedded devices are becoming increasingly complicated as a result of the fast growth of technology, and they are employed in a broad variety of applications. The ability to relate such gadgets to huge resource pools, such as the cloud, is a significant advancement in modern technology. The integration of embedded devices and cloud servers enables the use of IoT in a wide range of commercial and government applications. However addressing the security issues, such as authentication and data privacy is important for the efficient integration of these two systems [1–3]. IoT has grown significantly over the years because of its relevance in smart applications. The internet of things (IoT) market was valued at USD 250.72 billion in 2019 and is expected to grow to USD 1,463.19 billion by 2027 [4]. This exponential advancement of IoT is governed by its role in developing applications that include smart parking, smart building, smart health, smart environment, smart agriculture, and smart homes [5, 6]. Smart parking can be employed for effective monitoring of parking areas in the city, and smart building applications can be used for monitoring the structural health of a building in terms of vibrations and material conditions. IoT can also be used for real-time motoring the health and the hydraulic parameters of the water bodies and effective monitoring of road conditions in terms of climate conditions [5]. In terms of security and emergency applications, IoT nodes can be deployed for unauthorized perimeter access, detection of harmful chemical and radiation leaks, and detection of gas leaks in industrial surroundings [6]. For smart agriculture, the nodes can be employed for monitoring soil quality, climate control in the greenhouse, and smart irrigation. The various applications in smart homes include surveillance, remote monitoring of appliances, energy, and water conservation. In the medical field, IoT can be employed for developing applications that include wireless body area networks, geriatric assistance, and automatic monitoring of medical freezers [5].A typical IoT-based smart application comprises a three-tier architecture that includes perception tier, network and server tier, and application tier [5, 7] as shown in Figure 1. The physical parameters are perceived in the perception layer using IoT devices, and the data perceived are further relayed to the server tier. The server tier serves as a communication backbone, employing different communication technologies [7]. As IoT applications generate a large volume of data, the server tier includes features for storing and processing it. A variety of servers, including mobile, web, and real-time communication servers, provide middleware support at the server tier. As the perception layer generates a very large volume of data, cloud servers can also be used at this layer for data storage and management. Various end-users connect to the server tier for offline and online data analysis in the user tier [8, 9]. The security of IoT-based smart applications is of paramount importance [10]. The communication between the server tier and client tier can be made secure using traditional security protocols. However, as IoT devices are resource-constrained, the communication between IoT devices in the perception tier and servers in the server tier becomes an emerging and active area of research [5].Figure 1
Three-tier architecture of IoT applications.Authentication and session key establishment are bedrock for all other security services between IoT nodes in the perception layer and the various servers in the server tier [11]. Many schemes have been suggested for securing communication between IoT devices and cloud servers. Liao and Hsiao [12] proposed a mutual authentication scheme with ID verifier protocol. However as indicated by [13], the scheme suffers from server impersonation attacks.Kalra and Sood [14] presented a mutual authentication scheme based on ECC. The scheme is resilient to various attacks. However, the scheme has design issues in terms of mutual authentication, insider, and traceability attacks. Chang et al. [15] pointed out the limitations of Kalra and Sood and highlighted its weakness in terms of mutual authentication and mistress of the session key. Chang et al. suggested an improved scheme that overcame the limitations of Kalra and Sood. Kumari et al. [16] pointed out the deficiencies of Kalra and Sood in terms of insider attacks, device anonymity, session key agreement, and mutual authentication. Kumari et al. also suggested an ECC-based scheme to overcome these limitations. Wang et al. [17] highlighted the deficiencies of the Chang et al. scheme in terms of impersonation attacks and suggested an improved scheme. Recently, Rostampour et al. [11] proposed an ECC-based scheme for authentication of IoT edge devices with the cloud server. Rostampour et al. made a detailed review of the schemes of Kalra and Sood, Chang et al., Kumari et al., and Wang et al. and highlighted their limitations. Rostampour et al. pointed out that all the existing schemes suffer from traceability attacks.When connecting an embedded system to the cloud, security is the main consideration. Mutual authentication must also be established between the cloud server and the embedded devices. To address these security concerns, many authentication systems for IoT and cloud servers have been developed. However, there are several faults in the existing approaches that must be addressed. When memory and power are limited and greater security with a low key length is required, elliptic curve cryptography (ECC) is the best public-key cryptography solution [18, 19]. The existing schemes presented in the literature have been analyzed under Dolev and Yoa (DY) [20, 21]. However, the eCK [22] adversary model is a more stringent model for authentication key agreement schemes [23]. In this paper, a detailed review of the Rostampour et al. scheme has been made. The Rostampour et al. scheme has been formally validated using Scyther-Compromise [24] under the eCK adversary model. Scyther-Compromise validation depicts that the Rostampour et al. scheme is not secure under the eCK adversary model. Furthermore, an improved scheme for authentication and key agreement between IoT devices and the server under the eCK adversary model has also been proposed.


### 1.1. Contributions

The major highlights of the paper are as follows:(a)
A review of the Rostampour et al. scheme has been made carried out. The scheme has been modeled on Scyther-Compromise and analyzed under the eCK adversary model.(b)
An ECC-based authentication scheme for IoT and cloud servers has been designed. The designed scheme provides better functionality and security specifications.(c)
The proposed scheme has been modeled on Scyther-Compromise. The results indicate that the scheme is safe under the eCK adversary model.(d)
The soundness and correctness of the proposed protocol have also been evaluated using BAN [25] logic.


### 1.2. Paper Organization

The remainder of the paper is laid out as follows. The preliminaries are presented in Section2. Section 3 reviews the Rostampour et al. scheme and discusses its formal security verification under the eCK adversary model. In Section 4, the design of the proposed ECC-based scheme for authentication between IoT devices and cloud servers is presented. In Section 5, an informal security analysis has been carried out. Section 6 provides the simulation details of formal security analysis using the Scyther under the eCK adversary model. In Section 7, security analysis using BAN logic has been carried out. Finally, Section 8 presents the comparison of the proposed scheme with other relevant schemes in terms of functional and security specifications.


## 1.1. Contributions

The major highlights of the paper are as follows:(a)
A review of the Rostampour et al. scheme has been made carried out. The scheme has been modeled on Scyther-Compromise and analyzed under the eCK adversary model.(b)
An ECC-based authentication scheme for IoT and cloud servers has been designed. The designed scheme provides better functionality and security specifications.(c)
The proposed scheme has been modeled on Scyther-Compromise. The results indicate that the scheme is safe under the eCK adversary model.(d)
The soundness and correctness of the proposed protocol have also been evaluated using BAN [25] logic.


## 1.2. Paper Organization

The remainder of the paper is laid out as follows. The preliminaries are presented in Section2. Section 3 reviews the Rostampour et al. scheme and discusses its formal security verification under the eCK adversary model. In Section 4, the design of the proposed ECC-based scheme for authentication between IoT devices and cloud servers is presented. In Section 5, an informal security analysis has been carried out. Section 6 provides the simulation details of formal security analysis using the Scyther under the eCK adversary model. In Section 7, security analysis using BAN logic has been carried out. Finally, Section 8 presents the comparison of the proposed scheme with other relevant schemes in terms of functional and security specifications.


## 2. Preliminaries

### 2.1. Notations

The notations used in the paper are tabulated in Table1.Table 1
Notations.
NotationMeaningEPa,bElliptical curveSServerDii-th IoT deviceIDiIdentity ofDiIDsIdentity ofSRiThe random number at the serverNiRandom number at the deviceXSPrivate key of SKIPrivate key ofDiSiEphemeral secret ofDiSsEphemeral secret ofSETExpiration timeGx,yGenerator point ofEPa,bSKSession key betweenS and DiHCollision resistant hash function⊕Xor operationP+QPoint additionX.GScalar multiplication


### 2.2. Adversary Model

An adversary model formulates the potential capabilities an attacker can have. Various adversary models exist that include Dolev and Yoa (DY) [20, 21], Canetti–Krawczyk (CK), and extended Canetti–Krawczyk models (eCK) models [22]. In all the models, the communication channel is completely insecure; however, they differ in their adversary query capabilities. In DY threat model, the communication parties are considered to be honest and can run multiple sessions with each other. The communication channel is completely insecure and totally under the adversary’s control, with the ability to record, delete, replay, redirect, rearrange, and completely control message schedule. The adversary can act as an active adversary in the middle and lead various man-in-the-middle attacks. The CK and eCK models are the most widely accepted models for authentication and key agreement protocols. In this adversary model, an attacker has abilities to compromise PRNG and get access to the secret randomness of the session. It is also assumed that an adversary can compromise the session and get access to it. An attacker can also get access to the long-term keys [26]. The major difference between the CK model and the eCK model is that in the eCK model, the adversary is capable of accessing ephemeral secrets, thus leading to an ephemeral-secret-key-leakage attack. An ephemeral key leakage indicates the weaknesses of a random number generator where the attacker can determine the randomness generated correctly with a high probability [26].


### 2.3. Elliptical Curve Cryptography

Koblitz [27] and Miller [28] introduced elliptical curve cryptography (ECC). ECC is a powerful cryptographic technology. It establishes security between key pairs for public-key encryption using elliptic curve mathematics. ECC has grown in popularity in recent years due to its smaller key size and ability to maintain security. This trend is expected to continue as the need for devices to be secure develops in response to the rising size of keys, putting pressure on limited mobile resources. This is why it is vital to understand elliptic curve cryptography in context of low power devices [29]. When compared to RSA, ECC is highly efficient with low overheads. With a key size of 160 bits, elliptical curve cryptography provides the same level of security as RSA with a key size of 1,024 bits, making it ideal for devices with limited resources [29]. Over a finite prime field Fp, an elliptical curve EP(a, b) is defined as follows [29]:(1)EPa,b:y2=x3+ax+b,where ▲ = 4a3+27b2!=0.Some of the essential definitions related to elliptical curve cryptography are listed below [29]:(a)
Point addition: point addition (+) between any two pointsAxA,yA,BxB,yB∈EPa,bis defined as follows:(2)CxR,yR=AxA,yA+BxB,yB,whereCxR,yR is a reflection of the point at which the line joining AxA,yA, and BxB,yB intersects the curve EPa,b. The algebraic computation is given as follows:(3)xR=λ2−xA−xBmodpyR=λxA−xB−yAmodp,Where,λ=yB−yAxB−xAmodp,ifA!=B,3xA2+a2yAmodp,ifA=B.(b)
Scalar multiplication: for any scalar numberX and Ax,y∈Ea,b, the scalar multiplication is defined as follows:(4)X.Ax,y=Ax,y+Ax,y+Ax,y+…+Ax,y,Xtimes.(c)
Elliptical discrete logarithmic property (ECDLP): given pointsRx,yGx,y∈EPa,b, ECDLP is a computational problem to find a scalar n such that Rx,y=n.Gx,y. ECDLP has been a prominent field of research in cryptography over many decades, and it is the essential foundation for elliptic curve cryptography (ECC) and pairing-based cryptography. ECDLP has exponential time complexity.


### 2.4. Scyther Simulation

Scyther is a tool for validating and verifying security protocols that was created by Cremers [24]. It is a software that provides security risk assessments and attack simulation capabilities. Scyther uses an infinite number of sessions to verify security protocols. Scyther also allows multiprotocol assaults to be verified. Figure 2 depicts the Scyther Tool’s design in its most basic form. To verify and validate a security protocol in Scyther, it is modeled using Scyther protocol description language (SPDL). The tool accepts the SPDL model to be validated as well as simulation settings. As an output, the Scyther tool generates a summary report showing if the necessary security assertions are valid. If an attack is discovered, it generates a trace pattern in the form of a visual graph or an XML representation. An SPDL model of security protocol comprises roles that define the communication pattern of sender and receiver principals. The term claim is used to specify the various security requirements. Claim secret declares the parameters that must remain confidential from the adversary. The claim alive ensures that the claimant is executing events with the intended party. Nisynch ensures that all the intended messages in the session are sent and received in a synchronized manner, whereas Niagree indicates that the communicating parties agree on the messages exchanged. Finally, the weakagree ensures resilience against impersonation attacks. SKR claim indicates whether the session key designated using SKR can be revealed using the session key adversary rule. To verify this claim, the session key rule in the adversary model setting must be enabled. More details about Scyther are given in [24].Figure 2
Basic architecture of Scyther.The adversary model by default in the Scyther standard version is Dolev and Yoa. The Scyther-Compromise provides extended support for various adversary models as compared to the standard Scyther version. In this paper, Scyther-Compromise version 0.9.2 has been used.


## 2.1. Notations

The notations used in the paper are tabulated in Table1.Table 1
Notations.
NotationMeaningEPa,bElliptical curveSServerDii-th IoT deviceIDiIdentity ofDiIDsIdentity ofSRiThe random number at the serverNiRandom number at the deviceXSPrivate key of SKIPrivate key ofDiSiEphemeral secret ofDiSsEphemeral secret ofSETExpiration timeGx,yGenerator point ofEPa,bSKSession key betweenS and DiHCollision resistant hash function⊕Xor operationP+QPoint additionX.GScalar multiplication


## 2.2. Adversary Model

An adversary model formulates the potential capabilities an attacker can have. Various adversary models exist that include Dolev and Yoa (DY) [20, 21], Canetti–Krawczyk (CK), and extended Canetti–Krawczyk models (eCK) models [22]. In all the models, the communication channel is completely insecure; however, they differ in their adversary query capabilities. In DY threat model, the communication parties are considered to be honest and can run multiple sessions with each other. The communication channel is completely insecure and totally under the adversary’s control, with the ability to record, delete, replay, redirect, rearrange, and completely control message schedule. The adversary can act as an active adversary in the middle and lead various man-in-the-middle attacks. The CK and eCK models are the most widely accepted models for authentication and key agreement protocols. In this adversary model, an attacker has abilities to compromise PRNG and get access to the secret randomness of the session. It is also assumed that an adversary can compromise the session and get access to it. An attacker can also get access to the long-term keys [26]. The major difference between the CK model and the eCK model is that in the eCK model, the adversary is capable of accessing ephemeral secrets, thus leading to an ephemeral-secret-key-leakage attack. An ephemeral key leakage indicates the weaknesses of a random number generator where the attacker can determine the randomness generated correctly with a high probability [26].


## 2.3. Elliptical Curve Cryptography

Koblitz [27] and Miller [28] introduced elliptical curve cryptography (ECC). ECC is a powerful cryptographic technology. It establishes security between key pairs for public-key encryption using elliptic curve mathematics. ECC has grown in popularity in recent years due to its smaller key size and ability to maintain security. This trend is expected to continue as the need for devices to be secure develops in response to the rising size of keys, putting pressure on limited mobile resources. This is why it is vital to understand elliptic curve cryptography in context of low power devices [29]. When compared to RSA, ECC is highly efficient with low overheads. With a key size of 160 bits, elliptical curve cryptography provides the same level of security as RSA with a key size of 1,024 bits, making it ideal for devices with limited resources [29]. Over a finite prime field Fp, an elliptical curve EP(a, b) is defined as follows [29]:(1)EPa,b:y2=x3+ax+b,where ▲ = 4a3+27b2!=0.Some of the essential definitions related to elliptical curve cryptography are listed below [29]:(a)
Point addition: point addition (+) between any two pointsAxA,yA,BxB,yB∈EPa,bis defined as follows:(2)CxR,yR=AxA,yA+BxB,yB,whereCxR,yR is a reflection of the point at which the line joining AxA,yA, and BxB,yB intersects the curve EPa,b. The algebraic computation is given as follows:(3)xR=λ2−xA−xBmodpyR=λxA−xB−yAmodp,Where,λ=yB−yAxB−xAmodp,ifA!=B,3xA2+a2yAmodp,ifA=B.(b)
Scalar multiplication: for any scalar numberX and Ax,y∈Ea,b, the scalar multiplication is defined as follows:(4)X.Ax,y=Ax,y+Ax,y+Ax,y+…+Ax,y,Xtimes.(c)
Elliptical discrete logarithmic property (ECDLP): given pointsRx,yGx,y∈EPa,b, ECDLP is a computational problem to find a scalar n such that Rx,y=n.Gx,y. ECDLP has been a prominent field of research in cryptography over many decades, and it is the essential foundation for elliptic curve cryptography (ECC) and pairing-based cryptography. ECDLP has exponential time complexity.


## 2.4. Scyther Simulation

Scyther is a tool for validating and verifying security protocols that was created by Cremers [24]. It is a software that provides security risk assessments and attack simulation capabilities. Scyther uses an infinite number of sessions to verify security protocols. Scyther also allows multiprotocol assaults to be verified. Figure 2 depicts the Scyther Tool’s design in its most basic form. To verify and validate a security protocol in Scyther, it is modeled using Scyther protocol description language (SPDL). The tool accepts the SPDL model to be validated as well as simulation settings. As an output, the Scyther tool generates a summary report showing if the necessary security assertions are valid. If an attack is discovered, it generates a trace pattern in the form of a visual graph or an XML representation. An SPDL model of security protocol comprises roles that define the communication pattern of sender and receiver principals. The term claim is used to specify the various security requirements. Claim secret declares the parameters that must remain confidential from the adversary. The claim alive ensures that the claimant is executing events with the intended party. Nisynch ensures that all the intended messages in the session are sent and received in a synchronized manner, whereas Niagree indicates that the communicating parties agree on the messages exchanged. Finally, the weakagree ensures resilience against impersonation attacks. SKR claim indicates whether the session key designated using SKR can be revealed using the session key adversary rule. To verify this claim, the session key rule in the adversary model setting must be enabled. More details about Scyther are given in [24].Figure 2
Basic architecture of Scyther.The adversary model by default in the Scyther standard version is Dolev and Yoa. The Scyther-Compromise provides extended support for various adversary models as compared to the standard Scyther version. In this paper, Scyther-Compromise version 0.9.2 has been used.


## 3. Review and Security Validation of Rostampour Et Al.’s Scheme

### 3.1. Review of Rostampour Et Al.’s Scheme

The Rostampour et al. scheme comprises two phases given as below:(1)
Registration phase(2)
Login and authentication phase


#### 3.1.1. Registration Phase

The registration phase is carried out between the device and the server over a secure channel. The steps are given below:(i)
Di generates a random number Xi and computes PIDi as (4):(5)PIDi=Xi⊕IDi.Di sends PIDi to the server Sas follows:(6)Di⟶S:PIDi.(ii)
The server generates a random numberRi and calculates (7) and (8):(7)CKi=HRi⊕Xs⊕ET⊕PIDi,(8)CKi′=CKi.G.Server storesPIDi,ET, and CKi in a secure database.(iii)
The server sendsCKi′ to the device as follows:(9)S⟶Di:CKi′.The deviceDi stores CKi along with generated PIDi.


#### 3.1.2. Login and Authentication Phase

(i)
Di generates a random number Ni and computes (10)–(12):(10)P1=N1.G,(11)P2=N1.CKi′,(12)PPIDi=PIDi.P1.And sends it to the server as follows:(13)Di⟶S:P1,P2,PPIDi.(ii)
The server finds the entry ofDi in its database and verifies P2≠CKi.P1. If the evaluation is false, then the process stops, and if true, then the device is authenticated.(iii)
The server generates a random numberN2 and computes (14) and (15):(14)P3=N2.G,(15)P4=CKi′+PPIDi+N2.P1.Also, it sends it to the device as follows:(16)S⟶Di:P3,P4.(iv)
Device verifiesP4?=PPIDi.CKi′+N1.P2. If the evaluation is false, then the process stops, and if true, then the device is authenticated. The device computes Vi as in the following equation and sends it to the server:(17)Vi=PPIDi.P3,(18)Di⟶S:Vi.(v)
The server receivesVi and verifies Vi≠N2.PPIDi. If the evaluation is false, then the process stops, and if true, then the device is authenticated.(vi)
The server computes its session key:SK=N2.P1, and the device computes its session key: SK=N1.P3, such that SK=N1,N2,G.The schematics of the Rostampour et al. scheme are given in Figure3.Figure 3
Schematics of the Rostampour et al. scheme.


### 3.2. Formal Validation of Rostampour Et Al.’s Scheme Using Scyther under the eCK Adversary Model

The SPDL model of the Rostampour et al. protocol is shown in Figure4. The SPDL modeling comprises two roles: role I and role R. role I models the communication of the Di, and role R models the S. Di sends P1,P2,PPIDi to the S using send_1(). The S receives the P1,P2,PPIDi using recv_1() function. S sends P3,P4 to the Di using send_2(). The Di receives the P3,P4 using recv_2() function. Finally, Di sends Vi to the S using send_3(). The S receives the Vi using recv_3() function. The claim_i1 in role I and claim_r1 in role I and R indicates that the N1,N2 must remain secret during the communication. The claim_i2 and claim_r2 in roles I and R indicate that SK=N1,N2,G can be revealed using the session key adversary rule. claim_r3, claim_r4, claim_r3, and claim_r4 are to verify whether the authentication in terms of Nisynch and Niagree is maintained.Figure 4
SPDL model of the Rostampour et al. Scheme.The SPDL model has been initially executed under Dolev and Yoa setting as shown in Figure5. The Scyther-Compromise verification results of the Rostampour et al. scheme under the Dolev and Yoa setting indicate that the scheme is safe and does not have any attacks. Subsequently, the model was executed under the eCK adversary setting shown in Figure 6. The Scyther verification results under eCK are shown in Figure 7.Figure 5
Scyther settings for Dolev and Yoa adversary models.Figure 6
Scyther settings for the eCK adversary model.Figure 7
Scyther verification results of the Rostampour et al. scheme under the eCK model.The results indicate that the scheme is not safe. The attack trace is shown in Figure8. The attack trace indicates that the Rostampour et al. scheme under the eCK adversary model is not resilient to session key reveal attack; thus, the adversary can reveal the session key. This is primarily due to the design issue in the Rostampour et al. scheme for computing the session key. In the Rostampour et al. scheme, the session key is computed as SK=N1.N2.G. The session key (SK) depends only on short-term session secrets N1 and N2. SK must also be dependent on long-term term secrets so that the reveal of short-term secrets does reveal session key.Figure 8
Attack trace under the eCK model for Rostampour et al.’ scheme.


## 3.1. Review of Rostampour Et Al.’s Scheme

The Rostampour et al. scheme comprises two phases given as below:(1)
Registration phase(2)
Login and authentication phase


### 3.1.1. Registration Phase

The registration phase is carried out between the device and the server over a secure channel. The steps are given below:(i)
Di generates a random number Xi and computes PIDi as (4):(5)PIDi=Xi⊕IDi.Di sends PIDi to the server Sas follows:(6)Di⟶S:PIDi.(ii)
The server generates a random numberRi and calculates (7) and (8):(7)CKi=HRi⊕Xs⊕ET⊕PIDi,(8)CKi′=CKi.G.Server storesPIDi,ET, and CKi in a secure database.(iii)
The server sendsCKi′ to the device as follows:(9)S⟶Di:CKi′.The deviceDi stores CKi along with generated PIDi.


### 3.1.2. Login and Authentication Phase

(i)
Di generates a random number Ni and computes (10)–(12):(10)P1=N1.G,(11)P2=N1.CKi′,(12)PPIDi=PIDi.P1.And sends it to the server as follows:(13)Di⟶S:P1,P2,PPIDi.(ii)
The server finds the entry ofDi in its database and verifies P2≠CKi.P1. If the evaluation is false, then the process stops, and if true, then the device is authenticated.(iii)
The server generates a random numberN2 and computes (14) and (15):(14)P3=N2.G,(15)P4=CKi′+PPIDi+N2.P1.Also, it sends it to the device as follows:(16)S⟶Di:P3,P4.(iv)
Device verifiesP4?=PPIDi.CKi′+N1.P2. If the evaluation is false, then the process stops, and if true, then the device is authenticated. The device computes Vi as in the following equation and sends it to the server:(17)Vi=PPIDi.P3,(18)Di⟶S:Vi.(v)
The server receivesVi and verifies Vi≠N2.PPIDi. If the evaluation is false, then the process stops, and if true, then the device is authenticated.(vi)
The server computes its session key:SK=N2.P1, and the device computes its session key: SK=N1.P3, such that SK=N1,N2,G.The schematics of the Rostampour et al. scheme are given in Figure3.Figure 3
Schematics of the Rostampour et al. scheme.


## 3.1.1. Registration Phase

The registration phase is carried out between the device and the server over a secure channel. The steps are given below:(i)
Di generates a random number Xi and computes PIDi as (4):(5)PIDi=Xi⊕IDi.Di sends PIDi to the server Sas follows:(6)Di⟶S:PIDi.(ii)
The server generates a random numberRi and calculates (7) and (8):(7)CKi=HRi⊕Xs⊕ET⊕PIDi,(8)CKi′=CKi.G.Server storesPIDi,ET, and CKi in a secure database.(iii)
The server sendsCKi′ to the device as follows:(9)S⟶Di:CKi′.The deviceDi stores CKi along with generated PIDi.


## 3.1.2. Login and Authentication Phase

(i)
Di generates a random number Ni and computes (10)–(12):(10)P1=N1.G,(11)P2=N1.CKi′,(12)PPIDi=PIDi.P1.And sends it to the server as follows:(13)Di⟶S:P1,P2,PPIDi.(ii)
The server finds the entry ofDi in its database and verifies P2≠CKi.P1. If the evaluation is false, then the process stops, and if true, then the device is authenticated.(iii)
The server generates a random numberN2 and computes (14) and (15):(14)P3=N2.G,(15)P4=CKi′+PPIDi+N2.P1.Also, it sends it to the device as follows:(16)S⟶Di:P3,P4.(iv)
Device verifiesP4?=PPIDi.CKi′+N1.P2. If the evaluation is false, then the process stops, and if true, then the device is authenticated. The device computes Vi as in the following equation and sends it to the server:(17)Vi=PPIDi.P3,(18)Di⟶S:Vi.(v)
The server receivesVi and verifies Vi≠N2.PPIDi. If the evaluation is false, then the process stops, and if true, then the device is authenticated.(vi)
The server computes its session key:SK=N2.P1, and the device computes its session key: SK=N1.P3, such that SK=N1,N2,G.The schematics of the Rostampour et al. scheme are given in Figure3.Figure 3
Schematics of the Rostampour et al. scheme.


## 3.2. Formal Validation of Rostampour Et Al.’s Scheme Using Scyther under the eCK Adversary Model

The SPDL model of the Rostampour et al. protocol is shown in Figure4. The SPDL modeling comprises two roles: role I and role R. role I models the communication of the Di, and role R models the S. Di sends P1,P2,PPIDi to the S using send_1(). The S receives the P1,P2,PPIDi using recv_1() function. S sends P3,P4 to the Di using send_2(). The Di receives the P3,P4 using recv_2() function. Finally, Di sends Vi to the S using send_3(). The S receives the Vi using recv_3() function. The claim_i1 in role I and claim_r1 in role I and R indicates that the N1,N2 must remain secret during the communication. The claim_i2 and claim_r2 in roles I and R indicate that SK=N1,N2,G can be revealed using the session key adversary rule. claim_r3, claim_r4, claim_r3, and claim_r4 are to verify whether the authentication in terms of Nisynch and Niagree is maintained.Figure 4
SPDL model of the Rostampour et al. Scheme.The SPDL model has been initially executed under Dolev and Yoa setting as shown in Figure5. The Scyther-Compromise verification results of the Rostampour et al. scheme under the Dolev and Yoa setting indicate that the scheme is safe and does not have any attacks. Subsequently, the model was executed under the eCK adversary setting shown in Figure 6. The Scyther verification results under eCK are shown in Figure 7.Figure 5
Scyther settings for Dolev and Yoa adversary models.Figure 6
Scyther settings for the eCK adversary model.Figure 7
Scyther verification results of the Rostampour et al. scheme under the eCK model.The results indicate that the scheme is not safe. The attack trace is shown in Figure8. The attack trace indicates that the Rostampour et al. scheme under the eCK adversary model is not resilient to session key reveal attack; thus, the adversary can reveal the session key. This is primarily due to the design issue in the Rostampour et al. scheme for computing the session key. In the Rostampour et al. scheme, the session key is computed as SK=N1.N2.G. The session key (SK) depends only on short-term session secrets N1 and N2. SK must also be dependent on long-term term secrets so that the reveal of short-term secrets does reveal session key.Figure 8
Attack trace under the eCK model for Rostampour et al.’ scheme.


## 4. Proposed Scheme

The proposed scheme comprises two phases that include(1)
Registration phase(2)
Login and authentication phase


### 4.1. Registration Phase

The registration phase includes the registration of an IoT device with the server. As with other schemes, the registration is performed on a secure channel [11]. The need for a secure channel for registration is highlighted as there is no preshared secret in the IoT device or any trusted third party is employed. The steps taken between the device and the server during the registration are listed as below:(i)
DeviceDi chooses its private key Ki and its identityIDi.(ii)
The device calculatesPIDi as in (19) and sends PIDi it to the server:(19)PIDi=Ki.IDi.G,Di⟶S:PIDi.(iii)
The server calculates the hash ofPIDi and splits its private key XS into two unequal halves XS1,XS2 such that XS1≠XS2. The server further computes (20) and (21):(20)CKi1=PIDi.XS1,(21)CKi2=PIDi.XS2.The server storesPIDi,CKi1,CKi2 and sends CKi1,CKi2 to the device as follows:(22)S⟶Di:CKi1,CKi2.(v)
The device receives and stores the parametersCKi1,CKi2 along with PIDi in its memory.


### 4.2. Login and Authentication Phase

During this phase, the device initiates to log in to the server. Subsequently, the server authenticates the device, and if the device is authenticated, a session key is subsequently established between the device and the server. The steps undertaken between the device and the server during the login and authentication phase is shown as below:(i)
DeviceDi chooses its ephemeral secret Si and calculates P1 and P2 as (23) and (24):(23)P1=CKi1+CKi2.Si.HPIDi,(24)P2=CKi1+CKi2.Si.The device sendsP1 and P2 to the server as follows:(25)Di⟶S:P1,P2.(ii)
The server receivesP1,P2 from Di and authenticates Di as follows:(a)
The server finds the corresponding entry ofDi and calculates HPIDi from PIDi of the device stored in the database.(b)
The server calculates the multiplicative inverse ofHPIDi as HPIDi−1 and computes P1’ as P1′=P1.HPIDi−1.(c)
The server comparesP1′≠P2. If true, then Step 3 is performed; else, login request from Di is rejected.(iii)
The server chooses its ephemeral secretSs and calculates P3 and P4 as (26) and (27):(26)P3=P1.Ss,(27)P4=CKi1+CKi2.Ss.(iv)
The server computes its session keySK with Di as follows:(28)SK=P2.Ss,(29)SK=CKi1+CKi2Si.Ss,SK=PIDi.XS1+PIDi.XS2Si.Ss,SK=XS1+XS2.PIDi.Si.Ss,SK=XS.Ki.IDi.G.Si.Ss.(v)
Server sendsP3,P4 to the device as follows:(30)S⟶Di:P3,P4.(vi)
The device receivesP3,P4 from the server and authenticates it as follows:(a)
The device calculates the multiplicative inverse ofHPIDi as HPIDi−1 and computes P3′ as P3′=P3.HPIDi−1.Si−1.(b)
The device comparesP3′≠P4. If true, then S is authenticated; else, login response from S is rejected.(vii)
The device computes its session key withS as follows:(31)SK=P4.Si,(32)SK=CKi1+CKi2Ss.Si,SK=PIDi.XS1+PIDi.XS2Ss.Si,SK=XS1+XS2.PIDiSi.Ss,SK=XS.Ki.IDi.G.Si.Ss.(viii)
The device encryptsESKHSK and sends it to the server as follows:(33)Di⟶S:ESKHSK.(ix)
The server decryptsESKHSK as V=DSKESKSK and verifies that whether V≠HSK. If true, then the login request is approved, and the device is authenticated.The schematics of the proposed scheme are given in Figure9.Figure 9
Schematics of the proposed scheme.


## 4.1. Registration Phase

The registration phase includes the registration of an IoT device with the server. As with other schemes, the registration is performed on a secure channel [11]. The need for a secure channel for registration is highlighted as there is no preshared secret in the IoT device or any trusted third party is employed. The steps taken between the device and the server during the registration are listed as below:(i)
DeviceDi chooses its private key Ki and its identityIDi.(ii)
The device calculatesPIDi as in (19) and sends PIDi it to the server:(19)PIDi=Ki.IDi.G,Di⟶S:PIDi.(iii)
The server calculates the hash ofPIDi and splits its private key XS into two unequal halves XS1,XS2 such that XS1≠XS2. The server further computes (20) and (21):(20)CKi1=PIDi.XS1,(21)CKi2=PIDi.XS2.The server storesPIDi,CKi1,CKi2 and sends CKi1,CKi2 to the device as follows:(22)S⟶Di:CKi1,CKi2.(v)
The device receives and stores the parametersCKi1,CKi2 along with PIDi in its memory.


## 4.2. Login and Authentication Phase

During this phase, the device initiates to log in to the server. Subsequently, the server authenticates the device, and if the device is authenticated, a session key is subsequently established between the device and the server. The steps undertaken between the device and the server during the login and authentication phase is shown as below:(i)
DeviceDi chooses its ephemeral secret Si and calculates P1 and P2 as (23) and (24):(23)P1=CKi1+CKi2.Si.HPIDi,(24)P2=CKi1+CKi2.Si.The device sendsP1 and P2 to the server as follows:(25)Di⟶S:P1,P2.(ii)
The server receivesP1,P2 from Di and authenticates Di as follows:(a)
The server finds the corresponding entry ofDi and calculates HPIDi from PIDi of the device stored in the database.(b)
The server calculates the multiplicative inverse ofHPIDi as HPIDi−1 and computes P1’ as P1′=P1.HPIDi−1.(c)
The server comparesP1′≠P2. If true, then Step 3 is performed; else, login request from Di is rejected.(iii)
The server chooses its ephemeral secretSs and calculates P3 and P4 as (26) and (27):(26)P3=P1.Ss,(27)P4=CKi1+CKi2.Ss.(iv)
The server computes its session keySK with Di as follows:(28)SK=P2.Ss,(29)SK=CKi1+CKi2Si.Ss,SK=PIDi.XS1+PIDi.XS2Si.Ss,SK=XS1+XS2.PIDi.Si.Ss,SK=XS.Ki.IDi.G.Si.Ss.(v)
Server sendsP3,P4 to the device as follows:(30)S⟶Di:P3,P4.(vi)
The device receivesP3,P4 from the server and authenticates it as follows:(a)
The device calculates the multiplicative inverse ofHPIDi as HPIDi−1 and computes P3′ as P3′=P3.HPIDi−1.Si−1.(b)
The device comparesP3′≠P4. If true, then S is authenticated; else, login response from S is rejected.(vii)
The device computes its session key withS as follows:(31)SK=P4.Si,(32)SK=CKi1+CKi2Ss.Si,SK=PIDi.XS1+PIDi.XS2Ss.Si,SK=XS1+XS2.PIDiSi.Ss,SK=XS.Ki.IDi.G.Si.Ss.(viii)
The device encryptsESKHSK and sends it to the server as follows:(33)Di⟶S:ESKHSK.(ix)
The server decryptsESKHSK as V=DSKESKSK and verifies that whether V≠HSK. If true, then the login request is approved, and the device is authenticated.The schematics of the proposed scheme are given in Figure9.Figure 9
Schematics of the proposed scheme.


## 5. Security Analysis

### 5.1. Replay Attack

In a replay attack, an adversary stores the messages exchanged between the communicating parties and retransmits them in the future to gain illegitimate access. In the proposed protocol, three messages are exchanged between the device and the server:(34)Di⟶S:P1,P2,S⟶Di:P3,P4,Di⟶S:ESKHSK.Let us assume during the initiation of the login and authentication phase, an adversary can eavesdrop on the messages and storesP1,P2,P3,P4 and ESKHSK for a replay attack. Let an adversary (A) replay stored P1,P2 of the previous session to gain illegitimate access as follows:(35)A⟶S:P1,P2.When the server receivesP1,P2, it validates the request and generates P3,P4 with a new ephemeral random secret. The adversary receives P3,P4 a new ephemeral secret. To validate P3,P4 and subsequently generate a session key SK, the adversary needs to know PIDi and the ephemeral random secret previously used for computing P1,P2. The adversary does not have access to either due to the exponential time complexity of ECDLP [30–32]. As the adversary cannot generate a legitimate session key SK of the current session, ESKHSK cannot be computed by the adversary. Moreover, if the adversary replays the old ESKHSK, the server will not authenticate it as the current SK is based on the fresh ephemeral random secret of the server. Thus, the design of the scheme thwarts replay attacks.


### 5.2. Impersonation Attack

In an impersonation attack, an adversary tries to impersonate a legitimate device. The login and authentication phase starts by computingP1,P2 For computing P1,P2, an adversary must have access and knowledge of CKi1,CKi2 and HPIDi. The CKi1,CKi2 and HPIDi are shared between the device and the server over a secure channel. Moreover, even if the adversary eavesdrop on P1,P2 of any previous login and authentication session between the device and the server, the CKi1,CKi2 and HPIDi cannot be extracted from P1,P2 due to the computational difficulty of ECDLP. Thus, without the knowledge of CKi1,CKi2 and HPIDi, a valid P1,P2 cannot be computed as such an adversary cannot impersonate any legitimate device by computing a malicious P1,P2.


### 5.3. Traceability Attack

In a traceability attack, the message with constant values may reveal the context of communication or the communication pattern. To avoid traceability attacks, messages exchanges must be randomized by incorporating pseudorandom numbers. In the proposed protocol, the ephemeral random secretsSi,Ss induce the required randomness in the messages for each login session. Thus, the traceability attack is mitigated in the proposed scheme.


### 5.4. Message Integrity Attack

The message exchanged between the device and the server cannot be masqueraded. During the communication, the following messages are exchanged between the device and the server:P1,P2,P3P4 and ESKHSK. Let us say an adversary intercepts the P1,P2,P3P4 and ESKHSK and wants to create malicious: P1S,P2S,P3S,P4S. However, to create P1S,P2S,P3S,P4S, the adversary must have access to XS and Ki. The adversary does not have access to XS and Ki. Moreover, extraction of the private key of XS from P1,P2,P3P4 is having exponential time complexity due to the computational complexity of ECDLP. Thus, the integrity of P1,P2,P3P4 is upheld by the computational infeasibility of ECDLP. Moreover, the message ESKHSK can also not be altered as it is protected by a symmetric encryption technique and one-way hash.


### 5.5. Man-in-the-Middle Attack

In a man-in-the-middle attack, an attacker can eavesdrop, disguise, and change communication in the middle by forging the key established between the device and the server. An adversary would be successful in executing the man in the middle attack if the adversary in the middle of the communication can create malicious:P1S,P2S,P3SP4S. However, to create malicious P1S,P2S,P3SP4S, the adversary must be able to forge CKi1,CKi2 as follows:(36)CKi1=PIDi.XS1,CKi2=PIDi.XS2.To forgeCKi1,CKi2, adversary must have access to XS. The adversary does not have access to XS. Moreover, from P1,P2,P3P4, XS cannot be extracted due to the exponential complexity of ECDLP. As the adversary cannot forge P1,P2,P3P4 and proper authentication is employed prior to the key establishment, the man-in-the-middle attack is mitigated in the proposed scheme.


## 5.1. Replay Attack

In a replay attack, an adversary stores the messages exchanged between the communicating parties and retransmits them in the future to gain illegitimate access. In the proposed protocol, three messages are exchanged between the device and the server:(34)Di⟶S:P1,P2,S⟶Di:P3,P4,Di⟶S:ESKHSK.Let us assume during the initiation of the login and authentication phase, an adversary can eavesdrop on the messages and storesP1,P2,P3,P4 and ESKHSK for a replay attack. Let an adversary (A) replay stored P1,P2 of the previous session to gain illegitimate access as follows:(35)A⟶S:P1,P2.When the server receivesP1,P2, it validates the request and generates P3,P4 with a new ephemeral random secret. The adversary receives P3,P4 a new ephemeral secret. To validate P3,P4 and subsequently generate a session key SK, the adversary needs to know PIDi and the ephemeral random secret previously used for computing P1,P2. The adversary does not have access to either due to the exponential time complexity of ECDLP [30–32]. As the adversary cannot generate a legitimate session key SK of the current session, ESKHSK cannot be computed by the adversary. Moreover, if the adversary replays the old ESKHSK, the server will not authenticate it as the current SK is based on the fresh ephemeral random secret of the server. Thus, the design of the scheme thwarts replay attacks.


## 5.2. Impersonation Attack

In an impersonation attack, an adversary tries to impersonate a legitimate device. The login and authentication phase starts by computingP1,P2 For computing P1,P2, an adversary must have access and knowledge of CKi1,CKi2 and HPIDi. The CKi1,CKi2 and HPIDi are shared between the device and the server over a secure channel. Moreover, even if the adversary eavesdrop on P1,P2 of any previous login and authentication session between the device and the server, the CKi1,CKi2 and HPIDi cannot be extracted from P1,P2 due to the computational difficulty of ECDLP. Thus, without the knowledge of CKi1,CKi2 and HPIDi, a valid P1,P2 cannot be computed as such an adversary cannot impersonate any legitimate device by computing a malicious P1,P2.


## 5.3. Traceability Attack

In a traceability attack, the message with constant values may reveal the context of communication or the communication pattern. To avoid traceability attacks, messages exchanges must be randomized by incorporating pseudorandom numbers. In the proposed protocol, the ephemeral random secretsSi,Ss induce the required randomness in the messages for each login session. Thus, the traceability attack is mitigated in the proposed scheme.


## 5.4. Message Integrity Attack

The message exchanged between the device and the server cannot be masqueraded. During the communication, the following messages are exchanged between the device and the server:P1,P2,P3P4 and ESKHSK. Let us say an adversary intercepts the P1,P2,P3P4 and ESKHSK and wants to create malicious: P1S,P2S,P3S,P4S. However, to create P1S,P2S,P3S,P4S, the adversary must have access to XS and Ki. The adversary does not have access to XS and Ki. Moreover, extraction of the private key of XS from P1,P2,P3P4 is having exponential time complexity due to the computational complexity of ECDLP. Thus, the integrity of P1,P2,P3P4 is upheld by the computational infeasibility of ECDLP. Moreover, the message ESKHSK can also not be altered as it is protected by a symmetric encryption technique and one-way hash.


## 5.5. Man-in-the-Middle Attack

In a man-in-the-middle attack, an attacker can eavesdrop, disguise, and change communication in the middle by forging the key established between the device and the server. An adversary would be successful in executing the man in the middle attack if the adversary in the middle of the communication can create malicious:P1S,P2S,P3SP4S. However, to create malicious P1S,P2S,P3SP4S, the adversary must be able to forge CKi1,CKi2 as follows:(36)CKi1=PIDi.XS1,CKi2=PIDi.XS2.To forgeCKi1,CKi2, adversary must have access to XS. The adversary does not have access to XS. Moreover, from P1,P2,P3P4, XS cannot be extracted due to the exponential complexity of ECDLP. As the adversary cannot forge P1,P2,P3P4 and proper authentication is employed prior to the key establishment, the man-in-the-middle attack is mitigated in the proposed scheme.


## 6. Formal Validation of the Proposed Protocol Using Scyther

The designed protocol has been modeled using SPDL to validate its security on Scyther-Compromise under the eCK adversary model. The SPDL model of the proposed protocol is shown in Figure10. The role Device and role Server model the communication pattern of the Di and S, respectively. The role Device initiates the login and authentication phase by sending (P1, P2) using the send_1 function. On receiving (P1, P2) using the recv1 function, the role server sends (P3, P4) using send_2 functions to the device. Finally, the device sends ESK[H(SK)] to the server using the send_3 function. The claim_i1 in role Device and claim_r1 in role Server indicate that the XS and Ki must remain secret during the communication. The claim_i2 in role Device and claim_r2 in role Server indicate whether SK=XS.Ki.IDi.G.Si.Ss can be revealed using the session key adversary rule. claim_r3, claim_r4, claim_r3, and claim_r4 is to verify whether the authentication in terms of Nisynch and Niagree is maintained.Figure 10
SPDL model of the proposed scheme.The SPDL model of the designed protocol was simulated on the compromise 0.9 under the eCK adversary model as indicated in Figure6. The verification results are shown in Figure 11. From Figure 11, we can infer that the protocol is safe and does not have any attack under the stringent eCK adversary model.Figure 11
Scyther verification results for the proposed scheme.


## 7. Formal Security Analysis Using BAN Logic

Burrows et al. proposed BAN logic to validate the soundness and correctness of a security protocol. This section employs BAN logic to determine the security validity of the proposed scheme.D and S denote the communicating principles, where KI and XS denote their private keys, respectively. The BAN notations are tabulated in Table 2 [31], and the BAN postulates are given in Table 3. Besides that, as derived in [33], synthesis rules are tabulated in Table 4.Table 2
BAN symbols.
NotationDescriptionD|≡MSGD believes MD⇐MSGD receives the message MD|∼MSGD sent the message M in pastD‖∼MSGD sent the message to M currentlyD|⟶FD has jurisdiction over V#MSGM is fresh⟶PrDPr is the public parameter calculated using the private key of DD⟶SKSSK is the key betweenD and SXSKSK is the key used to encryptXF1/F2If F1 is true, then F2 is trueTable 3
BAN postulates.
Rule no.NameRepresentationR1Message-meaning ruleD|≡⟶PrS,D⇐MSGXS/D|≡S|∼MSGR2Nonce verification ruleD|≡#MSG,D≡S|∼MSG/D|≡S|≡MSGR3Jurisdiction ruleD|⟶MSG,D|≡S|≡MSG/D|≡MSGR4Seeing ruleD⇐MSG1,D⇐MSG2/D⇐MSG1,MSG2R5Belief ruleD|≡MSG1,D|≡MSG2/D|≡MSG1,MSG2R6Freshness ruleD|≡#MSG1/D|≡#MSG1,MSG2R7Session key ruleD|≡#SK,D|≡S|≡X/D|≡D⟶SKSX is part of SKTable 4
Synthesis rules.
Rule no.Synthesis ruleS1D⇐MSG1¬D⇐MSG1,MSG2S2D|≡S|∼MSG1¬D|≡S|∼MSG1,MSG2S3D|≡S|∼MSG1,MSG2¬D|≡S|∼MSG1S4D|≡S|∼MSG1¬D|≡#MSG1


### 7.1. Assumptions

(A1)
D|≡⟶CKi1,CKi2S(A2)
S|≡⟶CKi1,CKi2DA3)D|≡#SI(A2)
S|≡#SSA5)S|≡D|⟶SI(A6)
D|≡S|⟶SS


### 7.2. Idealized Form

D⟶S;P1,P2KIMSG1S⟶D;P3,P4XSMSG2


### 7.3. Goals

G1)S|≡D⟶SKS G2) S|≡D|≡D⟶SKSG3)D|≡D⟶SKS G4) D|≡S|≡D⟶SKS


### 7.4. BAN Analysis

From (MSG1), we get that(1)
D|≡P1,P2KI(2)
D⇐P1,P2KIFrom (2), (A1), and (R1), we get(3)
D|≡S|∼P1,P2KISI is a part of P1,P2; thus, as per (A3) and (R6), we get(4)
D|≡#P1,P2From (3) and (5), we get(5)
S|≡D|∼P1,P2From (7) and (S4), we get(6)
S|≡#P1,P2From (3) and (6) on applying (R2), we get(7)
S|≡D|≡P1,P2SI is the part of the P1,P2; thus, on applying (R5), we get(8)
S|≡D|≡SINow as per (A5), (8), and (R3), we get(9)
S|≡SIFrom (S3) and (3), we get(10)
S|≡D|∼SIFrom (A3) and (10), we get(11)
S|≡D‖∼SIAs per (R4) and (11), we get(12)
S|≡#SISI is a part of (SK); thus, as per (R6), we get(13)
S|≡#SKFrom (13), (8), and (R7), we get(14)
S|≡D⟶SKS(Goal G1)Due to the symmetry of the protocol,(15)
S|≡D|≡S⟶SKD(Goal G2)From (MSG2), we infer that(16)
S|≡P3,P4XS(17)
S⇐P3,P4XSFrom (17), (A2), (R1), we get(18)
D|≡S|∼P3,P4XSSs is a part of P3,P4; thus, as per (A4) and (R6), we get(19)
S|≡#P3,P4From (17) and (19), we get(20)
D|≡S‖∼P3,P4From (20) and (S4), we get(21)
D|≡#P3,P4From (18) and (21) on applying (R2), we get(22)
D|≡S|≡P3,P4SS is the part of the formulae P3,P4; thus, on applying (R5), we get(23)
D|≡S|≡SSNow, as per (A6) and (23) and (R3), we get(24)
D|≡SSFrom (SR3) and (18), we get(25)
D|≡S|∼SSFrom (A4) and (25), we get(26)
D|≡S‖∼SSAs per (R4) and (26), we get(27)
D|≡#SSFrom (R6), we get(28)
D|≡#SKFrom (28) and (22) and on applying (R7), we get(29)
D|≡D⟶SKS(Goal G3)Due to the symmetry of the protocol,(30)
S|≡D|≡D⟶SKS(Goal G4)


## 7.1. Assumptions

(A1)
D|≡⟶CKi1,CKi2S(A2)
S|≡⟶CKi1,CKi2DA3)D|≡#SI(A2)
S|≡#SSA5)S|≡D|⟶SI(A6)
D|≡S|⟶SS


## 7.2. Idealized Form

D⟶S;P1,P2KIMSG1S⟶D;P3,P4XSMSG2


## 7.3. Goals

G1)S|≡D⟶SKS G2) S|≡D|≡D⟶SKSG3)D|≡D⟶SKS G4) D|≡S|≡D⟶SKS


## 7.4. BAN Analysis

From (MSG1), we get that(1)
D|≡P1,P2KI(2)
D⇐P1,P2KIFrom (2), (A1), and (R1), we get(3)
D|≡S|∼P1,P2KISI is a part of P1,P2; thus, as per (A3) and (R6), we get(4)
D|≡#P1,P2From (3) and (5), we get(5)
S|≡D|∼P1,P2From (7) and (S4), we get(6)
S|≡#P1,P2From (3) and (6) on applying (R2), we get(7)
S|≡D|≡P1,P2SI is the part of the P1,P2; thus, on applying (R5), we get(8)
S|≡D|≡SINow as per (A5), (8), and (R3), we get(9)
S|≡SIFrom (S3) and (3), we get(10)
S|≡D|∼SIFrom (A3) and (10), we get(11)
S|≡D‖∼SIAs per (R4) and (11), we get(12)
S|≡#SISI is a part of (SK); thus, as per (R6), we get(13)
S|≡#SKFrom (13), (8), and (R7), we get(14)
S|≡D⟶SKS(Goal G1)Due to the symmetry of the protocol,(15)
S|≡D|≡S⟶SKD(Goal G2)From (MSG2), we infer that(16)
S|≡P3,P4XS(17)
S⇐P3,P4XSFrom (17), (A2), (R1), we get(18)
D|≡S|∼P3,P4XSSs is a part of P3,P4; thus, as per (A4) and (R6), we get(19)
S|≡#P3,P4From (17) and (19), we get(20)
D|≡S‖∼P3,P4From (20) and (S4), we get(21)
D|≡#P3,P4From (18) and (21) on applying (R2), we get(22)
D|≡S|≡P3,P4SS is the part of the formulae P3,P4; thus, on applying (R5), we get(23)
D|≡S|≡SSNow, as per (A6) and (23) and (R3), we get(24)
D|≡SSFrom (SR3) and (18), we get(25)
D|≡S|∼SSFrom (A4) and (25), we get(26)
D|≡S‖∼SSAs per (R4) and (26), we get(27)
D|≡#SSFrom (R6), we get(28)
D|≡#SKFrom (28) and (22) and on applying (R7), we get(29)
D|≡D⟶SKS(Goal G3)Due to the symmetry of the protocol,(30)
S|≡D|≡D⟶SKS(Goal G4)


## 8. Comparison with Other Schemes

### 8.1. Security Comparison

The security comparison of the proposed scheme with relevant existing schemes is shown in Table5. Kalra and Sood [14] do not support any security resistance. Chang et al. [15] are not resilient to traceability and impersonation attack. Kumari et al. [16] support only AK3 and AK4 features. Among the existing schemes, Rostampour et al.’s [11] scheme is the only scheme that supports AK1–AK5. However, from Table 5, we can infer that Kalra and Sood [14], Chang et al. [15], Kumari et al. [16], Wang et al. [17], and Rostampour et al. [11] have not been evaluated under the eCK adversary model. The formal validation of Rostampour et al. [11] under eCK adversary indicates that the scheme is not safe under the eCK model. The proposed scheme supports all the security requirements from AK1 to AK5 and is also safe under the eCK model.Table 5
Security comparison.
SchemeAK1AK2AK3AK4AK5eCKKalra and Sood [14]✘✘✘✘✘✘Chang et al. [15]✘✘✔✔✔✘Kumari et al. [16]✘✘✔✔✘✘Wang et al. [17]✘✔✔✔✘✘Rostampour et al. [11]✔✔✔✔✔✘Proposed scheme✔✔✔✔✔✔AK1: traceability attack; AK2: impersonation attack; AK3: replay attack; AK4: message integrity attack; and AK5: man-in-the-middle attack.


### 8.2. Computation and Communication Overhead

The comparison in terms of computational and communication overhead is shown in Table6. The time complexities of various critical operations considered include TECM: scalar multiplication, TEADD: point addition, THASH: one-way hash, TSENC/TSDEC: symmetric encryption, and Tinv: multiplicative inverse. TECM is the most computationally intense operation. As IoT devices are resource constraints in nature, the computational overhead on these devices plays an important role in determining the efficiency of the scheme as the server is considered computationally more powerful. From Table 6, we can infer that a computational overhead of 4 TECM for the IoT device and 8 TECM in total is required in the proposed scheme. The highest device overhead is that of the Rostampour et al. scheme with 7 TECM and the lowest is that of Kalra and Sood [14]. However, from Table 5, we can infer that none of the security specifications are supported by Kalra and Sood [14]. In terms of scalar multiplication (TECM) overhead, the proposed scheme is required the same no of scalar multiplication as compared to other schemes considered for comparison. The communication cost is estimated based on the number of bits transmitted. We consider an elliptical curve E(a,b) of 160 bit. The size of an ECC point P(x,y) on the 160 bit curve is 320 bits (X[160], Y[160]). The symmetric encryption considered generates a ciphertext of 128 bit. In the proposed scheme, 03 messages are exchanged that include (P1, P2), (P3, P4), and ESK[H(SK)]. The 03 messages requires [(320 + 320),(320 + 320)+128] = 1,408 bits.Table 6
Comparison of computational and communication overhead.
SchemeComputation overheadCommunication overheadDeviceServerTotalKalra and sood [14]3 TECM + 4 THASH4TECM + 5 THASH8TECM + 9 THASH1,760Chang et al. [15]4TECM + 4 THASH4TECM + 4 THASH8TECM + 8 THASH1,632Kumari et al. [16]4TECM + 3 THASH4TECM + 4 THASH8TECM + 7 THASH1,760Wang et al. [17]4TECM + 5 THASH4TECM + 3 THASH8TECM + 8 THASH1,632Rostampour et al. [11]7TECM + TEADD6TECM + TEADD13 TECM+2 TEADD1,920Proposed schemeTECM + TEADD + 2 THASH + TSENC/TSDEC + Tinv4 TECM + TEADD + 2 THASH + TSENC/TSDEC + Tinv8 TECM + 2TEADD + 4 THASH + 2 TSENC/TSDEC + 2 Tinv1,408


### 8.3. Energy Overhead

To compare estimated energy consumed on an IoT device, the time consumed by various critical operations as indicated in [34] on a MicaZ mote [35] is shown in Table 7. The energy is consumed using E = V ∗ I ∗ T, where V is the voltage, I is the current drawn, and T is the time taken for the operation. For a MicaZ mote, V = 3 V and I = 8 mA. The proposed scheme has an energy overhead of 278.16 mJ for the IoT device. The comparison of the energy analysis of the proposed scheme with the relevant existing scheme is shown in Figure 12. The highest energy overhead is that of the Rostampour et al. scheme with 477.6 mJ. Rostampour et al. is not secure under the eCK adversary model. Though Kalra and Sood [12] have the lowest energy overhead for the IoT device, it has a high communication overhead and suffers from various security limitations that include AK1, AK2, AK3, AK4, and AK5. Kalra and Sood [12] have not been evaluated under the eCK model. Chang et al. [15], Kumari et al. [16], and Wang et al. [17] have the energy overheads of 271.44 mJ, 271.2 mJ, and 271.68 mJ, respectively. However, Chang et al. [15], Kumari et al. [16], and Wang et al. [17] do not suffice to all security requirements and have not been modeled under the eCK model. The designed scheme supports all the security specifications and is the only scheme that is formally validated under the eCK adversary model. Thus, with the computational requirement of 278.16 mJ and communication overhead of 1,408 bits, the proposed scheme supports all the security requirements and is also safe under eCK adversary.Table 7
Time consumed for critical operations [34].
OperationSecondsTECM2.82TSENC/TSDEC0.000029THASH0.0091Tinv0.14TEADD0.16Figure 12
Energy overhead comparison.


## 8.1. Security Comparison

The security comparison of the proposed scheme with relevant existing schemes is shown in Table5. Kalra and Sood [14] do not support any security resistance. Chang et al. [15] are not resilient to traceability and impersonation attack. Kumari et al. [16] support only AK3 and AK4 features. Among the existing schemes, Rostampour et al.’s [11] scheme is the only scheme that supports AK1–AK5. However, from Table 5, we can infer that Kalra and Sood [14], Chang et al. [15], Kumari et al. [16], Wang et al. [17], and Rostampour et al. [11] have not been evaluated under the eCK adversary model. The formal validation of Rostampour et al. [11] under eCK adversary indicates that the scheme is not safe under the eCK model. The proposed scheme supports all the security requirements from AK1 to AK5 and is also safe under the eCK model.Table 5
Security comparison.
SchemeAK1AK2AK3AK4AK5eCKKalra and Sood [14]✘✘✘✘✘✘Chang et al. [15]✘✘✔✔✔✘Kumari et al. [16]✘✘✔✔✘✘Wang et al. [17]✘✔✔✔✘✘Rostampour et al. [11]✔✔✔✔✔✘Proposed scheme✔✔✔✔✔✔AK1: traceability attack; AK2: impersonation attack; AK3: replay attack; AK4: message integrity attack; and AK5: man-in-the-middle attack.


## 8.2. Computation and Communication Overhead

The comparison in terms of computational and communication overhead is shown in Table6. The time complexities of various critical operations considered include TECM: scalar multiplication, TEADD: point addition, THASH: one-way hash, TSENC/TSDEC: symmetric encryption, and Tinv: multiplicative inverse. TECM is the most computationally intense operation. As IoT devices are resource constraints in nature, the computational overhead on these devices plays an important role in determining the efficiency of the scheme as the server is considered computationally more powerful. From Table 6, we can infer that a computational overhead of 4 TECM for the IoT device and 8 TECM in total is required in the proposed scheme. The highest device overhead is that of the Rostampour et al. scheme with 7 TECM and the lowest is that of Kalra and Sood [14]. However, from Table 5, we can infer that none of the security specifications are supported by Kalra and Sood [14]. In terms of scalar multiplication (TECM) overhead, the proposed scheme is required the same no of scalar multiplication as compared to other schemes considered for comparison. The communication cost is estimated based on the number of bits transmitted. We consider an elliptical curve E(a,b) of 160 bit. The size of an ECC point P(x,y) on the 160 bit curve is 320 bits (X[160], Y[160]). The symmetric encryption considered generates a ciphertext of 128 bit. In the proposed scheme, 03 messages are exchanged that include (P1, P2), (P3, P4), and ESK[H(SK)]. The 03 messages requires [(320 + 320),(320 + 320)+128] = 1,408 bits.Table 6
Comparison of computational and communication overhead.
SchemeComputation overheadCommunication overheadDeviceServerTotalKalra and sood [14]3 TECM + 4 THASH4TECM + 5 THASH8TECM + 9 THASH1,760Chang et al. [15]4TECM + 4 THASH4TECM + 4 THASH8TECM + 8 THASH1,632Kumari et al. [16]4TECM + 3 THASH4TECM + 4 THASH8TECM + 7 THASH1,760Wang et al. [17]4TECM + 5 THASH4TECM + 3 THASH8TECM + 8 THASH1,632Rostampour et al. [11]7TECM + TEADD6TECM + TEADD13 TECM+2 TEADD1,920Proposed schemeTECM + TEADD + 2 THASH + TSENC/TSDEC + Tinv4 TECM + TEADD + 2 THASH + TSENC/TSDEC + Tinv8 TECM + 2TEADD + 4 THASH + 2 TSENC/TSDEC + 2 Tinv1,408


## 8.3. Energy Overhead

To compare estimated energy consumed on an IoT device, the time consumed by various critical operations as indicated in [34] on a MicaZ mote [35] is shown in Table 7. The energy is consumed using E = V ∗ I ∗ T, where V is the voltage, I is the current drawn, and T is the time taken for the operation. For a MicaZ mote, V = 3 V and I = 8 mA. The proposed scheme has an energy overhead of 278.16 mJ for the IoT device. The comparison of the energy analysis of the proposed scheme with the relevant existing scheme is shown in Figure 12. The highest energy overhead is that of the Rostampour et al. scheme with 477.6 mJ. Rostampour et al. is not secure under the eCK adversary model. Though Kalra and Sood [12] have the lowest energy overhead for the IoT device, it has a high communication overhead and suffers from various security limitations that include AK1, AK2, AK3, AK4, and AK5. Kalra and Sood [12] have not been evaluated under the eCK model. Chang et al. [15], Kumari et al. [16], and Wang et al. [17] have the energy overheads of 271.44 mJ, 271.2 mJ, and 271.68 mJ, respectively. However, Chang et al. [15], Kumari et al. [16], and Wang et al. [17] do not suffice to all security requirements and have not been modeled under the eCK model. The designed scheme supports all the security specifications and is the only scheme that is formally validated under the eCK adversary model. Thus, with the computational requirement of 278.16 mJ and communication overhead of 1,408 bits, the proposed scheme supports all the security requirements and is also safe under eCK adversary.Table 7
Time consumed for critical operations [34].
OperationSecondsTECM2.82TSENC/TSDEC0.000029THASH0.0091Tinv0.14TEADD0.16Figure 12
Energy overhead comparison.


## 9. Conclusion

Authentication between IoT devices in the perception layer and the cloud server is critical for developing secure IoT-based smart applications. The existing schemes presented for authenticated key agreements between IoT devices and the cloud services have not been validated using the eCK adversary model. Recently, Rostampour et al. presented a scheme for authenticated key agreement between IoT devices and the cloud server that is secure under the Dolev and Yoa model. A formal security validation of Rostampour et al. has been carried out using Scyther-Compromise under the eCK model. The verification indicates that the scheme susceptible to session key disclosure attacks under the eCK model. A lightweight ECC-based authentication technique for IoT devices and the cloud server has been presented in this paper. The Scyther-Compromise simulation indicates that the proposed scheme is secure under the eCK model. BAN logic analysis and evaluation indicate that the design of the proposed scheme is sound and correct. The overhead analysis indicates that the proposed scheme requires 199.44 mJ and 512 bits less in terms of energy and communication overhead as compared to the scheme presented by Rostampour et al.



---

*Source: 7707543-2022-03-03.xml*