ProVerif是一款基于 Dolev-Yao 模型的密码协议形式化验证工具。由Bruno Blanchet开发并开源。ProVerif 能够用于处理各种密码学原语，包括对称加密和非对称加密应用（加密和签名）、哈希函数和 Diffie-Hellman 密钥协商等。并且，ProVerif还能够处理无穷多的会话（即使并行）和无穷消息空间，解决了密码协议验证过程中的状态爆炸等问题。
l强保密性（攻击者不仅无法直接获得某消息，并且当值发生变化时，无法看到差异）
2.1 协议建模
ProVerif使用π推演（pi calculus）语言编写，下面详细介绍该语法。
2.1.1 声明
type（定义类型） ：用户可以使用 type 定义自定义类型。如定义密钥类型 key，使用type key即可。
free（自由名称声明）：在一个输入文件中出现的所有自由名称必须使用free进行声明，并且可以通过增加 private 标志来声明该自由名称为秘密的。语法为：free n:t [private]，如声明一个 bitstring类型的自由名称 n，可以通过以下语句实现：free n:bitstring。
fun（构造函数）：构造函数主要用于建立加密协议所使用的建模原语，如：单项哈希函数、加密和数字签名等。构造函数通过 fun 定义。语法为：fun f(t1,…,tn) : t. 如 fun enc(bitstring, key):bitstring 意味着定义一个名为 enc 的构造函数，该函数的输入有两个参数，分别为 bitstring类型和key类型，输出为bitstring类型。
reduc（析构函数）：密码学原语之间的关系是通过析构函数进行捕获的。直接从字面意思看不是很好理解，我们可以结合前面的知识，通过定义一个完整的对称加密协议来理解。
fun senc(bitstring, key): bitstring.
reduc forall m: bitstring, k: key; sdec(senc(m,k),k) = m.
例1首先定义了key类型，代表着对称加密使用的对称密钥。接着定义了构造函数senc，senc接收两个参数，分别是bitstring类型和key类型。其中bitstring类型是ProVerif自带的，所以不需要单独的进行声明，代表着比特串类型。senc的输出也是bitstring类型。最后，和构造函数相对应的析构函数，则是名为 sdec 的解密函数。sdec 和构造函数一样，接收2个参数，类型依次是bitstring类型和key类型。而为了与构造函数相对应，形成闭环。就有了最后的sdec(senc(m,k),k) = m 语句。其中senc(m,k)表示密文。
2.1.2 宏
ProVerif 主要提供了功能宏和进程宏。这里主要讲解进程宏。引入进程宏主要是为了方便开发，考虑到一些复杂的协议不太可能仅通过一个主进程就能完成，所以通过进程宏来声明子进程。具体语法为：let R(x1:t1, x2:t2, …) = P. R 表示宏名称，P 是被定义的子进程。具体的用法会在后续的例子中详细介绍。
2.1.3 安全属性
ProVerif作为能够证明可达性属性、相关性断言和观测等价性。
可达性证明是ProVerif最基础的功能，ProVerif能够用于判别在协议中，哪一项是对攻击者可见的，所以，可达性证明也可用于评估某一项的保密性。在ProVerif中，判断M的保密性，可以通过以下语句实现：query attacker (M ) . 使用了上述语句后，ProVerif 会在协议测试完成后返回相应的结果。
相关性断言可以通过 query event(M) ==> event(M’) 进行判断，其表达的意思是，如果M被执行，那么M’也被执行。
3.1 ProVerif 安装
ProVerif的源码可以通过访问网站 http://proverif.inria.fr/ 进行下载，不过ProVerif 已经针对主流的操作系统如：Linux、Mac和Windows操作系统都已经有了二进制安装包。官方推荐使用OPAM进行安装。OPAM可以通过访问 https://opam.ocaml.org/ 进行安装。在安装了OPAM以后，只需要执行 opam update 即可更新软件源。接着执行下列语句：
opam depext conf-graphviz
3.2 ProVerif 实例
3.2.1 可达性检验
为了测试ProVerif提供的可达性检验功能，请先观察下列代码：
代码第1行是注释语句，ProVerif 的注释语句以 （* 开头，以 *) 结束。在第2行声明了一个公共信道c，公共信道意味着在上面传输的一切信息都是可能被泄露、窃听和篡改的。代码第5-6行分别声明了比特类型的变量 Cocks 和 RSA, 并且都是私有不公开的。第7-8行分别对 RSA 和 Cocks进行了可达性属性的检验。第10行开始，是协议的整个进程过程，由于是示范，该进程只包含第11行一个执行语句，表示通过公共信道c输出RSA。最后用0表示进程的结束。所以在这个demo中，表达的密码协议非常简单，就是在公共信道输出秘密变量RSA. 然后再来看这个协议经过ProVerif检验以后，输出的结果。结果如下：
输出结果中可以清晰的发现，Query not attacker(RSA[]) 的值为 false，也就是说RSA实际上对攻击者是可见的。这是因为尽管对RSA使用了private修饰，但是由于RSA最终通过了公共信道c输出，所以还是会被攻击者获取。而Cocks从始至终都是private，并没有输出。所以Query not attacker(Cocks[]) 是true。
3.2.2 相关性断言
为了测试ProVerif提供的相关性断言检测功能。请观察以下代码：
代码第8-9行分别声明了两个事件，evCocks和evRSA, 并且在第11行给出了断言检验语句，该语句意味着，如果evCocks 已经发生，那么evRSA也在此之前就已经发生。继续往下看，本例中的进程首先在公共信道输出了RSA，接着使用公共信道c接受了参数x，并且如果x = Cocks，那么执行事件 evCocks ，接着执行事件 evRSA。否则，直接执行 evRSA。我们先首先分析一下该进程，不难发现，如果 evCocks 被执行了，说明x=Cocks，那么evRSA 最终也会被执行。再来看最终的ProVerif运行结果，如下图所示:
原文始发于微信公众号（山石网科安全技术研究院）：实例介绍密码协议形式化验证工具ProVerif
