Formal verification and security analysis of MQTT-SN

The wireless sensor network (WSN) is a foundational technology for the Internet of Things (IoT), and the application of WSN has experienced significant growth in recent years. The MQTT-SN (Message Queuing Telemetry Transport for Wireless Sensor Networks) protocol is widely used to meet the communication needs of low-power, resource-constrained sensor nodes in WSN. These sensor nodes are often exposed to security risks in wireless communication. Therefore, it is important to verify the security of MQTT-SN to ensure the confidentiality and reliability of the network and data. In this paper, we first propose an MQTT-SN application model that combines the MQTT-SN protocol with an efficient and lightweight cryptographic authentication algorithm called ChaCha20-Poly1305. Then, we formalize the proposed model using the process algebra CSP (Communicating Sequential Process). Afterward, we verify whether the model satisfies the five basic properties with the help of the model checker PAT (Process Analysis Toolkit). We further utilize C# to implement the complex functions and data structures in our model. Finally, we introduce four kinds of attacks and incorporate these attacks into the original model. And we verify the corresponding security properties again with PAT to assess the performance of our model under security threats. According to the verification results, our proposed model of the MQTT-SN protocol combined with the ChaCha20-Poly1305 algorithm satisfies all the basic and security properties. It can be concluded that our model demonstrates a high level of security.