ProVerif：自动化协议验证
使用 ProVerif 规定并验证 TLS 握手属性
ProVerif：自动化协议验证 是 CoddyKit 上的免费 Cryptology Academy 课时。 这是第 3 节课，共 4 节。 你可以在下方免费阅读本课时的完整内容 — 然后在浏览器中使用内置代码编辑器和全天候 AI 导师进行实践。 这是 Cryptology Academy 学习路径的一部分，你的进度在网页和 CoddyKit 应用中同步。 Cryptology Academy 课程共包含 4 节课。
什么是 ProVerif
ProVerif（Bruno Blanchet，2001）是一种自动化的密码协议验证器。它接收使用应用 π 演算描述的协议，并自动判定保密性和身份认证属性。
ProVerif 的工作原理
ProVerif 将协议转换为霍恩子句，并应用基于归结的算法来推导攻击者能够学习的内容。如果某个保密性事实可以被推导出来，协议就已被攻破；否则，协议就被证明是安全的。
ProVerif 输入语言
协议以声明式方式描述：声明信道、类型、函数（enc、dec、sign、verify）、方程（dec(enc(m,k),k)=m）以及通过信道通信的进程。
声明密码学原语
ProVerif 声明示例：
(* Symmetric encryption *)
fun senc(bitstring, key): bitstring.
fun sdec(bitstring, key): bitstring.
equation forall m: bitstring, k: key; sdec(senc(m, k), k) = m.
(* Asymmetric encryption *)
fun pk(skey): pkey.
fun aenc(bitstring, pkey): bitstring.
fun adec(bitstring, skey): bitstring.
equation forall m: bitstring, sk: skey; adec(aenc(m, pk(sk)), sk) = m.编写一个简单的协议进程
将 Alice 和 Bob 建模为并行进程：
(* Alice sends nonce to Bob, encrypted *)
let Alice(skA: skey, pkB: pkey) =
new na: nonce;
out(c, aenc((na, pk(skA)), pkB));
in(c, m: bitstring);
let nb = adec(m, skA) in
out(c, aenc(nb, pkB)).
(* Main process: run attacker with full channel control *)
process
new skA: skey; new skB: skey;
out(c, pk(skA)); out(c, pk(skB)); (* publish public keys *)
(Alice(skA, pk(skB)) | Bob(skB, pk(skA)))陈述安全性查询
ProVerif 会检查如下查询：
(* Secrecy: attacker cannot learn na *)
query attacker(na).
(* Authentication: if Bob completes, Alice started *)
query event(BobFinished(nb)) ==> event(AliceStarted(nb)).解读 ProVerif 输出
ProVerif 输出“RESULT ... 为真”（已证明安全），或者输出“RESULT ... 为假”并打印显示攻击者消息的反例攻击轨迹。该轨迹会准确展示攻击如何发生。
使用 ProVerif 验证 TLS 1.3
Bhargavan 等人（2016）使用 ProVerif 分析了 TLS 1.3 的一个模型。他们发现并报告了一个针对 0-RTT 恢复机制的攻击，该问题在 RFC 定稿前得到了修复。
局限性：近似与循环
ProVerif 使用过度近似：它可能报告并不存在的攻击（在协议实际安全时报告“假”），但绝不会漏掉真实攻击。无界协议会话可能无法终止——ProVerif 会以启发式方式展开循环。
当 ProVerif 报告“CANNOT BE PROVED”时
如果 ProVerif 无法在其近似范围内确定结果，就会输出“CANNOT BE PROVED”。这并不证明协议不安全——这意味着工具的启发式能力已经耗尽。Tamarin 可能能够处理这些情况。
知识检查
对于保密性查询，ProVerif 输出“RESULT ... 为假”意味着什么？
课程回顾
ProVerif 使用霍恩子句归结实现协议验证自动化。协议使用带密码学方程的应用 π 演算编写。查询用于询问保密性和身份认证。“假”表示已证明安全；“真”表示协议已被攻破（并附有攻击轨迹）。局限性：近似可能导致“CANNOT BE PROVED”。
用 AI 导师学习 Cryptology Academy — 免费
在浏览器中编写并运行真实代码，获得全天候 AI 导师的即时帮助，并在网页或应用中继续学习。
- 课程
- 67
- 课程
- 261
常见问题解答
「ProVerif：自动化协议验证」课时是免费的吗？
是的 — 「ProVerif：自动化协议验证」的完整文本可在网页上免费阅读。要进行交互式练习（内置代码编辑器和全天候 AI 导师）并解锁 Cryptology Academy 课程的其余内容，请升级到 CoddyKit PRO。 Cryptology Academy 课程共包含 4 节课。
「ProVerif：自动化协议验证」这节课中我会学到什么？
使用 ProVerif 规定并验证 TLS 握手属性 你通过在浏览器中直接运行的动手代码来练习 Cryptology Academy，全天候 AI 导师会在你学习这节课的过程中回答你的问题。
学习 Cryptology Academy 需要有经验吗？
无需任何先前经验。CoddyKit 上的 Cryptology Academy 课程适合初学者到高级学习者，你可以从这里开始或从头开始，按照自己的节奏学习。 这是第 3 节课，共 4 节。
「ProVerif：自动化协议验证」课时需要多长时间？
大多数 CoddyKit 课程大约需要 5–10 分钟。每节课都很精短且互动，所以你能稳步进步，并在网页和应用中从离开的地方继续。
我能在这节 Cryptology Academy 课中编写并运行代码吗？
能。每节 Cryptology Academy 课都包含内置代码编辑器，你可以在浏览器中直接编写并运行真实代码，并获得即时 AI 反馈 — 无需本地设置。
此课程中的所有课时
- 为何非正式证明还不够
- Dolev-Yao 攻击者模型与符号密码学
- ProVerif：自动化协议验证
- Tamarin 与计算型证明