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.
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.
The proliferation of the Internet of Things (IoT) has worsened the challenge of maintaining data and user privacy. IoT end devices, often deployed in unsupervised environments and connected to open networks, are susceptible to physical tampering and various other security attacks. Thus, robust, efficient authentication and key agreement (AKA) protocols are essential to protect data privacy during exchanges between end devices and servers. The previous work in "Provably Secure ECC-Based Anonymous Authentication and Key Agreement for IoT" proposed a novel AKA scheme for secure IoT environments. They claimed their protocol offers comprehensive security features, guarding against numerous potential flaws while achieving session key security. However, this paper demonstrates through logical and mathematical analyses that the previous work is vulnerable to various attacks. We conducted a security analysis using the extended Canetti and Krawczyk (eCK) model, which is widely employed in security evaluations. This model considers scenarios where an attacker has complete control over the network, including the ability to intercept, modify, and delete messages, while also accounting for the potential exposure of ephemeral private keys. Furthermore, we show that their scheme fails to meet critical security requirements and relies on flawed security assumptions. We prove our findings using the automated validation of internet security protocols and applications, a widely recognized formal verification tool. To strengthen attack resilience, we propose several recommendations for the advancement of more robust and efficient AKA protocols specifically designed for IoT environments.
The rapid proliferation of the Internet of Things (IoT) has connected billions of devices that continuously exchange sensitive data over public wireless channels, making secure authentication a critical requirement. However, most IoT end devices are severely resource-constrained, which renders conventional public-key infrastructures based on RSA, bilinear pairings, or digital certificates impractical. Although many authentication and key agreement schemes have been proposed, recent cryptanalytic studies show that they often either omit essential security properties such as perfect forward secrecy or resistance to ephemeral secret leakage or incur overhead that is unacceptable for low-power nodes. To address this gap, this paper proposes a lightweight Elliptic Curve Cryptography (ECC)-based authentication and key agreement protocol for a three-tier IoT architecture consisting of a user, a semi-trusted gateway server, and an IoT sensor. The protocol relies solely on elliptic-curve scalar multiplication, one-way hash functions, and bitwise XOR operations, avoiding bilinear pairings and certificate management. It achieves mutual authentication among all three parties through timestamped, hash-based authenticators and establishes a contributory session-key derived from fresh ephemeral keys, ensuring perfect forward secrecy. The security of the protocol is established through a detailed informal analysis, demonstrating resistance to major attacks, and is formally verified using the AVISPA tool, where both the OFMC and CL-AtSe back-ends report the protocol as SAFE under the Dolev–Yao adversary model. A comparative performance evaluation against several recent ECC-based authentication schemes shows that the proposed protocol maintains low cost requirements suitable for constrained IoT devices, and resulting in a communication overhead of 1828 bits, which is competitive with most recent ECC-based schemes evaluated, and imposing a minimal storage burden on end devices. The results demonstrate that the proposed protocol achieves a favorable balance between security and efficiency, making it well suited to resource-constrained IoT environments.
The Internet of Things (IoT) cloud model provides an efficient scheme for rapid collection, storage, processing, and analysis of massive node data, and its application has gradually expanded to key areas such as healthcare and transportation. However, the security issues of open channel transmission in IoT still persist. Researchers have proposed a lot of solutions, but the forward secrecy, session key security, and other aspects have not been effectively solved. This paper proposes a provably secure authenticated key agreement scheme, which constructs a secure channel between endpoint, gateway, and cloud server (CS). Compared with other schemes, this scheme has three characteristics: (1) According to the different computing resources of devices, gateways and CSs, a segmented differential authentication and secret key negotiation protocol is designed by using cryptographic primitives with different computing overheads; (2) after verification with the ProVerif tool, rigorous proof with the real‐or‐random (ROR) model, and informal analysis, the protocol has been proven to be secure, effectively guarding against typical threats; and (3) compared with the five most recent schemes, it can be seen that the protocol is at least 35% superior to other schemes in endpoint computational overhead, and it meets 10 security objectives, making it very suitable for application scenarios where endpoint resources are limited.
The internet of things (IoT) and cloud computing are evolving technologies in the information technology field. Merging the pervasive IoT technology with cloud computing is an innovative solution for better analytics and decision-making. Deployed IoT devices offload different types of data to the cloud, while cloud computing converges the infrastructure, links up the servers, analyzes information obtained from the IoT devices, reinforces processing power, and offers huge storage capacity. However, this merging is prone to various cyber threats that affect the IoT-Cloud environment. Mutual authentication is considered as the forefront mechanism for cyber-attacks as the IoT-Cloud participants have to ensure the authenticity of each other and generate a session key for securing the exchanged traffic. While designing these mechanisms, the constrained nature of the IoT devices must be taken into consideration. We proposed a novel lightweight protocol (Light-AHAKA) for authenticating IoT-Cloud elements and establishing a key agreement for encrypting the exchanged sensitive data was proposed. In this paper, the formal verification of (Light-AHAKA) was presented to prove and verify the correctness of our proposed protocol to ensure that the protocol is free from design flaws before the deployment phase. The verification is performed based on two different approaches, the strand space model and the automated validation of internet security protocols and applications (AVISPA) tool.
With the rise of the Internet of Things (IoT), maintaining data confidentiality and protecting user privacy have become increasingly challenging. End devices in the IoT are often deployed in unattended environments and connected to open networks, making them vulnerable to physical tampering and other security attacks. Different authentication key agreement (AKA) schemes have been used in practice; several of them do not cover the necessary security features or are incompatible with resource-constrained end devices. Their security proofs have been performed under the Random-Oracle model. We present an AKA protocol for end devices and servers. The proposal leverages the ECC-based key exchange mechanism and one-way hash function-based message authentication method to achieve mutual authentication, user anonymity, and forward security. A formal security proof of the proposed scheme is performed under the standard model and the eCK model with the elliptic curve encryption computational assumptions, and formal verification is performed with ProVerif. According to the performance comparison, it is revealed that the proposed scheme offers user anonymity, perfect forward security, and mutual authentication, and resists typical attacks such as ephemeral secret leakage attacks, impersonation attacks, man-in-the-middle attacks, and key compromise impersonation attacks. Moreover, the proposed scheme has the lowest computational and communication overhead compared to existing schemes.
Real-time and high-efficient communication becomes a vital property for IoT-enabled equipment, since the application range of the Internet of Things has extended widely. At the same time, the centralized characterization of the cloud computing is gradually unable to meet the demand for both low latency and high computing efficiency. To resolve these issues, new computing paradigms have been introduced, such as edge, dew, and fog computing. Recently, Saurabh et al. introduced a mutual authentication protocol, which was claimed to resist various attacks without the requirement of a trusted server, for dew-assisted IoT devices. However, this paper will show that Saurabh et al.’s scheme lacks forward security and user anonymity. Then, a new authenticated key agreement (AKA) protocol, named e-SMDAS, will be put forward and formally proven secure under the eCK security model. Further, the analysis results of BAN logic and Scyther tool will also confirm the security of e-SMDAS. Finally, the comparative analysis of security features and computation efficiency between e-SMDAS and several recent schemes will be demonstrated at the end of this paper.