形式化工具 Proverif 2.0 的使用

calendar Aug 25, 2019 · 3 分钟 阅读 · cryptography

一、简介

安全协议已广泛地应用到身份认证、接入控制、密钥分配、电子商务等多个领域，其安全性的需求也越来越迫切。自安全协议出现以来，人们一直对它进行分析设计研究。但由于安全协议总是运行在复杂的、不安全的网络环境中，许多攻击方法产
生的错误用人工检测很难识别，从而保证对协议安全性分析的准确性。

ProVerif 是 Bruno Blanchet 开发的基于Dolev-Yao模型的形式化自动验证密码学协议工具，是用 Prolog 语言实现的系统。它能够描述各种密码学原语，包括：共享密钥密码学和公钥密钥密码学 (加密和数字签名)，Hash 函数和 Deffie-Hellman密钥交换协议，并指定了重写规则和方程式， 输入语言为应用 PI 演算或 Horn 字句。

ProVerif能处理一个无穷会话并发协议和无穷消息空间，克服了状态空间爆炸的问题。应用 ProVerif 工具验证密码协议时，如果协议有漏洞，此工具会给出一个相应的攻击序列。

其主要特点是：

  • 它可以处理许多不同的密码原语，包括共享密钥和公用密钥密码术（加密和签名），哈希函数和Diffie-Hellman密钥协议，这些协议既指定为重写规则，也指定为等式。
  • 它可以处理无限制数量的协议会话（即使是并行的）和无限制的消息空间。由于一些精心选择的近似值，因此获得了该结果。这意味着验证者可以发出错误的攻击，但是如果声称协议满足某些属性，则实际上满足该属性。所考虑的解析算法终止于一大类协议（所谓的“标记”协议）。当工具无法证明属性时，它会尝试重建攻击，即伪造所需属性的协议执行跟踪。

ProVerif可以证明以下属性：

  • 保密（对手无法获得秘密）
  • 身份验证以及更一般的对应属性
  • 高度机密性（机密值更改时，对手看不到差异）
  • 仅术语不同的过程之间的等价关系

二、ProVerif2.0（程序及文档） 下载：

 http://prosecco.gforge.inria.fr/personal/bblanche/proverif/

备用下载地址

三、编辑工具

推荐 Sublime 3

3.1 可以自行设置 pv 文件语法高亮，具体设置：

Pv.tmLanguage

3.2 可以将 proverif 设置为默认 Builder System：

先添加环境变量，再创建 Proverif.sublime-build文件，内容如下:

{
"cmd": ["proverif", "$file"],
"file_regex": "pv$",
"selector": "source.pv"
}

三、简单使用

1、打开 sublime 3，输入以下内容并保存为：test.pv

2、从 命令行 进入 proverif 源代码文件夹

推荐使用 git软件，安装好后可以从命令行快速进入某一个文件夹： Git Bash Here

输入

proverif 文件名

四、语法

1.声明（declaration）

1.1 声明变量
格式：type t.
例子：free n:t. 表示n的类型是t，free是关键词，表示公开的，是可以被攻击者获取的。
如果不想被攻击者获取，则需要声明为私密的，关键词为private，格式如下：
free n:t [private].

1.2 声明函数
格式：fun f(t1,…,tn):t.
解释：f是关于n的函数构造器，t是该函数f的返回值类型，t1…tn是函数f的自变量。
例子1：fun f(t1,…,tn):t [private]. 表示攻击者无法获取由函数f生成的t。
例子2：fun senc(bitstring, key):bitstring. 表示用类型key加密bitstring类型明文，生成的密文是bitstring类型值。

1.3 析构函数
格式：
reduc forall x1,1 : t1,1,…,x1,n1 : t1,n1; g(M1,1,…,M1,k)=M1,0;
…
forall xm,1 : tm,1,…,xm,nm : tm,nm; g(Mm,1,…,Mm,k)=Mm,0.
作用：将密码学原语中的关系连接起来。
例子：reduc forall m : bitstring, k : key; sedc(senc(m,k),k) = m.
m表示明文；k表示系统密钥；senc(m,k)用密钥k加密明文m生成密文；sedc(senc(m,k),k)=m用密钥k解密密文senc(m,k)生成明文m。

1.4 子进程
格式：let R(x1 : t1,…,xn : tn) = P.
R是宏（macros）的名字，P是定义的子进程，t1,…,tn类型x1,…,xn。

1.5 主进程
格式：process A
process是关键字，相当于编程语言中的main()函数。

1.6 术语语法
假设M和N都是多项式表达式；
格式：**M = N **表示M和N相等；M<>N表示M和N不相等。
等式和不等式都是一个等式理论的模，它们接受相同类型的两个参数，并返回bool类型的结果。
格式：M&&N表示M和N是布尔连接的；M || N表示M和N是非布尔连接即布尔断开。
格式：**not(M)**表示布尔否定。
例子：M || N，如果M是真的，那么N不需要计算，这个表达式的结果是真的。

1.7 进程语法

假设P和Q都是进程；
格式：P | Q表示进程P和Q是并行组成的；!P表示P | P | …,表示进程P有无限个。
格式：new n : t; P表示在进程P中绑定类型为t的n，相当于编程语言中在类中（或函数）设置新的局部变量。
格式：in(M, x : t); P表示等待来自通道M的类型为t的消息，然后表现为P，其中接收的消息绑定到变量x，P中每次出现x都是指收到的消息，当P为0时，P可以省略不写。
格式：out(M, N); P表示在通道M发送N，然后运行进程P，当P为0时，P可以省略不写。
格式：if M then P else Q表示当M的值为真时，运行进程P；当M的值为其他值时，运行进程Q。当术语M失败时它不执行任何操作（例如，当M包含不适用重写规则的析构函数时）。
例子1：if M=N then P else Q表示如果M=N，执行P，或者执行Q
例子2：if x=M then P else Q表示如果对于M中的所有析构函数没有失败，那么x被绑定到M中，并执行P，否则执行Q。

1.8 模式匹配语法


格式：x : t表示将类型t的任何术语绑定到x。
格式：M = N表示相等测试。

1.9 关键词、注释和标识符
关键词：among, channel, choice, clauses, const, def, elimtrue, else, equation, equivalence, event, expand, fail, forall, free, fun, get, if, in, inj-event, insert, let, letfun, new, noninterf, not, nounif, or, otherwise, out, param, phase, pred, proba, process, proof, putbegin, query, reduc, set, suchthat, table, then, type, weaksecret, yield。
注释：用英文括号加星号组成，将星号放在括号内；
标识符：包括字母、数字、单引号、下划线等，第一个字符是字母，区分大小写，关键词不可做标识符。
内置类型：bitsring, bool。bool类型分为true和false。

重要知识点：

事件执行查询：
Event:
为了用 Correspondence assertions (对应断言)进行推理，我们用 Event 注释过程，这些 Event 标记了协议所达到的重要阶段且不会影响协议流程。

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

if  x = Cocks  then  //evCocks先执行，evRSA 后执行，query event...==>... 为 false
    event evCocks; 
    event evRSA
else  //evRSA 先执行，evCocks后执行，uery event...==>... 为 true
    event evRSA

含义：

对于协议的所有执行，事件  evRSA  先于事件  evCocks  执行，则此 query 才为真

query x1 : t1 , . . . , xn : tn ; inj−event (e(M1 , . . . , Mj )) ==> inj−event (e'(N1 , . . . , Nk ) )

含义：
在需要每个参与者执行的协议运行次数之间一一对应的情况下，event 的对应关系定义不足以完全捕获身份验证。
例如，考虑一个金融交易，其中服务器请求客户付款； 服务器应仅对客户端启动的每个事务完成一次事务。 （如果不是这种情况，则即使客户仅启动了一笔交易，也可能需要向客户收取几笔交易的费用。）
inj-event 关系断言捕获一对一关系，对于事件e（M1，...，Mj）的每次出现，事件e'（N1，...，Nk）的出现都较早。e'（N1，...，Nk）的出现次数大于或等于e（M1，...，Mj）的出现次数。请注意，在箭头==>之前使用inj-event或event不会更改查询的含义，在箭头后才重要。

关联事件的关系

简单 handshake:
A → B : pk(skA)
B → A : aenc(sign((pk(skB),k),skB),pk(skA))
A → B : senc(s,k)

handshake.pv文件内容如下:

(*=================== sym ===========================*)
type key.

fun senc(bitstring, key): bitstring.
reduc forall m:bitstring, k:key; sdec(senc(m, k), k) = m.

(*=================== asym ===========================*)
type skey.
type pkey.

fun pk(skey): pkey.
fun aenc(bitstring, pkey): bitstring.
reduc forall m:bitstring, sk:skey; adec(aenc(m, pk(sk)), sk) = m.

(*=================== sign ===========================*)
type sskey.
type spkey.

fun spk(sskey): spkey.
fun sign(bitstring, sskey): bitstring.
reduc forall m:bitstring, ssk:sskey; checksign(sign(m, ssk), spk(ssk)) = m.
reduc forall m:bitstring, ssk:sskey; getmess(sign(m, ssk)) = m.

(*==============================================*)

free c : channel .

free s: bitstring [private].
query attacker(s).

客户端A使用acceptsClient(key)来记录信任关系，
即客户端A已接受使用服务器B和提供的对称密钥key来运行协议。
event acceptsClient(key).

用于记录服务器B认为他已接受与客户端A一起运行协议的事实，
并以提议的密钥key作为第一个参数，客户的公钥pkey为第二个参数。
event acceptsServer(key, pkey).

表示客户端A认为她已终止运行协议，第一个参数key提供对称密钥，
第二个参数是由客户端提供的公钥pkey。
event termClient(key, pkey).

表示服务器B认为其已经终止了与客户端A一起运行的协议，
并以第一个参数key作为对称密钥
event termServer(key).

query x:key, y:pkey; event(termClient(x, y)) ==> event(acceptsServer(x, y)).
query x:key; inj-event(termServer(x)) ==> inj-event(acceptsClient(x)).

let clientA(pkA: pkey, skA: skey, pkB: spkey) =
    in(c, x:bitstring);
    let y = adec(x, skA) in
    let (=pkB, k:key) = checksign(y, pkB) in
    event acceptsClient(k);
    out(c, senc(s, k));
    event termClient(k, pkA).

let serverB(pkB: spkey, skB: sskey, pkA: pkey) =
    in(c, pkX:pkey);
    new k:key;
    event acceptsServer(k, pkX);
    out(c, aenc(sign((pkB, k), skB), pkX));
    in(c, x:bitstring);
    let z = sdec(x, k) in
    if pkX = pkA then
    event termServer(k).

process
    new skA: skey;
    new skB: sskey;
    let pkA = pk(skA) in out(c, pkA);
    let pkB = spk(skB) in out(c, pkB);
    ((!clientA(pkA, skA, pkB)) | (!serverB(pkB, skB, pkA))  )

在服务器终止时（通常在协议末尾）放置事件 termServer，而acceptsClient则在客户端接受时放置（通常在客户端发送其最后一条消息之前）。
因此，当最后一条消息（消息n）是从客户端到服务器的事件时，客户端发送的最后一条消息是消息n，因此acceptsClient放在客户端发送消息n和termServer之前在服务器收到消息n之后放置。

服务器发送的最后一条消息是消息n-1，因此acceptsServer放置在服务器发送消息n-1之前，而termClient放置在客户端接收消息n-1之后（该接收之后的任意位置都是正确的）。

更一般地，在箭头==>之前发生的事件可以放在协议的末尾，但是在箭头==>之后发生的事件必须后面至少输出一条消息。否则，可以在不执行后一个事件的情况下执行整个协议，因此对应关系当然不成立。

还可以注意到，将发生在箭头==>之前发生的事件移到协议的开头会增强对应性，而将发生在箭头==>之后的事件发生向协议的结尾也将增强对应性

2、手册 **manual.pdf **学习

第二章 入门

hello.pv 内容同 test.pv

第三章 使用

第四章 语言特征

第五章 Needham-Schroeder public key protocol

第六章 高级特点