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.

A model-based approach for vulnerability analysis of IoT security protocols: The Z-Wave case study / C. Braghin, M. Lilli, E. Riccobene. - In: COMPUTERS & SECURITY. - ISSN 0167-4048. - 127:(2023 Apr), pp. 103037.1-103037.16. [10.1016/j.cose.2022.103037]

A model-based approach for vulnerability analysis of IoT security protocols: The Z-Wave case study

C. Braghin
Primo
;
M. Lilli;E. Riccobene
Ultimo
2023

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.
Z-Wave protocol; IoT security; MITM; formal verification; abstract state machines; ASMETA
Settore INF/01 - Informatica
apr-2023
5-dic-2022
Article (author)
File in questo prodotto:
File Dimensione Formato  
Z-Wave-journal.pdf

embargo fino al 09/04/2025

Tipologia: Post-print, accepted manuscript ecc. (versione accettata dall'editore)
Dimensione 878.71 kB
Formato Adobe PDF
878.71 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
1-s2.0-S0167404822004291-main.pdf

accesso riservato

Tipologia: Publisher's version/PDF
Dimensione 3.04 MB
Formato Adobe PDF
3.04 MB Adobe PDF   Visualizza/Apri   Richiedi una copia
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2434/961510
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 8
  • ???jsp.display-item.citation.isi??? 3
social impact