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

Ahmed H. Aly, Atef Ghalwash, Mona M. Nasr, Ahmed A. Abd-El Hafez


The Internet of Things (IoT) and Cloud Computing are evolving technologies in the area of information technology. Merging the IoT pervasive 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 to 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. In [1] 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. The verification is performed based on two different approaches, Strand Space Model and Automated Validation of Internet Security Protocols and Applications (AVISPA) tool.


AVISPA; Formal verification; IoT; Lightweight authentication; Strand space model;



  • There are currently no refbacks.

Creative Commons License
This work is licensed under a Creative Commons Attribution-ShareAlike 4.0 International License.

shopify stats IJEECS visitor statistics