【ProVerif学习笔记】1：基本使用流程

1 简介

ProVerif可以用来自动分析密码协议的Security性质，功能涵盖对称和非对称加密、数字签名、哈希函数、比特承诺、非交互式零知识证明。ProVerif可以证明可达性(reachability)，对应断言(correspondence assertion)，和可观察的等价性(observational equivalence)。这个能力使得它能对计算机安全领域中的机密性和认证性质进行分析，也可以考虑一些新兴的性质，如隐私性(privacy)、可追溯性(traceability)、可验证性(verifiability)。它还具有攻击重构的功能，如果某个性质不能被证明，ProVerif就会尝试构造一个反例trace。

2 安装

Windows上可以直接下载一个绿色版的二进制包，解压就能用了。然后为了显示ProVerif给出的攻击，还要安装GraphViz，并且把它的bin目录加到PATH里。

如果要用交互式的模拟程序，要下载GTK+2.24（里面第一个）,然后解压放到C:\GTK，再把里面的bin目录加到PATH里。

3 命令行操作

ProVerif的命令行操作总是以这样的格式出现：
$$./proverif[options]⟨filename⟩$$

实际上它能处理多种语言的输入文件（原手册里将这种把协议用这些语言描述成文件的过程叫protocol encode），最常见的一种是.pv文件，这是类型$\pi$演算(typed pi calculus)的文件。$\pi$演算是为了表达并发过程用通信信道通信而设计的。

4 有关Reachability的例子

书写文件simple-reach.pv，如下：

(* simple-reach.pv: 学习最简单的可达性质 *)

free c:channel.

free Cocks:bitstring [private].
free RSA:bitstring[private].

query attacker (RSA).
query attacker (Cocks).

process
  out(c, RSA);
  0
1
2
3
4
5
6
7
8
9
10
11
12
13

第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不会被攻击者窃取】是否是成立的。

运行命令proverif simple-reach.pv，结果如下：

Process 0 (that is, the initial process):
{1}out(c, RSA)

-- Query not attacker(RSA[]) in process 0.
Translating the process into Horn clauses...
Completing...
Starting query not attacker(RSA[])
goal reachable: attacker(RSA[])

Derivation:

1. The message RSA[] may be sent to the attacker at output {1}.
attacker(RSA[]).

2. By 1, attacker(RSA[]).
The goal is reached, represented in the following fact:
attacker(RSA[]).


A more detailed output of the traces is available with
  set traceDisplay = long.

out(c, ~M) with ~M = RSA at {1}

The attacker has the message ~M = RSA.
A trace has been found.
RESULT not attacker(RSA[]) is false.
-- Query not attacker(Cocks[]) in process 0.
Translating the process into Horn clauses...
Completing...
Starting query not attacker(Cocks[])
RESULT not attacker(Cocks[]) is true.

--------------------------------------------------------------
Verification summary:

Query not attacker(RSA[]) is false.

Query not attacker(Cocks[]) is true.

--------------------------------------------------------------
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

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

out(c, ~M) with ~M = RSA at {1}

The attacker has the message ~M = RSA.
1
2
3

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

5 有关Correspondence Assertion的例子

这个性质的含义在谷歌上搜的结果如下，大意就是如果通信协议的某个点执行过，那么另一个点一定也在某个时间执行过。

Correspondence assertions: To a first approximation, a correspondence assertion about a communication protocol is an intention that follows the pattern: If one principal ever reaches a certain point in a protocol, then some other principal has previously reached some other matching point in the protocol.

例子文件hello_ext.pv如下：

(* hello_ext.pv: Hello Extended World Script *)

free c:channel.

free Cocks:bitstring [private].
free RSA:bitstring [private].

event evCocks.
event evRSA.

query event(evCocks) ==> event(evRSA).

process
	out(c,RSA);
	in(c,x:bitstring);
	if x = Cocks then
		event evCocks;
		event evRSA
	else
		event evRSA
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20

第8第9行用event关键字定义了两个事件。

第13行定义了一个进程，第14行是通过通道c将RSA发送出去，第15行是通过通道c接受一个数据，放在bitstring类型的变量x中，第16行判断x是否是Cocks，如果是就依次执行刚刚定义的两个event，否则只执行后一个。

第11行定义了一个查询，意思是如果事件evCocks发生了，那么事件evRSA一定发生。

运行命令proverif hello_ext.pv，结果如下：

Process 0 (that is, the initial process):
{1}out(c, RSA);
{2}in(c, x: bitstring);
{3}if (x = Cocks) then
    {4}event evCocks;
    {5}event evRSA
else
    {6}event evRSA

-- Query event(evCocks) ==> event(evRSA) in process 0.
Translating the process into Horn clauses...
Completing...
Starting query event(evCocks) ==> event(evRSA)
RESULT event(evCocks) ==> event(evRSA) is true.

--------------------------------------------------------------
Verification summary:

Query event(evCocks) ==> event(evRSA) is true.

--------------------------------------------------------------
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21

从结果中可以看到这个验证是通过了的，即执行了事件evCocks就一定执行了事件evRSA。实际上在这个例子里evCocks肯定没有执行，可以尝试验证query event(evCocks).，结果（是反过来证not）：

Query not event(evCocks) is true.
1

参考阅读

ProVerif的manual第1~2章节