实例介绍密码协议形式化验证工具ProVerif


1. ProVerif 介绍

ProVerif是一款基于 Dolev-Yao 模型的密码协议形式化验证工具。由Bruno Blanchet开发并开源。ProVerif 能够用于处理各种密码学原语,包括对称加密和非对称加密应用(加密和签名)、哈希函数和 Diffie-Hellman 密钥协商等。并且,ProVerif还能够处理无穷多的会话(即使并行)和无穷消息空间,解决了密码协议验证过程中的状态爆炸等问题。
ProVerif能够证明以下属性:
l机密性(即攻击者无法获得某消息)
l认证性和相对于的更加普遍的属性
l强保密性(攻击者不仅无法直接获得某消息,并且当值发生变化时,无法看到差异)

2. ProVerif 语法介绍

2.1   协议建模

ProVerif使用π推演(pi calculus)语言编写,下面详细介绍该语法。

2.1.1    声明

type(定义类型) :用户可以使用 type 定义自定义类型。如定义密钥类型 key,使用type key即可。
free(自由名称声明):在一个输入文件中出现的所有自由名称必须使用free进行声明,并且可以通过增加 private 标志来声明该自由名称为秘密的。语法为:free n:t [private],如声明一个 bitstring类型的自由名称 n,可以通过以下语句实现:free n:bitstring
fun(构造函数):构造函数主要用于建立加密协议所使用的建模原语,如:单项哈希函数、加密和数字签名等。构造函数通过 fun 定义。语法为:fun f(t1,...,tn) : t.  fun enc(bitstring, key):bitstring 意味着定义一个名为 enc 的构造函数,该函数的输入有两个参数,分别为 bitstring类型和key类型,输出为bitstring类型。
reduc(析构函数):密码学原语之间的关系是通过析构函数进行捕获的。直接从字面意思看不是很好理解,我们可以结合前面的知识,通过定义一个完整的对称加密协议来理解。
1
type key.
fun senc(bitstring, key): bitstring.
reduc forall m: bitstring, k: key; sdec(senc(m,k),k) = m.
1首先定义了key类型,代表着对称加密使用的对称密钥。接着定义了构造函数sencsenc接收两个参数,分别是bitstring类型和key类型。其中bitstring类型是ProVerif自带的,所以不需要单独的进行声明,代表着比特串类型。senc的输出也是bitstring类型。最后,和构造函数相对应的析构函数,则是名为 sdec 的解密函数。sdec 和构造函数一样,接收2个参数,类型依次是bitstring类型和key类型。而为了与构造函数相对应,形成闭环。就有了最后的sdec(senc(m,k),k) = m 语句。其中senc(m,k)表示密文。

2.1.2     宏

ProVerif 主要提供了功能宏和进程宏。这里主要讲解进程宏。引入进程宏主要是为了方便开发,考虑到一些复杂的协议不太可能仅通过一个主进程就能完成,所以通过进程宏来声明子进程。具体语法为:let R(x1:t1, x2:t2, ...) = P. R 表示宏名称,是被定义的子进程。具体的用法会在后续的例子中详细介绍。

2.1.3     安全属性

ProVerif作为能够证明可达性属性、相关性断言和观测等价性。
可达性证明是ProVerif最基础的功能,ProVerif能够用于判别在协议中,哪一项是对攻击者可见的,所以,可达性证明也可用于评估某一项的保密性。在ProVerif中,判断M的保密性,可以通过以下语句实现:query attacker (M ) . 使用了上述语句后,ProVerif 会在协议测试完成后返回相应的结果。
相关性断言可以通过 query event(M) ==> event(M’) 进行判断,其表达的意思是,如果M被执行,那么M’也被执行。

3. ProVerif 实例讲解

3.1   ProVerif 安装

ProVerif的源码可以通过访问网站 http://proverif.inria.fr/ 进行下载,不过ProVerif 已经针对主流的操作系统如:LinuxMacWindows操作系统都已经有了二进制安装包。官方推荐使用OPAM进行安装。OPAM可以通过访问 https://opam.ocaml.org/ 进行安装。在安装了OPAM以后,只需要执行 opam update 即可更新软件源。接着执行下列语句:
opam depext conf-graphviz
opam depext proverif
opam install proverif
即可完成 ProVerif 的安装。

3.2   ProVerif 实例

3.2.1    可达性检验

为了测试ProVerif提供的可达性检验功能,请先观察下列代码:

实例介绍密码协议形式化验证工具ProVerif

代码第1行是注释语句,ProVerif 的注释语句以 开头,以 *) 结束。在第2行声明了一个公共信道c,公共信道意味着在上面传输的一切信息都是可能被泄露、窃听和篡改的。代码第5-6行分别声明了比特类型的变量 Cocks  RSA, 并且都是私有不公开的。第7-8行分别 RSA  Cocks进行了可达性属性的检验。第10行开始,是协议的整个进程过程,由于是示范,该进程只包含第11行一个执行语句,表示通过公共信道c输出RSA。最后用0表示进程的结束。所以在这个demo中,表达的密码协议非常简单,就是在公共信道输出秘密变量RSA. 然后再来看这个协议经过ProVerif检验以后,输出的结果。结果如下:

实例介绍密码协议形式化验证工具ProVerif

输出结果中可以清晰的发现,Query not attacker(RSA[]) 的值为 false,也就是说RSA实际上对攻击者是可见的。这是因为尽管对RSA使用了private修饰,但是由于RSA最终通过了公共信道c输出,所以还是会被攻击者获取。而Cocks从始至终都是private,并没有输出。所以Query not attacker(Cocks[]) true

3.2.2    相关性断言

为了测试ProVerif提供的相关性断言检测功能。请观察以下代码:

实例介绍密码协议形式化验证工具ProVerif

代码第8-9行分别声明了两个事件,evCocksevRSA, 并且在第11行给出了断言检验语句,该语句意味着,如果evCocks 已经发生,那么evRSA也在此之前就已经发生。继续往下看,本例中的进程首先在公共信道输出了RSA,接着使用公共信道c接受了参数x,并且如果x = Cocks,那么执行事件 evCocks ,接着执行事件 evRSA。否则,直接执行 evRSA。我们先首先分析一下该进程,不难发现,如果 evCocks 被执行了,说明x=Cocks,那么evRSA 最终也会被执行。再来看最终的ProVerif运行结果,如下图所示:

实例介绍密码协议形式化验证工具ProVerif

和分析的一致,最终相关性断言结果也为真。
       

原文始发于微信公众号(山石网科安全技术研究院):实例介绍密码协议形式化验证工具ProVerif

版权声明:admin 发表于 2023年1月16日 下午4:36。
转载请注明:实例介绍密码协议形式化验证工具ProVerif | CTF导航

相关文章

暂无评论

暂无评论...