系列文章目录

1. 【proverif】proverif的下载安装和初使用
2. 【proverif】proverif的语法（本文）

---

---

前言：proverif-密码学领域中的客观第三方评价工具

在密码学领域，"客观、第三方"评价指标通常指的是对密码学方案、协议或算法进行评估和验证时所采用的一种方法或标准。这种评价方法侧重于通过独立、客观的标准和工具对密码学系统进行评估，以确保其安全性、可靠性和功能性。一般包括：数学证明和分析、安全模型的定义和评估、标准化和认证机构的测试等。

1. 数学证明和分析： 对密码学方案的安全性进行数学证明是一种常见的方法。这确保了方案的安全性不依赖于假设，而是基于严格的数学原理。

2. 安全模型的定义和评估： 通过定义具体的安全模型，并在此基础上评估密码学方案，可以提供一种客观的方式来衡量其安全性。

3. 公开评审和审查： 将密码学方案、协议或算法提交给公开的审查或评审，让来自领域内外的专家进行独立的审查，以确保系统的可靠性和安全性。

4. 标准化和认证机构的测试： 一些密码学方案可能会通过国际标准化组织或认证机构的测试来验证其符合特定的安全标准和规范。

这些方法旨在确保密码学系统经过了全面的审查和评估，不仅仅依赖于设计者的声称或内部测试。这样的方法有助于增强密码学系统的安全性和可信度，从而提供更可靠的安全保障。

ProVerif是一种用于验证协议安全性的工具，它可以被视为密码学领域中的第三方评价工具。ProVerif 主要用于形式化方法，特别是验证协议的形式化安全性。使用 ProVerif，你可以创建协议的形式模型，然后通过自动分析来检查该协议是否满足一些安全性属性。
proverif之所以能成为第三方评价工具，主要考虑一下几点：

1. 独立性： ProVerif 是一个独立的工具，它不是由协议设计者开发的，因此具有独立性。

2. 客观性： ProVerif 提供了一种基于数学原理的形式化方法，这使得评价相对客观，因为它依赖于严格的数学推理。

3. 自动化： ProVerif 是自动化的，这意味着可以通过计算机程序进行协议的验证，而不仅仅是依赖于人工审查。

---

一、从官网学正规语法

学一门语言最好的方法是查看官方文档。访问 ProVerif 的官方网站，查看官方文档和用户手册。官方文档通常提供了详细的语法说明、示例和使用指南。
首先进入proverif官网：https://bblanche.gitlabpages.inria.fr/proverif/
在Downloads章节中找到用户手册：User manual，点击下载（用户手册共160页）

从用户手册第三章开始，认真学习语法内容。

二、细看用户手册

语法分为四部分：声明形式的加密原语；声明握手协议的加密原语；声明宏定义；将协议编程为主进程。接下来我尽量通过注释形式展示代码和解释之间的关联性。

1. 声明形式的加密原语

使用（* *）对内容进行注释。
语言是强类型的，用户定义的类型声明如下（示例）：

(*输入文件中出现的所有自由名称都必须使用该语法声明*)
type t.

(*其中n是名称，t是类型。可以声明相同类型t的多个自由名*)
type n:t.
(**同时声明多个相同类型的自由名)
type n1,...,nk:t
例如：
(*bitstring类型的变量RSA*)
free RSA:bitstring.
free Cocks,RSA:bitstring.

2. 握手协议-中间人攻击的解决方案

原始协议中，A通过非对称加密将自己公钥告知B（公钥生成算法是pk（），通过输入A私钥生成A公钥）。B用同样方式生成自己的公私钥对，并用B私钥进行签名sign，签名内容包括（B公钥、只有A和B知道的秘密值k），并用A公钥加密信息发送给A。A收到信息后用A私钥解密得到签名sign，然后用B公钥验证签名。接着使用秘密值k加密内容s发送给B。

但该协议容易遭到中间人攻击：

解决办法是：签名中加入A的公钥，便于收到此消息的客户端确认确实是发给自己的。

相关知识点的代码如下：

(*语法channel c是free c: channel的同义词。默认情况下，攻击者知道自由名称。*)
(*攻击者不知道的自由名称必须声明为private*)
free n : t [ private ] .

例如：c是一个通道channel类型，free代表全局类型，所有人都知道，包括敌手。
free c:channel.

(*构造函数(函数符号)用于构建加密协议使用的术语建模原语;例如:单向哈希函数、加密、数字签名等。*)
fun f(t1, . . . , tn) : t.

例如：对称加密中senc函数输入的参数是两个，一个bitstring类型,一个key类型，输出的参数是bitstring类型。
fun senc(bitstring, key): bitstring.

(*除非将构造函数声明为私有，否则攻击者可以使用它们:*)
fun f(t1, . . . , tn) : t [ private ] .

析构函数使用：密码原语之间的关系由析构函数捕获，析构函数用于操作由构造函数形成的术语。

可以在每个重写规则的声明中使用let绑定。例如，在一些投票协议中使用的抽象零知识证明可以声明如下:

(*析构函数使用*)
例如：对称加密-生成密文函数：输入m,ssk,函数名getmess（签名），签名函数sign()
reduc forall m: bitstring, ssk: sskey; getmess(sign(m,ssk)) = m.

非对称加密-proverif代码分析：

(*非对称加密*)
type skey.
type pkey.
(*密钥生成*)
fun pk(skey):pkey.
(*加密*)
fun aenc(bitstring,pkey):bitstring.
(*解密.注意：析构函数是完全由构造函数组成的*)
不对：reduc forall m: bitstring, sk: skey，pk:pkey; adec(aenc(m,pk),sk) = m.因为pk是由构造函数pk(sk)生成的
reduc forall m:bitstring,sk:skey;denc(aenc(m,pk(sk)),sk)=m.

握手协议（抗中间人攻击）完整代码如下：包括对称加密、非对称加密、数字签名、事件设置、进程设置。

(* Symmetric key encryption *)

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


(* Asymmetric key encryption *)

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.


(* Digital signatures *)
(*
析构函数允许消息恢复和签名验证。
析构函数getmess允许攻击者从签名中获取消息m，即使没有密钥。
析构函数checksign检查签名，只有当签名正确时才返回m。诚实进程通常只使用checksign。这个签名模型假设签名总是伴随着消息m。也可以为不显示消息m的签名建模。
*)
type sskey.
type spkey.

fun spk(sskey): spkey.
fun sign(bitstring, sskey): bitstring.

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


free c:channel.

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

event acceptsClient(key).
event acceptsServer(key,pkey).
event termClient(key,pkey).
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) = 
	out(c,pkA);
	in(c,x:bitstring); 
	let y = adec(x,skA) in
	let (=pkA,=pkB,k:key) = checksign(y,pkB) in
	(*=pkA，对自己的公钥进行确认，证明确实是发给自己的*)
	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((pkX,pkB,k),skB),pkX));
	(*签名里添加了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)) )

该段代码运行结果为：

上述代码可以和非抗中间人攻击的代码对比学习，下面代码只列举不同处：

let clientA(pkA:pkey,skA:skey,pkB:spkey) = 
	out(c,pkA);
	in(c,x:bitstring); 
	let y = adec(x,skA) in
	let (=pkB,k:key) = checksign(y,pkB) in
	(*缺少=pkA*)
	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));
	(*签名里缺少了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)) )

3. 相关表达

关键字列表：不用用作标识符

内置类型：any_type, bitstring , bool, nat, sid, time

4. 详细分析握手定理的编码

代码如下：

(*声明公开通道c*)
free c:channel.

free s:bitstring [private].
query attacker(s).
(* Reachability and secrecy可达性和保密性：为了测试模型中术语M的保密性，在主进程之前的输入文件*)

event acceptsClient(key).
event acceptsServer(key,pkey).
event termClient(key,pkey).
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) = 
	out(c,pkA);
	in(c,x:bitstring); 
	let y = adec(x,skA) in
	let (=pkA,=pkB,k:key) = checksign(y,pkB) in
	(*=pkA，对自己的公钥进行确认，证明确实是发给自己的*)
	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((pkX,pkB,k),skB),pkX));
	(*签名里添加了pkX，便于收到此消息的客户端确认确实是发给自己的*)
	in(c,x:bitstring); 
	let z = sdec(x,k) in
	if pkX = pkA then event termServer(k).

process 
	new skA:skey; (*创建A和B的私钥*)
	new skB:sskey;
	let pkA = pk(skA) in out(c,pkA);(*通过宏定义生成A和B的公钥，并在公开通道c中传输*)
	let pkB = spk(skB) in out(c,pkB);
	( (!clientA(pkA,skA,pkB)) | (!serverB(pkB,skB,pkA)) 

相关知识点：

1. 可达性和保密性： proverif基本功能。为了测试模型中术语M的保密性，在主进程之前的输入文件中包含以下查询:

query attacker(M).
(*其中M是一个基本项，没有析构函数，包含自由名(可能是私有的，因此攻击者最初不知道)。*)

2. 通信断言、事件和身份验证： “如果事件e已经执行，那么事件e’在e之前已经执行。”查询基本通信断言的语法是:

query x:t1,y:t2,z:t3; event(e(x,y))==>event(e'(y,z)).
(*对于所有的x, y，对于每一个e(x, y)的出现，对于某个z有一个e'(y, z)的先前出现.*)

3. 内射Injuective: 在需要每个参与者执行的协议运行数量之间的一对一关系的情况下考虑使用Injective，内射对应断言捕获一对一关系。此语法中，箭头后面的事件运行次数≥箭头前事件运行次数（例如服务器和客户端之间通信，客户端只愿意和一个服务器进行一次密钥协商，而服务器愿意和多个客户端进行密钥协商，故inj-event（客户端事件)==>inj-event（服务器事件)）。语法：注意，在箭头==>之前使用inj−event或event并不会改变查询的含义，而箭头后是inj−event则查询通讯次数，event则查询通信顺序。

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

4. 四个事件声明的含义：

event acceptsClient(key). ：客户端使用它来记录自己已接受使用服务器B和提供的对称密钥运行协议。
event acceptsServer(key,pkey). ：服务器认为他已接受与客户端一起运行协议的事实，将提议的密钥作为第一个参数提供，并将客户端的公钥作为第二个参数提供。
event termClient(key,pkey). ：客户端认为自己已经终止了使用作为第一个参数提供的对称密钥和作为第二个参数的客户端公钥运行的协议。
event termServer(key). ：服务器相信他已经终止了与客户端a运行的协议，并将对称密钥作为第一个参数提供。

5. 理解通信断言和内射的语法逻辑：
   

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

注意： 在箭头==>之前发生的事件可以放在协议的末尾，但是在箭头 ==>之后发生的事件必须至少有一个消息输出。否则，整个协议可以在不执行后一个事件的情况下执行，因此通信肯定不成立。

还可以注意到，将箭头==>之前发生的事件移动到协议的开始处可以增强对应属性，将箭头==>之后发生的事件移动到协议的结束处也可以增强对应属性。向事件添加参数也增强了对应属性。

5. 看懂proverif的输出

一般结构如上图。
[Equations]总结了输入文件中给出的方程的内部表示(如果有的话)；
[Process]表示输入过程，其中扩展了所有宏，并将不同的标识符分配给唯一的名称/变量;此外，部分过程用标识符{n}进行注释。
[Query] ProVerif试图证明违反属性的状态是不可达的,如果违反了一个属性，那么ProVerif将尝试用英语重建一个[攻击派生]，并在应用的pi演算中重建一个[攻击跟踪]
Verification summary: 验证结果摘要。result有三种结果，如下图所示。

从下面这段结果可看见，Query not attacker(RSA[]) is false.这个结论从Derivation中推到了整个攻击过程。

---

总结

输入：in(M,x:t).
输出：out(M,N).