proverif软件的下载与安装

一、proverif 的下载与安装

先哭诉下，这个软件的安装可是太不容易了，官 都成这个熊样子了，我以为这里没有安装包了呢，于是全 寻安装包未得又回来看了一眼，妈呀，这杂乱的几乎不知道东西南北的 页里竟然有下载地址。 

页链接： http://prosecco.gforge.inria.fr/personal/bblanche/proverif/(可下载)

下载后是个.tar.gz的文件，在我的电脑（win10系统）上显示是一个空白的文档，上 查看之后发现这是linux系统中的压缩软件，有很多种解压方式，我选择了最省时省力的方式——代码解压。

首先进入任务管理模式（win+R  cmd），进入下载.tar.gz的文件夹，我放在了D盘，先进入D盘，然后进入文件夹。输入tar -zxvf (文件夹名)proverifbin2.02.tar.gz，然后再将proverifdoc2.0.tar.gz用同样的方式解压，就会出现一个文件夹。

点开其中的使用手册，发现还需要下载graphciz和gtk，在使用手册上的安装地址就可以。

graphciz的作用是绘制代表ProVerif发现的攻击的图表。gtk是为运行交互式仿真器证明协议。

graphciz:http://graphviz.org

gtk:ftp://ftp.gnome.org/pub/gnome/binaries/win32/gtk+/2.24/（当时在电脑上打不开，在手机上可以打开，再将下载 址发回电脑下载）

graphciz下载后直接安装即可，安装后在任务管理器中查看是否安装成功。

可以看到successfully loaded即为成功。

gtk下载后直接解压就可以了，但是需要配置环境变量。将解压后的文件夹中的GTKbin文件加入到PATH路径中即可。

至此必备的安装完成。

二、test文件的试用

安装完成后写一个简单的小程序测试下安装是否成功。test.txt文档，左边是文档内容，右边是解释。

然后更改文档的后缀，更改为.pv文件。和解压缩一样，仍然是需要代码行来运行。首先切换到proverif.exe所在的文件夹，然后输入proverif test1.pv(文件名)。

最开始的只是添加的一个语句标 ，没有什么特殊意义，仅仅是因为后面会提到这个位置。每个后面跟的是一个查询的结果，对于RSA因为没能通过验证，下会去说明导致攻击的原因（攻击者是如何实施攻击来破坏这个性质的），还给了一个简短的反例trace，即：

从最下面的Verification summary中也可以看到，的验证结果是，也就是会被攻击（因为它被通过公有通道发送出去了），而不会被攻击。