TY - GEN
T1 - Formal Verification of a Dynamic Multi-factor Secure Communication Protocol
AU - Scott, Kyler R.
AU - Khatri, Sunil P.
AU - Ghrayeb, Ali
N1 - Publisher Copyright:
© 2022 IEEE.
PY - 2022
Y1 - 2022
N2 - In a smart grid, there is much sensitive data that must be transmitted continually. This requires secure communication protocols that are well-suited for use in a smart grid context. A typical smart grid is composed of many agents-like smart meters and control centers-and hence it is necessary that its communication protocols not only are cryptographically secure, but also fast and lightweight. In this paper, we perform formal verification on a novel secure communication protocol to be used in a smart grid. In each protocol iteration, the two parties that wish to communicate will exchange authentication tokens to establish trust and generate session keys. The authentication tokens have three key features: (1) each token is constructed using multiple factors, preventing a single point of failure, (2) the factors are updated dynamically during every protocol iteration, ensuring that authentication keys potentially snooped by an attacker are never reused, and (3) factor updates utilize a True Random Number Generator (TRNG), and therefore cannot be deterministically or algorithmically predicted. This paper describes the protocol as implemented between two arbitrary agents in a smart grid. We realize the protocol in software, and formally verify the protocol using ProVerif. Our results demonstrate that our protocol is a secure and lightweight communication protocol that would be suitable for use in a smart grid.
AB - In a smart grid, there is much sensitive data that must be transmitted continually. This requires secure communication protocols that are well-suited for use in a smart grid context. A typical smart grid is composed of many agents-like smart meters and control centers-and hence it is necessary that its communication protocols not only are cryptographically secure, but also fast and lightweight. In this paper, we perform formal verification on a novel secure communication protocol to be used in a smart grid. In each protocol iteration, the two parties that wish to communicate will exchange authentication tokens to establish trust and generate session keys. The authentication tokens have three key features: (1) each token is constructed using multiple factors, preventing a single point of failure, (2) the factors are updated dynamically during every protocol iteration, ensuring that authentication keys potentially snooped by an attacker are never reused, and (3) factor updates utilize a True Random Number Generator (TRNG), and therefore cannot be deterministically or algorithmically predicted. This paper describes the protocol as implemented between two arbitrary agents in a smart grid. We realize the protocol in software, and formally verify the protocol using ProVerif. Our results demonstrate that our protocol is a secure and lightweight communication protocol that would be suitable for use in a smart grid.
KW - cyber security
KW - lightweight cryptography
KW - secure communication
KW - smart grid
UR - http://www.scopus.com/inward/record.url?scp=85130947732&partnerID=8YFLogxK
U2 - 10.1109/SGRE53517.2022.9774119
DO - 10.1109/SGRE53517.2022.9774119
M3 - Conference contribution
AN - SCOPUS:85130947732
T3 - 3rd International Conference on Smart Grid and Renewable Energy, SGRE 2022 - Proceedings
BT - 3rd International Conference on Smart Grid and Renewable Energy, SGRE 2022 - Proceedings
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 3rd International Conference on Smart Grid and Renewable Energy, SGRE 2022
Y2 - 20 March 2022 through 22 March 2022
ER -