proverif模型工具安装流程

这段代码是一个调用ProVerif可执行文件并运行ProVerif脚本的Python脚本。以下是整理后的代码，包含中文注释：

import subprocess

# ProVerif 可执行文件的路径
proverif_executable_path = "C:\\Users\\GXKL\\Desktop\\proverif2.05\\proverif.exe"

# ProVerif 脚本的路径（更新为您的脚本实际位置）
proverif_script_path = "C:\\Users\\GXKL\\Desktop\\proverif2.05\\test2.pv"

# 调用 ProVerif
result = subprocess.run([proverif_executable_path, proverif_script_path], capture_output=True, text=True)

# 打印 ProVerif 的输出
print(result.stdout)

安装环境

一、proverif 的下载与安装

官网已经更新

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

proverifbin2.05.tar.gz

下载的文件是一个.tar.gz格式，显示为空白文档，这是Linux系统的压缩格式。通过网络查询，我发现多种解压方法。我选择了代码解压，它既快捷又高效。

首先，我打开命令提示符（win+R cmd），导航至含有.tar.gz文件的目录，位于D盘。进入该目录后，我输入命令 tar -zxvf (文件夹名)proverifbin2.02.tar.gz 以解压该文件。接着，用相同方法解压 proverifdoc2.0.tar.gz 文件，此时会生成一个新的文件夹。

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

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

graphciz: http://graphviz.org

graphciz.zip

gtk: ftp://ftp.gnome.org/pub/gnome/binaries/win32/gtk+/2.24/

gtk+-bundle_2.24.10-20120208_win32.zip

（当时在电脑上打不开，在手机上可以打开，再将下载网址发回电脑下载）

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

可以看到successfully loaded即为成功。

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

至此必备的安装完成。

二、test文件的试用

新建一个txt文件，命名test2.pv

构建示例代码

(* ProVerif 脚本示例 *)

(* 通信通道声明 *)
(* 定义了一个公共的通信通道，名为 'c' *)
(* 'free' 相当于公共全局变量的意思，在 ProVerif 里表示这是一个全局都知道的知识，即攻击者也可以获取 *)
free c: channel.

(* 私有数据声明 *)
(* 'bitstring' 是一种数据类型 *)
(* 这两行定义了变量 'Cocks' 和 'RSA' *)
(* 它们是全局的 ('free')，但 '[private]' 限制表示它们不可被攻击者直接获取 *)
free Cocks: bitstring[private].
free RSA: bitstring[private].

(* 安全性查询 *)
(* 对协议性质进行查询 *)
(* 'query attacker(RSA)' 在底层判断命题 "[RSA 不会被攻击者窃取]" 是否成立 *)
query attacker(RSA).
query attacker(Cocks).

(* 进程定义 *)
(* 定义了一个进程 *)
process
    (* 进程内的操作 *)
    (* 通过通道 'c' 发送 'RSA' *)
    out(c, RSA); 0
    (* '0' 是进程结束标志，也可以省略 '0' 和 ';' *)

(* 注：上述脚本中的 'out(c, RSA); 0' 表示在进程中通过公共通道 'c' 发送 'RSA'，
   然后进程结束。这在分析中可能是一个关注点，因为将私有数据发送到公共通道可能存在安全风险。 *)

最后运行

构建结果