Towards formal verification of IoT protocols: A Review

Formal Verification is one of the crucial methods to detect possible weaknesses and vulnerabilities at an early stage. This paper reviews formal methods for an extensive variety of protocols used in the IoT environment. It gives detailed descriptions of the considered properties and the applied methods. An in-depth literature review shows that four application fields can be distinguished, namely: (1) functional checks, (2) checks on security properties, (3) suggestions for enhanced schemes including a priori security property checks and (4) implementation checks of protocols. This paper further offers a comprehensive overview of the covered security properties and of commonly used tools for protocols in the field. Additionally, an extensive description and overview of commonly used model checkers is given and open issues and challenges in the IoT field are addressed.