蓝牙Mesh配网协议的形式化安全性分析

Formal Security Analysis of Bluetooth Mesh Provisioning Protocol

蓝牙Mesh是一种无线网状网络组网技术。新设备必须经过配网才能加入蓝牙Mesh网络。配网协议的安全性是蓝牙Mesh网络安全性的基础,但目前针对该协议安全性的研究尚不充足,现有的模型无法捕获协议中存在的某些攻击。因此,借助符号模型下的协议分析工具Tamarin Prover对蓝牙Mesh配网协议进行形式化建模,该模型覆盖了所有的配网阶段和方法。同时,借助Tamarin Prover的构建和解构规则以及内置的消息理论,提出了一种在符号模型下建模AES-CMAC原语的新方法,该方法可以准确地描述消息长度为任意块的AES-CMAC函数的性质,从而能对配网过程中的认证阶段进行更细粒度的建模。对该模型的安全属性进行了验证,验证结果表明,该形式化模型可以捕获之前发现的原语误用攻击。此外,借助该形式化模型和验证的结果,提出了针对原语误用攻击的修复方案,并通过形式化的方法验证了该方案的有效性。

Bluetooth Mesh is a wireless mesh networking technology.To join a Bluetooth Mesh network,new devices must undergo a provisioning process.The security of the provisioning protocol is the foundation of Bluetooth Mesh network security,but currently there is insufficient research on the security of this protocol,and existing models cannot capture certain attacks that exist in the protocol.Therefore,a formal modeling of the Bluetooth Mesh provisioning protocol is performed using Tamarin Prover,which covers all phases and methods of the provisioning protocol.At the same time,a new method for modeling the AESCMAC primitive under the symbolic model is proposed with the help of Tamarin Prover’s construction and deconstruction rules and the built-in message theory.The method can accurately describe the properties of AES-CMAC functions with arbitrary message lengths,thus enabling a more fine-grained modeling of the authentication phase.The security properties of the model were verified,and the verification results showed that the proposed formal model could capture the previously identified primitive misuse attacks.Furthermore,with the help of this formal model and the verifications results,a countermeasure plan for the primi⁃tive misuse attack is proposed and verified through the formal approach.