Proverif工具的安装_环境中输入dot version是什么

@作者邮箱：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) in
	new 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))	) in
	let 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) in
	new 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))	) in
	let 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) in
	let A1 = Add(alphaA,Mult(betaA,A0)) in
	let MA = Mult(Mult(DA,Powzn(g,sA)),Powzn(g2,Negative(alphaA))) in
	let NA = dA in
	let ZA = Powzn(g2,betaA) in 
	let CA = Mult(Powzn(g,Negative(sA)),Powzn(g2,Negative(betaA))) in
	out(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) in
	if(verifyResultA = Tpub) then
	let SK = H3(WA,WB,ZA,ZB,Powzn(ZB,betaA)) in
	event 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) in
	if(verifyResultB = Tpub) then
	new alphaB:element;
	new betaB:element;
	new sB:element;
	new TB:bitstring;
	let B0 = H1(WB,TB) in
	let B1 = Add(alphaB,Mult(betaB,B0)) in
	let MB = Mult(Mult(DB,Powzn(g,sB)),Powzn(g2,Negative(alphaB))) in
	let NB = dB in
	let ZB = Powzn(g2,betaB) in 
	let CB = Mult(Powzn(g,Negative(sB)),Powzn(g2,Negative(betaB))) in

	let sessionKey' = H3(WA,WB,ZA,ZB,Powzn(ZA,betaB)) in
	out(Pub,(WB,B1,MB,NB,CB,ZB,TB));
	event endVehicleB(WB)
	else 0.

(*Processes Replication*)
process 
(!VehicleA | !VehicleB | !KGC)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159

3、Win+R 打开cmd窗口，输入cd D:\proverifbin2.04\proverif2.04切换到Proverif文件目录下，输入Proverif test.pv.

如果输出这些内容，到这里就已经成功安装Proverif工具了！！！！

官方文档：

Proverif手册，提取码：0m9j

参考链接：

[1]https://blog.csdn.net/weixin_43863334/article/details/110006348?
[2]https://blog.csdn.net/IYLlove/article/details/123336598