用 ProVerif 分析第一个协议：手把手解读 .pv 文件与命令行输出
从零开始用ProVerif分析协议：详解.pv文件编写与结果解读
第一次打开ProVerif的.pv文件时，那些看似晦涩的语法和命令行输出往往让人望而生畏。作为安全协议分析领域的瑞士军刀，ProVerif的强大功能与其陡峭的学习曲线同样出名。本文将从一个最简单的RSA协议示例出发，手把手带你理解.pv文件的每一行代码含义，并教你如何解读命令行输出的关键信息。
1. 准备工作与环境配置
在开始分析第一个协议之前，我们需要确保ProVerif环境已正确配置。虽然安装过程不是本文重点，但几个关键点值得注意：
- Graphviz可视化支持：当ProVerif发现攻击路径时，需要Graphviz生成可视化图表。安装后记得将
bin目录加入系统PATH - GTK+运行时库：这是运行交互式模拟器的前提条件，Windows用户需特别注意版本兼容性
- 测试文件目录：建议将所有.pv测试文件集中存放在ProVerif安装目录下的
examples文件夹中
验证安装是否成功的最快方法是运行示例协议。打开命令行，导航到ProVerif安装目录，执行：
proverif examples/needham-schroeder.pv如果看到类似下面的输出，说明环境已就绪：
Verification summary: Query not attacker(pkA[]) is true. Query not attacker(pkB[]) is true. Query inj-event(endB(x)) ==> inj-event(beginA(x)) is false.2. 第一个协议：Cocks/RSA示例解析
让我们从一个精简的RSA协议示例开始，逐步拆解.pv文件的结构。创建一个名为cocks-rsa.pv的文件，内容如下：
free c:channel. free Cocks:bitstring[private]. free RSA:bitstring[private]. query attacker(RSA). query attacker(Cocks). process out(c,RSA); 02.1 协议基础元素定义
通道声明：
free c:channel.这行代码定义了一个名为c的公开通信通道。在ProVerif中，所有消息交换都通过这样的通道进行，模拟现实网络中的通信链路。
密钥声明：
free Cocks:bitstring[private]. free RSA:bitstring[private].这里声明了两个私有比特串：
Cocks：代表Clifford Cocks提出的早期RSA变体密钥RSA：标准RSA算法的密钥
[private]标记表示这些值最初不会被攻击者知晓，是协议要保护的秘密。
2.2 安全属性查询
query attacker(RSA). query attacker(Cocks).这两个查询语句定义了我们要验证的安全属性：
- 检查攻击者是否能获取
RSA密钥 - 检查攻击者是否能获取
Cocks密钥
ProVerif将基于Dolev-Yao攻击者模型自动验证这些属性，该模型假设攻击者可以：
- 拦截所有网络通信
- 解密已知密钥的消息
- 构造新消息并注入网络
2.3 协议流程定义
process out(c,RSA); 0这个简单的进程描述协议行为：
out(c,RSA)：通过通道c发送RSA密钥0：表示进程终止
分号;是顺序操作符，表示动作按顺序执行。这个极简的协议实际上存在明显漏洞——它直接发送了应该保密的密钥。
3. 运行分析与结果解读
将上述内容保存为cocks-rsa.pv后，在命令行运行：
proverif cocks-rsa.pv3.1 理解输出结果
典型输出如下：
RESULT not attacker(RSA[]) is false. RESULT not attacker(Cocks[]) is true.结果解读：
not attacker(RSA[]) is false：- 双重否定逻辑：攻击者可以获取RSA密钥
- 这与我们的协议设计一致，因为进程明确输出了RSA密钥
not attacker(Cocks[]) is true：- 攻击者无法获取Cocks密钥
- 因为协议中从未泄露这个密钥
3.2 攻击轨迹分析
当属性验证失败时（如RSA密钥泄露），ProVerif可以生成攻击轨迹。添加-graph参数获取可视化攻击路径：
proverif -graph cocks-rsa.pv这将生成一个.dot文件，用Graphviz转换为图像后，可以看到：
- 攻击者监听到通道
c上的消息 - 直接获取了明文RSA密钥
这种可视化对于复杂协议尤其有用，能清晰展示攻击者如何逐步破坏安全属性。
4. 增强协议安全性
让我们修改原始协议，使其更符合实际场景。新建cocks-rsa-v2.pv：
free c:channel. free Cocks:bitstring[private]. free RSA:bitstring[private]. free msg:bitstring. (* 非对称加密函数 *) fun aenc(bitstring, bitstring):bitstring. reduc forall x:bitstring, y:bitstring; adec(aenc(x,y),y) = x. query attacker(RSA). query attacker(Cocks). process out(c, aenc(msg, RSA)); 04.1 新增加密原语
fun aenc(bitstring, bitstring):bitstring. reduc forall x:bitstring, y:bitstring; adec(aenc(x,y),y) = x.这部分定义了非对称加密：
aenc：加密函数，接受明文和公钥adec：解密函数，ProVerif通过reduc规则描述其行为- 还原规则表示：用正确私钥解密加密消息能得到原始明文
4.2 修改后的协议流程
process out(c, aenc(msg, RSA)); 0现在协议不再直接泄露密钥，而是发送用RSA加密的消息。重新运行分析：
RESULT not attacker(RSA[]) is true. RESULT not attacker(Cocks[]) is true.两个查询结果都为"true"，表明攻击者无法获取任一密钥。注意这并不保证消息msg的保密性——如果需要验证这点，应添加：
query attacker(msg).5. 进阶协议元素解析
让我们扩展协议，引入更多典型元素。创建cocks-rsa-complex.pv：
free c:channel. free Cocks:bitstring[private]. free RSA:bitstring[private]. free msg:bitstring. (* 加密原语 *) fun aenc(bitstring, bitstring):bitstring. reduc forall x:bitstring, y:bitstring; adec(aenc(x,y),y) = x. fun sign(bitstring, bitstring):bitstring. reduc forall x:bitstring, y:bitstring; checksign(sign(x,y),y) = x. (* 事件用于对应断言 *) event beginProtocol(bitstring). event endProtocol(bitstring). query attacker(msg). query inj-event(endProtocol(x)) ==> inj-event(beginProtocol(x)). process let pkA = RSA in let skA = Cocks in event beginProtocol(msg); out(c, sign(aenc(msg, pkA), skA)); event endProtocol(msg); 05.1 新增安全特性
数字签名：
fun sign(bitstring, bitstring):bitstring. reduc forall x:bitstring, y:bitstring; checksign(sign(x,y),y) = x.sign：用私钥签名消息checksign：用公钥验证签名- 还原规则确保签名验证的正确性
事件标记：
event beginProtocol(bitstring). event endProtocol(bitstring).事件用于验证协议执行的正确顺序，常用于对应断言(injective correspondence)验证。
5.2 复杂查询示例
query inj-event(endProtocol(x)) ==> inj-event(beginProtocol(x)).这个对应断言验证：
- 每次
endProtocol事件的执行 - 都必须有唯一的
beginProtocol事件与之对应 inj-前缀确保一对一的映射关系
5.3 完整协议流程
process let pkA = RSA in let skA = Cocks in event beginProtocol(msg); out(c, sign(aenc(msg, pkA), skA)); event endProtocol(msg); 0协议现在执行以下操作：
- 绑定密钥对
- 标记协议开始事件
- 用RSA加密消息并用Cocks密钥签名
- 发送加密签名消息
- 标记协议结束事件
运行分析将验证消息保密性和事件对应关系。这种结构更接近实际安全协议的设计模式。