A model-based approach for vulnerability analysis of IoT security protocols: The Z-Wave case study. Issue 127 (April 2023)

• Record Type: Journal Article
• Authors: Braghin, Chiara; Lilli, Mario; Riccobene, Elvinia
• Is Part Of: Computers & security. Issue 127(2023)
• Publication Date: 2023-04
• Subjects: Z-Wave protocol -- IoT security -- MITM -- Formal verification -- Abstract state machines -- ASMETA; Computer security -- Periodicals; Electronic data processing departments -- Security measures -- Periodicals; 005.805
• DOI: 10.1016/j.cose.2022.103037
• Languages: English
• ISSNs: 0167-4048

Abstract

Highlights: Definition of a library of primitives to model security communication protocols. Definition of a set of schema for temporal logic formulas to specify confidentiality, integrity and authentication properties and verify protocol security goals. Formal specification of the IoT Z-Wave protocol using the S2 Security class, and model-based validation and verification to analyse protocol properties and vulnerabilities. Abstract: IoT (Internet of Things) devices are extensively used in security-critical services, as for example home door opening, gas monitoring, alarm systems, etc. Often, they use communication protocols with no standardisation and no security guarantee. Unsecured use of connected devices can cause threats or damages to the users, so security assurance, which can be ensured by the use of formal methods, must be guaranteed. Unfortunately practical usage of formal methods during the protocol design is very limited or missing at all. To address the problem of providing the designer with a user-friendly but rigorous design approach based on the use of formal methods, supporting security assurance already at the model level, but hiding the complexity of formal notations and verification techniques, in this paper we propose an approach, based on the Abstract State Machine formal method, for the specification and verification of security protocols. Specifically, we introduce a set of built-in primitives to model communication protocols and their security properties. Security verification can be carried out under the hypothesis of either a passive or an active attacker. The effectiveness of this approach is shown by means of its application to the Z-Wave protocol, claimed to be one of the most secure protocol for IoT devices communication thanks to the addition of the S2 Security class. We show the formal specification of the Z-Wave protocol and the security verification process.