Formal-Based Modeling and Analysis of a Network Communication Protocol for IoT: MQTT Protocol

The MQTT protocol is a widespread standard in the IoT world as it is widely deployed in different IoT applications. In the context of the IoT, a certain level of assurance that a given device does not incorporate vulnerabilities based on its protocol compliance is very fundamental to ensure. Such requirements could be reached through formal verification. In this work, we propose a formal model for the description of the MQTT protocol. In particular, we define a generic model expressive enough to model the different Quality of Service levels of the MQTT protocol. Our model is based on the formalism of timed automata. The formal verification of different properties as well as analysis experiments of the proposed model have been performed automatically using Model-checking.