---

一、proverif下载

1. 下载proverif安装包

官网：proverif
首先下载全过程无需开外网，而且安装包下载和安装都很快，半小时内可以完成。
进入官网，看到downloads的标题下面有一个download for windows,直接下载。

下载之后是一个.tar.gz的文件,将该文件放入D盘（D盘新建一个文件夹，命名为proverif，将.tar.gz安装包放入文件夹内），我们用代码方式进行解压。

2. 解压proverif安装包

进入cmd命令行，按一下步骤逐次输入命令行，完成解压。

1. 进入proverif的文件夹cd /d D:\proverif2. 解压安装包tar -zxvf proverif2.04.tar.gz

解压完成后，proverif文件夹就会出现一个名为proverif2.04的文件。

3. 点开其中的README，安装graphciz和gtk

README中表示还要安装两个包，下面是他们的地址，两个文件均下载到proverif文件夹中：

graphciz:https://www.graphviz.org/download/
GTK：download

graphciz的安装按照自己电脑位数来选择，我选择了64位。

---

GTK安装是按照README中指定的文件下载：

下载完之后是一个压缩包：gtk+-bundle_2.24.10-20120208_win32.zip，解压到proverif文件中，将解压文件改名为GTK。

配置路径：控制面板-》系统-》高级系统设置-》环境变量，然后设置如图：

至此，GTK安装和环境配置结束。

4. 查看安装是否成功

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

dot -version

可以看到successfully loaded即为成功。

5. 测试

在proverif文件中新建一个txt文件，编写下面代码：

free c:channel.free Cocks:bitstring[private].
free RSA:bitstring[private].query attacker(RSA).
query attacker(Cocks).processout(c,RSA);0

然后将txt文件后缀改成.pv，在cmd中进入proverif文件，并执行语句：

proverif test1.pv

若出现该图的情况，是因为后缀没有改成功：

Win11的后缀修改方式：打开此电脑——查看更多——选项——查看——隐藏已知文件类型扩展名。然后在txt文件重命名中，将.txt改成.pv。

若出现该页面时，证明安装成功：

该段代码的解释：

第1行用(*和*)括起来的是注释。

第3行定义了一个通信通道，通道的名字是c，这里的free类似于编程语言中的全局变量，在ProVerif里这表示这是一个全局都知道的知识，即攻击者也可以获取，具体到这一行说明通道c是公共的。

第5行和第6行定义了bitstring类型的变量Cocks和RSA，它们都是free的，但是用[private]限制了它们无法被攻击者获取到。

第11行定义了一个进程，第12行是这个进程内的一条语句，表示通过通道c将RSA发送出去，第13行的0是进程结束标志（也可以不写这个0和最后一个;）。

第8行和第9行定义了对性质的查询，需要注意，如query attacker (RSA)在底层实际查询的是【not attacker (RSA)】，即要判断命题【RSA不会被攻击者窃取】是否是成立的。

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

参考博客：

1. https://blog.csdn.net/SHU15121856/article/details/107927165

2. https://blog.csdn.net/weixin_43863334/article/details/110006348