1 Introduction

The Internet of Things (IoT) is a setup of different entities like objects, people, and animals capable of transferring data over networks without head-to-head or head-to-computer connection. IoT is an acronym for Any time, Anything, Any place connections. In recent years, the Internet of Things (IoT) has risen to prominence as a critical technological component for overcoming interoperability, heterogeneity, and Internet-aware resistances.

The deployment of IoT devices has increased exponentially, resulting in a large amount of data handling and analysis [8]. There is a need for a standard platform to manage heterogeneous natured gadgets and data. Cloud-based infrastructures are well suited to this need. Ray, in his survey paper, describes applications for the IoT cloud platforms [39]. In general, cloud services are of two types: public cloud services and private cloud services. A person or organization owns private cloud services that make cloud security essential [53]. Analysis of the cloud-based IoT (CIoT) device mechanism [2, 7, 14, 36] shows that most applications carry essential information, and leakage of such information may lead to a significant loss and several attacks. Also, the nature of attacks changes from time to time. Computing resources are employed on-demand via a network in the Cloud services. It consumes a significant amount of energy, which does not measure easily with computational resources. Pete et al. [37] proposed an experimental energy-efficient model for Virtual Machines (VMs) scheduling over the Cloud; furthermore, Kumar et al. [27] illustrate an economically efficient model for virtualization over the Cloud using a docker container.

Authentication is a primary security mechanism for all network-based services that prevent unauthorized users or adversaries from gaining access [48]. It is compulsory to ensure that only authenticated users should access the resources. For information exchange through an unsecured network such as the Internet, IoT authentication can ensure the trust of IoT devices. A robust IoT authentication model is needed to protect unauthorized users and devices. Traditional public-key cryptosystems are commonly used in authentication procedures. Traditional public-key cryptosystems, such as RSA, have large key sizes and use a lot of computing resources [46]. As a result, most standard authentication systems are incompatible with the limited computational power of IoT devices. Recently, several research papers addressed IoT authentication and the possibility of attacks [4, 22, 30, 34, 51, 52]. However, many attacks are still unresolved, such as packet analysis, gateway forgery, and Sybil attacks. Choosing an appropriate protocol to address recent attacks is tough task, due to unavoidable resource constraints, such as low power support, small storage, low computational support, and low latency support. The proposed protocol is a solution for above said challenges. The significant contributions of this paper have been listed as follows:

  • A novel protocol has been proposed for the IoT infrastructure based on a cloud environment.

  • The proposed novel authentication protocol prevents adversaries from common attacks such as Man in the middle, Masquerade, Denial of Services (DoS), Forging, Guessing, and physical attacks.

  • It can provide robust and secure authentication using the Elliptic Curve Discrete Logarithm Problem (ECDLP) property of ECC with hash and XOR functions. NP-hard complexity of ECDLP makes the protocol resistant to attacks such as Forging, guessing, and Man in the middle, and the inclusion of XOR and hash keeps it lightweight.

  • The proposed protocol has been compared with the existing protocols to explore its ability to resist attacks, reduce computation power and storage requirements, etc. Its computational cost is very low (0.2 s) and resists more than fifteen modern attacks. It also shows its usefulness more than other existing protocols.

  • The modular structure of protocols varies from application to application. We have tried to modal the proposed protocol in such a way so that it suits 90% of IoT infrastructures.

  • Simulation of the proposed protocol using AVISPA [5, 44] and BAN logic [43, 50] proves its power against active adversaries.

  • Description of BAN logic and AVISPA in the present article would allow readers to understand and apply these tools for other protocols easily.

The rest of the paper deals with the following way - Section 2 discusses the related work, followed by section 3, which describes the Preliminaries. Section 4 presents the details of the proposed protocol. Section 5 discusses the performance and security analysis. Finally, the paper presents the conclusion and future work in section 6.

2 Related works

The selection of proper methodology for securing the flow of information plays a vital role in secured and safe communication. This selection varies for different applications, such as polynomial congruence is used for multimedia encryption over the Cloud [26]. Similarly, the secret-sharing concept has been used to encrypt video [31, 40]. The proposed protocol meets the requirements of real-time applications by minimizing the required time and enhancing the efficiency of the encryption process. Similarly, Gadicha et al. [17] present a multimode approach of data encryption in images through Quantum Steganography. This work opens a new chapter in modern quantum cryptography dealing with images in multi-modal aspects.

In general, Confidentiality, Integrity, and Availability (CIA) are the main features to be taken care of in the case of traditional security. In contrast, in the case of IoT, security measures vary from application to application. In 2020, Iqbal et al. [21] assessed IoT security requirements, challenges, and remedies in-depth. From there, it is clear that authentication is mandatory for almost all applications related to cloud-based IoT infrastructure.

In their survey paper, Nandy et al. [35] reviewed all aspects of IoT authentication. It also explains the taxonomy of all possible attacks on IoT authentication, factors involved in choosing the authentication technique, and the tools for simulation of authentication protocols for IoT devices. Authentication protocols are usually based on three parameters: biometric features of users, credentials, and smart cards. In 1981, Lamport [29] proposed a password-based authentication protocol for untrusted networks. However, a stolen-verifier attack was found in password table-based protocols at the server end. After that, numerous protocols have been proposed using a single or combination of the techniques such as Smart card, Password, and Biometrics. In 1985, Victor Saul Miller [33] and Neal I. Koblitz [19] came up with the elliptic curve in cryptography. Elliptic curve cryptography (ECC) algorithms have been used since 2004 widely due to their small size and low computational requirements with the same security level as RSA [21, 48]. In [10, 23, 28, 38], authors have worked with the Computational hardness of ECC for IoT devices. In [24], Kim et al. have done cryptanalysis of the hash function. Protocols like [22, 42, 52], and others have used hashed-based algorithms, which are helpful to ensure the integrity of the messages and verify the sender as well.

In 2015, Li et al. [30] proposed a mutually authenticated protocol based on a smart card in cloud computing. Their protocol does not persist against physical attack, forging attack, and masquerade attack [50]. Furthermore, Sun et al. [43] proposed a novel remote user authentication and key agreement protocol for the mobile client-server Environment. Still, it does not provide a pleasant process of password update and biometric change [50].

After that, in 2016, an efficient authentication protocol was proposed for IoT-enabled devices in a distributed cloud environment by Amin et al. [4]. In this work, different attacks has been discussed, such as user anonymity, insider attack. In 2018, Challa et al. [26] analyzed that Amin et al. protocol [4] does not resist masquerade attacks such as privileged-insider attacks and impersonation attacks. An adversary can send a valid login message on behalf of the user. In 2018, Wu et al. [51] explained that Irshad et al. [22] and Amin et al. [4] are vulnerable to Privileged Insider (PI) attacks and Offline Password Guessing (OPG) attacks, respectively. They both do not guarantee User Anonymity (UA).

Recently, Wu et al. [52] analyzed Xu et al. protocol [51]. They concluded that Xu et al. protocol could not resist Privileged Insider (PI) and stolen Smart Card (SSC) attacks and did not provide pre-verification and Perfect Forward Secrecy (PFS). If we look deep into the hash functions, we can get an exciting result. If the attacker replaces the contents of two messages, such as msg1 with msg2, the receiver will not detect this change since both messages generate the message same hash. This defect may allow adversaries to play with the networks that lead to various attacks such as user and sensor impersonation attacks and guessing attacks. In this scenario, the protocols discussed above may not be able to resist modern attacks.

Considering the shortcomings of the above-discussed protocols, we have proposed this protocol. It uses ECC along with the hash and XOR operators. ECDLP makes the proposed protocol resist the above-discussed attacks and other recent attacks due to its NP-hard complexity. The use of hash and XOR functions keeps the proposed protocol computationally lightweight.

3 Preliminaries

3.1 Elliptic curve discrete logarithm problem (ECDLP)

For two points, P and Q, of an elliptic curve EP(a, b) the ECDLP is to find an integer k ∈ [1, n − 1] such Q = k. P.

ECDLP is more complicated than most discrete logarithm and factorization problems in cryptography. There are several attempts to break this problem; however, it is still unbreakable.

3.2 One-way cryptographic hash function

Here we describe the brief properties of the hash function, which are as follows

  • This function is deterministic h :{0, 1}∗ → {0, 1}n

  • h is the hash function, where output produces y = h(x) (hash digest)y ∈ {0, 1}.

  • Any tiny modification to the input string potentially leads to an entirely different hash value (message digest).

3.3 System model

The modular architecture of IoT-based systems may vary from application to application. We have tried to consider the most common approach suited for 90% of IoT infrastructure. As shown in Fig. 1, the main components of the proposed system are following:

  • User (U),

  • Cloud Server (Sm) directly associated with IoT devices, and

  • Trusted authority (TA) sometimes called a control server

Fig. 1
figure 1

Cloud-based IoT environment authentication model

Full size image

Both user (U) and cloud server (Sm) must register with TA before U can access (Sm) data via a secure channel. Necessary Credentials for U and (Sm) are generated by a Trusted Authority (TA) and stored in their memory. A session key is established (After mutual authentication between U and (Sm) for future independent communication.

3.4 Adversary model

If there is a protocol for some security purpose, there must be some adversary model against which the protocol is safe. A fundamental and most common adversary model was proposed by Dolev and Yao [16] in 1983. It is a broadly accepted model. According to this model, an adversary can read, alter and perform decryption (if got right keys) on messages. Adversaries are unable to carry out any statistical or cryptanalytic assaults. Due to rapid transformation in technologies, adversaries are now more advanced and have extraordinary capacities. Along with the Dolev and Yao model, we have considered that adversaries would know critical information from smart cards (if lost/stolen) using power analysis of smart cards [25, 32]. An adversary would also extract data from network flow using a network analyzer and recent AI techniques [15, 54].

4 Proposed protocol

This section presents an ECC-based protocol designed mainly to ensure that the devices are accessible in a secure manner on public channels. Cloud involvement in all entities and clock synchronization is our assumption for the proposed protocol. In Table 1, we listed necessary and frequent notations with their explanation for the proposed protocol. The proposed protocol comprises different phases, viz., pre-deployment, registration, login, and authentication. In the pre-deployment phase, the setup of the elliptic curve is discussed with the declaration of public and private keys. Registration of cloud server and user have been described in sections 4.2 and 4.3, respectively. After successful registration, verification of the user is done in the login phase via smart card by a trusted authority. In section 4.5, firstly, user authentication proceeded by cloud server authentication is done by a trusted authority. Later, trusted authority is authenticated by both user and cloud server consecutively. At the same time, a session key is established for further communications between the user and the cloud server.

Table 1 Notation used in the proposed protocol
Full size table

4.1 Pre-deployment phase

An elliptic curve EP(b1, b2)of non-singular nature over a finite field Zp is selected by TA, where P is a large prime and 4b13 + 27b22 ≠ 0(mod p). At the same time, a base point P of order n over EP(b1, b2) where TA also chooses n.P = O, and a private keydTA ∈ Zp. Then TA computes the public key QTA = dTA.P corresponding todTA. TA chooses the one-way cryptographic hash function. In the same way, cloud servers and the user also compute private keys and public keys using ECC properties.

4.2 Registration of cloud server

  1. 1.

    Cloud server Sm chooses identity (sidm),dcs ∈ Zcsand Qcs = dcs. P after that sends {sidm, dcs and Qcs} securely to TA as shown in Fig. 2.

  2. 2.

    TA computespsidm= h (sidm||dcs) andBsm = h(psidm‖ QTA).

  3. 3.

    TA sends BsmtoSm, which saves Bsm and dcs in the server memory.

Fig. 2
figure 2

Cloud Server Registration

Full size image

4.3 User registration phase

  1. 1.

    User chooses identity (Ui), password (Pu), du ∈ ZP and Qu = du. P as shown in Fig. 3.

  2. 2.

    User calculate Au = h(pu‖du), PIDu = h(Ui‖Qu) and bbu = Qu ⊕ Au

  3. 3.

    Then user send Au and PIDu to a Trusted Authority (TA)

  4. 4.

    After receiving Au and PIDu, TA calculates h(Au‖PIDu), Du = h(PIDu‖dTA) and Eu = Du ⊕ Au

  5. 5.

    After step 4, TA send [Cu, Eu] to the user

  6. 6.

    User again calculate DPu = h(Ui‖Pu) ⊕ du

  7. 7.

    User saves [Cu, Eu, DPu]in the smart card.

  8. 8.

    Finally, a smart card holds [Cu, Eu, DPu, h(.), ECC parameters]

Fig. 3
figure 3

User Registration

Full size image

4.4 Login phase

  1. 1.

    Firstly, a smart card is punched into the card reader by the legal user for accessing server resources, and then the user provides Id and password (Ui∗, Pu∗) in the card reader terminal, as shown in Fig. 4.

Fig. 4
figure 4

pre-verification from card reader

Full size image
  1. 2.

    After first step card reader calculates the following

  1. (i)
    $$ {d}_u\ast ={DP}_u\oplus h\left({U}_i\ast \parallel {P}_u\right)\kern1em and\kern1em {A}_u\ast =h\left({p}_u\ast \parallel {d}_u\ast \right) $$
  2. (ii)
    $$ \kern0.5em {Q}_u\ast ={bb}_u\ast \oplus {A}_u\ast $$
  3. (iii)
    $$ {PID}_u\ast =h\left({U}_i\ast \parallel {Q}_u\ast \right) $$
  4. (iv)
    $$ {C}_u\ast =h\left({A}_u\ast \parallel {PID}_u\ast \right) $$

Card reader checks the condition Cu ∗  = Cu, Ui ∗  = Ui,and Pu ∗  = Pu if satisfies, then proceed for an authentication phase.

4.5 Authentication phase

After the login phase, the smart card produces a nonce Nu, Calculate Du = Eu ⊕ Au, Fu = Du ⊕ Nu, and Zu = SIDm ⊕ h(Du‖Nu) and send [Fu, Zu, PIDu, TSu],to the cloud-serverSm, here (SIDm) is the cloud server identity chosen by the user and TSu is the user’s timestamp.

The following steps are done on the Cloud server-side, as shown in Fig. 5.

  • 1.1 At the cloud server, it checks timestamp TSm − TSu < ΔT (Stop here if it fails, where TSm is a current timestamp and ΔT is the time interval to be expected during message transmission, respectively)

  • 1.2 Cloud server produces 128 bits nonce Nm .

Fig. 5
figure 5

Authentication of User and Cloud Server

Full size image
  1. 1.

    3 Calculates Jm = Bsm ⊕ Nm and sends [Jm, psidm, Fu, Zu, PIDu, TSu, TSm] to TA.

  2. 2.

    After receiving the above keys, TA confirms the validity of timestamp (TTA − Tsu < ΔT) and calculatesNu ∗  = Fu ⊕ Du, SIDm ∗  = Zu ⊕ Du and check SIDm ∗  = SIDm and \( {\mathrm{N}}_{\mathrm{u}}^{\ast }={\mathrm{N}}_{\mathrm{u}} \). If this is ok then TA authenticates the user as the legal user.

  3. 3.

    After authenticated User, TA computes Bsm = h(psidm‖QTA) and \( {N}_m^{\ast }={B}_{sm}^{\ast}\oplus {J}_m \) and checks \( {B}_{sm}^{\ast }={B}_{sm} \) and Nm ∗  = Nm if it is ok, TA authenticates the Cloud server.

  4. 4.

    After Authenticated User and Cloud server, TA chooses a 128-bit nonce NTAand computes the following:

  1. (v)
    $$ {P}_{TA}={N}_m\oplus {N}_{TA}\oplus h\left({N}_u\parallel {D}_u\right) $$
  2. (vi)
    $$ {SK}_{TA}=h\left({N}_u\oplus {N}_m\oplus {N}_{TA}\right) $$
  3. (vii)
    $$ {R}_{TA}={N}_u\oplus {N}_{TA}\oplus h\left({B}_{sm}^{\ast}\parallel {N}_m^{\ast}\right) $$
  4. (viii)
    $$ {Z}_{TA}=h\left(\left({N}_m\oplus {N}_{TA}\right)\parallel \kern1em {SK}_{TA}\right) $$
  5. (ix)
    $$ {V}_{TA}=h\left(\left({N}_u\parallel \kern1em {N}_{TA}\right)\parallel \kern1em {SK}_{TA}\right) $$

Finally SKTA is the secret session key.

The TA sends [PTA, RTA, ZTA, VTA ]to the Sm through public communication.

  1. 5.

    After receiving from TA the Sm computes following:

  1. (x)
    $$ {W}_m=h\left({\mathbf{B}}_{\mathbf{sm}}\parallel \kern1em {N}_m\right),{N}_u\oplus {N}_{TA}={R}_{TA}\oplus {W}_m,{SK}_m=h\left({N}_u\oplus {N}_{TA}\oplus {N}_m\right) $$
  2. (xi)
    $$ and\kern1em {V}_{TA}\ast =h\left(\left({N}_u\oplus {N}_{TA}\right)\parallel \kern1em {SK}_m\right) $$

Then, Sm check the condition (VTA∗ = VTA). If yes, then proceed and send [PTA, ZTA] it to the user publicly.

  1. 6.

    On obtaining [PTA, ZTA] fromSm, the user calculates the following:

Lu = h(Nu‖Du ), and SKu = h(Nm ⊕ NTA ⊕ Nu)ZTA∗  = h((Nm ⊕ NTA )‖SKu )

A user checks the condition(ZTA∗  = ZTA) and Nm ⊕ NTA = PTA ⊕ Lu, and an affirmative answer proves that Sm and TA are authentic.

Finally, we see that (as shown in Fig. 6)

  • Mutual authentication is achieved among users Sm and TA.

  • Session key SKm=SKu are established for future communication.

Fig. 6
figure 6

TA authentication

Full size image

5 Security analysis

To demonstrate and validate the security and correctness of our proposed protocol, we use BAN logic [3, 9, 18, 41, 43, 50], followed by Automated Validation of Internet Security Protocols and Applications (AVISPA) [5, 6, 13, 45]. Furthermore, an informal discussion has also been done in the latter part of this section.

5.1 BAN logic (a formal approach of security analysis)

It is very much essential to ensure the correctness of the authentication protocol. In Feb. 1990, MICHAEL BURROWS, MARTIN ABADI, and ROGER NEEDHAM came logically to verify the correctness of an authentication protocol, efficiency, and applicability, termed BAN Logic. Although detailed descriptions are illustrated by M. Burrows et al. [9] and more such as [3, 18, 41, 43, 50], we have tried to summarize BAN logic to understand the main concepts of BAN logic.

By using BAN logic, we can get the following important information about an authentication protocol:

  1. 1.

    The purpose of each protocol (Goal).

  2. 2.

    The cryptosystem that was used.

  3. 3.

    Whether secrets are used or not (other than the key).

  4. 4.

    Is there a guarantee that messages will arrive on time?

  5. 5.

    Whether protocol establishes each party’s presence.

  6. 6.

    To remove redundancy.

The main goal of our protocol is that a user (U), Cloud server (Sm), and Trusted authority (TA) must authenticate one another. A session key (SK) is established for further communication between the server and the user.

Following are the steps used in the proposed protocol. Sentences with bold letters are common in all authentication protocols.

  • In First step, goals are written

  • G1: U believes \( U\overset{SK}{\iff }{S}_m \)

  • G2:UbelievesSm believes \( U\overset{SK}{\iff }{S}_m \)

  • G3: Sm believes \( U\overset{SK}{\iff }{S}_m \).

  • G4:SmbelievesUbelieves \( U\overset{SK}{\iff }{S}_m \).

  • G5:Smbelieves\( {S}_m\overset{SK}{\iff } TA \)

  • G6:Smbelieves TA believes \( {S}_m\overset{SK}{\iff } TA \)

  • G7: TA believes\( {S}_m\overset{SK}{\iff } TA \)

  • G8: TA believesSm believes \( {S}_m\overset{SK}{\iff } TA \)

  • In the second step, the proposed protocols are idealized and written in the form of language of formal logic.

M1 (Message 1): U → Sm: pidu, TSu, Au, \( {E}_u:{\left\langle A\right\rangle}_{\left({D}_u\right)} \), \( {F}_u:{\left\langle {N}_u\right\rangle}_{\left({D}_u\right)} \), \( {Z}_u:{\left\langle {SID}_m\right\rangle}_{\left({D}_u\parallel {N}_u\right)} \).

M2 (Message 2):Sm→TA: M1, psidm, \( {J}_u:{\left\langle {N}_m\right\rangle}_{\left({B}_{sm}\right)} \).

M3(Message3): TA→Sm: \( {P}_{TA}:{\left\langle {N}_m\oplus {N}_{TA}\right\rangle}_{\left(h\left({N}_u\parallel {D}_u\right)\right)} \), \( {V}_{TA}:{\left\langle {N}_u\oplus {N}_{TA}\right\rangle}_{\left({SK}_{TA}\right)} \).

M4(Message4):Sm → U: \( {P}_{TA}:{\left\langle {N}_m\oplus {N}_{TA}\right\rangle}_{\left(h\left({N}_u\parallel {D}_u\right)\right)} \)

  • In the third step, we identify the assumptions which show the initial state of the proposed protocol.

A1 (First assumption):  U ∣  ≡  # (Nu)[U believes fresh(Nu)].

A2: Sm|≡ # (Nu), A3: TA |≡ # (Nu), A4: Sm|≡#(Nm),

A5: U| ≡#(Nm), A6: TA |≡#(Nm).

A7: TA|≡#(NTA), A8: U| ≡#(Nm ⊕ NTA), A9: U |≡#(Nu ⊕ NTA).

A10:U|\( \equiv U\overset{D_u}{\iff }{S}_m \), A11:Sm|≡(\( U\overset{SK}{\iff }{S}_m \)),

A12:Sm|≡(\( {S}_m\overset{B_{sm}}{\iff } TA \)), A13: TA|≡(\( U\overset{SK}{\iff }{S}_m \)). Many other assumptions can be added in the initial assumption, such as Sm|≡U controls (Nu), TA |≡Sm controlsNm, but they are already evident, so we do not expand that.

In the fourth step (proof), the idealized forms (M1, M2… Mn) of the proposed protocol are analyzed. The basis of the analysis is based on the assumptions and BAN logic rules such as message meaning (MM), Freshness- Conjunction (FC), Belief (BL), Nonce -Verification (NV), Jurisdiction (JR), Session keys (SK). Based on the analysis in the fourth step, we reach the goals.

Using Message 1: U → Sm: pidu, TSu, Au, \( {E}_u:{\left\langle A\right\rangle}_{\left({D}_u\right)} \), \( {F}_u:{\left\langle {N}_u\right\rangle}_{\left({D}_u\right)} \), \( {Z}_u:{\left\langle {SID}_m\right\rangle}_{\left({D}_u\parallel {N}_u\right)} \) and seeing rule we get.

S1: Sm ⊲ pidu, TSu, Au, \( {E}_u:{\left\langle A\right\rangle}_{\left({D}_u\right)} \), \( {F}_u:{\left\langle {N}_u\right\rangle}_{\left({D}_u\right)} \), \( {Z}_u:{\left\langle {SID}_m\right\rangle}_{\left({D}_u\parallel {N}_u\right)} \).

Applying MM rule with S1, A11 results in S2: Sm ∣  ≡ U ∣  ≡ Nu.

Applying FC and NV rules A2, S2, results in S3: Sm ∣  ≡ U ∣  ≡ Nu (hereNu is a required parameter of the proposed protocol’s session key.)

Applying JR rule with A14, S3 results in S4: Sm ∣  ≡ (Nu).

Applying SK rule with A2, S3 results in S5: \( {S}_m\mid \equiv U\overset{SK}{\iff }{S}_m \)(G3).

Applying the NV rule with A2, S3 results in S6: \( {S}_m\mid \equiv U\mid \equiv U\overset{SK}{\iff }{S}_m \)(G4).

Applying seeing rule on M2: Sm→TA: M1, psidm, \( {J}_u:{\left\langle {N}_m\right\rangle}_{\left({B}_{sm}\right)} \)and results S7: TA ⊲ M1, psidm, \( {J}_u:{\left\langle {N}_m\right\rangle}_{\left({B}_{sm}\right)} \).

Applying MM rule with A13, S7, and results in S8: TA ∣  ≡ Sm ∣  ≡ Nm.

Applying A6, S7, MM, and NV rule results S9: TA ∣  ≡ Sm ∣  ≡ Nm. (Nmis a required parameter of the proposed protocol’s session key.)).

Applying JR rule with A15, S9 results in S10: TA ∣  ≡ Nm.

Applying SK rule with A6, S10 results in S11: \( TA\mid \equiv {S}_m\overset{SK}{\iff } TA \)(G7).

Applying NV rule with A6, S11 results in S12: \( TA\mid \equiv {S}_m\mid \equiv {S}_m\overset{SK}{\iff } TA \)(G8).

Applying seeing rule with M3 results S13: Sm ⊲ PTA, VTA. Results S14: Sm ∣  ≡ TA ∣  ≡ (Nu ⊕ NTA).

Applying FC and NV rule with A12, S14 results in S15: Sm ∣  ≡ TA ∣  ≡ (Nu ⊕ NTA).

Applying SK rule with A9, S15 results in S16: \( {S}_m\mid \equiv {S}_m\overset{SK}{\iff } TA \)(G5).

Applying NV rule with A9, S16 results in S17: \( {S}_m\mid \equiv TA\mid \equiv {S}_m\overset{SK}{\iff } TA \)(G6).

Applying seeing rule with M4: Sm → U: \( {P}_{TA}:{\left\langle {N}_m\oplus {N}_{TA}\right\rangle}_{\left(h\left({N}_u\parallel {D}_u\right)\right)} \) results in S18: U ⊲ PTA.

Applying MM rule with S18, A8 results in S19: U ∣  ≡ Sm ∣  ≡ (Nm ⊕ NTA).

Applying FC and NV rule with S19, A10 results in S20: U ∣  ≡ Sm ∣  ≡ (Nm ⊕ NTA).

Applying SK rule with A10, S20 results in S21: \( U\mid \equiv U\overset{SK}{\iff }{S}_m \) (G1).

Applying NV rule with A8, S21 results in S22: \( U\mid \equiv {S}_m\mid \equiv U\overset{SK}{\iff }{S}_m \)(G2).

Thus, the above steps are used in BAN logic to verify the authentication protocols.

5.2 AVISPA: A simulator for authentication protocols

It is vital to have tools that support the rigorous analysis of security protocols to speed up the next generation of security protocols and improve their security. For that, it detects weaknesses and establishes their correctness. In 2005, Armando et al. [6] came with a push-button tool for the automated validation of Internet security-sensitive protocols and applications named AVISPA. The tool is used by a protocol designer who describes a security problem in the High-Level Protocol Specification Language HLPSL [20]. Moreover, detailed studies of AVISPA and its execution are available in [5, 6, 13]. In addition to this, some essential tricks to write the protocols in HLPSL language are reported in our work, followed by screenshots of our protocol result.

  • First and foremost, the Role of each participant is written, which contains the Role name, declaration of local as well as constant variables, and transition.

  • When the Roles of participants are defined, Roles are combined in a session.

  • Define the Environment in which protocol is analyzed that contains prior knowledge about the intruder, the scenario to be executed, and the session instances to be run in parallel.

  • Finally, we declare security properties of protocol to be executed.

We have passed our protocol with all four utilities provided by AVISPA tools that are following:

  1. 1.

    On-the-fly Model-Checker (OFMC): Performs protocol falsification and bounded verification.

  2. 2.

    Constraint-Logic-based Attack Searcher (CL-AtSe): It can identify type flaws and manage message concatenation associativity.

  3. 3.

    SAT-based Model-Checker (SATMC): constructs a propositional formula encoding a bounded unrolling of the IF’s specified transition relation, the initial state, and the set of conditions denoting a breach of the security properties.

  4. 4.

    TA4SP (Tree Automata based on Automatic Approximations for the Analysis of Security Protocols): Regular tree languages and rewriting are used to approximate attacker knowledge. Our protocol passed all four tests.

5.3 Informal analysis of attacks

In these subsections that follow, we do a preliminary study to show the secrecy of the proposed protocol against a wide range of threats.

5.3.1 User anonymity and un-traceability

The identity of user must not be revealed during the exchange of keys among the user, cloud server, and trusted authority. User, cloud server, and trusted authority are generated for each fresh session nonce, respectively. At the same time, different timestamps (TTA,TsuandTsm) validate the session. User identity is concatenated with Qu and hashed with PIDu: ( PIDu = h(Ui‖Qu)). It is passed to the trusted authority. Hence, it is obvious that extracting information about the user’s identity (Ui) is impossible by a third party. So, the proposed protocol preserves user anonymity and the un-traceability of the user’s identity.

5.3.2 Offline guessing attacks (OGA)

The adversary can know various information saved in smart cards using power analysis or differential power analysis attacks [32, 54]. In the proposed protocol, the smart card holds {Cu,Eu,DPu,}. Concatenation and XOR operation on user identity and password preceded by hashing results above parameters. One-way collision resistance property of hash function and uniqueness of ECC makes too hard to get knowledge about user identity and password. Wu.et.al [51] and Tsu et al. [52] are also using almost the same parameters as Amin’s protocol [4]. Possibilities of the same attacks are there in these two protocols. In the proposed protocol, parameters such as user id (Ui), password, and server identity are concatenated with the private key generated on ECC. Then it is hashed with one-way hash function functions. So these consecutive steps eliminate the chance of power analysis attacks.

5.3.3 Perfect forward secrecy (PFS)

Some keys and parameters are readily available to adversaries. PFS ensures that session keys among users, cloud servers, and trusted authorities are unknown to adversaries at any cost. Here in the proposed protocol, assume an adversary wants to compute SKu = SKm = h(Nm ⊕ NTA ⊕ Nu).These three parameters NmNTA and Nu are not available to the adversary because these parameters are always used in hashed conditions and concatenated with elliptic curve points. It is very tough to get a polynomial-time solution to this problem. Hence, the proposed protocol can provide PFS.

5.3.4 Sybil attack (SA)

In a Sybil attack, multiple accounts/nodes are created by an adversary to take over the network. In the proposed protocol, TA’s elliptic curve QTA is involved in the registration and first phase of authentication. Thus ECDLP property of ECC eliminates the chance of private computing key from known parameters. So the uniqueness of private keys disaffects the harm of multiple accounts.

5.3.5 Known session-specific temporary information (KSTIA)

In KSTIA attack, session ephemeral secrets are exposed to the adversary, based on this an adversary would be able to get the session keys. In the proposed protocol, almost all information is hashed and concatenated with the private key. It is very tough to extract information from temporary information. Some researcher explains this attack with the name of Ephemeral Secret Leakage (ESL) Attack.

5.3.6 Stolen smart card attack (SSCA)

At the worst, there may be the situation that information {Cu,Eu,DPu,} are known to intruder A due to the loss or steal of a smart card. But due to h (·) protection secret entities of U, viz.,Cu,Eu and DPu,, are not known to A. Therefore, our protocol is secure against this attack.

5.3.7 Privileged insider attack (PIA)

There is always the possibility of two types of adversaries in a system, outside adversaries and inside adversaries. An inside adversary may have privileged access to TA. In this case an adversary can get information such as Au and PIDuwhile user is registering to TA, but Au = h(Pu‖du), PIDu = h(Ui‖Qu) and {du,Qu} are the points on elliptic curve, so to reveal Pu and Ui from Au and PIDu is almost impossible. Furthermore, if the intruder fetches the information {Cu, Eu and DPu,} from the smart card directly by smart card attack [43, 50], in this case also getting Pu and Ui is very difficult as discussed in stolen smart card attack.

5.3.8 User impersonation attack (U-IA)

An adversary may put Pu and Ui in authentication phase, to impersonate a user U, but to complete authentication by TA, there is need of SIDm and Nu. Getting SIDm and Nu is not possible because Nu = Fu ⊕ Du and Du = Eu ⊕ Au, forAu, Pu is concatenated with du (point of elliptic curve) and transferred to TA in hashed form. Therefore getting Nu is too tough, similar is the condition with SIDm.

5.3.9 Cloud server impersonation attack (C-IA)

An adversary may get the identity of a cloud server (sidm) to impersonate the cloud server, but to be authenticated from trusted authority (TA), Bsm = h(psidm‖ QTA) should be known where psidm= h (sidm||dcs). Here, in this case QTA and dcs are the points of two different elliptic curves. Hence, by using the ECDLP property of ECC, we conclude that our protocol is safe from Cloud server Impersonation attacks.

5.3.10 Trusted authority (TA) impersonation attack (TA-IA)

To impersonate TA, an adversary may attempt to get the key {PTA, RTA, ZTA, VTA } but at cloud server end VTA = h((Nu‖ NTA)‖ SKm)and at user end ZTA = h((Nm ⊕ NTA)‖ SKu) are used for authentication, getting nonces Nu, NTA and Nm in correct form is tough, also collision resistance property of hash function makes almost impossible to get correct keys. Thus, this protocol is safe from TA impersonation attack.

5.3.11 Pre-verification in the smart card

In the login phase several protocols such as [12, 28, 47], does not support smart card to verify the identity and password of user. It puts an extra burden on the server. While in the proposed protocol the smart card checks Cu∗  = Cu, Ui ∗  = Ui, and Pu ∗  = Pu in the login phase. If it is found valid, the proposed protocol proceeds for the authentication phase. Otherwise, the session will be deferred until the right password and identity have been submitted. This means that the proposed protocol saves computational and communication expenses whether there is inaccurate input or an unlawful user. As a result, the proposed protocol successfully provides pre-verification..

5.3.12 Known-key attack (K-KA)

If one session key is compromised, it does not necessarily mean that all other session keys would be as well. The accepted session key in the proposed protocol is based on three random ephemeral secrets Nu, NTA and Nm, which are different for each session. Due to the difficulty of the ECDLP problem, the adversary may not be able to derive all of these at the same time. As a result, revealing one session key does not allow the adversary to learn about additional session keys.

Sometimes researchers call it No key control property.

5.3.13 Replay attack (RA)

In the authentication phase, we have used timestamps {TSu, TSm, TSTA}, and accepted delay (ΔT) is sufficiently tiny, which makes replaying of old messages useless. Hence, our protocol is secure against replay attacks. In Table 2, the summary of the security features of recently published protocols and proposed protocols is given.

Table 2 Security features comparison
Full size table

5.4 Performance comparison

The computational cost of the proposed protocol is compared to that of other protocols in Table III. We have taken experimented values as reported in [1, 3, 10, 49] are following:

Time to compute hash function (Th): 0.0005 s, time to compute ECC multiplication (Tecm):0.06307 s, time to compute fuzzy extractor (Tfe):0.063075. Time to compute ECC point addition (Teca): 0.010875 s. we have ignored time consumed in XOR and concatenation operations. At last, we have plotted a graph for better judgment between security features supported and time consumed by the proposed protocol and other protocols. The graph of summary of security analysis is presented for the ease of readers.

5.5 The efficiency of the proposed protocol

Table 2 compares the proposed protocol to other relevant existing protocols in terms of security and functional elements that are desired or required. Our protocol includes all essential security features. Existing protocols are missing several key features (as discussed in section 5.3, informal analysis of proposed protocols), such as protection against offline password guessing attacks, known key attacks, stolen card attacks, and impersonation attacks. In addition, the proposed protocol provides rigorous security analysis and formal security verification using the widely-accepted AVISPA tool. Table 3 shows that the total overhead of the proposed protocol is 0.2 s, which is much less than most of the existing protocols. Results from Tables 2 and 3 proves the efficiency of the proposed protocol. Furthermore, Fig. 7 makes our claim more claim in terms of performance comparison.

Table 3 Comparison of the computational overhead of our protocols with related protocols
Full size table
Fig. 7
figure 7

Performance Comparison

Full size image

6 Conclusion

This paper first discusses crucial role of IoT devices in our daily lives, the advantages of using cloud computing in IoT devices, and authentication requirements in such an environment. Efficient authentication is the need for the hours for IoT devices. The proposed protocol is computationally very light and successfully resists attacks that are not covered by the currently existing protocol. Elliptic curve discrete logarithm problem (ECDLP) is used with one way hash function and XOR operator. ECDLP property makes the proposed protocols hard to break. The use of one way hash function and XOR operator maintains the efficiency of authentication along with secrecy. The proposed protocol is verified using BAN logic and simulated using HLPSL language for the AVISPA tool. We have added essential tricks to play with BAN logic and the AVISPA tool for any protocols related to the secure use of IoT devices. The generalized approach of the system model makes the proposed protocol implementable for the different scenarios of IoT devices such as Medical IoT, Industrial IoT, and cyber-physical systems. The proposed protocol can be extended for healthcare IoT devices and Industrial IoT by incorporating novel biometric, homomorphic encryption, and iterative learning techniques.