A Formal Analysis of Bluetooth Mesh Provisioning Protocol
Min Shi, Jing Chen, Haoran Zhao, Kun He, Ruiying Du · IEEE Internet of Things Journal · 2025
Bluetooth Mesh is a wireless mesh networking technology based on Bluetooth Low Energy, where new devices need to be provisioned to join an existing network. Currently, security research on the Bluetooth Mesh provisioning protocol primarily focuses on the manual analysis of potential vulnerabilities, while existing formal models are too simplistic to capture all the attacks present in the protocol. In this paper, we utilize Tamarin Prover to conduct a comprehensive formal analysis of the Bluetooth Mesh provisioning protocol. Our model encompasses all phases of the protocol from beaconing to data distribution, and includes the modeling of all public key exchanges and authentication methods specified in the Bluetooth Mesh specification. Additionally, we accurately model the AES-CMAC primitive used in the protocol, with the help of deconstruction rules and built-in message theories in Tamarin. This AES-CMAC model enables the analysis of subtle behaviors that were previously beyond the scope of symbolic analysis. Our model successfully reproduces reflection and primitive misuse attacks found in previous studies and identifies two new vulnerabilities. We propose countermeasures for the aforementioned attacks and extend our provisioning model to verify the effectiveness of these countermeasures.