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

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