Formal verification of security properties of the Lightweight Authentication and Key Exchange Protocol for Federated IoT devices
Michał Jarosz, Konrad Wrona, Zbigniew Zieliński
DOI: http://dx.doi.org/10.15439/2022F169
Citation: Proceedings of the 17th Conference on Computer Science and Intelligence Systems, M. Ganzha, L. Maciaszek, M. Paprzycki, D. Ślęzak (eds). ACSIS, Vol. 30, pages 617–625 (2022)
Abstract. The federated nature of many high-impact IoT applications introduces several challenges from a security perspective. To address critical challenges related to the authentication and secure communication of Internet of Things devices operating in federated environments, we have developed a Lightweight Authentication and Key Exchange Protocol for Federated IoT (LAKEPFI). LAKEPFI provides a flexible authentication and cryptographic key exchange protocol based on Hyperledger Fabric, leverages the unique configuration fingerprint of an IoT device, and does not require secure storage space in participating IoT devices. Constructing a complex security protocol is an error-prone process. Therefore, it is essential to verify its security properties using various techniques. In this article, we discuss the formal modeling and verification of the security properties of LAKEPFI using verification tools such as Verifpal and Tamarin prover.
References
- N. Suri et al. “Exploring Smart City IoT for Disaster Recovery Operations”. In: Internet of Things (WF-IoT), 2018 IEEE 4th World Forum on. IEEE. 2018, pp. 463–468.
- P. K. Panda and S. Chattopadhyay. “A secure mutual authentication protocol for IoT environment”. In: Journal of Reliable Intelligent Environments 6.2 (June 2020), pp. 79–94.
- Z. Qikun et al. “Multidomain security authentication for the Internet of things”. In: Concurrency and Computation: Practice and Experience ().
- U. Khalid et al. “A decentralized lightweight blockchain-based authentication mechanism for IoT systems”. In: Cluster Computing 23.3 (2020).
- G. Shaoyong et al. “Master-slave chain based trusted cross-domain authentication mechanism in IoT”. In: J of Network and Computer Applications 172 (2020).
- C. Chen et al. “A secure blockchain-based group key agreement protocol for IoT”. In: The Journal of Supercomputing (Feb. 2021).
- M. Santos et al. “FLAT: Federated lightweight authentication for the Internet of Things”. In: Ad Hoc Networks 107 (2020).
- M. Alshahrani and I. Traore. “Secure mutual authentication and automated access control for IoT smart home using cumulative Keyed-hash chain”. In: J of Inf Sec and App 45 (2019), pp. 156–175.
- N. Kshetri. “Can Blockchain Strengthen the Internet of Things?” In: IT Professional 19.4 (2017), pp. 68–72.
- N. Haur et al. Building decentralized applications with Hyperledger Fabric and Composer. Packt Publishing, 2018.
- A. Babaei and G. Schiele. “Physical Unclonable Functions in the Internet of Things: State of the Art and Open Challenges”. In: Sensors 19.14 (2019).
- K. Hofer-Schmitz and B. Stojanović. “Towards formal verification of IoT protocols: A Review”. In: Computer Networks 174 (2020), p. 107233.
- C. B. Z. Shelby K. Hartke. The Constrained Application Protocol (CoAP). Request for Comments (RFC) 7252. IETF, 2014.
- C. Bormann and P. Hoffman. Concise Binary Object Representation (CBOR). RFC 7049. IETF, Oct. 2013.
- C. Bormann, M. Ersue, and A. Keranen. Terminology for Constrained-Node Networks. Request for Comments (RFC) 7228. IETF, May 2014.
- B. Blanchet. “Security Protocol Verification: Symbolic and Computational Models”. In: Principles of Security and Trust. Berlin, Heidelberg: Springer Berlin Heidelberg, 2012, pp. 3–29.
- D. Dolev and A. Yao. “On the security of public key protocols”. In: IEEE Transactions on Information Theory 29.2 (1983), pp. 198–208.
- A. Armando et al. “The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications”. In: Computer Aided Verification. Ed. by K. Etessami and S. K. Rajamani. Berlin, Heidelberg: Springer Berlin Heidelberg, 2005, pp. 281–285. ISBN: 978-3-540-31686-2.
- N. Kobeissi. Verifpal User Manual. Manual. Symbolic Software, 2021. https://verifpal.com/res/pdf/manual.pdf.
- B. Blanchet et al. ProVerif 2.04: Automatic Cryptographic Protocol Verifier, User Manual and Tutorial. 2021.
- D. Basin et al. “Symbolically Analyzing Security Protocols Using Tamarin”. In: ACM SIGLOG News 4.4 (2017).
- M. Abadi. Security Protocols and their Properties. 2001.
- H. Krawczyk. “The Order of Encryption and Authentication for Protecting Communications (or: How Secure Is SSL?)” In: Proceedings of the 21st Annual International Cryptology Conference on Advances in Cryptology. CRYPTO ’01. Berlin, Heidelberg: Springer-Verlag, 2001, pp. 310–331.
- A. Zanatta. Comparison of Tools for the Verification of Cryptographic Protocols. 2021. https://github.com/AlessandroZanatta/Verification-of-Cryptographic-Protocols.