1 Introduction

IoT is a grid of interconnected computer-reliant ‘things’ such as smart gadgets, digital machines, sensors, heart monitors, or people, who are assigned an identifier to be exclusive among all entities and have the tendency to transport data across a network automatically. Entities in IoT environment can be used for unlawful boundary contact, recognition of dangerous radiation and chemical leakage, and revealing gas leakage in industrialized environments with regard of emergency and secure applications [1]. The entities can be used for soil quality monitoring, greenhouse climate control, and smart irrigation in smart agriculture. Surveillance, continuous monitoring of real-time appliances, water saving, and energy are just a few of the smart home uses. IoT can be used to generate applications like wireless body sensor networks, automatic monitoring of smart devices in the medical industry, and geriatric aid [2].

Important security concepts and services that should be provided and ensured while accessing real-time applications through an open network are:

  1. (i)

    Trust—The distributed and dynamic nature of IoT systems necessitates trust. The importance of ensuring the trustworthiness of interacting devices cannot be overstated. Restriction of power usage is also an important aspect of developing a trust management system.

  2. (ii)

    Confidentiality — Ensuring the confidentiality of messages exchanged between two entities in an open network must be protected. Data monitoring, gathering, sharing, and security are all areas where privacy is a problem.

  3. (iii)

    Reliability – This is a must-have feature that ensures data and service accessibility.

  4. (iv)

    Session Key Usability—In any authentication strategy, the usage of a session key is critical. It is primarily used to protect communications against third-party assaults.

Smart real-time applications built on the Internet of Things must be secure [3]. Traditional security methods can be used to provide secure communication with smart devices to the cloud server. However, because IoT devices have limited resources, simple message exchanges between smart devices residing in the sensitivity layer and server are becoming a hot topic of research [2]. Additional security services offered between the perception layer and server are built on the foundation of authentication, integrity, and session key exchange [4]. Many approaches for protecting communication exchange between smart devices residing in IoT environments and cloud servers have been proposed in the past. A mutual authentication technique with a unique identifier verification protocol was suggested by Liao and Hsiao [5]. However, Roel and Hermans [6] point out, the method is vulnerable to server impersonation assaults.

Kalra and Sood [7] presented an Elliptic Curve Cryptography (ECC) reliant mutual authentication system to resist a wide range of attacks. The approach, however, contains design flaws with regard to reciprocal verification, insider assaults, and the discovery of their traces. Chang et al. [8] discovered flaws in the work proposed by Kalra and Sood, particularly with regard to shared authentication along with the mistress of sensitive information like session key. Thus, Chang et al. proposed a better strategy that circumvented Kalra and Sood’s flaws. Similarly, about concerning device anonymity, insider attacks, session/secret key agreement, and mutual authentication. Kumari et al. [9] discovered the flaws in Kalra and Sood’s scheme concerning impersonation-reliant attacks and proposed a better scheme. To circumvent these restrictions, Kumari et al. proposed an ECC-reliant approach. Wang et al. [10] discovered the flaws concerning impersonation-based attacks in Chang et al. scheme and proposed a better solution.

Rostampour et al. [4] suggested an ECC-reliant technique for IoT edge device authentication with the cloud server. Rostampour et al. examined various existing solutions [8,9,10] in detail and claimed that they were vulnerable to traceability attacks. In [13], Ummer et al. explored the flaws present in Rostampour’s scheme and presented a better solution. When linking an implant device to the cloud, the most important factor to consider is security. Shared authentication between the implant devices and the cloud server is also required. ECC scheme is the popular and the strongest public-key cryptography option when storage space, memory area, and power are restricted and more security by a short key is desired [11, 12]. Furthermore, using the xck adversary model (ad-model), an enhanced approach for proving authentication and a secret key contract between smart devices in IoT and the server, namely sd-to-cs has been developed.

1.1 Contributions

Three previous authentication schemes, Kumari, Rostampour, and Ummer, addressed security concerns between fog computing devices and the cloud server by leveraging ECC to defend against various attacks. Although session key exposing is one of the most important security issues that aids in achieving mutual validation and device secrecy, we show in this paper that Kumari, Rostampour, and Ummer's strategy fails in this regard. We have proposed an improved ECC-reliant authentication mechanism that has been designed specifically for IoT and cloud servers to address the aforementioned weakness of the Kumari, Rostampour, and Ummer schemes. The suggested approach was modeled after the Scyther compromise. The results of the XCK rival prototype demonstrate the security and safety of the method.

1.2 Paper organization

The rest of the paper is formatted as follows. Section 2 contains the preliminaries. Three existing approaches, namely Kumari et al., Rostampour et al., and Umar Iqbal et al. approaches are reviewed in Sect. 3 along with its recognized security verification using the xck rival model. The proposed ECC-reliant system for authenticating between smart devices residing in the IoT environment and the cloud server is detailed in Sect. 4. The outcome of a formal security investigation utilizing the scyther against the xck ad-model is provided in Sect. 5. Section 6 briefs about security analysis of the suggested scheme by exploring BAN logic. The proposed scheme is compared to other appropriate authentication schemes given in Sect. 7. Finally, in Sect.  8, we conclude our work.

2 Preliminaries

Table 1 lists the various notations used in the next sections.

Table 1 Notations used

2.1 Rival model

An ad-model expresses the attacker's prospective capabilities. Dolev and Yoa [14, 15], namely DY, Canetti–Krawczyk referred to as CK, and its improved version (xck) models [16] are examples of adversarial models. The communication channel is completely unsafe in all of the models; nevertheless, they contrast in their challenger query abilities. The communicating parties are deemed honest in the DY threat model and can have several sessions between them. The communication medium is entirely unsafe and completely controllable by the opponent, who can able to perform operations like the record, delete, replay, reroute, reshuffle, and manage the message list. In the middle, the adversary can behave as a legitimate user and conduct different kinds of attacks. The xck and CK schemes for key sharing and authentication procedures are the most extensively utilized.

In this adversary scenario, an attacker can breach the pseudo-random number generator (PRNG) and gain access to the session's secret randomness. An opponent is also expected to be able to conciliate the session and gain access to it. Long-term keys can also be obtained by an attacker [18]. The xck paradigm differs from the CK model in that the adversary can obtain ephemeral secrets, resulting in an ephemeral-secret-key-leakage attack.

2.2 Elliptical curve cryptography

The application of elliptic-curve in cryptographic systems was first advocated by Koblitz [19] and Miller [20]. ECC is one of the most general and widely utilized encryption algorithms, yet it is also one of the least well-known. It is the famous next-generation and more secure public-key cryptography method. When compared to a first-generation public key cryptographic system like RSA, it provides far more security. Elliptical curve cryptography, with a key size of 160 bits, provides a similar level of security as RSA, which makes it perfectly suitable for power-constrained devices [21]. Because of its lower key length and capability to preserve security, ECC has gained prominence in recent years. This tendency is projected to remain as the requirement for secure devices grows in response to the growing key length, affecting the vital resources of smart devices. This is the reason why understanding the encryption process in ECC in the context of low-power devices is critical [21].

ECC is one of the popular and secure public cryptography schemes that relied on the algebraic organization of elliptical curves well-defined over a finite field. When compared to non-ECC encryption, ECC delivers equivalent safety for a lower key. The elliptic curve cryptosystem was first established as the cornerstone of the public-key cryptographic system, and suggestion has demonstrated that it is a critical component of the system. Cryptography in the modern era ECC has relied on the fundamentals of elliptic curves. The ECC’s security relied on the effort of handling the elliptical curve’s complex algorithm. Over a finite field, K an elliptical curve, i.e., E over K is defined as given in Eq. 1 [21].

$${\text{E}}_{{\text{K}}} \left( {{\text{x}},{\text{ y}}} \right){ } \leftarrow {\text{y}}^{2} :{\text{ x}}^{3} + {\text{ax}} + {\text{b}}.{\text{ where x}},{\text{ y }} \in {\text{K}}$$
(1)

A few important operations to be applied on elliptic curves are itemized below.

  1. (i)

    Addition of two points—The addition of two different points M1 = (x1, y1) and M2 = (x2, y2) of an elliptic curve can be calculated using the formulas as follows.

    $${\text{M}}_{{1}} + {\text{ M}}_{{2}} = {\text{ M}}_{{3}} = \, \left( {{\text{x}}_{{3}} ,{\text{ y}}_{{3}} } \right)$$
    (2)

In equation 2, x3 is computed as λ2 – x1 – x2, the value of y3 is computed as λ (x1 – x3) – y1, and

$$\lambda = \left\{ {\begin{array}{*{20}c} {\frac{{({\text{y}}_{{2 - }} {\text{y}}_{1} )}}{{({\text{x}}_{{2 - }} {\text{x}}_{1} )}},\;if\;{\text{M}}_{{1 \ne }} {\text{M}}_{2} } \\ {\frac{{\left( {3x_{1}^{2} + a} \right)}}{{\left( {2y_{1} } \right)}},\;if\;{\text{M}}_{{1 = }} {\text{M}}_{2} } \\ \end{array} } \right\}$$
  1. (b)

    Scalar Multiplication—An elliptic curve’s scalar multiplication represents an operation which adds a unique point ‘P’ to the curve k number of times.

Q = kM = M + M +···+ M, k number of times.

Where M is an elliptical curve point, and k denotes a large positive integer.

  1. (iii)

    Discrete Logarithm on Elliptic Curve—Let an elliptic curve, E, and its points, A and B, with B = kA = (A + A + … + A) – k times for some k. The discrete logarithm issue for elliptic curves is the task of locating such a k. There is no efficient algorithm or good general attacks for computing discrete logarithm problems for elliptic curves. The cryptography based on elliptic curves is grounded on these facts.

2.3 Scyther simulation

Simulation of a Scyther Cremers [17] designed Scyther, a tool for assessing and certifying security protocols. It’s software that can perform security risk assessments and attack simulations. Scyther verifies security protocols using an endless number of sessions. Scyther also provides for the verification of multiprotocol assaults. In Scyther, a security protocol is represented using the SPDL (Scyther protocol description language) to verify and validate it. When attacks are found, attack graphs are generated in scyther tool but not in AVISPA tool. This is one of the noted features of scyther tool.

When an attack is detected, a trace pattern is produced as either an XML representation or a visual graph. The sender and receiver principals' communication pattern is defined by roles in the SPDL representation of security protocol. To express the various security needs, the phrase claim is utilized. Dolev and Yoa are the default opponent models in the Scyther version. In comparison to the conventional Scyther version, the ScytherCompromise provides more support for diverse opponent models. Scyther Compromise tool version 0.9.2 was utilized in this paper to generate different claims and attacks.

3 Review of appropriate existing schemes

3.1 Preview of Kumari et al. method

Kumari et al. [9] proposed an ECC cryptosystem-reliant authentication approach for smart devices in the Internet of Things. The protocol is divided into three phases, which are detailed below.

3.1.1 Registration phase

The registering stage takes place through a secure connection between the SD and CS. The steps are as follows:

  1. (i)

    SDi computes Li = h(SIDi || PDi) and transmits it to CS over a secure communication medium for registration purposes.

  2. (ii)

    After the registration is successfully processed, CS generates a random number Ni and computes the pseudo-identity for SIDi as h(Ni || IDCS|| Li). Afterward, it computes a few other vital secret information as follows: \(Ci = h(Ni||XCS||Et||Li),C_{i} = C_{i} \, \times G,T_{i} = N_{i} \oplus h(X_{C} S||SD_{i} ),M_{i} = h(N_{i} \oplus h(X_{C} S||SD_{i} ) \oplus L_{i} \oplus C_{i} ),M_{i} = M_{i} \times G\). In addition, SDi calculates \(t_{i} = T_{i} \oplus X_{CS}\),\(m_{i} = M_{i} \oplus X_{CS}\), and \(e_{t} = (E_{t} \oplus X_{CS} )\) and keeps it in the database. Then, ‘CS’ transmits SIDi, \({C}_{i}^{|}\) to SD using a secure channel. After\(\{{SID}_{i}, {C}_{k}^{|}\)) is received by the SD, it keeps all data safely in a protected memory area. After the time expiration of cookies, Ci is re-computed as\({C}_{i}=h({N}_{i} || {X}_{CS}\left|\left|{E}_{t}\right|\right|{SID}_{i})\).

3.1.2 Login phase and validation phase

  1. (i)

    Initially, SDi selects a random number N1 and then determines (M1, M2) where M1 = (N1.G) and \({\mathrm{M}}_{2}=h\left({N}_{1} . {C}_{i}^{|}\right)\) and asks for login demand to SD.

  2. (ii)

    After successfully receiving login credentials, SD computes \(N_{s} = T_{i} \oplus h(X_{CS} || SID_{i} )\;and\;C_{i} = h\left( {N_{s} || X_{CS} || E_{t} || SID_{i} } \right)\). SD re-computes \({\mathrm{M}}_{2}^{*}\) value as h(M1. Ci) and cross-check with the received M2. If both are the same, the SDi proceeds further otherwise the request was discarded.

  3. (iii)

    Now, the SD selects a random number N2, and calculates another point over ECC as M3 = (N2. G) and M4 = (N2. Mi) and transmits (M3, M4) along with Ti to SDi.

  4. (iv)

    Upon receiving M3, M4, and Ti, SD assess\({M}_{i}= {T}_{i} {L}_{i } {C}_{i})\),\({{\mathrm{M}}_{4}^{*}= {\mathrm{M}}_{3} .\mathrm{ M}}_{\mathrm{i}}\). Then, SDi validates the received M4 value against the computed M4 value. If matches, login is successful, otherwise asks to re-login again.

  5. (v)

    Then, SIDi generates the new session key i.e., SY = (N1. M3) = (N1.N2.G), and Oi = h(N1. Ci) || SY and then transmits Oi to the cloud server.

  6. (vi)

    After receiving Oi, CS re-computes the session key to validate against the received SY. If matches, authentication is successful.

3.2 Security attacks and flaws in Kumari scheme

3.2.1 Security attacks

  1. (i)

    Exposing session-key information–If the random number selected for generating a session key is exposed to the adversary in some means, SK’s secrecy is jeopardized. In Kumari et al. approach's the session key is computed using only the session’s ephemeral secrets, which is (N1.N2.G) where N1 and N2 are random numbers chosen by SIDi and CS, respectively.

The random numbers created for a particular session are one-of-a-kind, and they must be deleted once the procedure has been completed. Assume that attacker A has access to the random numbers N1 and N2. As G is a public key, A will be able to calculate the session key with ease, as it does not rely depend on other confidences. As a result, the authentication mechanism is vulnerable to this attack.

  1. (b)

    Denial of Service attack (DoSA) – A can perform DoSA by performing the following operations.

    1. a.

      A intercepts login operation is involved between SDi and CS.

    2. b.

      At any point, after the original message has been transmitted, A can explore the captured message to CS and launch a DoSA assault.

    3. c.

      Due to accurate {M1, M2, and SIDi}, CS will validate A. As a result, A can pretend to be a legitimate user. Then, CS replies to A with the message {M3, M4, Ti}.

3.2.2 Ineffective authentication and login phases

  1. (i)

    Let’s say A obtains the device, but the device does not know this because it never confirms its user. EDi will continue to carry through the procedures even if the user enters the password, identity, or both, incorrectly. It immediately generates a random number to start the procedure, then it does \({M}_{1}= ({N}_{1}. G) and {M}_{2}\)=\(h(N1.{C}_{i}^{|})\). Now that M1 has been stored, A sends the request message {M1, M2, SIDi} to the server, which appears to be an appropriate request for a login to the control server. Because it allows any user to log in as a legal user, the strategy becomes ineffective.

  2. (ii)

    A can perform a replay attack to compromise the authentication phase. After CS accepts the login request, CS finds Ns matching to SIDi as\(N_{s} = T_{i} \oplus h\left( {X_{CS} || SID_{i} } \right)\)). Afterward, CS computes Ci and \({M}_{2}^{*}\) and verifies\({M}_{2} ?={M}_{2}^{*}\). It holds \({M}_{2}^{*}=h\left({M}_{1} . {C}_{i}\right)= {M}_{2}\). This operation helps to authenticate A legally. This is one of the design flaws of the Kumari scheme.

  3. (iii)

    An authentication protocol must include the password-changing phase. This is necessary if the user forgets or loses their password, or if the old password is vulnerable to attack. Once the password is revealed, there should be a way to prevent it from being used illegally. By regularly changing passwords, you lower the chance that A will gain access. However, Kumari et al., do not provide a password-changing method that could stop an attacker from impersonating a legitimate user.

3.3 Formal security investigation of Rostampour’s scheme

Rostampour’s method consists of two different phases, namely (i) Registration phase (ii) Login phase followed by the authentication phase. The SPDL using property-driven model checking is utilized to reveal the Rostampour scheme as given in Fig. 1.

Fig. 1
figure 1

Scyther setting for DY adversary models

Roles I and R are included in the SPDL modeling where the communication of the SDi is modeled by role I, while the S is modeled by role R. Using send1() method, SDi sends (M1, M2, SIDi) to the server. Using the recv1() function, the server obtains (M1, M2, SIDi). S uses send2() to send (M3, M4) to the DDi. Using the recv2() function, the SDi obtains the (M3, M4). Finally, SDi uses send3() to send Vi to the server. Utilizing the recv3() method, the server obtains the Vi. The N1, N2 must remain a secret throughout the conversation, according to the claim_i1 that belongs to role I besides claim_r1 that resides roles I and R. The SPDL properties-driven model has been primarily conducted under DY model setup as indicated in Fig. 1.

The authentication outcome of the Rostampour et al. system under the DY setup in Scyther Compromise version suggests that the method is secure and involves no attacks. Next, the method was performed under the xck rival scenario illustrated in Fig. 2. The Scyther authentication findings under xck are displayed in Fig. 3. The outcomes show that the system is not secure.

Fig. 2
figure 2

Scyther settings for the xck adversary model

Fig. 3
figure 3

Scyther verification results of the Rostampour et al. scheme under the xck model

Figure 4 displays the assault trace of the Rostampour technique beneath the xck rival model failed to resist against session key disclose, according to the attack trail; as a result, the adversary can leak the secret key. In addition, the Rostampour scheme’s design flaw in computing the session key is the main cause of this. The session key used by Rostampour et al. is calculated using the formula (N1.N2.G). Only the temporary session secrets N1 and N2 are a source of the session key. For the revelation of short-standing secrets to expose the session key, the session key must also be reliant on long-standing secrets.

Fig. 4
figure 4

Attack graph for Rostampour et al. scheme under the xck model

3.4 Formal security investigation of Ummer Iqbal et al. scheme

Ummer Iqbal et al. presented a design of an ECC-reliant technique to offer authentication between smart devices in IoT and the cloud server under the xck challenger model is put forth to get over the drawback of Rostampour’s method. However, using the Scyther Compromise simulation version, we automated the security validation and verification scheme of the Ummer Iqbal et al. under the xck challenger model. The validation shows that, according to the xck adversary model, the technique is not safe and is defenseless to various attacks. The Scyther proof of the Ummer Iqbal et al. scheme under the xck model is displayed in Fig. 5, and attack graph is given in Fig. 6. The outcomes indicate that the system proposed by Ummer Iqbal et al. is also not secure.

Fig. 5
figure 5

Scyther authentication results of the Ummer Iqbal et al. scheme under the xck model

Fig. 6
figure 6

Attack graph for Ummer Iqbal et al. scheme under the xck model

Figure 6 shows the trace of the Ummer et al. method under the xck rival model which is weak against replay and session key disclosing, according to the attack simulation. As a result, the adversary can act as a legitimate device. In Ummer et al. scheme, M1, M2, M3, and M4 values are sent to the server in plain format, thus, the challenger can determine the session key which becomes a main cause to compromise the entire system.

4 Proposed security scheme

The suggested scheme covers two different phases, namely (i) Registration phase, (ii) Login phase, and Validation through the Authentication phase. An IoT device must be registered with the server during the registration step. The registration is carried out over a secure channel, much like with other methods [4]. As there are no shared credentials or a trusted third party used in the smart device, the requirement for a secure registration method is stressed. The following is a list of the actions that were conducted between the smart device in the IoT environment and the cloud server after the registration phase begins.

4.1 Registration phase

  • Step 1: Device SDi selects its identification ITYi and secret key KCS.

  • Step 2: The smart device computes SIDi according to Eqs. 3 and 4 and transmits SIDi to CS as given in Eqs. 3 and 4.

$${\text{ SID}}_{i} {\text{ = K}}_{{cs}} {\text{ }} \cdot \;{\text{ITY}}_{i} {\text{ }} \cdot {\text{G}}$$
(3)
$$ITY_{i} \leftarrow CS : E_{{K_{CS} }} (SID_{i} || T_{1} )$$
(4)
  • Step 3: CS calculates \(h\left({SID}_{i}\right)\)

and generates two subkeys i.e.,\({S}_{CS}^{1}\) and \({S}_{CS}^{2}\) of the same size from \({X}_{CS}\). Also, ensures that \({S}_{CS}^{1} \ne {S}_{CS}^{2}\). The CS computes:

$$C_{i}^{1} = SID_{i} \cdot S_{{CS}}^{1}$$
(5)
$$C_{i}^{2} = SID_{i} \cdot S_{CS}^{2}$$
(6)

The cloud server stores (\({(SID}_{i}, h({SID}_{i})\)) pair along with \({C}_{i}^{1}\) and \({C}_{i}^{2}\) in its database and transmits:\({S\to {SD}_{i}: E}_{{K}_{CS}}({C}_{i}^{1} || {C}_{i}^{2})\).

Step 4: SDi decrypts the received message and stores both \({C}_{i}^{1}\) and \({C}_{i}^{2}\) in it write protected memory area.

4.2 Login phase and authentication phase

The smart device starts the process of logging in to the cloud server at this phase. The server then verifies the device's identity and if it passes muster, a session key is created which can be used between SDi and CS. The following important steps are carried out between SDi and CS during the period of login and authentication.

  • Step 1: Device SDi selects ephemeral secret (ESi) and computes M1 value and M2 value as listed in Eqs. 7 and 8

.

$$M_{1} = (C_{i}^{1} + C_{i}^{2} ). ES_{i} \cdot h\left( {SID_{i} } \right)$$
(7)
$$M_{2} = (C_{i}^{1} + C_{i}^{2} ) \cdot ES_{i}$$
(8)

Then, SDI transmits (M1, M2) to CS as given in Eq. 9.

$$ITY_{i} \to CS : E_{{K_{CS} }} (M_{1} || M_{2} )$$
(9)
  • Step 2: Upon receiving the message, CS authenticates \({ITY}_{i}\)

by executing the steps as follows.

  1. (i)

    The cloud server, CS computes \(h({SID}_{i})\) using \({SID}_{i}\) which exists in its database.

  2. (ii)

    Also, CS computes the multiplicative inverse of \(h({SID}_{i})\) as \({h({SID}_{i})}^{-1}\) and determines\({(M}_{1} . {[h\left({SID}_{i}\right)]}^{-1}\)) = \({M}_{1}^{|}\).

  3. (iii)

    CS checks if \({(M}_{1}^{|} \ne {M}_{2})\) then

  4. (iv)

    {

    $$M_{3} = M_{1} . ES_{s}$$
    (10)
    $$M_{4} = (C_{i}^{1} + C_{i}^{2} ). ES_{i}$$
    (11)

    }

else

discard “login request”.

  1. (v)

    CS generates a session key,\({SK}_{k}=({M}_{2 }. {ES}_{s})= ({X}_{CS} . {K}_{sc} . {SID}_{i} . G . {ES}_{i} . {ES}_{s})\).

  2. (w)

    CS transmits \({M}_{3}\) and \({M}_{4}\) to SDi i.e.,\(C{S \to SD}_{i}\): \({E}_{{K}_{i}}({M}_{3} || {M}_{4})\). Afterward, SDi authenticates the received data by performing the following operations.

  3. (x)

    SDi computes the multiplicative inverse of \(h({SID}_{i})\) as \({h({SID}_{i})}^{-1}\) and determines\({(M}_{3} . {[h\left({SID}_{i}\right)]}^{-1}\)). \({ES}_{i}^{-1}\) =\({M}_{3}^{|}\).

  4. (y)

    CS: if \({(M}_{3}^{|} \ne {M}_{4})\) then

  5. (z)

    Authentication “Successful”

  6. ()

    else

  7. ()

    discard “login response”

  8. ()

    SDi generates a session key,\({SK}_{k}=({M}_{4}. {ES}_{i})= ({X}_{CS} . {K}_{CS} . {SID}_{i} . G . {ES}_{i} . {ES}_{s})\).

  9. ()

    SDi transmits SK to SDi i.e., \({SD}_{i}\to CS\): \({E}_{{SK}_{i}}(h(ES))\).

  10. ()

    Finally, CS decrypts the received \({E}_{{SN}_{i}}(h(ES))\) and checks whether the acknowledged ‘h’ value is not equal to the computed ‘h’ value i.e., h|. If so, the smart device is legitimate.

The overall graphical diagram of the suggested method is given in Fig. 8, and Fig. 7 depicts its SPDL model.

Fig. 7
figure 7

Graphical representation of the proposed method

5 Formal proof of the suggested scheme

To validate the proposed protocol’s security strength on Scyther Compromise 0.9.2 beneath the xck challenger model, it was modeled using SPDL. The roles Device and Server represent the Di and S’s communication patterns, respectively. The send1 function is utilized by the role Device to start the login phase and authentication phase. When the role server receives (M1, M2) using the recv1 function, it transmits (M3, M4) to the device using the send2 function. Finally, the smart device uses the send3 function to send ESK[H(SK)] to the server. The claim_i1 belongs to the Device role and the claim_r1 resides in the server role specifying that the Ki and XS be kept private during communication.

The claim_i2 belongs to the role device and claim_r2 resides in the role server specify whether the session key of the adversary rule can reveal \({S}_{k}={X}_{s}.{K}_{sc}.{SID}_{i}.G.{S}_{i}.{S}_{s}\). The purpose of all claims is to check if the authentication operation concerning the security claim (Nisynch, Niagree) is still working. As shown in Fig. 8, the SPDL prototype of the proposed method was validated and verified on the Scyther Compromise 0.9.2 using the xck challenger model and Fig. 8 depicts its outcome. Under the strict xck adversary model, Fig. 9 shows that the suggested protocol is secure and does not weak against any attacks.

Fig. 8
figure 8

SPDL code of the proposed method

Fig. 9
figure 9

Verification results of the proposed scheme

5.1 Security analysis

5.1.1 Replay attack

This type of attack permits a challenger to archive and retransmit messages being exchanged between communicating parties in the future to acquire unauthorized access. Three messages are exchanged between the smart device residing in the IoT environment and the cloud server in the proposed protocol:

$$SD_{i} \to CS:E_{{K_{sc} }} (M_{1} ||M_{2} )$$
(12)
$$CS \to SD_{i} :E_{{K_{sc} }} (M_{3} ||M_{4} )$$
(13)
$$SD_{i} \to CS:E_{{K_{SC} }} \left[ {h\left( {ES} \right)} \right]$$
(14)

Assume that a challenger can eavesdrop on the messages exchanged and keep (M1, M2, M3, M4) along with \({E}_{{K}_{SC}}[h\left(ES\right)]\) during the commencement of the login phase and validation through the authentication phase to perform a replay attack. Allow a challenger to replay the session values (M1, M2) to acquire unauthorized access as given in Eq. 15.

$${{Adversary}} \to CS:E_{{K_{sc} }} [h(M_{1} |{|}M_{2} {)}]$$
(15)

The server checks the request using the time stamp and produces M3 and M4 with a fresh ephemeral secret when it receives (M1, M2). A fresh ephemeral secret is given to the opponent. The adversary has to identify \({SID}_{i}\) and the ephemeral secret formerly used for computation to validate (M3, M4) and then produce a session key. Due to the elliptic curve discrete logarithm (ECDL) problem’s exponential time complexity [22,23,24], the attacker does not have access to either. Because the adversary is unable to provide a valid session key SK for the recent session, \({E}_{{K}_{SC}}\left[h\left(ES\right)\right]\) cannot be computed. Furthermore, the server will not validate the adversary's old \({E}_{{K}_{SC}}\left[h\left(ES\right)\right]\) because the present SK is created on the server's new ephemeral secret. In addition, a small change in one bit in ES will affect many bits in the receiver side when re-computing the hash code. As a result, the scheme's design prevents replay attacks.

5.1.2 Impersonation attack

A challenger attempts to mimic a legitimate smart device in an impersonation attack. Computing is the first step in the login process and verification process (M1, M2). An opponent must have access to information about \({(C}_{i}^{1}, {C}_{i}^{2})\) and H in order to compute (M1, M2) and (SIDi). Over a secure channel, the \({(C}_{i}^{1}, {C}_{i}^{2})\), and H(SIDi) are exchanged between the smart device residing in the IoT environment and the server. Furthermore, because of the computational difficulties of the ECDL problem, although the challenger eavesdrops on (M1, M2) of any preceding login process and verification of session information between the smart device residing in IoT and CS, the \({(C}_{i}^{1}, {C}_{i}^{2})\), and H(SIDi) can never be derived from (M1, M2). Thus, a result, a valid (M1, M2) cannot be computed without knowledge of \({(C}_{i}^{1}, {C}_{i}^{2})\), and H(SIDi), as a challenger cannot mimic any genuine smart device by calculating a malevolent (M1, M2).

5.1.3 Message integrity-based attack

The communication sent from the smart device to the cloud server cannot be disguised. During the conversation, the smart device resides in the IoT layer and CS exchange the following messages: M1, M2, M3, M4 and \({E}_{{K}_{SC}}\left[h\left(ES\right)\right]\). Assume an attacker intercepts M1, M2, M3, M4, and ESK[H(SK)] and wishes to construct malevolent: MS1, MS2, MS3, MS4. However, the enemy must access XS and Ki to generate MS1, MS2, MS3, and MS4. XS and Ksc are unavailable to the adversary. Furthermore, due to the computational difficulty of the ECDL problem, extracting the private key of XS from M1, M2, M3, and M4 takes an exponential amount of time. As a result, the computational infeasibility of the ECDL problem protects the integrity of M1, M2, M3, and M4. Furthermore, because it is secured using the symmetric key encryption algorithm and the one-way hash, the message \({E}_{{K}_{CS}}\left[h\left(ES\right)\right]\) cannot be changed.

5.1.4 Man in middle (MIM) attack

In this type, a remote invader can snoop, masquerade, and modify communication in the middle of a MIM assault by forging any sensitive information shared between the smart device and the server. If the opponent in the middle of the transmission can construct malicious: MS1, MS2, MS3, and MS4 then the MIM attack will be successful. However, the opponent must be able to forge \({(C}_{i}^{1}, {C}_{i}^{2})\) in order to generate malicious MS1, MS2, MS3, and MS4:

$$C_{i}^{1} = {\text{SID}}_{i} \cdot M_{1} \cdot S$$
(16)
$$C_{i}^{2} = {\text{SID}}_{i} \cdot M_{2} \cdot S$$
(17)

The adversary must access XS to forge (\({C}_{i}^{1}\), \({C}_{i}^{1}, { X}_{s})\) is not accessible to the opponent. Furthermore, due to the ECDL problem’s exponential complexity, XS cannot be retrieved from M1, M2, M3, or M4. The MIM attack is alleviated in the proposed approach since the attacker cannot fake M1, M2, M3, or M4 and sufficient authentication is used prior to key formation.

5.1.5 DoS attack

The login processes taking place between SDi and CS can be intercepted by eavesdropper ‘A’. A can investigate the captured message to CS and attempt to conduct a DoS attack at any time after the original message has been broadcast. A cannot launch a denial-of-service attack because all sensitive data transferred between SDi and CS is protected by enciphering and hashing functions.

6 Security study through BAN logic

The suggested scheme's security validity is assessed using BAN logic. The communication principles are denoted by X and Y, while their private keys are denoted by PRI and PRJ, respectively. The BAN symbols are listed in Table 2 [23], and Table 3 lists the BAN claims. Additionally, as deduced in [27], Table 4 lists the synthesis rules.

Table 2 Symbols used in BAN logic
Table 3 BAN claims
Table 4 Security comparison

Assumptions

\(\mathrm{A}1:\mathrm{X}1 \equiv \to {\mathrm{C}}_{\mathrm{i}}^{1}, {\mathrm{C}}_{1}^{2}\) I.

\(\mathrm{A}2:\mathrm{Y}1 \equiv \to {\mathrm{C}}_{\mathrm{j}}^{1}, {\mathrm{C}}_{1}^{2}\) J.

\(\mathrm{A}3:\mathrm{X}| \equiv \#(\mathrm{Y}\) I).

\(\mathrm{A}4:\mathrm{Y}| \equiv \#(\mathrm{Y}\) Y).

\(\mathrm{A}5:\mathrm{Y}\left| \equiv \mathrm{ X}\right|\to \mathrm{Y}\) I.

\(\mathrm{A}6:\mathrm{X}\left| \equiv \mathrm{ Y}\right|\to\) YY.


Idealized form

$$\mathrm{X}\to \mathrm{Y};{\{{\mathrm{Q}}_{1},{\mathrm{Q}}_{2}\}}_{{\mathrm{PR}}_{\mathrm{I}}}\mathrm{ MG}1$$
$$\mathrm{Y}\to \mathrm{X};{\{{\mathrm{Q}}_{3},{\mathrm{Q}}_{4}\}}_{{\mathrm{PR}}_{\mathrm{J}}}\mathrm{ MG}2$$

Goals

$$\mathrm{G}1:\mathrm{Y}| \equiv \mathrm{X}{\to }^{\mathrm{Y}}{\mathrm{PR}}_{\mathrm{X}} \mathrm{Y}$$
$$\mathrm{G}2:\mathrm{Y}\left| \equiv \mathrm{X}\right|\equiv \mathrm{X}{\to }^{\mathrm{Y}}{\mathrm{PR}}_{\mathrm{X}} \mathrm{Y}$$
$$\mathrm{G}3:\mathrm{X}|\equiv \mathrm{X}{\to }^{\mathrm{Y}}{\mathrm{PR}}_{\mathrm{X}} \mathrm{Y}$$
$$\mathrm{G}4:\mathrm{X}\left| \equiv \mathrm{Y}\right|\equiv \mathrm{X}{\to }^{\mathrm{Y}}{\mathrm{PR}}_{\mathrm{X}} \mathrm{Y}$$

BAN analysis

With MG1, we obtain

$$1:\mathrm{X}|\equiv {\{{\mathrm{Q}}_{1}, {\mathrm{Q}}_{2}\}}_{{\mathrm{PR}}_{\mathrm{I}}}$$
$$2:\mathrm{X}\equiv {\{{\mathrm{Q}}_{1}, {\mathrm{Q}}_{2}\}}_{{\mathrm{PR}}_{\mathrm{I}}}$$

From (2), A1 and Rule1, we obtain

$$3:\mathrm{X}|\equiv {\mathrm{Y}| \sim \{{\mathrm{P}}_{1}, {\mathrm{P}}_{2}\}}_{{\mathrm{PR}}_{\mathrm{I}}}$$

YI is part of Q1, Q2. So, as per A3 and Rule6, we obtain

$$4:\mathrm{X}|\equiv \#({\mathrm{Q}}_{1}, {\mathrm{Q}}_{2})$$

From 3 and 4, we obtain

$$5:\mathrm{Y}|\equiv \mathrm{X}| \sim ({\mathrm{Q}}_{1},{\mathrm{Q}}_{2})$$

From 7 and S4, we obtain

$$6:\mathrm{Y}|\equiv \#({\mathrm{Q}}_{1},{\mathrm{Q}}_{2})$$

From 3 and 6 by applying Rule2, we obtain

$$7:\mathrm{Y}|\equiv \mathrm{X}| \equiv {\mathrm{Q}}_{1},{\mathrm{Q}}_{2}$$

YI is the part of Q1 and Q2. As a result, by using Rule 5, we obtain

$$8:\mathrm{ Y}\left|\equiv \mathrm{X}\right|\equiv {\mathrm{Y}}_{\mathrm{I}}$$

As a result of A5, A8, and Rule3, we now have

$$9:\mathrm{ Y}| \equiv {\mathrm{Y}}_{\mathrm{I}}$$

Rules 3 and 10 give us the following

$$10:\mathrm{ Y}| \equiv {\mathrm{X}| \sim \mathrm{ Y}}_{\mathrm{I}}$$

A3 and A10 gives the following

$$11:\mathrm{ Y}| \equiv {\mathrm{X}|| \sim \mathrm{ Y}}_{\mathrm{I}}$$

Rule4 and Rule11 gives the following

$$12:\mathrm{ Y}| \equiv {\#(\mathrm{S}}_{\mathrm{I}})$$

SI is a component of N. As a result, we achieve

$$13:\mathrm{ Y}| \equiv \#(\mathrm{N})$$

From 8, 13 and Rule7, we obtain.

\(14:\mathrm{ Y}| \equiv \mathrm{X}{\to }^{\mathrm{Y}}{\mathrm{PR}}_{\mathrm{X}}\) Y(Goal G1).

The protocol's symmetry characteristic makes it possible for,

\(15:\mathrm{ Y}\left| \equiv \mathrm{X}\right|\equiv \mathrm{Y}{\to }^{\mathrm{Y}}{\mathrm{PR}}_{\mathrm{X}}\) X(Goal G2).

From MG2, we infer that

$$16:\mathrm{ Y}| \equiv {\{{\mathrm{Q}}_{3},{\mathrm{Q}}_{4}\}}_{{\mathrm{PR}}_{\mathrm{J}}}$$
$$17:\mathrm{ Y} \leftarrow {\{{\mathrm{Q}}_{3},{\mathrm{Q}}_{4}\}}_{{\mathrm{PR}}_{\mathrm{J}}}$$

Form 17, Rule1 and A2, we obtain

$$18:\mathrm{ X}\left| \equiv Y\right| \sim {\{{\mathrm{Q}}_{3},{\mathrm{Q}}_{4}\}}_{{\mathrm{PR}}_{\mathrm{J}}}$$

The PRJ is a component of Q3 and Q4. Thus, in accordance with A4 and Rule6, we obtain

$$19:\mathrm{ Y}| \equiv \#({\mathrm{Q}}_{3}, {\mathrm{Q}}_{4})$$

From 17 and 19, we obtain

$$20:\mathrm{ X}\left| \equiv \mathrm{Y}\right|| \sim {\mathrm{Q}}_{3}, {\mathrm{Q}}_{4}$$

From 20 and Rule11, we obtain

$$21:\mathrm{ X}|\equiv \#({\mathrm{Q}}_{3}, {\mathrm{Q}}_{4})$$

Applying Rule 1 to 18, 21, we obtain

$$22:\mathrm{ X}\left|\equiv \mathrm{Y}\right| \equiv {\mathrm{Q}}_{3}, {\mathrm{Q}}_{4}$$

The YY component of the Q3 and Q4 formulas. As a result, while using Rule 5, we obtain

$$23:\mathrm{ X}\left|\equiv \mathrm{Y}\right| \equiv {\mathrm{Y}}_{\mathrm{Y}}$$

As a result of A6, 23 and Rule3, we now have

$$24:\mathrm{ X}|\equiv {\mathrm{Y}}_{\mathrm{Y}}$$

Rule 10 and Rule 18 give us

$$25:\mathrm{ X}\left|\equiv \mathrm{Y}\right| \sim {\mathrm{Y}}_{\mathrm{Y}}$$

A4 and 25 give us

$$26:\mathrm{ X}\left|\equiv \mathrm{Y}|\right| \sim {\mathrm{Y}}_{\mathrm{Y}}$$

From Rule4 and 26, we obtain

$$27:\mathrm{ X}| \equiv \#({\mathrm{Y}}_{\mathrm{Y}})$$

Using Rule 6, we obtain

$$28:\mathrm{ X}| \equiv \#(\mathrm{N})$$

Using 22, 28, and Rule 7 in combination, we arrive at

$$29:\mathrm{ X}|\equiv \mathrm{X}{\to }^{\mathrm{Y}}{\mathrm{PR}}_{\mathrm{X}} \mathrm{Y}$$

The protocol's symmetry characteristic makes it possible for,

$$30:\mathrm{Y}\left| \equiv \mathrm{X}\right|\equiv \mathrm{X}{\to }^{\mathrm{Y}}{\mathrm{PR}}_{\mathrm{X}} \mathrm{Y}$$

7 Performance comparison with existing schemes

7.1 Based on security

Table 4 compares the proposed scheme's security to that of relevant existing systems. Chang et al. solution is susceptible to impersonation and traceability attacks and only TA3 and TA4 traits are supported by Kumari et al. Rostampour et al.’s design is the only one that offers TA1–TA5 among the available schemes. Rostampour et al., Kumari et al., and Chang et al. schemes have been analyzed using the xck adversary model, according to Table 1. Rostampour et al. formal validation under xck adversary demonstrate that the technique is not secure against the xck model. In Ummer et al. scheme, values exchanged between the smart device and the server are not secured. This permits the opponent to violate the message integrity and replay attack possible (TA3 – TA4). The suggested method meets all of the TA1 to TA5 security requirements and is secure under the xck paradigm.

7.2 Based on computational overhead

Table 5 shows the assessment concerning computational overhead. TSM: scalar multiplication, TAP: point addition, TOH: one-way hash, TSE/TSD: symmetric encryption, and TMI: multiplicative inverse is among the time complexities considered. The most computationally intensive operation is TECM. Because smart devices in IoT are resource constrained, the computational cost of these smart devices has a significant impact on the scheme's efficiency, as the cloud server becomes computationally influential. Table 5 shows that the suggested solution requires a computational overhead of 1 TSM for the smart device, 4 TSM for the server, and 8 TSM in total. Both, Chang et al. and Kumari et al. schemes require 8TSM + 8 TOH in total. The Rostampour et al. method has the largest device overhead (7 TSM). As the smart device is power constrained, the proposed scheme incurs less computation compared to Ummer et al. scheme. When it comes to scalar multiplication (TSM) overhead, the suggested system requires the same number of scalar multiplications as the other strategies under consideration.

Table 5 Comparison of computational Overhead [13]

7.3 Based on communication overhead

The cost of communication is calculated based on the length of bits shared among the smart device in the IoT layer and the cloud server. We assume a 160-bit elliptical curve E(a,b). The symmetric encryption used generates a 128-bit ciphertext. Three messages are exchanged in the proposed method between SDi and the server, including (M1, M2), (M3, M4), and ESK[H(SK)]. [(320 + 320), (320 + 320)+128] = 1,408 bits are required for completion. Fig. 10 shows the communication cost of the proposed scheme including existing solutions.

Fig. 10
figure 10

Performance comparison based on Communication overhead

7.4 Based on energy overhead

Fig. 11 shows the time spent by different important actions as mentioned in [25] on a MicaZ [26] for assessing the energy spent on a smart IoT device. E = I × V × T [13] is used to calculate how much energy is wasted, where I refers to the current strained, V denotes the voltage, and T refers to the time it takes to complete the process. For a MicaZ mote value i.e., when I = 8 mA and V = 3 V, the proposed approach has a 278.16 mJ energy overhead. Ummer et al. also incur almost the same energy overhead. Figure 11 shows a comparison of the suggested plan’s energy expenditure with that of the relevant current scheme. The Rostampour et al. method has incurred maximum energy overhead at 477.6 mJ.

Fig. 11
figure 11

Performance Analysis based on Energy overhead

Under the xck rival model, Rostampour et al. are insecure. The energy overheads of Ummer et al., Rostampour et al., Kumari et al., and Chang et al. are 278.16 mJ, 477.6 mJ, 271.2 mJ, and 278.16 mJ correspondingly. In addition, Rostampour et al., Kumari et al., besides Chang et al. on the other hand, do not satisfy all security necessities and Ummer et al. scheme partially incorporated replay and message integrity security features. The proposed technique complies with all security requirements and is the only one that has been formally validated by exploring the xck rival model. Therefore, with a computational cost of 272.07 mJ and a communication cost of 1,408 bits, our suggested method is also secure against the xck adversary and satisfies all vital security requirements.

8 Conclusion

For establishing secure IoT-based smart applications, providing authentication between smart devices that specifically reside in the IoT environment and the cloud server is essential. The xck adversary model has not been used to validate the existing approaches for authentic keys shared between smart devices in IoT environments and cloud services. This article presents an improved and lightweight ECC-reliant authentication method between smart devices residing in the IoT environment and the cloud server. The suggested approach is safe and protected under the xck model, according to the Scyther Compromise simulation. In comparison to existing schemes, the proposed method incurs low communication and energy overhead. As, the cloud server is used as a trusted authority, the whole system is dependent on the cloud server which becomes the limitation of the suggested work. Hence, in future we would like to strengthen the security of the cloud server.