Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

Indonesian Journal of Electrical Engineering and Computer Science

Formal security analysis of lightweight authenticated key agreement protocol for IoT in cloud computing

Ahmed H. Aly, Atef Z. Ghalwash, Mona Mohamed Nasr, Ahmed Hafez

Published Oct 1, 2021• 6 citations
Publisher

Abstract

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.

DOI
10.11591/ijeecs.v24.i1.pp621-636

Related papers

Secure and Ultra-Lightweight Scheme for Authentication and Key Agreement in the Industrial IoT Environment

Zaid Thabit Hassan, Sanaz Asadinia, Saad Abdulazeez Shaban +1 more

The Industrial Internet of Things (IIoT) refers to the expansion and application of the Internet of Things (IoT) in various industrial settings. Despite the numerous applications of the Industrial Internet of Things and its numerous advantages, the security of data exchanged in the Industrial Internet of Things remains one of the challenges facing this emerging technology. When this data is accessed and manipulated by attackers, the consequences may include disruptions to production processes, financial losses, and even threats to human life. Therefore, given the demand not only to protect information but also to ensure the health and safety of industries, the utmost attention should be paid to the security of data and entities involved in the Industrial Internet of Things. In this paper, an innovative protocol for authentication and key agreement between Industrial Internet of Things devices and cloud servers is proposed. This protocol is designed to deal with security threats and meet various security requirements. The Scyther tool has been used to evaluate the performance and security of the proposed scheme. The evaluation results demonstrate that the proposed protocol effectively maintains all security aspects and outperforms similar schemes in terms of efficiency.

•Feb 9, 2026•0 citations

A Survey on Key Agreement and Authentication Protocol for Internet of Things Application

Mohammad Kamrul Hasan, Zhou Weichen, Nurhizam Safie +2 more

The Internet of Things (IoT) represents a dynamic infrastructure, leveraging sensing and network communication technology to establish ubiquitous connectivity among people, machines, and objects. Due to its end devices’ limited computing resources and storage space, it is not feasible to merely transpose traditional internet security technologies directly to IoT endpoints. Maintaining security while concurrently ensuring performance is a particularly challenging endeavor. This paper provides a review of key agreements and authentication protocols pivotal to the security of IoT. First, this survey discusses the applications that need authentication and key agreement to strengthen their security and current research on these application fields. Subsequently, this paper engages in an in-depth exploration of the phase involved in the scheme of authentication and key agreement, including an examination of the cryptographic techniques employed within these processes. This survey also thoroughly studies the scheme’s security services, potential attacks, formal analysis and informal analysis to ensure resilience against such threats. This study aims to provide a profound understanding of the recent research on authentication and key agreement in IoT applications. It strives to contribute towards strengthening security systems for IoT applications, ensuring their sustainability in the face of evolving threats.

IEEE Access•Jan 1, 2024•127 citations

A Lightweight Authentication and Key Agreement Schemes for IoT Environments

Dae-Hwi Lee, Im-Yeong Lee

In the Internet of Things (IoT) environment, more types of devices than ever before are connected to the internet to provide IoT services. Smart devices are becoming more intelligent and improving performance, but there are devices with little computing power and low storage capacity. Devices with limited resources will have difficulty applying existing public key cryptography systems to provide security. Therefore, communication protocols for various kinds of participating devices should be applicable in the IoT environment, and these protocols should be lightened for resources-restricted devices. Security is an essential element in the IoT environment, so for secure communication, it is necessary to perform authentication between the communication objects and to generate the session key. In this paper, we propose two kinds of lightweight authentication and key agreement schemes to enable fast and secure authentication among the objects participating in the IoT environment. The first scheme is an authentication and key agreement scheme with limited resource devices that can use the elliptic curve Qu-Vanstone (ECQV) implicit certificate to quickly agree on the session key. The second scheme is also an authentication and key agreement scheme that can be used more securely, but slower than first scheme using certificateless public key cryptography (CL-PKC). In addition, we compare and analyze existing schemes and propose new schemes to improve security requirements that were not satisfactory.

Sensors•Sep 18, 2020•23 citations

Authenticated Key Agreement Protocol for Device-to-Gateway Communication in IoT

Cong Pu, Jongho Seol, Nohpill Park +1 more

The advent of Internet of Things (IoT) ushers in a significant potential to integrate individuals, devices, and data, leading to a profound change in our professional and social environments. The small, resource-constrained IoT devices are usually deployed to collect various types of critical data in remote or unmonitored locations. Due to extensive interconnectivity, limited resources, and inadequate security design, IoT systems are vulnerable to communication-specific cyber threats, which aim to disrupt operations, steal sensitive information, or cause damage. To resolve the security concerns in IoT communications, many recent efforts have been devoted to designing authenticated key agreement protocols for IoT systems. However, not only most of the existing solutions fail to adopt cost-effective techniques for resource-limited IoT devices, but also they ignore the differentiation among various data types in the established session keys. A few approaches use traditional physical unclonable functions (PUFs) to address resource concerns, yet they introduce new security issues into IoT systems. Once the PUF cryptographic information is compromised by machine learning attacks, the entire authentication framework collapses. Therefore, in this paper we propose an authenticated key agreement protocol for device-to-gateway communication in IoT systems based on Chebyshev polynomial and probability-based PUF. We examine the proposed protocol’s security features through formal security validation. We also conduct performance evaluation through a simulation-oriented study, and the results clearly prove that the proposed protocol offers superior security and privacy, while maintaining low computational overhead.

IEEE Consumer Communications and Networking Conference•Jan 9, 2026•1 citation

Security Evaluation of Provably Secure ECC-Based Anonymous Authentication and Key Agreement Scheme for IoT

Kisung Park, Myeonghyun Kim, Youngho Park

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.

Sensors•Jan 3, 2025•6 citations

A LIGHTWEIGHT ECC-BASED AUTHENTICATION AND KEY AGREEMENT PROTOCOL FOR RESOURCE-CONSTRAINED IOT

Nusrat Hamid Shah, Saiful Adli Ismail, Azızul Azizan

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.

Journal of Information System and Technology Management•Jun 30, 2026•0 citations
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.
The Industrial Internet of Things (IIoT) refers to the expansion and application of the Internet of Things (IoT) in various industrial settings. Despite the numerous applications of the Industrial Internet of Things and its numerous advantages, the security of data exchanged in the Industrial Internet of Things remains one of the challenges facing this emerging technology. When this data is accessed and manipulated by attackers, the consequences may include disruptions to production processes, financial losses, and even threats to human life. Therefore, given the demand not only to protect information but also to ensure the health and safety of industries, the utmost attention should be paid to the security of data and entities involved in the Industrial Internet of Things. In this paper, an innovative protocol for authentication and key agreement between Industrial Internet of Things devices and cloud servers is proposed. This protocol is designed to deal with security threats and meet various security requirements. The Scyther tool has been used to evaluate the performance and security of the proposed scheme. The evaluation results demonstrate that the proposed protocol effectively maintains all security aspects and outperforms similar schemes in terms of efficiency.
The Internet of Things (IoT) represents a dynamic infrastructure, leveraging sensing and network communication technology to establish ubiquitous connectivity among people, machines, and objects. Due to its end devices’ limited computing resources and storage space, it is not feasible to merely transpose traditional internet security technologies directly to IoT endpoints. Maintaining security while concurrently ensuring performance is a particularly challenging endeavor. This paper provides a review of key agreements and authentication protocols pivotal to the security of IoT. First, this survey discusses the applications that need authentication and key agreement to strengthen their security and current research on these application fields. Subsequently, this paper engages in an in-depth exploration of the phase involved in the scheme of authentication and key agreement, including an examination of the cryptographic techniques employed within these processes. This survey also thoroughly studies the scheme’s security services, potential attacks, formal analysis and informal analysis to ensure resilience against such threats. This study aims to provide a profound understanding of the recent research on authentication and key agreement in IoT applications. It strives to contribute towards strengthening security systems for IoT applications, ensuring their sustainability in the face of evolving threats.
In the Internet of Things (IoT) environment, more types of devices than ever before are connected to the internet to provide IoT services. Smart devices are becoming more intelligent and improving performance, but there are devices with little computing power and low storage capacity. Devices with limited resources will have difficulty applying existing public key cryptography systems to provide security. Therefore, communication protocols for various kinds of participating devices should be applicable in the IoT environment, and these protocols should be lightened for resources-restricted devices. Security is an essential element in the IoT environment, so for secure communication, it is necessary to perform authentication between the communication objects and to generate the session key. In this paper, we propose two kinds of lightweight authentication and key agreement schemes to enable fast and secure authentication among the objects participating in the IoT environment. The first scheme is an authentication and key agreement scheme with limited resource devices that can use the elliptic curve Qu-Vanstone (ECQV) implicit certificate to quickly agree on the session key. The second scheme is also an authentication and key agreement scheme that can be used more securely, but slower than first scheme using certificateless public key cryptography (CL-PKC). In addition, we compare and analyze existing schemes and propose new schemes to improve security requirements that were not satisfactory.
The advent of Internet of Things (IoT) ushers in a significant potential to integrate individuals, devices, and data, leading to a profound change in our professional and social environments. The small, resource-constrained IoT devices are usually deployed to collect various types of critical data in remote or unmonitored locations. Due to extensive interconnectivity, limited resources, and inadequate security design, IoT systems are vulnerable to communication-specific cyber threats, which aim to disrupt operations, steal sensitive information, or cause damage. To resolve the security concerns in IoT communications, many recent efforts have been devoted to designing authenticated key agreement protocols for IoT systems. However, not only most of the existing solutions fail to adopt cost-effective techniques for resource-limited IoT devices, but also they ignore the differentiation among various data types in the established session keys. A few approaches use traditional physical unclonable functions (PUFs) to address resource concerns, yet they introduce new security issues into IoT systems. Once the PUF cryptographic information is compromised by machine learning attacks, the entire authentication framework collapses. Therefore, in this paper we propose an authenticated key agreement protocol for device-to-gateway communication in IoT systems based on Chebyshev polynomial and probability-based PUF. We examine the proposed protocol’s security features through formal security validation. We also conduct performance evaluation through a simulation-oriented study, and the results clearly prove that the proposed protocol offers superior security and privacy, while maintaining low computational overhead.
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.