开放科学（资源服务）标志码（OSID）：

0 概述

安全协议旨在通过应用密码原语在不安全的网络上提供安全通信。然而，安全协议的设计特别容易出错，研究者在5G^[1]、TLS^[2]等协议中都发现了设计上存在的缺陷。这使得安全协议的安全性验证成为一个热门的研究课题。

目前，已有许多对安全协议进行建模与分析的工作。最早的协议分析工具如Interrogator^[3]和NRL Protocol Analyzer^[4]，能够验证时序逻辑中的安全属性。一些通用的模型检测工具也已经被用于分析协议，如FDR^[5]和Murphi^[6]。最近，研究的重点转向了设计专门用于分析安全协议的模型检测工具，如Blanchet’s ProVerif^[7]、AVISPA tool^[8]、MaudeNPA^[9]和Tamarin prover^[10]。

虽然在安全协议的设计中利用形式化的方法能够成功地找到漏洞，但实现对安全协议的全自动分析仍然是一个挑战。smartVerif^[11]是基于强化学习的一般性框架，其能提高目前最先进验证工具的自动化能力，但不足之处在于无泛化性，需要对每个安全协议训练一个对应的神经网络模型，每个安全协议的验证都需要从完全随机探索开始训练，因此验证效率较低。

本文基于无人工特征的强化学习模型对smartVerif框架进行优化。该优化方案通过Alpha Go zero^[12]中将深度神经网络与蒙特卡洛树搜索相结合的形式，与smartVerif中所使用的DQN网络结构相比，只需要利用安全协议训练一个模型即可验证新的安全协议，无需重新训练网络。此外，关注形式化验证数据所包含的结构化信息，在向量表示方法中使用树型结构作为中间表达对形式化数据进行转换，同时考虑验证过程中的历史信息。与smartVerif中对字符串进行哈希的向量化方式相比，特征向量包含了形式化数据的结构信息。

1 相关研究

在用于验证安全协议的典型模型检测方法中，ProVerif ^[7]是一种有效且使用广泛的协议分析工具，其通过在Horn逻辑下对协议编码的抽象来进行分析验证。这种抽象方法非常适合攻击者知识不变的情形，因此该工具能够有效地验证具有无限数量协议会话的协议^[13-14]，可证明可达性性质、对应断言和观察等价性。StatVerif^[15]是对ProVerif的一种扩展。StatVerif中的扩展设计目的是为了避免许多错误的攻击，常用于自动推断操纵全局状态的协议。GSVerif^[16]将ProVerif扩展到全局状态，提供了包括私有信道、工作单元和计数器在内的几种合理的转换，能够验证具有全局状态的协议是有效的。

另一种支持状态性协议验证的验证工具是Tamarin-prover^{[10, 17]}，其未使用抽象技术，而是利用反向搜索和引理来处理验证中的无限状态空间。tamarin及其相关工具的优势在于，在处理不能通过抽象和解析的方法捕获到的数据之间的形式化关系时，有极大的灵活性。tamarin能够处理全局状态协议^[18]、无限会话协议^[10]、观察等价属性^[19]、异或操作^[1]等。然而，这是以失去自动化能力为代价的，即用户必须通过证明复杂协议的辅助引理来解决问题。目前，tamarin已经被用来分析Yubikey device^[20]、security APIs in PKCS#11^[21]和TPM协议族^[22]，并且有研究者通过tamarin prover发现了V2X^[23]协议的攻击方式。

上述工具在验证过程中都是使用静态策略，这会在验证复杂协议时导致验证无法成功终止。为了应对这些无法终止的情形，需要分析原因并添加手工证明过程。而smartVerif则是使用动态策略对协议进行验证，其通过强化学习的方式，使用DQN网络结构^[24]学习得到动态的策略。由于smartVerif视不同的协议为不同的任务，因此针对不同的安全协议需要训练不同的网络，导致网络失去泛化能力，与静态策略相比，验证效率相对较低。

2 优化方案设计

为更高效地使用动态策略对安全协议进行形式化验证，同时使得模型学习的策略具有泛化性，需要对验证框架中的强化学习模型进行一定的优化设计，其中存在以下两个挑战：1）如何将形式化验证数据在相对完整地保留数据信息的前提下，转换成神经网络的输入；2）如何对强化学习网络结构进行改进与优化，使得模型具有泛化性。本文提出一种关注数据结构信息的向量表达方式，并且使用Alpha Go Zero中的强化学习框架替代smartVerif中的DQN神经网络结构。

2.1 优化步骤

本文优化设计的具体步骤如下：

步骤1  选取smartVerif中所使用的24个协议随机进行分割，将其中的20个作为训练集，4个作为验证集。

步骤2  以多线程的方式对训练集中的协议进行训练。对训练的每一个轮次中的每个协议：

步骤2.1  使用Tamarin-prover产生形式化数据，并将数据转换为证明定理树。

步骤2.2  对当前证明定理树中仍未完成证明的每个结点构建特征向量$ \boldsymbol{S} $，使用深度神经网络$ {f}_{\theta } $计算所有这些结点相应的动作选择概率P以及当前结点的价值$ v $：$ (\boldsymbol{P}, v)={f}_{\theta }\left(\boldsymbol{S}\right) $。

步骤2.3  对步骤2.2中所有进行计算的结点使用蒙特卡洛树搜索（MCTS），每一次对每个结点执行选择、扩展、更新操作。重复100次后，利用MCTS的结果进行当前结点的动作选择。直到对所有结点完成动作选择。

步骤2.4  将步骤2.3中所有的动作选择加入证明定理树，利用循环检测算法检测证明定理树中每一条没有终止的证明路径。

步骤2.5  如果路径已经产生循环，则将路径标记为循环路径，不再进行证明，否则继续对路径重复执行步骤2.1~步骤2.4。

步骤2.6  若证明定理树上所有路径都已经终止证明，则说明当前协议证明成功或者无法终止证明。此时，需要对证明定理树上的各个结点进行评估并设置奖励z，最后将数据$ （\boldsymbol{S}, \boldsymbol{P}, z） $保存到数据缓冲区。

步骤2.7  本轮所有协议完成验证后，从数据缓冲区中随机取出256个数据进行训练。

步骤3  每进行5次训练，对$ {f}_{\theta } $进行一次评估。比较本次训练的$ {f}_{\mathrm{n}\mathrm{o}\mathrm{w}} $与保存下的最佳模型$ {f}_{\mathrm{b}\mathrm{e}\mathrm{s}\mathrm{t}} $，留下效果更好的模型作为新的$ {f}_{\mathrm{b}\mathrm{e}\mathrm{s}\mathrm{t}} $。

2.2 强化学习框架

本文优化方案使用一个深度神经网络$ {f}_{\theta } $，其中，$ \theta $表示网络的参数。网络的输入是由Tamarin-prover验证协议过程中形成的证明定理树中每条路径结点信息组成的向量，以及当前叶结点的所有可选动作的结点向量这2个部分组成特征向量$ \boldsymbol{S} $。网络的输出是当前叶结点的所有可选动作的概率P以及当前叶结点的价值$ v $，$ (\boldsymbol{P}, v)={f}_{\theta }\left(\boldsymbol{S}\right) $，其中叶结点的价值表示当前叶结点能够完成证明的可能性。这个神经网络将策略网络和价值网络组合成一个单一的体系结构^[25]。在整个协议验证过程中，需要利用神经网络选择后续用来完成协议证明的结点扩展定理树。重复扩展直至协议证明完成或者产生循环证明的路径。

2.2.1 特征向量结构

特征向量由2个部分组成：第1部分是证明定理树中某条未完成证明的路径上的所有结点向量化后所构成的向量$ \boldsymbol{V}=[{\boldsymbol{v}}_{1}, {\boldsymbol{v}}_{2}, \cdots , {\boldsymbol{v}}_{t}] $。其中，$ {\boldsymbol{v}}_{i} $$ (1\le i\le t) $是路径中某个结点的形式化数据向量化表达；第2部分是所有当前可选子结点向量$ \boldsymbol{U}=[{\boldsymbol{u}}_{1}, {\boldsymbol{u}}_{2}, \cdots , {\boldsymbol{u}}_{t}] $，其中，$ {\boldsymbol{u}}_{i} $$ (1\le i\le s) $是当前证明定理树中的叶结点的某个可选动作的向量化表达。因此，特征向量$ \boldsymbol{S}=[\boldsymbol{V}, \boldsymbol{U}] $。

如图 1所示，虚线框标识了当前证明定理树中的一条证明路径，路径中末尾结点的4个子结点代表当前的4个可选动作，因此，在当前状态下，方框中末尾结点的特征向量$ \boldsymbol{S}=[\boldsymbol{V}, \boldsymbol{U}] $，$ \boldsymbol{V}=[{\boldsymbol{v}}_{1}, {\boldsymbol{v}}_{2}, \cdots , {\boldsymbol{v}}_{t}] $，$ \boldsymbol{U}=[{\boldsymbol{u}}_{1}, {\boldsymbol{u}}_{2}, \cdots , {\boldsymbol{u}}_{t}] $。

2.2.2 结点向量化

本文所使用的向量转换方式为：首先将结点中的形式化数据从字符串形式转换成一个树形结构形式，然后将树形结构中的结点信息转换为向量，最后利用树形结构的结构表达进一步地将结点信息整合，利用根节点的向量表示形式化数据的向量，从而使形式化数据的向量化表达包含数据的结构化信息。所有的形式化数据可分为5种类型，分别是Split、Action、Premise、Disj和Chain^[17]。由于每个结点仅属于某一种类型，因此可用不同的根结点表示不同的结点类型，同时以所有的叶结点表示各个变量，非叶结点表示一种操作。然后以哈希的形式将树形结构中的每一个结点转换为向量的形式，再采取自下而上的方式更新树形结构中的每一层结点的向量表达。最后以根节点的向量作为整个树形结构的向量化表达。

图 2所示为结点No的形式化数据“State_11111111111（~lock12，pid，k，nonce，npr，otc，secretid，tc1，tuple）▶₀#t1”所对应的树形结构表达，其中：“▶₀”是Premise类型结点的唯一操作符，可以以“▶₀”为根节点的树形结构表示类型为Premise的结点；非叶结点的“State_11111111111”操作视为一个函数；“#t1”表示时间戳，视为一个变量，括号内各个操作数也视为变量。

将形式化数据的字符串表达形式转换为树形结构的结构化表达形式，然后将树形结构中每个结点中的字符串以哈希的方式转换成一个128位的01串，以128维的向量表示。在此基础上，以自下而上的顺序更新树形结构中每一层结点的向量表达，并以根节点的向量结果表示整个树形结构的向量化表达。具体而言，对树中的某个结点No，若其子结点向量化表达为$ {\boldsymbol{c}}_{1}, {\boldsymbol{c}}_{2}, \cdots , {\boldsymbol{c}}_{p}, {\boldsymbol{d}}_{1}, {\boldsymbol{d}}_{2}, \cdots , {\boldsymbol{d}}_{q} $，其中：$ {\boldsymbol{c}}_{i} $表示结点No的子结点为叶节点；$ {\boldsymbol{d}}_{j} $表示结点No的子结点为非叶节点。因此，则结点No的叶子结点总数为p+q，则结点No的向量表达$ {\boldsymbol{x}}_{n} $为：

$ {\boldsymbol{x}}_{n}=\left\{\begin{array}{l}\frac{1}{3}\left({\boldsymbol{x}}_{n}+\frac{1}{p}\sum \limits_{w}{\boldsymbol{c}}_{w}+\frac{1}{q}\sum \limits_{t}{\boldsymbol{d}}_{t}\right), p\ne 0, q\ne 0\\ \frac{1}{2}\left({\boldsymbol{x}}_{n}+\frac{1}{p}\sum \limits_{w}{\boldsymbol{c}}_{w}\right), p\ne 0, q=0\\ \frac{1}{2}\left({\boldsymbol{x}}_{n}+\frac{1}{p}\sum \limits_{t}{\boldsymbol{d}}_{t}\right), p=0, q\ne 0\\ {\boldsymbol{x}}_{n}, p=0, q=0\end{array}\right. $

2.2.3 深度强化学习网络

深度神经网络由安全协议通过强化学习验证过程中产生的形式化数据进行训练。对每一个特征向量$ \boldsymbol{S} $，都会在神经网络$ {f}_{\theta } $的指导下执行蒙特卡洛树搜索（MCTS）。MCTS搜索结束后会产生当前所有可选动作的概率$ \boldsymbol{\pi } $。$ \boldsymbol{\pi } $经过MCTS后往往会比神经网络$ {f}_{\theta } $产生的动作概率$ \boldsymbol{P} $更接近想要的结果（协议完成验证）。因此，在协议验证的过程中使用基于MCTS的增强策略选择每个动作，然后使用能够完成验证的数据与无法终止验证的数据作为样本训练神经网络，可以将MCTS过程看作一种有力的策略评估器。本文使用的强化学习算法重复策略迭代的过程，以MCTS产生的动作选择策略$ \boldsymbol{\pi } $作为神经网络$ {f}_{\theta } $产生的动作选择策略P的指导，更新神经网络的参数。神经网络的参数更新使得迭代过程中产生的策略和价值逐步逼近能够成功验证协议的策略和价值。

深度神经网络整体由公共网络部分和2个分离的策略网络与价值网络组成。网络的输入为特征向量$ \boldsymbol{S}=[\boldsymbol{V}, \boldsymbol{U}] $。首先将$ \boldsymbol{V} $经过一个公共的textCNN层^[26]，将不定长路径向量$ \boldsymbol{V} $转换为一个1×128维的向量$ \boldsymbol{A} $。然后将$ \boldsymbol{A} $分别输入策略网络和价值网络。策略网络对$ \boldsymbol{A} $与$ \boldsymbol{U} $进行注意力计算^[27]，再经过一个softmax层得到各个动作的选择概率。价值网络首先将$ \boldsymbol{U} $进行最大池化操作得到特征向量$ \boldsymbol{B} $，再将$ \boldsymbol{A} $与$ \boldsymbol{B} $进行点积运算，最后通过一个tanh层得到当前特征向量$ \boldsymbol{S} $的价值。网络的训练是在损失函数$ l $上的梯度下降过程，损失函数由方差和交叉熵以及网络参数的二阶范式（防止过拟合）组成：

$ l={\left(z-v\right)}^{2}-{\boldsymbol{\pi }}^{\mathrm{T}}\mathrm{l}\mathrm{o}{\mathrm{g}}_{a}\boldsymbol{P}+c{‖\theta ‖}^{2} $

MCTS模拟探索过程可分为选择、扩展评估、参数更新3个阶段。在MCTS的搜索树中，每条边（s，a）存储了选择概率P（s，a）、当前结点访问次数N（s，a）和当前结点的价值Q（s，a）。

在选择阶段，t时刻在搜索树中模拟通过选择有最大结点价值Q，再额外加上一个由选择概率和当前结点访问次数决定的置信上限U的动作。

$ {a}_{t}=\underset{a}{\mathrm{a}\mathrm{r}\mathrm{g} \ \mathrm{m}\mathrm{a}\mathrm{x}}\left(Q\left({s}_{t}, a\right)+U\left({s}_{t}, a\right)\right) $

$ U\left({s}_{t}, a\right)={c}_{\mathrm{p}\mathrm{u}\mathrm{c}\mathrm{t}}P\left(s, a\right)\frac{\sqrt{\sum \limits_{b}N\left(s, b\right)}}{1+N\left(s, a\right)} $

其中，c_puct=3为探索常数，用来在MCTS模拟搜索的过程中探索尽可能多的结点。

在扩展评估阶段，选择达到叶结点时，如果可以继续进行协议验证，则需要用$ {f}_{\theta } $扩展搜索树。

在参数更新阶段，对搜索树上的边存储的信息在每个时间节点向后更新：

$ N\left({s}_{t}, {a}_{t}\right)=N\left({s}_{t}, {a}_{t}\right)+1 $

$ W\left({s}_{t}, {a}_{t}\right)=W\left({s}_{t}, {a}_{t}\right)+v $

$ Q\left({s}_{t}, {a}_{t}\right)=\frac{W\left({s}_{t}, {a}_{t}\right)}{N\left({s}_{t}, {a}_{t}\right)} $

在MCTS模拟搜索T次后，从开始模拟的根节点根据模拟结果做出动作选择：

$ \pi \left(a|{s}_{0}\right)=\frac{N{\left({s}_{0}, a\right)}^{\frac{1}{\tau }}}{\sum \limits_{b}N{\left({s}_{0}, b\right)}^{\frac{1}{\tau }}} $

其中，$ \tau $是一个探索参数，根据$ \tau $设置不同的值控制当前执行探索或者是按策略进行动作选择。

前5步选择动作时概率为：

$ P\left(s, a\right)=\frac{N\left({s}_{0}, a\right)}{\sum \limits_{b}N\left({s}_{0}, b\right)} $

5步之后选择动作的概率为：

$ P\left(s, a\right)=\left(1-\varepsilon \right){p}_{a}+\varepsilon {\eta }_{a} $

其中，$ \eta \sim \mathrm{D}\mathrm{i}\mathrm{r}\left(1.2\right) $，$ \varepsilon =0.25 $。添加狄利克雷噪声的目的是为了覆盖所有的可选动作。

2.2.4 循环检测算法

本文使用smartVerif中所使用的循环检测算法^[11]来检测当前证明定理树中的某条路径是否已经产生循环。对于已经产生循环的路径，不再继续进行验证。由于在smartVerif中的参数设置会使得部分安全协议的循环路径被判定为正确证明路径，因此本文的循环检测算法中的参数与smartVerif中所使用的参数设置不同：$ \alpha =20，\beta =0.2，\rho =20，\delta =3 $，确保不在循环路径上耗费过多的时间而降低验证效率。

3 实验结果与分析 3.1 训练与评估方法

通过上文所提到的流程执行算法得到每个协议验证产生的证明定理树。对每个证明定理树中的每条路径而言，路径上的结点价值设置为：循环路径上从循环开始的结点到末尾结点价值为-1；证明结束路径上的最长不与循环路径相交部分所有结点价值为1，其余结点不做评估，防止陷入局部最优。将评估后的数据$ （\boldsymbol{S}, \boldsymbol{P}, z） $存放到数据缓冲区。

数据缓冲区是一个大小为10 000的队列。每次训练数据的批量大小为256，每训练5次对当前模型进行一次评估。分别使用上一次保存的最佳模型$ {f}_{\mathrm{b}\mathrm{e}\mathrm{s}\mathrm{t}} $与本次训练后的模型$ {f}_{\mathrm{n}\mathrm{o}\mathrm{w}} $对验证集进行验证，有以下3种情况：1）$ {f}_{\mathrm{b}\mathrm{e}\mathrm{s}\mathrm{t}} $与$ {f}_{\mathrm{n}\mathrm{o}\mathrm{w}} $都不能验证所有验证集中的协议文件，此时取能够验证协议个数最多的模型作为$ {f}_{\mathrm{b}\mathrm{e}\mathrm{s}\mathrm{t}} $；2）$ {f}_{\mathrm{b}\mathrm{e}\mathrm{s}\mathrm{t}} $和$ {f}_{\mathrm{n}\mathrm{o}\mathrm{w}} $中只有一个能证明所有验证集中的协议，此时取能够证明所有验证集中协议的模型作为$ {f}_{\mathrm{b}\mathrm{e}\mathrm{s}\mathrm{t}} $；3）$ {f}_{\mathrm{b}\mathrm{e}\mathrm{s}\mathrm{t}} $和$ {f}_{\mathrm{n}\mathrm{o}\mathrm{w}} $都能证明验证集中所有协议。

对于第3种情况，设置信比例为$ \theta =0.1 $，若$ {f}_{\mathrm{b}\mathrm{e}\mathrm{s}\mathrm{t}} $证明验证集中协议时间分别是$ {t}_{1}^{\mathrm{b}\mathrm{e}\mathrm{s}\mathrm{t}}, {t}_{2}^{\mathrm{b}\mathrm{e}\mathrm{s}\mathrm{t}}, \cdots , {t}_{k}^{\mathrm{b}\mathrm{e}\mathrm{s}\mathrm{t}} $（k为验证集大小），$ {f}_{\mathrm{n}\mathrm{o}\mathrm{w}} $证明第j个协议（1≤j≤k）时间$ {t}_{j}^{\mathrm{n}\mathrm{o}\mathrm{w}} $满足$ \left|{t}_{j}^{\mathrm{n}\mathrm{o}\mathrm{w}}-{t}_{j}^{\mathrm{b}\mathrm{e}\mathrm{s}\mathrm{t}}\right|\le \theta {t}_{j}^{\mathrm{b}\mathrm{e}\mathrm{s}\mathrm{t}} $，则认为模型训练效果对第j个协议而言没有变化。

设$ {c}_{\mathrm{S}} $表示$ {t}_{j}^{\mathrm{b}\mathrm{e}\mathrm{s}\mathrm{t}}-{t}_{j}^{\mathrm{n}\mathrm{o}\mathrm{w}}\le \theta {t}_{j}^{\mathrm{b}\mathrm{e}\mathrm{s}\mathrm{t}} $的协议个数，$ {c}_{\mathrm{L}} $表示$ {t}_{j}^{\mathrm{n}\mathrm{o}\mathrm{w}}-{t}_{j}^{\mathrm{b}\mathrm{e}\mathrm{s}\mathrm{t}}\ge \theta {t}_{j}^{\mathrm{b}\mathrm{e}\mathrm{s}\mathrm{t}} $的协议个数。当$ {c}_{\mathrm{S}} > {c}_{\mathrm{L}} $时，说明当前网络模型更优，使用$ {f}_{\mathrm{n}\mathrm{o}\mathrm{w}} $替代$ {f}_{\mathrm{b}\mathrm{e}\mathrm{s}\mathrm{t}} $；当$ {c}_{\mathrm{S}}\le {c}_{\mathrm{L}} $时，说明$ {f}_{\mathrm{n}\mathrm{o}\mathrm{w}} $相比$ {f}_{\mathrm{b}\mathrm{e}\mathrm{s}\mathrm{t}} $没有得到优化，保留$ {f}_{\mathrm{b}\mathrm{e}\mathrm{s}\mathrm{t}} $。

3.2 实验结果

本文实验在Intel Broadwell E5-2660V4 2.0 GHz CPU、128 GB内存、4个GTX 1080 Ti显卡、Ubuntu 16.04 LTS的环境下进行，强化学习交互对象是tamarin prover v1.5.1。实验的验证集中包含随机抽取的TPM-toy、Feldhofer’s RFID、CANauth和Okamoto协议，实验结果如表 1所示，其中，$ \mathrm{\infty } $表示证明时间超过150 min。

3.3 案例分析

以Okamoto协议为案例进行分析。该协议在没有安全专家设置的静态策略指导下，容易陷入状态爆炸的证明状态。当网络训练轮次较少时，Okamoto协议无法在有限的时间内完成证明。由表 1所示的实验结果可知：Okamoto协议在训练至85轮次、证明时间为150 min时，搜索遍历的证明定理树结点数量为24 853个；当训练至165轮次时，完成协议验证共访问了18 649个结点；当训练至260轮次时，完成协议验证共访问了13 468个结点；而当训练至350轮次时，访问结点减少到了9 635个。因此，使用训练集数据对神经网络的训练，对验证集中的协议验证起到了指导作用，使得验证集中的协议进行验证时遍历访问的结点总数逐渐减少。

4 结束语

基于强化学习的形式化验证工具普遍存在模型无泛化性和验证效率低的问题。本文使用一种具有泛化能力的神经网络，并通过将形式化数据字符串表达形式转换为树形结构表达形式来保留形式化数据所具有的结构信息。通过引入完全自学习而不添加人工特征的强化学习模型替代原有的DQN模型结构，使得模型经过训练后对安全协议的验证具有泛化性。同时，保留形式化数据的结构特征以提高协议验证效率，缩短协议验证时间。后续将在形式化数据的转换上保留语义特征，进一步提高验证效率，并寻找合适的模型评估手段加快神经网络收敛速度。此外，还将使用手工建模的方式对一些安全协议^[28-30]进行建模，探究改进后smartVerif的泛化性和验证效率。