形式化工具 Proverif 2.0 的使用

一、简介

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

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

第六章 高级特点


Comments are closed.