A Decoupled and Automata-Based Approach for Formal Verification of MeshCoP

Thread is an important mesh networking technology that enables reliable and secure communication among Internet of Things (IoT) devices. At the core of Thread, the Mesh Commissioning Protocol (MeshCoP) authenticates and securely joins new devices. However, the complexity of MeshCoP which arises from cryptographic handshakes among multiple participants poses challenges for the verification. Existing approaches based on the overall models often suffer from state space explosion and limited scalability, making it difficult to analyze both local and global cross phase properties in a tractable way. To address these challenges, we propose a decoupled and automata-based approach for the formal verification of MeshCoP. The commissioning process of MeshCoP is decomposed into four individual phases, and each phase is modeled as a network of timed automata in UPPAAL. Then, the four decoupled models are independently verified to ensure internal correctness, effectively reducing complexity. Subsequently, inspired by the Assume-Guarantee method, we further abstract these submodels based on the verified properties, omitting the details of the interactions and preserving local correctness. Finally, we integrate them into a unified system and verify the cross phase properties of MeshCoP. The results demonstrate that the decoupled approach can provide a reusable and extensible framework for analyzing complex protocols.