Symbolic Verification of Mesh Commissioning Protocol of Thread

The popularity of the Internet of Things (IoT) has raised the critical need for secure, bug-free protocols, where minor design flaws can lead to significant losses. This work focuses on the Thread protocol, an extensively used solution for IoT security and device diversity. We present a formal π -calculus model of Mesh Commissioning Protocol (MeshCoP), a Thread sub-protocol to securely authenticate and commission new distrusted devices to a Thread Network. Our goal is specifically to verify MeshCoP specification. This study highlights the challenges associated with manually modeling a widely used protocol in the industry. Our analysis confirms the secrecy, key consistency, registration, petitioning, and secure network credentials transfer properties held in MeshCoP.