Proverif工具的安装

本文主要是介绍Proverif工具的安装，希望对大家解决编程问题提供一定的参考价值，需要的开发者们随着小编来一起学习吧！

@作者邮箱：caolei2000@snnu.edu.cn

密码学中协议形式化验证工具Proverif的安装与使用

首先准备依赖项和验证工具
1、Graphciz：是一款开源图形可视化软件。图形可视化是一种将结构信息表示为抽象图形和网络图的方法。它在网络、生物信息学、软件工程、数据库和网页设计、机器学习以及其他技术领域的可视化界面中有着重要的应用。
2、GTK：是为运行交互式仿真器证明协议。
3、Proverif：形式模型（即 Dolev-Yao 模型）中的自动加密协议验证器。

Graphciz的安装

下载地址：https://graphviz.org/download/

1、点击左侧项目栏中的Download —> 下翻找到Windows下载项 —> 选择最新版本graphviz-version (64-bit) EXE installer [sha256]

在这里插入图片描述

2、点击安装，途中选择为所有用户添加Path环境变量

在这里插入图片描述

3、检查是否安装成功

打开Cmd窗口，输入dot -version，如果出现以下内容，则表明安装成功。
在这里插入图片描述

安装GTK

下载地址：https://download.gnome.org/binaries/win32/gtk+/2.8/

1、下载解压到本地

点击gtk±2.8.10.zip下载
在这里插入图片描述

2、添加环境变量

右击此电脑—>属性—>高级系统设置—>环境变量—>在系统变量里找到Path双击—>新建—>将解压后的gtk\bin目录添加进去—>保存
在这里插入图片描述

安装Proverif工具

下载地址：https://bblanche.gitlabpages.inria.fr/proverif/
1、在Download中找到binary package ProVerif version 2.04, for Windows，点击下载并解压到本地。
2、准备一个测试用例：在 D:\proverifbin2.04\proverif2.04下新建一个test.txt文件，将以下代码（根据协议内容由Proverif语言编写）复制到文本文件中，修改文件后缀为.pv。

type element. (*element in finite field or group*)
type attribute.
free Sec:channel [private].		(*secure channel*)
free Pub:channel.			(*public channel*)(*-------Names & Variables-------*)
(*elements of cyclic group*)
const g:element.
const g2:element.(*1 . master public key*)
free Tpub:element.(*2. VehicleA & attributes & Each vehicle identity contains four attributes *)
free WA:bitstring.
free deltaA1:attribute.
free deltaA2:attribute.
free deltaA3:attribute.(*3. VehicleB & attributes*)
free WB:bitstring.
free deltaB1:attribute.
free deltaB2:attribute.
free deltaB3:attribute.(*4. master secret key*)
free y:element [private].(*5. vehicles' private key*)
free DA:element [private].
free dA:element [private].
free DB:element [private].
free dB:element [private].(*6. session key*)
free sessionKey:bitstring [private].
free sessionKey':bitstring [private].(*-------Constructors, Destructors & Equations------*)
fun identityCompose(attribute,attribute,attribute):bitstring.
fun H1(bitstring,bitstring):element.
fun H3(bitstring,bitstring,element,element,element):bitstring.fun concat(element,element,element):element.
fun pairing(element,element):element.  (*Pairing operation:e(g,g)*)
fun Mult(element,element):element.  (*Multiplication in group: G×G*)
fun Add(element,element):element.	 (*Addition*)
fun Powzn(element,element):element. 	(*g^s:Powzn(g,s)*)
fun T(attribute):element.
fun Attrcheck(bitstring,element,element,element,element,element,bitstring):element.
fun q1(attribute):element.
fun q2(attribute):element.
fun Negative(element):element.
equation forall a:element; Negative(Negative(a))=a.
(*Event*)
event beginVehicleA(bitstring).
event endVehicleA(bitstring).
event beginVehicleB(bitstring).
event endVehicleB(bitstring).(*Queries*)
query attacker(sessionKey).
query attacker(sessionKey').
query id:bitstring; inj-event (endVehicleA(id)) ==> inj-event(beginVehicleA(id)).
query id:bitstring; inj-event (endVehicleB(id)) ==> inj-event(beginVehicleB(id)).(*Processes*)
(*KGC Processes*)
let VehicleAReg=in(Sec,(deltaA1:attribute,deltaA2:attribute,deltaA3:attribute));let WA = identityCompose(deltaA1,deltaA2,deltaA3) innew rA1:element;new rA2:element;new rA3:element;let DA = concat(	Mult(Powzn(g2,q1(deltaA1)),Powzn(T(deltaA1),rA1)),Mult(Powzn(g2,q1(deltaA2)),Powzn(T(deltaA2),rA2)),Mult(Powzn(g2,q1(deltaA2)),Powzn(T(deltaA2),rA2))	) inlet dA = concat(	Powzn(g,Negative(rA1)),Powzn(g,Negative(rA1)),Powzn(g,Negative(rA1))	) in out(Sec,(WA,DA,dA));0.let VehicleBReg=in(Sec,(deltaB1:attribute,deltaB2:attribute,deltaB3:attribute));let WB = identityCompose(deltaB1,deltaB2,deltaB3) innew rB1:element;new rB2:element;new rB3:element;let DB = concat(	Mult(Powzn(g2,q2(deltaB1)),Powzn(T(deltaB1),rB1)),Mult(Powzn(g2,q2(deltaB2)),Powzn(T(deltaB2),rB2)),Mult(Powzn(g2,q2(deltaB2)),Powzn(T(deltaB2),rB2))	) inlet dB = concat(	Powzn(g,Negative(rB1)),Powzn(g,Negative(rB1)),Powzn(g,Negative(rB1))	) in out(Sec,(WB,DB,dB));0.
let KGC=VehicleAReg | VehicleBReg.(*VehicleA Processes*)
let VehicleA=(*Registration*)out(Sec,(deltaA1,deltaA2,deltaA3));in(Sec,(WA:bitstring,DA:element,dA:element));(*Login & Authentication*)event beginVehicleA(WA);new alphaA:element;new betaA:element;new sA:element;new TA:bitstring;let A0 = H1(WA,TA) inlet A1 = Add(alphaA,Mult(betaA,A0)) inlet MA = Mult(Mult(DA,Powzn(g,sA)),Powzn(g2,Negative(alphaA))) inlet NA = dA inlet ZA = Powzn(g2,betaA) in let CA = Mult(Powzn(g,Negative(sA)),Powzn(g2,Negative(betaA))) inout(Pub,(WA,A1,MA,NA,CA,ZA,TA));in(Pub,(WB:bitstring,B1:element,MB:element,NB:element,CB:element,ZB:element,TB:bitstring));let verifyResultA = Attrcheck(WB,B1,MB,NB,CB,ZB,TB) inif(verifyResultA = Tpub) thenlet SK = H3(WA,WB,ZA,ZB,Powzn(ZB,betaA)) inevent endVehicleA(WA)else 0.
(*VehicleB Processes*)
let VehicleB=(*Registration*)out(Sec,(deltaB1,deltaB2,deltaB3));in(Sec,(WB:bitstring,DB:element,dB:element));(*login & Authentication*)event beginVehicleB(WB);in(Pub,(WA:bitstring,A1:element,MA:element,NA:element,CA:element,ZA:element,TA:bitstring));let verifyResultB = Attrcheck(WA,A1,MA,NA,CA,ZA,TA) inif(verifyResultB = Tpub) thennew alphaB:element;new betaB:element;new sB:element;new TB:bitstring;let B0 = H1(WB,TB) inlet B1 = Add(alphaB,Mult(betaB,B0)) inlet MB = Mult(Mult(DB,Powzn(g,sB)),Powzn(g2,Negative(alphaB))) inlet NB = dB inlet ZB = Powzn(g2,betaB) in let CB = Mult(Powzn(g,Negative(sB)),Powzn(g2,Negative(betaB))) inlet sessionKey' = H3(WA,WB,ZA,ZB,Powzn(ZA,betaB)) inout(Pub,(WB,B1,MB,NB,CB,ZB,TB));event endVehicleB(WB)else 0.(*Processes Replication*)
process 
(!VehicleA | !VehicleB | !KGC)