Introduction

ProVerif是一款基于 Dolev-Yao 模型的密码协议形式化验证工具。由Bruno Blanchet开发并开源。ProVerif 能够用于处理各种密码学原语，包括对称加密和非对称加密应用（加密和签名）、哈希函数和 Diffie-Hellman 密钥协商等。并且，ProVerif还能够处理无穷多的会话（即使并行）和无穷消息空间，解决了密码协议验证过程中的状态爆炸等问题。

ProVerif能够证明以下属性：

  • 机密性（即攻击者无法获得某消息）
  • 认证性和相对于的更加普遍的属性
  • 强保密性（攻击者不仅无法直接获得某消息，并且当值发生变化时，无法看到差异）

Installation

ProVerif的源码可以通过访问网站 http://proverif.inria.fr/ 进行下载，不过 ProVerif 已经针对主流的操作系统如：Linux、Mac 和 Windows 操作系统都已经有了二进制安装包。官方推荐使用 OPAM 进行安装。OPAM可以通过访问 https://opam.ocaml.org/ 进行安装。在安装了 OPAM 以后，只需要执行 opam update 即可更新软件源。接着执行下列语句：

opam depext conf-graphviz

opam depext proverif

opam install proverif

即可完成 ProVerif 的安装。

Reference

  1. https://mp.weixin.qq.com/s/NRrwfTt8BCd9DfgzoD6QFg - 实例介绍密码协议形式化验证工具ProVerif