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

Formal Security Analysis of Bluetooth Mesh Provisioning Protocol

摘要

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

Abstract

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 AES-CMAC 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 primitive misuse attack is proposed and verified through the formal approach.

Graphical abstract

关键词

蓝牙Mesh / 形式化分析 / 符号模型

Key words

Bluetooth Mesh / formal analysis / symbolic model

0　 引 言

蓝牙Mesh（Bluetooth Mesh， BM）是由蓝牙技术联盟（Bluetooth Special Interest Group， Bluetooth SIG）于2017年提出的一种无线网状网络组网技术^[1]。相较于只支持一对一或者一对多通信场景的低功耗蓝牙（Bluetooth Low Energy， BLE），蓝牙Mesh技术使得多个蓝牙设备可以通过配网（Provisioning）组建Mesh网络，扩大通信范围，实现多个蓝牙设备间的多对多通信。Bluetooth SIG预测^[2]，截至2022年底，具备蓝牙Mesh组网功能设备的出货量将超过6亿。目前蓝牙Mesh已成为智能家居、智慧城市、照明控制等应用场景的主流解决方案之一。

2021年，Claverie等^[3]发现了配网过程中存在的反射攻击和原语误用攻击。在反射攻击中，攻击者可以反射来自配网器的承诺值和随机数（Nonce），绕过后续的承诺校验。在原语误用攻击中，由于协议对函数AES-CMAC^[4]的不当使用，攻击者可以从Nonce中反向计算出对应的承诺值，从而伪装成新设备与配网器完成配网。攻击者可以利用这些攻击获取配网器分发的网络密钥，解密和篡改蓝牙Mesh网络中发送的信息。针对反射攻击，Bluetooth SIG的修补方案是令配网器在收到与自己发送的承诺值相同的信息时拒绝配网。但针对原语误用攻击，Bluetooth SIG并未提出特定的修复方案，只是建议使用带外信道（out-of-band， OOB）机制，即蓝牙无线电之外的安全信道，例如NFC、二维码等方式，来交换公钥。这使得整个配网过程的安全性事实上完全依赖于OOB信道的安全性，而协议本身设计的认证机制则完全失效。

尽管蓝牙Mesh已经被广泛应用，但目前针对其配网协议安全性的研究尚不充足，尚未有系统完备的安全性证明或验证工作，无法确定蓝牙Mesh设备在不依赖OOB信道的情况下是否能够完成配网，并确保协议设计时所需的安全性。

本文将借助符号模型下的另一协议分析工具Tamarin Prover^[5]对蓝牙Mesh的配网过程进行更细粒度的建模。本文模型通过对AES-CMAC函数性质的准确刻画，探讨了配网过程的安全性，能够捕获原语误用攻击。此外，本文还提出了在不依赖OOB信道的情况下保证配网协议安全性的解决方案。

本文的主要贡献如下：

1） 提出了一个蓝牙Mesh配网协议的形式化模型。模型覆盖了配网协议的所有阶段和配网方法，并根据协议设计时的安全需求形式化地描述了协议应该满足的安全属性。

2） 提出了一种新的在符号模型中建模AES-CMAC原语的方法。借助Tamarin Prover的构建和解构规则以及内置的消息理论，该方法可以准确地刻画消息长度为任意块的AES-CMAC函数的性质。

3） 借助上述形式化模型和验证的结果，提出了针对原语误用攻击的修复方案，并通过形式化的方法验证了该方案的有效性。

1　 相关工作

对蓝牙协议安全性的形式化研究起步很早。2007年，Chang等^[6]使用符号模型下的协议验证工具ProVerif^[7]对经典蓝牙（Bluetooth Classic， BT）协议中的数值比较（numeric comparison， NC）配对方法进行建模，该模型支持无限个并发的配网会话，发现用户在某个会话下的行为可能会被解释为另一会话中的操作，从而导致设备无法正确认证。Arai等^[8]使用ProVerif对一个由Yeh等^[9]提出的改进版NC配对方法进行了验证，发现改进后的协议存在伪装和重放攻击，不过这个改进版本并没有被推广使用或吸纳为新的蓝牙标准。Sethi等^[10]使用ProVerif对BT和BLE协议中的NC配对方法进行了建模，该模型通过将用户、设备间的私有信道泄露给攻击者的方式建模了蓝牙设备和用户行为被攻击者控制的场景，并发现了误绑定攻击。Cremers等^[11]提出了一种使用Tamarin Prover建模迪菲-赫尔曼（Diffie-Hellman， DH）群的新方法，并借此验证了存在于蓝牙配对协议的DH密钥交换过程中的无效曲线攻击^[12]，但该模型对协议使用的AES-CMAC函数的建模粒度较粗，只是将其抽象为单向函数。上述模型都只建模了配对过程中的一种方法（NC配对方法），但2021年Von Tschirschnitz等^[13]提出的方法混淆攻击则借助了蓝牙配对过程中不同方法间的交互。在此之后，Wu等^[14]使用ProVerif对BC、BLE和Mesh三个协议栈中的所有配对（配网）方法进行了建模。这个综合模型可以复现方法混淆攻击，并独立地发现了与Claverie等^[3]提出的反射攻击相同的攻击场景。但是，由于该模型同样将AES-CMAC函数抽象为单向函数，因此无法揭示任何与原语误用攻击相关的信息。此外，该模型忽略了方法选择阶段，只是将不同的配对方法作为模块进行排列组合。这使得模型无法反映出Von Tschirschnitz等^[13]对于不同能力设备可能受到不同安全威胁程度的相关分析。

综上所述，尽管已有不少工作对蓝牙相关的协议进行了形式化的分析与验证，但针对蓝牙Mesh配网协议的分析尚不充分。现有的模型不仅忽略了协议的某些环节，并且对协议中使用的密码原语的建模也过于简单，以至于无法捕获协议中存在的原语误用攻击。本文使用Tamarin Prover对蓝牙Mesh的配网协议进行更为全面和细致的建模，在覆盖所有阶段和配网方法的同时，通过对AES-CMAC原语性质的细粒度建模，对配网协议进行系统的安全性分析。

2　 背景知识

2.1　蓝牙Mesh配网协议

配网协议是组建蓝牙Mesh网络的第一步，它定义了配网器将新设备加入现有Mesh网络时进行的通信过程。配网器可以是智能手机、笔记本电脑或其他特定设备。在配网过程中，配网器会和新设备进行一次DH密钥交换，分发必要的配网信息并对新设备进行配置，使其成为Mesh网络中的一个节点。双方借助用户与设备间的交互进行身份认证。蓝牙Mesh网络中所有节点间的通信都会由网络密钥（network key，NetKey）加密和认证。此外，配网器和每个新设备之间也会共享一个设备密钥（device key，DevKey），用于保护设备配置或者密钥刷新等过程中配网器和特定设备间的直接通信。因此配网协议的安全性是保证整个蓝牙Mesh网络通信安全的基础。

根据Mesh Profile 1.0.1（蓝牙Mesh协议规范）的第5.4节^[1]，配网协议分为5个阶段：广播、邀请、公钥交换、认证和分发，如图1所示。

① 广播：未配网的新设备广播它的设备标识符（DeviceUUID）以及它是否有OOB数据（OOBInfo）。配网器选择某个广播中的新设备与其建立连接，并在需要的情况下提示用户收集OOB数据。

② 邀请：在收到来自配网器的邀请信息之后，新设备发送它的设备能力信息（pkType、staticOOB、outputOOB、inputOOB）至配网器。这些字段分别表明了新设备能否使用OOB技术交换公钥、在认证阶段是否支持对应的认证方法。配网器会根据双方的能力选择恰当的公钥交换方法和认证方法，并将选择的结果发送给新设备。

③ 公钥交换：该阶段有两种不同的公钥交换方法。一是通过公开的蓝牙信道交换各自的公钥PKp和PKd，双方在每次交换时都会生成一对新的公私钥；另一种方法则是配网器通过合适的OOB技术读取新设备的静态公钥PKd，然后将自己新生成的公钥PKp通过蓝牙信道发送给新设备，之后它们计算出共享秘密ECDHSecret。

④ 认证：根据配网器在邀请阶段的选择结果，有四种不同的方法可以获取并共享认证值AuthValue：静态OOB、输出OOB、输入OOB和无OOB。静态OOB方法使用广播阶段收集的OOB数据作为AuthValue。当使用输出OOB和输入OOB时，配网器或者新设备会随机生成并显示一个数值，用户在观察到输出后将其输入另一方。无OOB则使用一个零值作为AuthValue。

配网协议使用一种有用户参与的承诺机制来认证设备的身份。图1中的配网器承诺值Cp和新设备承诺值Cd由公式(1)和(2)计算得到：

\mathrm{C}\mathrm{p}=\mathrm{A}\mathrm{E}\mathrm{S}–\mathrm{C}\mathrm{M}\mathrm{A}{\mathrm{C}}_{\mathrm{C}\mathrm{K}}(\mathrm{N}\mathrm{p}||\mathrm{A}\mathrm{u}\mathrm{t}\mathrm{h}\mathrm{V}\mathrm{a}\mathrm{l}\mathrm{u}\mathrm{e})(1)

\mathrm{C}\mathrm{d}=\mathrm{A}\mathrm{E}\mathrm{S}–\mathrm{C}\mathrm{M}\mathrm{A}{\mathrm{C}}_{\mathrm{C}\mathrm{K}}\left(\mathrm{N}\mathrm{d}||\mathrm{A}\mathrm{u}\mathrm{t}\mathrm{h}\mathrm{V}\mathrm{a}\mathrm{l}\mathrm{u}\mathrm{e}\right)(2)

其中，AES-CMAC是一个消息认证码函数，需要密钥和消息作为输入，具体计算方法将在第2.2节介绍；CK是AES-CMAC函数的密钥，由共享秘密ECDHSecret以及其他公开的信息计算得到。AES-CMAC函数的消息部分由Np或Nd与AuthValue拼接后得到，Np和Nd是配网器和新设备各自生成的随机数（Nonce）。

配网器和新设备会以图1中的顺序交换Cp和Cd以及Np和Nd并校验承诺。

⑤ 分发：配网器使用会话密钥（session key，SesKey）加密配网数据（例如网络密钥NetKey）发送给新设备，之后双方计算生成设备密钥DevKey。SesKey和DevKey由ECDHSecret、随机数Np和Nd以及协议中交换的其他公开信息计算得到。NetKey由配网器随机生成。

值得注意的是，Mesh Profile 1.0.1（蓝牙Mesh规范）^[1]的第5.4.3节中指出只有以下两类配网是安全的：

1) 使用OOB机制传输公钥并使用静态OOB方法进行认证。

2) 使用输入OOB或输出OOB方法认证。

配网器可以开启安全策略，只使用安全的配网方法完成配网，并拒绝不安全的配网请求。

2.2　AES-CMAC函数

AES-CMAC函数是一种基于分组加密的消息认证码（cipher-based message authentication code, CMAC），使用高级加密标准（advanced encryption standard, AES）作为其构建模块，详细定义可参考规范RFC 4493^[4]。它可以为任意长度的输入消息提供完整性保护。

图2展示了消息长度为N块的AES-CMAC函数（图片来自RFC 4493^[4]中的计算流程示意图）。每块消息的大小为128 bit。图中的AES _k 是密钥为k的AES加密函数。k也是AES-CMAC函数的密钥。最后一轮使用的k₁由k计算得到。AES-CMAC函数计算得到的标签是图2中的T_N，虚线框中的T₁,T₂,…,T_i 只用于说明计算过程，并不会被输出。第i-1轮的结果会与第i块消息M_i 异或得到第i轮的输入，之后加密异或的结果得到该轮的输出。

虽然AES-CMAC提供了消息认证码所需的不可伪造性（简单来说，攻击者在没有密钥的情况下不能伪造任意消息的有效标签），但该函数并非完全不可逆。当攻击者已知标签T_N，密钥k，以及N-1块消息时，他可以恢复出剩余的一块未知消息。

配网协议使用的AES-CMAC函数消息长度为2块。128位的随机数为第一块，填充后的AuthValue为第二块。第3.3节将介绍如何使用Tamarin Prover建模一个通用的（消息长度为任意块）AES-CMAC函数。

2.3　Tamarin Prover相关知识

Tamarin Prover^[5]是符号模型下的协议验证工具，可以自动地证明协议的安全属性能否得到满足。作为知名的协议验证工具之一，Tamarin Prover有着丰富的表达能力，并且已经成功地应用于许多现实协议的分析工作，包括5G^[15，16]、TLS 1.3^[17]、WPA2^[18]等等。本节将介绍如何在Tamarin Prover中建模协议和定义安全属性。

建模协议：Tamarin Prover使用多集重写规则将协议参与方与攻击者的并发执行定义为一个标记迁移系统。该系统的状态是事实（facts）的多重集合，初始状态为空集。规则定义了系统如何从当前状态转移为新的状态。规则包括名称和其他三个部分：左侧、行为和右侧。以规则example为例：

rule example:

[Fr(~k), Fr(~m)]--[Send(~m)]->

[Out(senc(~m, ~k))]

该规则的名称为example，左侧是两个Fr事实，行为是自定义的事实Send，右侧是Out事实。只有当左侧的所有事实均出现于当前状态时，Tamarin Prover才能使用该规则进行状态转移。执行规则时会消耗左侧的事实，并生成右侧的事实（将左侧事实从当前状态移除并添加右侧事实）。事实一般只能消耗一次，但以!符号开头的事实可以消耗任意次（持久性事实）。行为部分则用于表达安全属性或定义限制（restriction）。

Tamarin Prover内置的三个事实Fr、In和Out分别用于生成唯一的随机值以及从（向）公开网络中接收（发送）消息。因此规则example表示某协议的参与方生成了密钥k和消息m，使用对称加密函数senc加密后将密文发送至公开信道。

定义安全属性：Tamarin Prover使用引理（lemma）定义安全属性，它是消息变量和时序变量上的一阶逻辑公式。以引理Secrecy为例：

lemma Secrecy:

“All m #t₁. Send(m) @t₁ ==>

not Ex #t₂. K(m) @t₂”

该引理表达了一个简单的机密属性，它要求对于协议运行过程中的所有时间点#t₁ 上出现的Send事实和事实的参数m，不存在一个时间点#t₂ 使得攻击者可以获取m（内置事实K）。

此外，Tamarin Prover使用限制来表达协议运行中的约束条件。用于定义限制的语法与引理相同，Tamarin Prover在验证时只会考虑满足这些限制的路径。

3　 模型设计与安全属性

本节介绍如何使用Tamarin Prover建模蓝牙Mesh的配网协议，包括建模时考虑的威胁模型和安全假设、模型的整体框架、如何准确建模AES-CMAC函数的性质以及安全属性的形式化定义。

3.1　威胁模型和安全假设

Tamarin Prover默认假设一个Dolev-Yao敌手模型^[19]，攻击者控制着整个网络，可以拦截、篡改和伪造公开信道上发送的任何消息。攻击者只有在拥有对应密钥的情况下才能加解密消息（或者计算签名和MAC等等）。

本文假设配网协议模型中使用的以下三类通信机制是安全的：

1） 设备与用户间通过输入输出进行的交互；

2） 用于获取AuthValue的OOB机制；

3） 用于获取新设备公钥的OOB机制。

上述通信机制会为它们传输的数据提供机密性、完整性、认证性以及抗重放攻击的保护。

本文的模型不考虑设备被攻击者控制的场景。用户手中正在配网的配网器和新设备都是诚实的。用户也会将他看到的数值正确地输入另一设备中。此外，本文假设配网器和新设备同一时间只会运行一个配网会话实例，不支持并发执行。对并发会话的支持是未来工作的方向之一，相关的讨论参见第4.2节。

3.2　模型框架

本文的模型将覆盖配网协议从广播到分发配网数据的全部5个阶段以及公钥交换和认证阶段所有的方法分支。这些不同的方法涉及到不同的用户与设备间交互。建模时需要考虑到用户所有可能的行为模式，包括协议设计时预料之外、但对于用户来说十分合理的行为，并用形式化的方式加以表述。

公钥交换和认证阶段的方法由广播和邀请阶段发送的能力信息决定。在进行初始化时，配网器和新设备会被赋予不同的能力。其中配网器有两个能力字段pkCollect和authCollect，分别表示配网器能否通过OOB技术收集新设备的公钥以及设备提供的静态OOB数据。新设备有四个能力字段pkType、staticOOB、outputOOB以及inputOOB，分别表示新设备是否支持OOB公钥传输，以及在认证阶段支持的认证方法。

公钥交换方法的选择较为简单，只有当配网器和新设备均支持OOB技术传输公钥（即，pkCollect和pkType均为1）时，才使用OOB技术传输公钥（安全信道），否则使用蓝牙信道传输（公开信道）。

认证方法的选择参见表1。简单来说，只有当新设备支持静态OOB方法，并且配网器也已经收集了静态OOB数据时，才选择静态OOB方法。否则，配网器会依次尝试选择输出OOB、输入OOB以及无OOB作为认证方法。

本文模型将用户看作协议的参与实体之一，对用户在认证阶段的行为进行了建模和描述。在协议设计中，输出OOB方法需要用户将新设备显示的随机数输入到配网器中，输入OOB方法则是将配网器的显示输入到新设备。然而，Von Tschirschnitz等^[13]提出的方法混淆攻击中提到，用户可能的操作并非只有协议规范中所预想的行为。考虑到参与配网的设备只有显示数值和等待输入两种交互方式，用户可能面对4种不同的场景。然而，双方都显示数值时用户无法做出任何操作，因此只需建模以下情况：

1) 一方显示数值另一方等待输入：用户将显示的值准确地输入另一方。

2) 两边同时等待输入：参考Core Specification 5.3（BLE协议规范）^[20]中的口令输入模式，用户将在两侧同时输入一个相同的值。

因此，本文模型的整体框架如图3所示。在配网协议的模板模型中，设备的能力均为占位符。使用m4宏处理器^[21]初始化设备的能力，实例化不同的设备组合，得到具体的配网场景作为子模型。将子模型作为Tamarin Prover的输入进行验证，分析不同能力的设备在配网时可能会遇到的具体安全问题。

3.3　AES-CMAC函数的建模

符号模型使用代数上的项（term）和等式理论（equational theory）来建模消息和密码函数的属性。函数只会满足这些代数上明确定义的性质。但根据2.2节对AES-CMAC函数性质的讨论，在已知密钥和部分消息的前提下，攻击者可以从AES-CMAC函数中计算出剩余的一块未知消息。在这个过程中，未知块的位置和消息的总长度都可以是任意的。但在符号模型中使用等式理论描述函数的性质时，参数的数量和位置都必须是确定的。本节将介绍如何使用Tamarin Prover的构建规则和解构规则以及内置的消息理论multiset定义一个通用的（指消息长度为任意块）AES-CMAC函数。

3.3.1　相关知识

在分析协议模型之前，Tamarin Prover会根据指定的等式理论定义构建和解构规则。读者可以参考文献[5，22]了解更详细的介绍。

构建规则会将函数符号应用于参数。每个函数符号都会有对应的构建规则，且形式较为统一，内容仅与该函数符号的名称和参数数量有关。例如，Tamarin Prover内置的对称加密的函数符号senc对应的构建规则如规则c_senc所示：

rule (modulo AC) c_senc:

[!KU(x), !KU(x₁)]--[!KU(senc(x,x₁))]->

[!KU(senc(x,x₁))]

其中，(modulo AC)表示该规则是构建规则或解构规则（而非用户定义的、用于建模协议参与方行为的一般规则）；事实!KU(x)表示攻击者的知识集中包含参数x。该规则表示攻击者可以在已知项x和x₁时，使用函数符号senc构建新的项senc(x,x₁)。

解构规则用于从参数中提取项。例如，内置的对称加密的解密函数sdec在预处理后会生成解构规则d_0_sdec，其代码如下所示：

rule (modulo AC) d_0_sdec:

[!KD(senc(x,x₁)),!KU(x₁)]-> [!KD(x)]

该规则表示攻击者可以在已知密钥x₁的情况下从密文senc(x,x₁)中提取明文x。规则中的!KD事实同样用于表示攻击者的知识。Tamarin Prover使用!KD标记之后可以继续应用解构规则的消息，!KU标记之后不能再应用解构规则的消息。借助这种方式，Tamarin Prover在分析时可以避免例如反复加解密这样的冗余操作。

Tamarin Prover内置消息理论中的multiset可用于建模多重集合。它引入了操作符“+”连接集合中的元素。本文的建模方法利用了集合中元素的无序性，使用multiset为不同位置上的未知块定义相同的规则。此外，建模时也定义了限制Atomic判断某个项是否是多重集下的原子项，其代码如下所示：

restriction Atomic:

“All atom #t₁. Atomic(atom) @t₁ ==>

not Ex at₁ at₂. at₁ + at₂ = atom”

该限制表示，对于任意时间点#t₁出现的项atom，都不存在at₁和at₂使得atom可以被分割为at₁+at₂，因此atom可以看作多重集合操作下的原子项。

3.3.2　建模方法

定义函数符号cmac/2、rm/3、rm1/2表示计算标签和恢复未知消息块的过程。斜线后的数字表示函数的参数个数。例如，当有两块消息ma和mb且AES-CMAC函数的密钥为k时，计算标签tag的代码如下所示：

let m1 = <ma, ‘1’>

m2 = <mb, ‘2’>

tag = cmac(m1+m2, k)

in …

其中，let-in语句用于在单条规则的上下文中定义局部宏，等号右侧的项会在处理前替换左侧的变量。代码中的m1+m2是一个多重集，被看作cmac函数的第一个参数。每块消息之后添加的位置字符用于表明消息块间的顺序。

同时，手动定义从标签中计算未知块的解构规则d_0_rm（而非定义等式理论并使用Tamarin Prover从中生成的解构规则），其代码如下所示：

rule (modulo AC) d_0_rm:

[!KD(cmac(km+um, k)),!KU(k),!KU(km)]

--[Atomic(um)]--> [!KD(km+um)]

攻击者可以使用解构规则d_0_rm在已知标签cmac(km+um, k)、密钥k和部分消息km的前提下，恢复未知消息块um，前提是um是多重集操作下的原子项（由规则中行为部分的Atomic事实对应的限制进行约束）。

上述规则适用于消息长度大于等于2块的情况。对于仅有一块的消息，定义用于从标签中计算消息的解构规则d_0_rm1，其代码如下所示：

rule (modulo AC) d_0_rm1:

[!KD(cmac(m,k)), !KU(k)]

--[Atomic(m)]--> [!KD(m)]

该规则表示当攻击者已知标签cmac(m,k)和密钥k时，如果消息m是原子项，则攻击者可以计算出消息m。

本文模型使用限制CheckCMAC建模AES-CMAC原语的验证算法，其代码如下所示：

restriction CheckCMAC:

“All tag m k #t₁. Check(tag,m,k) @t₁ ==>

( tag = cmac(m,k) )

| (Ex km um. (km+um = m)

& (not Ex um₁ um₂. um₁+um₂ = um)

& (um = rm(tag,km,k)) )

| (not Ex m₁m₂. (m₁+m₂ = m)

& (m = rm1(tag,k)) )”

该限制表示，对于协议运行的任意时间点#t₁出现的事实Check(tag,m,k)，有如下三种情况下可以满足约束，分别由表示逻辑或的符号“|”连接：

1） 标签tag是由消息m和密钥k通过cmac函数计算得到的，对应常规的承诺校验过程；

2） 未知消息um是由标签tag、密钥k和部分消息km通过函数rm计算得到的，且um是原子项。这使得攻击者可以计算出随机承诺对应的合法Nonce，并使用该Nonce通过承诺校验；

3） 未知消息仅有一块，由标签tag和密钥k通过函数rm1计算得到。这种情况与2）类似，只是AES-CMAC函数的消息长度为1块。

从数学的角度看，限制CheckCMAC和上文定义的解构规则并没有本质上的不同。它们都是从已知的标签、密钥和消息中计算出未知的一块消息。但是，符号模型中的项并没有内在的数学关系。因此建模时必须定义限制CheckCMAC和函数符号rm、rm1，从而使得协议的模型也可以使用从标签中计算出的消息完成承诺校验。

3.4　安全属性的定义

本文将配网协议看作一个认证密钥交换协议，它应该满足机密性和认证性两类属性。

机密性方面，本文主要考虑配网协议中涉及到的3个密钥：用于保证分发过程安全性的会话密钥SesKey，用于保证配网器和当前设备之间后续配置和密钥更新等过程的安全性的设备密钥DevKey，以及在该Mesh网络中由所有节点共享的网络密钥NetKey。引理定义如下：

lemma Secrecy_Keys:

“All SesKey DevKey NetKey #t₁.

Secret(SesKey,DevKey,NetKey) @t₁

==> not (Ex #t₂. K(SesKey) @t₂

| Ex #t₃. K(DevKey) @t₃

| Ex #t₄. K(NetKey) @t₄)”

认证性方面，本文主要考虑配网过程的非单射一致性（non-injective agreement）。非单射一致性的定义可以参考Lowe^[23]关于认证性层级的研究。在配网协议的上下文中，非单射一致性要求当配网器认为它已经和新设备完成了配网时，新设备的确和配网器进行过配网，并且双方需要在某些数据上达成一致。反之亦然。由于本文模型的安全假设不考虑并发的多个配网会话，因此这里定义的认证性仅局限于非单射一致性。在本文定义的安全属性中需要达成一致的数据是公钥交换阶段生成的共享秘密和认证阶段的Nonce。因此相关的引理定义如下：

lemma Noninj_Agreement_Prov:

“All prov ndev ecdh nd #t₁.

Commit_Prov(prov,ndev,ecdh,nd) @t₁

==> (Ex #t₂. Running_NDev(ndev,

prov,ecdh,nd) @t₂ & t₂ < t₁)”

其中，Commit_Prov事实出现在配网器的最后一条规则中，表示配网器已经完成了配网，它的参数包括配网器的身份标识prov、新设备的身份标识ndev、共享秘密ecdh以及认证阶段配网器收到的Nonce（nd）；Running_NDev出现在新设备生成Nonce并发送承诺的规则中，表示它正在被配网。因此，该引理表示当配网器prov在时间点#t₁完成了与新设备ndev的配网时，一定存在一个时间点#t₂使得新设备ndev正在与配网器进行配网，并且时间点#t₂早于#t₁。类似地，引理Noninj_Agreement_NDev用于定义新设备认为自己完成了和配网器的配网时的认证性，其代码如下所示：

lemma Noninj_Agreement_NDev:

“All prov ndev ecdh np #t₁.

Commit_NDev(ndev,prov,ecdh,np) @t₁

==> (Ex #t₂. Running_Prov(prov,ndev,

ecdh,np) @t₂ & t₂ < t₁)”

该引理只是交换了Commit和Running事实对应的设备，并将Nonce换为配网器发送的Np，因此这里不再赘述。

4　 验证结果与分析

本节将对本文提出的蓝牙Mesh配网协议模型的验证结果进行详细阐述。首先是所有子模型的安全属性的验证，然后是本文模型和已有工作的对比，最后是Tamarin Prover复现的AES-CMAC原语误用攻击的流程以及相应的修补方案。所有的验证都使用Ubuntu 18.04进行，CPU为Intel Xeon Gold 5218 @ 3.9 GHz，内存为32 GB。

4.1　安全属性的验证

表2展示了各个安全属性的验证结果。在本文的模型中，新设备有4个能力字段（pkType、staticOOB、outputOOB、inputOOB），因此有16（2\times2\times2\times2）种不同类型的新设备。类似地，配网器有两个能力字段（pkCollect、authCollect），因此有4（2\times2）种不同类型的配网器。模型总共验证了64（16\times4）种不同的配网场景（子模型）。简洁起见，以各个模型在没有攻击者干涉的情况下本应选择的配网方法为标准，对64个子模型进行了分类，得到表2中编号为1~8的8类模型。下文将使用分类编号描述不同子模型的验证结果。

由表2结果可知，第3.4节中考虑的安全属性在所有配网方法下均无法满足。第4类模型的配网方法本身即不安全；对于第1~3类模型，攻击者可以使用原语误用攻击绕过校验机制完成配网，具体流程参见第4.3节；对于第5~8类的模型，使用OOB机制交换公钥本应保证各个安全属性的满足，但根据Mesh Profile 1.0.1（蓝牙Mesh协议规范）^[1]中定义的安全策略，这些认证方法可以通过篡改邀请阶段发送的能力字段降级为第2或3类模型中的配网方法，之后使用原语误用攻击完成配网。

4.2　与其他蓝牙协议形式化模型的对比

表3展示了本文模型和其他关于蓝牙协议的形式化验证模型的对比。其中只有文献[14]的模型和本文模型建模了蓝牙Mesh的配网过程，其他模型则主要关注BT或BLE协议中的某一种配对方法。

文献[14]的模型覆盖了BT、BLE和Mesh这3个常用的蓝牙协议栈，以及这3个协议栈中所有的配对和配网方法。此外，该模型还覆盖了后续的数据传输过程。但是，该模型中的配网（和配对）不包括邀请阶段中的方法选择。不同的配网方法只是作为不同的模块进行排列组合，因此会错过与协议降级相关的攻击场景。

在对AES-CMAC函数的建模方面，本文模型是首个对该函数性质做出细粒度建模的模型。之前的所有模型都只是将AES-CMAC函数建模为单向函数，通过只定义函数符号、不提供等式的方式，使得该原语只能从消息单向计算标签。在BT和BLE协议栈中也用到了AES-CMAC函数，不过由于AES-CMAC原语的用法与蓝牙Mesh协议不同，BT和BLE中目前还没有发现与AES-CMAC原语误用相关的攻击。本文的建模方法可以迁移到BT和BLE协议的建模中，并通过形式化的方式验证这一点。

在并发会话方面，文献[14]的模型只在数据传输阶段支持并发会话，而配网阶段只允许单个会话，与本文模型的假设一致。根据Mesh Profile 1.0.1（蓝牙Mesh协议规范）的5.2.1节^[1]，未配网的新设备同时只支持一个配网会话，但配网器则没有该限制。因此单一配网会话的假设可能导致模型错过与并发配网相关的攻击。根据文献[6]对BC协议的验证结果，并发会话有可能会导致用户无法分辨显示的数值属于哪一次会话，从而错误地与攻击者完成配对。

4.3　原语误用攻击的路径

通过对AES-CMAC原语性质更为准确的建模，Tamarin Prover可以自动地发现Claverie等^[3]提出的原语误用攻击。本文的模型也可以捕获文献[3]和[14]中发现的反射攻击，但这里不再赘述具体过程。

原语误用攻击的流程如图4所示，图中红色文字表示攻击者应执行的操作和发送的消息。配网协议使用的AES-CMAC函数消息长度为2块，其中随机数Np或者Nd是第一块，AuthValue是第二块，密钥是CK。根据图2中的计算流程，用于计算承诺的公式(1)等价于公式(3)：

\mathrm{C}\mathrm{p}=\mathrm{A}\mathrm{E}{\mathrm{S}}_{\mathrm{C}\mathrm{K}}(\mathrm{A}\mathrm{E}{\mathrm{S}}_{\mathrm{C}\mathrm{K}}\left(\mathrm{N}\mathrm{p}\right)\oplus \mathrm{C}{\mathrm{K}}_{\mathrm{1}}\oplus \mathrm{A}\mathrm{u}\mathrm{t}\mathrm{h}\mathrm{V}\mathrm{a}\mathrm{l}\mathrm{u}\mathrm{e})(3)

其中，AES_CK表示密钥为CK的AES加密函数，\oplus表示异或操作，CK₁由CK计算得到。

如果中间人攻击者与配网器完成了DH公钥交换并使用共享秘密ECDHSecret计算出密钥CK，那么当他收到配网器发送的Cp和Np时，就可以使用公式(4)计算出AuthValue：

\mathrm{A}\mathrm{u}\mathrm{t}\mathrm{h}\mathrm{V}\mathrm{a}\mathrm{l}\mathrm{u}\mathrm{e}=\mathrm{A}\mathrm{E}{\mathrm{S}}_{\mathrm{C}\mathrm{K}}^{-\mathrm{1}}\left(\mathrm{C}\mathrm{p}\right)\oplus \mathrm{A}\mathrm{E}{\mathrm{S}}_{\mathrm{C}\mathrm{K}}(\mathrm{N}\mathrm{p})\oplus \mathrm{C}{\mathrm{K}}_{\mathrm{1}}(4)

其中，AES^-1表示AES加密函数对应的解密函数。

攻击者可以在收到Np前随机生成并向配网器发送一个承诺Ca，之后他可以根据公式(5)计算Ca对应的合法随机数Na：

\mathrm{N}\mathrm{a}=\mathrm{A}\mathrm{E}{\mathrm{S}}_{\mathrm{C}\mathrm{K}}^{-\mathrm{1}}(\mathrm{A}\mathrm{E}{\mathrm{S}}_{\mathrm{C}\mathrm{K}}^{-\mathrm{1}}(\mathrm{C}\mathrm{a})\oplus \mathrm{C}{\mathrm{K}}_{\mathrm{1}}\oplus \mathrm{A}\mathrm{u}\mathrm{t}\mathrm{h}\mathrm{V}\mathrm{a}\mathrm{l}\mathrm{u}\mathrm{e})(5)

之后，攻击者可以遵循正常的流程完成配网，获取NetKey和DevKey。这违反了表2中的机密性C1和认证性A1。同时，攻击者从Cp和Np计算出AuthValue后，即可伪装成配网器与新设备完成配网，这违反了表2中的认证性A2。

图5是Tamarin Prover在交互模式下输出的原语误用攻击的攻击路径。由于空间限制，图5对完整的路径进行了裁剪和空间位置的调整，以突出攻击的关键步骤。图中蓝色文字标注了Tamarin Prover中的项在协议中对应的消息，便于理解攻击的上下文。椭圆代表对不同规则的应用，实线箭头和虚线箭头分别代表!KD和!KU事实的消耗。

从图5中可以看出，对于配网器发送的承诺Cp（由配网器的规则输出），当攻击者拥有Np（同样来自配网器的规则，但攻击者在#vr.39和#vk.13时间点进行了处理，主要是一些复合项的拆分）和CK（由#vk.4时间点的规则构建得到，来自攻击者知识集内不同项的组合）时，他可以使用解构规则d_0_rm计算AuthValue。此外，对于攻击者自己发送的随机承诺Ca，他可以使用构建规则c_rm计算对应的Na。

4.4　原语误用攻击的修补方案

本节主要讨论对原语误用攻击的修复方案。针对反射攻击，文献[14]和Bluetooth SIG都提出了简单但行之有效的修补^[24]：检查收到的承诺是否和自己发送的承诺相同。因此这里不再详细论述。

作为原语误用攻击的发现者，Claverie等^[3]没有提出相应的修补方案。Bluetooth SIG目前也没有提出针对该攻击的补丁，只是建议使用OOB机制交换公钥。在这种情况下，配网协议的认证阶段将失去设计意义。配网协议的安全性会完全依赖于用于交换公钥的OOB机制的安全性。考虑到OOB机制本身可能存在的安全问题，以及并非所有设备都支持相关的OOB机制，这无疑影响了蓝牙Mesh协议的安全性与适用性。

本文的修补方案只需交换AES-CMAC函数中参数和密钥的位置。具体来说，在原本的协议中，CK被用作密钥，Np被用作消息的第一块。在修复方案中使用Np作为密钥，CK作为第一块消息，如公式(6)所示：

\mathrm{C}\mathrm{p}=\mathrm{A}\mathrm{E}\mathrm{S}–\mathrm{C}\mathrm{M}\mathrm{A}{\mathrm{C}}_{\mathrm{N}\mathrm{p}}(\mathrm{C}\mathrm{K}||\mathrm{A}\mathrm{u}\mathrm{t}\mathrm{h}\mathrm{V}\mathrm{a}\mathrm{l}\mathrm{u}\mathrm{e})(6)

虽然攻击者仍然可以在收到Cp和Np之后计算出AuthValue，但他无法计算出自己发送的承诺Ca对应的随机数Na。上述过程与BLE协议中计算和交换承诺的方式类似。

使用Tamarin Prover建模并验证的结果表明，在部署了该修复方案后，配网器一侧的认证性以及网络密钥的机密性可以得到保证，即攻击者无法伪装成新设备与配网器完成配网。

5　 结 语

本文使用Tamarin Prover对蓝牙Mesh配网协议进行了形式化建模与分析。模型覆盖了配网协议的所有阶段和配网方法，并使用Tamarin Prover的解构规则和内置的消息理论multiset提出了一种新的建模AES-CMAC函数的方法，从而能对配网过程中的认证阶段进行更细粒度的建模。这种建模方法足够通用，可以建模任意块消息的AES-CMAC函数。

本文的模型可以捕获到之前发现的反射攻击和原语误用攻击，并提出了针对原语误用攻击的修补方案。通过形式化的方法对该修补方案进行了验证，结果表明该方案可以保证配网器侧的认证性以及分发的网络密钥的机密性。在未来的工作中，笔者将扩展现有模型以支持并发的配网会话以及对单射认证性的验证，并在具体蓝牙设备上验证发现的攻击。

参考文献

[1] BLUETOOTH SIG MESH WORKING GROUP. Mesh Profile 1.0.1［EB/OL］. ［2019-01-21］.

[2] BLUETOOTH SIG. 2022 Bluetooth Market Update ［EB/OL］. ［2022-10-01］.

[3] CLAVERIE T， ESTEVES J L. BlueMirror： Reflections on Bluetooth pairing and provisioning protocols［C］//2021 IEEE Security and Privacy Workshops （SPW）. New York： IEEE Press， 2021： 339-351. DOI： 10.1109/SPW53761.2021.00054 .

[4] The AES-CMAC algorithm： RFC 4493 ［S/OL］.［2019-01-22］.

[5] MEIER S， SCHMIDT B， CREMERS C， et al. The TAMARIN prover for the symbolic analysis of security protocols［C］//International Conference on Computer Aided Verification. Berlin： Springer， 2013： 696-701.10.1007/978-3-642-39799-8_48. DOI: 10.1007/978-3-642-39799-8_48 .

[6] CHANG G， SHMATIKOV V. Formal analysis of authentication in Bluetooth device pairing［EB/OL］. ［2021-04-18］.

[7] BLANCHET B. Modeling and verifying security protocols with the applied pi calculus and ProVerif［J］. Foundations and Trends in Privacy and Security， 2016， 1（1/2）： 1-135. DOI： 10.1561/3300000004 .

[8] ARAI K， KANEKO T. Formal verification of improved numeric comparison protocol for secure simple paring in Bluetooth using ProVerif［EB/OL］. ［2020-07-25］.

[9] YEH T C， PENG J R， WANG S S， et al. Securing Bluetooth communications［EB/OL］. ［2021-03-20］.

[10] SETHI M， PELTONEN A， AURA T. Misbinding attacks on secure device pairing and bootstrapping［C］//Proceedings of the 2019 ACM Asia Conference on Computer and Communications Security. New York： ACM， 2019： 453-464. DOI： 10.1145/3321705.3329813 .

[11] CREMERS C， JACKSON D. Prime， order please！ revisiting small subgroup and invalid curve attacks on protocols using Diffie-Hellman［C］//2019 IEEE 32nd Computer Security Foundations Symposium （CSF）. New York： IEEE Press， 2019： 78-7815. DOI： 10.1109/CSF.2019.00013 .

[12] BIHAM E， NEUMANN L. Breaking the Bluetooth pairing–the fixed coordinate invalid curve attack［C］//International Conference on Selected Areas in Cryptography. Berlin： Springer， 2020： 250-273. DOI： 10.1007/978-3-030-38471-5_11 .

[13] TSCHIRSCHNITZ M V， PEUCKERT L， FRANZEN F， et al. Method confusion attack on Bluetooth pairing［C］//2021 IEEE Symposium on Security and Privacy （SP）. New York： IEEE Press， 2021： 1332-1347. DOI： 10.1109/SP40001.2021.00013 .

[14] WU J L， WU R Y， XU D Y， et al. Formal model-driven discovery of Bluetooth protocol design vulnerabilities［C］//2022 IEEE Symposium on Security and Privacy （SP）. New York： IEEE Press， 2022： 2285-2303. DOI： 10.1109/SP46214.2022.9833777 .

[15] 贾凡， 严妍， 袁开国， 等. 5G网络认证及密钥协商协议的安全性分析［J］. 清华大学学报（自然科学版）， 2021， 61（11）： 1260-1266. DOI： 10.16511/j.cnki.qhdxxb.2021.26.001 .

[16] JIA F， YAN Y， YUAN K G， et al. Security analysis of 5G authentication and key agreement protocol［J］. Journal of Tsinghua University （Science and Technology）， 2021， 61（11）： 1260-1266. DOI： 10.16511/j.cnki.qhdxxb.2021.26.001（Ch ）.

[17] CREMERS C， DEHNEL-WILD M. Component-based formal analysis of 5G-AKA： Channel assumptions and session confusion［C］//Proceedings 2019 Network and Distributed System Security Symposium. Reston： Internet Society， 2019：1-15. DOI： 10.14722/ndss.2019.23394 .

[18] CREMERS C， HORVAT M， HOYLAND J， et al. A comprehensive symbolic analysis of TLS 1.3［C］//Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security. New York： ACM， 2017： 1773-1788. DOI： 10.1145/3133956.3134063 .

[19] CREMERS C， KIESL B， MEDINGER N. A formal analysis of IEEE 802.11’sWPA2： Countering the kracks caused by cracking the counters［EB/OL］. ［2020-06-13］.

[20] DOLEV D， YAO A. On the security of public key protocols［J］. IEEE Transactions on Information Theory， 1983， 29（2）： 198-208. DOI： 10.1109/TIT.1983.1056650 .

[21] BLUETOOTH SIG CORE SPECIFICATION WORKING GROUP. Core Specification 5.3［EB/OL］. ［2021-07-13］.

[22] VAUGHAN G V， BLAKE E. GNU M4［EB/OL］. ［2021-07-12］.

[23] SCHMIDT B， MEIER S， CREMERS C， et al. Automated analysis of Diffie-Hellman protocols and advanced security properties［C］//2012 IEEE 25th Computer Security Foundations Symposium. New York： IEEE Press， 2012： 78-94. DOI： 10.1109/CSF.2012.25 .

[24] LOWE G. A hierarchy of authentication specifications［C］//Proceedings 10th Computer Security Foundations Workshop. New York： IEEE Press， 2002： 31-43. DOI： 10.1109/CSFW.1997.596782 .

[25] BLUETOOTH SIG. Bluetooth SIG statement regarding the ‘impersonation attack in Bluetooth mesh provisioning’ vulnerability ［EB/OL］. ［2021-05-24］.

基金资助

国家重点研发计划(2021YFB2700200)

国家自然科学基金(U1836202)

国家自然科学基金(62076187)

国家自然科学基金(62172303)