XMPP is an open-standard communication protocol, offering services including near-real-time messaging, presence information and request-response.Owing to its exceptional openness, flexibility and scalability, it has been extensively adopted in cloud computing and the Internet of Things (IoT).Consequently, ensuring the reliability and security of the XMPP protocol is of great importance.In this paper, we employ process algebra CSP (Communicating Sequential Processes) to model the communication mechanism of the XMPP system.Additionally, the model checking tool PAT (Process Analysis Toolkit) is utilized to verify six critical properties: deadlock freedom, client faking, server faking, data reachability, key leakage and data leakage.The verification results demonstrate that the XMPP communication mechanism guarantees reliability and security.

AMQP, serving as the application layer standard protocol for advanced message queuing systems, has garnered widespread adoption in middleware systems, including Rab-bitMQ, ActiveMQ, and Qpid. However, the key properties and security of AMQP's messaging mechanism remain unverified. Hence, in this paper, we employ process algebra CSP to formalize the AMQP and verify properties such as deadlock freedom, data reachability, concurrency, sequence consistency, and scala-bility. The verification results indicate that AMQP satisfies these properties, demonstrating the reliability in message transmission. Moreover, to further analyze the security of AMQP messaging mechanism, the intruder model and SSL protocol model are introduced in this work. Meanwhile, the comparison of the verification results with and without SSL is also presented, showing an improvement of the AMQP messaging mechanism security.

With the booming development of Internet of Things (IoT), the LoRaWAN protocol, a crucial technology in Low Power Wide Area Network (LPWAN), has attracted academic attention. Numerous studies on the security of LoRaWAN have been proposed, and some of these studies have been rigorously verified. However, there is a lack of a unified verification framework for the LoRaWAN protocol. In this paper, we present a unified, comprehensive, and systematic security verification framework for the LoRaWAN protocol. The framework facilitates the construction of CSP model for the LoRaWAN protocol and enables the implementation of these CSP models in PAT with C#. Additionally, it supports the formal verification of the models. By integrating C# into PAT, our framework gains extensibility, flexibility, and broad applicability. Simultaneously, we introduce intruders in our CSP model to simulate five different types of attacks (Replay attacks, DoS attacks, ACK Spoofing attacks, Bit Flipping attacks, and MITM attacks) to evaluate LoRaWAN’s performance in vulnerable environments. To demonstrate the applicability of our framework, we extend it to higher versions of LoRaWAN and apply it in the manufacturing industry. We not only verify the fundamental properties but also validate the security properties by simulating attacks in PAT. Our work would help to diversely analyze the security aspects related to the LoRaWAN protocol, and provide the foundation for the analysis of enhancing its security and robustness.