Formal-Modeling-and-Verification-of-MQTT-Using-UPPAAL

We propose a four-step methodological approach for analyzing the security of MQTT using the UPPAAL tool. First, we modeled the three essential protocol components (1) Publisher, (2) Subscriber, and (3) Broker as timed automata to capture their behaviors and interactions. Second, we introduced an additional automaton representing a universal attacker, capable of simulating various malicious behaviors without being restricted to a specific scenario. Third, we formalized fifteen attacks from the CVE repository as CTL properties. These formulas were then adapted and translated into queries compatible with UPPAAL-SMC, enabling verification on the modeled automata and the automatic generation of corresponding attack sequences. Finally, we complemented our analysis by testing generic system properties, such as deadlock and liveness, to ensure the overall reliability of the protocol beyond specific attack scenarios. The results show that all fifteen attack scenarios are satisfied if the attacker knows a valid ID or the name of a topic of a connected client. For the generic properties, all liveness properties are satisfied, ensuring the delivery of essential messages. In contrast, the safety and deadlock properties are not fully guaranteed, revealing intermediate states that may be vulnerable. Reproducibility and Execution of the Proposed Approach To reproduce our results, the UPPAAL-SMC tool must first be installed. The provided XML files can then be imported into the UPPAAL graphical interface to visualize the system modeling and execute the different tests. We provide three files: (i) “VMCAI.XML”, which contains the modeling along with the specific properties of each attack scenario; (ii) “with attacker.XML”; and (iii) “without attacker.XML”, which specify the generic properties with and without the presence of an attacker. For automated evaluation, these files can also be analyzed from the command line using the “verifyta.exe” executable provided by UPPAAL-SMC. The verifier explores the model according to the selected options and produces an execution trace indicating whether the property is satisfied. In case of a violation, a counterexample is generated, detailing the states and transitions that lead to it. Among the options used, the “-t” option controls the level of diagnostic trace (essential, shortest, or fastest), while the “-o” option specifies the search order (breadth-first, depth-first, random depth, or optimized depth). These parameters provide flexibility in the analysis and ensure a consistent execution of our approach across all studied scenarios.