ProVerif: 形式化证明工具

参考文献：

1. [Blan22] Bruno Blanchet. The Security Protocol Verifier ProVerif and its Horn Clause Resolution Algorithm. arXiv:2211.12227.
2. [BSCS23] Blanchet, B., Smyth, B., Cheval, V., Sylvestre, M.: ProVerif 2.05: automatic cryptographic protocol verifier, user manual and tutorial (2023)
3. ProVerif: Cryptographic protocol verifier in the formal model
4. Graphviz
5. 使用 proverif 来分析密码协议
6. 一小时实践入门 Graphviz

ProVerif

ProVerif 是一种密码协议的自动化验证工具，由 Bruno Blanchet 开发，于 2002 年发布。目前已经有大量的密码协议分析工作使用了 ProVerif 的辅助。

ProVerif 采用符号模型（Dolev-Yao model），将密码协议使用霍恩子句（Horn clauses）来表示。ProVerif 支持 SE, PKE, Hash, NIZK 等密码原语，能够对于安全属性的可达性、相关的断言和等价性，以及隐私、可追溯、可验证等新兴属性给出证明。当其不满足时，可以重建攻击路径。

需要注意的是：在 symbolic model 中证明安全的协议，在 computational model 中不一定安全，进一步在 real world 内可能存在更多漏洞。但是 ProVerif 足以分析出很多实际存在的攻击。

ProVerif 的工作流程为：

1. 输入协议描述（Pi calculus + cryptography）和要证明的属性（Secrecy, authentication, …）
2. 将其翻译为 Horn clauses，它们形如 $R=(F\wedge H\Rightarrow C)$，其中 $R$ 是子句，$F,H$ 是假设，$C$ 是结论，其等价于 $R=(\neg F\vee \neg H\wedge C)$
3. 对 clauses 迭代执行 “带选择的消除”，达到一个不动点，可分为三种输出：
   1. RESULT [Query] is true: 可证明不存在攻击，从而属性是真的；
   2. RESULT [Query] is false: 找到了一种攻击，即证明了属性是假的；
   3. RESULT [Query] cannot be proved: 没能证明属性是真的，但也没有给出攻击。

安装

在 Windows 中安装 ProVerif 密码协议形式化证明工具，以及 Graphviz 图形可视化软件。

ProVerif

在官网中，下载最新的 ProVerif version 2.05, for Windows 二进制发行版工具包，解压后将 proverif2.05 配置到 PATH 变量中。

Graphviz

在官网中，下载最新的 graphviz-14.0.0 (64-bit) ZIP archive (contains all tools and libraries) 二进制发行版工具包，解压后将 Graphviz-14.0.0-win64/bin 配置到 PATH 变量中。

使用

用法

ProVerif 的密码协议描述文件为 .pv 后缀的文本文件，分为三个部分：

1. 类型和名称的声明
   • type t，类型声明，内置类型有 channel, bitstring, bool 等（其余 pkey, skey 等均需要自行定义）
   • free n: t，自由名称，默认可被敌手查看，添加 [private] 以隐藏
   • fun f(t1, .., tn): t，构造函数 f，用于声明密码原语（比如 senc, aenc, sign）
   • reduc forall x1:t1, ..., xn:tn, g(M1, ..., Mk) = M0，析构函数 g，用于定义密码原语的功能（比如 sdec, adec, checksign），其中 Mi 是关于 xj 的构造函数（分别对应 senc, aenc, sign）
   • event e(t1, ..., tn)，事件声明，其中 ti 是类型
2. 属性和推倒关系的要求
   • query attacker(M)，要求敌手不知道 M 的知识（机密性）
   • query x1:t1, ..., xn:tn; event(e1(M1, ..., Mk)) ==> event(e2(N1, ..., Nl))，如果 xi 出现在 Mj 中则为全称量词，如果只出现在 Nj 中则为存在量词，要求这些自由名称总是满足 e1 导致 e2
   • query x1:t1, ..., xn:tn; inj-event(e1(M1, ..., Mk)) ==> inj-event(e2(N1, ..., Nl))，额外要求从 e1 到 e2 是单射
3. 原语和过程的描述
   • let R(x1:t1, ..., xn:tn) = P，子过程宏（比如 client, server），其中 P 是一些语句
   • process P，执行 P（主函数），它是一些语句
   • new n:t; P，定义局部的名称（比如 k: skey）
   • out(c, n)，将自由名称输出到信道
   • in(c, x:t)，从信道获取类型为 t 的名称
   • if M then P else Q，分支语句
   • let x = M in P else Q，尝试执行 M 并赋值给 x，如果成功则执行 P（使用 x），否则执行 Q
   • event e(M1, ..., Mn); P，事件发生的语句，其中 Mi 的输出类型为 ti
   • R(M1, ..., Mn)，在过程中调用宏

上述的 M,N 被称为 terms（名称、调用，及其组合），

• M = N，相等
• M <> N，不相等
• M && N，合取
• M || N，析取
• not(M)，取反
• (M1, ..., Mk)，内置元组，其中 $k\ge 2$，其类型被视为 bitstring

上述的 P,Q 被称为 processes（一些语句）

• 0，空过程，常作为过程的终止
• P | Q，并行组合（例如 client | server）
• !P，无界的副本（意为 P | P | ...）

示例

编写 handshake.pv 文件

(*=================== sym ===========================*)
type key.fun senc(bitstring, key): bitstring.
reduc forall m:bitstring, k:key; sdec(senc(m, k), k) = m.(*=================== asym ===========================*)
type skey.
type pkey.fun pk(skey): pkey.
fun aenc(bitstring, pkey): bitstring.
reduc forall m:bitstring, sk:skey; adec(aenc(m, pk(sk)), sk) = m.(*=================== sign ===========================*)
type sskey.
type spkey.fun spk(sskey): spkey.
fun sign(bitstring, sskey): bitstring.
reduc forall m:bitstring, ssk:sskey; checksign(sign(m, ssk), spk(ssk)) = m.
reduc forall m:bitstring, ssk:sskey; getmess(sign(m, ssk)) = m.(*==============================================*)free c : channel .free s: bitstring [private].
query attacker(s).event acceptsClient(key).
event acceptsServer(key, pkey).
event termClient(key, pkey).
event termServer(key).query x:key, y:pkey; event(termClient(x, y)) ==> event(acceptsServer(x, y)).
query x:key; inj-event(termServer(x)) ==> inj-event(acceptsClient(x)).let clientA(pkA: pkey, skA: skey, pkB: spkey) =in(c, x:bitstring);let y = adec(x, skA) inlet (=pkB, k:key) = checksign(y, pkB) inevent acceptsClient(k);out(c, senc(s, k));event termClient(k, pkA).let serverB(pkB: spkey, skB: sskey, pkA: pkey) =in(c, pkX:pkey);new k:key;event acceptsServer(k, pkX);out(c, aenc(sign((pkB, k), skB), pkX));in(c, x:bitstring);let z = sdec(x, k) inif pkX = pkA thenevent termServer(k).processnew skA: skey;new skB: sskey;let pkA = pk(skA) in out(c, pkA);let pkB = spk(skB) in out(c, pkB);((!clientA(pkA, skA, pkB)) | (!serverB(pkB, skB, pkA)))

打开 cmd 执行如下指令：

proverif.exe -graph ./ ./handshake.pv > proof.txt

1. 查看 ./proof.txt 最后的 Verification summary 结果
2. 查看 ./trace1.pdf, ./trace2.pdf 绘制的攻击路径