Formal verification of security properties of the Lightweight Authentication and Key Exchange Protocol for Federated IoT devices

• Autorzy: Jarosz Michał , Wrona Konra , Zieliński Zbigniew

Identyfikatory

DOI

10.15439/2022F169

• Języki publikacji: EN

Abstrakty

EN

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.

• Wydawca: Polskie Towarzystwo Informatyczne
• Czasopismo: Annals of Computer Science and Information Systems
• Rocznik: 2022
• Tom: Vol. 30
• Strony: 617--625
• Opis fizyczny: Bibliogr. 24 poz.

Twórcy

autor

Jarosz Michał

autor

Wrona Konra

autor

Zieliński Zbigniew