Security model design and formal verification of MQTT protocol

As a lightweight message transmission protocol, MQTT protocol has been widely used in various application scenarios of the IoT due to its high efficiency and flexibility. With the rapid increase in the number of IoT devices and the diversification of application scenarios, security issues have become particularly important. However, the MQTT protocol’s own security mechanism has security loopholes, such as data tampering during data transmission. This paper focuses on the security of the MQTT protocol, designs and proposes a protocol security mechanism scheme called MQTT-SA, which completes the identity authentication of the communicating parties and ensures that the key generation of both parties is equal and fair, and encrypts the transmitted data. In order to verify whether the protocol is secure, we use formal modeling methods to verify the security of the protocol and verify the protocol model. The results show that the MQTT-SA protocol is secure.