Haewon Byeon

Formal Verification and Statistical Evaluation of a Strengthened Lightweight AMI Authentication and Key Agreement Protocol for Smart Grid Environments

PDF (820KB), PP.152-160

Views: 0 Downloads: 0

Author(s)

1. Department of Future Technology, Korea University of Technology and Education (KOREATECH), Cheonan 31253, South Korea

* Corresponding author.

DOI: https://doi.org/10.5815/ijieeb.2026.04.10

Received: 19 Feb. 2026 / Revised: 15 May 2026 / Accepted: 29 Jun. 2026 / Published: 8 Aug. 2026

Index Terms

Advanced Metering Infrastructure, Authenticated Key Agreement, Formal Verification, Smart Grid Security, Statistical Evaluation

Abstract

Advanced Metering Infrastructure (AMI) connects smart meters, data concentrator units, and utility control centers through persistent two-way communication. This architecture improves demand response and distributed-energy management, but it also exposes resource-constrained meters to replay, false-data injection, physical extraction, and long-term key compromise. This article develops a formally verified and statistically evaluated lightweight AMI authentication and key agreement protocol for resource-constrained smart-grid deployments. We first reconstruct the AMI authentication workflow as a four-message lightweight authenticated key exchange and map each entity, message, and key dependency to a smart-grid deployment model guided by NISTIR 7628 and IEC 62351. We then identify replay-within-window exposure, insufficient responder freshness, weak identity-to-key binding, missing key-compromise impersonation protection, and retrospective session-key recovery. To address these weaknesses, we propose AMI-AKE, a transcript-bound protocol using ephemeral Curve25519 contributions, session identifiers, nonce and timestamp binding, binding signatures, and separate key-derivation function (KDF) outputs for encryption and integrity. ProVerif-style verification queries and an extended Canetti-Krawczyk (eCK)-oriented game proof are provided for mutual authentication, secrecy, forward secrecy, and key-compromise impersonation (KCI) resistance. A Contiki-OS and ARM Cortex-M4 benchmark with 1,000 repeated trials reports 18.4 +/- 1.2 ms authentication latency, 542 +/- 9.1 sessions/s throughput, and 99.2 +/- 0.4% false-data-injection detection under controlled prototype conditions. The proposed design replaces subjective security labels with objective metrics, confidence intervals, and a reproducible simulation plan for 1,000-10,000 smart meters.

Cite This Paper

Haewon Byeon, "Formal Verification and Statistical Evaluation of a Strengthened Lightweight AMI Authentication and Key Agreement Protocol for Smart Grid Environments", International Journal of Information Engineering and Electronic Business(IJIEEB), Vol.18, No.4, pp. 152-160, 2026. DOI:10.5815/ijieeb.2026.04.10

Reference

[1]National Institute of Standards and Technology, “Guidelines for Smart Grid Cybersecurity,” NISTIR 7628 Study 1, 2014. doi: 10.6028/NIST.IR.7628r1.
[2]International Electrotechnical Commission, “IEC 62351: Power systems management and associated information exchange - Data and communications security,” IEC, Geneva, Switzerland, 2024.
[3]E. Bou-Harb, C. Fachkha, M. Pourzandi, M. Debbabi, and C. Assi, “Communication security for smart grid distribution networks,” IEEE Communications Magazine, vol. 51, no. 1, pp. 42-49, 2013. doi: 10.1109/MCOM.2013.6400446.
[4]A. Hahn and M. Govindarasu, “Cyber attack exposure evaluation framework for the smart grid,” IEEE Transactions on Smart Grid, vol. 2, no. 4, pp. 835-843, 2011. doi: 10.1109/TSG.2011.2163829.
[5]M. Tanveer, M. N. M. Bhutta, B. A. Alzahrani, A. Albeshri, K. Alsubhi, and S. A. Chaudhry, “CMAP-IoT: Chaotic Map-Based Authentication Protocol for Crowdsourcing Internet of Things,” Arabian Journal for Science and Engineering, vol. 49, no. 3, pp. 3453-3466, 2024. doi: 10.1007/s13369-023-08456-9.
[6]C. Tian, J. Ma, T. Li, J. Zhang, C. Ma, and N. Xi, “Provably and Physically Secure UAV-Assisted Authentication Protocol for IoT Devices in Unattended Settings,” IEEE Transactions on Information Forensics and Security, vol. 19, pp. 4448-4463, 2024. doi: 10.1109/TIFS.2024.3378901.
[7]K. Lounis, S. H. H. Ding, and M. Zulkernine, “D2D-MAP: A Drone to Drone Authentication Protocol Using Physical Unclonable Functions,” IEEE Transactions on Vehicular Technology, vol. 72, no. 4, pp. 5079-5093, 2023. doi: 10.1109/TVT.2022.3224567.
[8]C. Boyd and J. M. G. Nieto, “Modeling Key Compromise Impersonation Attacks on Group Key Exchange Protocols,” Journal of Cryptology, vol. 23, no. 4, pp. 597-619, 2010. doi: 10.1007/s00145-009-9048-z.
[9]D. Basin and C. Cremers, “Modeling and Analyzing Security in the Presence of Compromising Adversaries,” in ESORICS 2010, LNCS 6345, pp. 340-356, 2010. doi: 10.1007/978-3-642-15497-3_21.
[10]D. Basin, C. Cremers, J. Dreier, and R. Sasse, “Tamarin: Verification of Large-Scale, Real World, Cryptographic Protocols,” IEEE Security & Privacy, vol. 20, no. 3, pp. 31-39, 2022. doi: 10.1109/MSEC.2022.3155789.
[11]B. Blanchet, “Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif,” Foundations and Trends in Privacy and Security, vol. 1, no. 1-2, pp. 1-135, 2016. doi: 10.1561/3300000004.
[12]R. Canetti and H. Krawczyk, “Analysis of Key-Exchange Protocols and Their Use for Building Secure Channels,” in EUROCRYPT 2001, LNCS 2045, pp. 453-474, 2001. doi: 10.1007/3-540-44987-6_28.
[13]B. LaMacchia, K. Lauter, and A. Mityagin, “Stronger Security of Authenticated Key Exchange,” in Provable Security, LNCS 4784, pp. 1-16, 2007. doi: 10.1007/978-3-540-75670-5_1.
[14]Y. Liu, P. Ning, and M. K. Reiter, “False Data Injection Attacks against State Estimation in Electric Power Grids,” ACM Transactions on Information and System Security, vol. 14, no. 1, Art. no. 13, 2011. doi: 10.1145/1952982.1952995.
[15]O. Kosut, L. Jia, R. J. Thomas, and L. Tong, “Malicious Data Attacks on the Smart Grid,” IEEE Transactions on Smart Grid, vol. 2, no. 4, pp. 645-658, 2011. doi: 10.1109/TSG.2011.2163807.
[16]S. M. Dibaji, M. Pirani, D. B. Flamholz, A. M. Annaswamy, K. H. Johansson, and A. Chakrabortty, “A Systems and Control Perspective of CPS Security,” Annual Reviews in Control, vol. 47, pp. 394-411, 2019. doi: 10.1016/j.arcontrol.2019.04.011.
[17]S. Sridhar, A. Hahn, and M. Govindarasu, “Cyber-Physical System Security for the Electric Power Grid,” Proceedings of the IEEE, vol. 100, no. 1, pp. 210-224, 2012. doi: 10.1109/JPROC.2011.2165269.
[18]C. Cremers and M. Feltz, “Beyond eCK: Perfect Forward Secrecy under Actor Compromise and Ephemeral-Key Reveal,” Designs, Codes and Cryptography, vol. 74, no. 1, pp. 183-218, 2015. doi: 10.1007/s10623-013-9852-1.
[19]H. Krawczyk, “HMQV: A High-Performance Secure Diffie-Hellman Protocol,” in CRYPTO 2005, LNCS 3621, pp. 546-566, 2005. doi: 10.1007/11535218_33.
[20]E. Rescorla, “The Transport Layer Security (TLS) Protocol Version 1.3,” RFC 8446, 2018. doi: 10.17487/RFC8446.
[21]National Institute of Standards and Technology, “Module-Lattice-Based Key-Encapsulation Mechanism Standard,” FIPS 203, 2024. doi: 10.6028/NIST.FIPS.203.
[22]National Institute of Standards and Technology, “Module-Lattice-Based Digital Signature Standard,” FIPS 204, 2024. doi: 10.6028/NIST.FIPS.204.
[23]National Institute of Standards and Technology, “Stateless Hash-Based Digital Signature Standard,” FIPS 205, 2024. doi: 10.6028/NIST.FIPS.205.
[24]S. Rose, O. Borchert, S. Mitchell, and S. Connelly, “Zero Trust Architecture,” NIST Special Publication 800-207, 2020. doi: 10.6028/NIST.SP.800-207.
[25]H. Beguinet, C. Chevalier, T. Ricosset, and H. Senet, “Formal Verification of a Post-Quantum Signal Protocol with Tamarin,” in VECOS 2023, LNCS 14315, pp. 105-121, 2023. doi: 10.1007/978-3-031-49503-1_7.

International Journal of Information Engineering and Electronic Business (IJIEEB)