A Security Verification Framework for the LoRaWAN Protocol with Application in the Manufacturing Industry

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.