Symbolic Security Verification of Mesh Commissioning Protocol in Thread (extended version)

The Thread protocol (or simply Thread ) is a popular networking protocol for the Internet of Things (IoT). It allows seamless integration of a set of applications and protocols, hence reducing the risk of incompatibility among different applications or user protocols. Thread has been deployed in many popular smart home products by the majority of IoT manufacturers, such as Apple TV, Apple HomePod mini, eero 6, Nest Hub, and Nest Wifi. Despite a few empirical analyses on the security of Thread, there is still a lack of formal analysis on this infrastructure of the booming IoT ecosystem. In this work, we performed a formal symbolic analysis of the security properties of Thread. Our main focus is on MeshCoP (Mesh Commissioning Protocol), the main subprotocol in Thread for secure authentication and commissioning of new, untrusted devices inside an existing Thread network. This case study presents the challenges and proposed solutions in modeling MeshCoP. We use ProVerif, a symbolic verification tool of π-calculus models, for verifying the security properties of MeshCoP.