Formal proof of a vulnerability in Z-wave IoT protocol

Nowadays, IoT (Internet of Things) devices are becoming part of our daily life. Unfortunately, many of them do not use standardized communication protocols with a provable security guarantee. The use of formal methods is, therefore, highly demanded in order to perform property verification and to prevent possible threats and accidents to users. In this paper, we propose a formal verification of the Z-Wave protocol, claimed to be one of the most secure IoT communication protocols thanks to the new S2 Security class, recently added. Specifically, our analysis targets the joining procedure of a device to the Z-Wave net. We exploit the ASMETA formal framework to model the protocol and to perform formal analysis in terms of model validation against informal documented requirements and verification of the protocol correct behaviour with respect to its security goals. The verification process revealed a vulnerability that could be used to perform a successful Man-In-The-Middle (MITM) attack compromising the secrecy of the exchanged symmetric keys.