【ProVerif学习笔记】2：协议建模中的声明

ProVerif验证的加密协议并发程序通过公共通道来进行信息较交互，最终实现一些目标。认为攻击者对这样的通道有完全的控制能力，包括阅读、修改、删除和注入消息，也可以解密自己持有密钥的消息（视解密为获取密文的唯一途径，不考虑攻击者用其它方式获取密文，所以如果自己没有解密的密钥就不行）。

1 握手协议

握手协议(Handshake protocol)是有一个客户端A和服务器B，假设每一方都有自己的公私钥对，然后A知道B的公钥pk(skB)，协议的目的是让客户端A能向服务器B分享自己的私密信息s。

协议按照如下的方式工作。应客户端A的要求，B生成一个新的对称的密钥k，作为会话密钥，把这个k和自己的公钥pk(skB)打包，然后先用自己的私钥skB签名，再用A的公钥pk(skA)加密，也就是说要发送的是：
aenc(sign((pk(skB),k),skB),pk(skA))aenc(sign((pk(skB),k),skB),pk(skA))aenc(sign((pk(skB),k),skB),pk(skA))

其中sign是签名，aenc是非对称加密。

A收到消息后，先用自己的密钥skA解密，再用B的公钥pk(skB)验证一下内容无误，然后提取出会话密钥k，就能用这个k给自己的私密信息s加密然后发送了。

这个协议背后的基本原理在于，A收到的是用她的公钥非对称加密的结果，因此她应该是唯一能够解密其内容的人。而数字签名是用来确保B是这个消息的发起者。

整个过程如下：
A→B:pk(skA)B→A:aenc(sign((pk(skB),k),skB),pk(skA))A→B:senc(s,k)\begin{aligned} A \to B &: pk(skA) \\ B \to A &: aenc(sign((pk(skB),k),skB),pk(skA)) \\ A \to B &: senc(s, k) \end{aligned} A→BB→AA→B:pk(skA):aenc(sign((pk(skB),k),skB),pk(skA)):senc(s,k)

上面的协议叙述还不够清晰，比如要检查每一步收到的格式是正确的，叙述里没有，但是协议建模到ProVerif时要做这些事。

用自然语言描述希望这个协议所具有的三个性质：

保密性：只有A和B知道s的值
认证性（A到B）：如果B运行到了末尾，他认为和A共享了k，那么A确实是B的对话者，共享了这个k
认证性（B到A）：如果B运行到了末尾，她认为和B共享了k，那么B确实是提供k的一方

这个协议可以受到中间人攻击，一个中间人I可以先和B通信，再冒充B和A通信：
I→B:pk(skI)B→I:aenc(sign((pk(skB),k),skB),pk(skI))A→B:pk(skA)I→A:aenc(sign((pk(skB),k),skB),pk(skA))A→I:senc(s,k)\begin{aligned} I \to B &: pk(skI) \\ B \to I &: aenc(sign((pk(skB),k),skB),pk(skI)) \\ A \to B &: pk(skA) \\ I \to A &: aenc(sign((pk(skB),k),skB),pk(skA)) \\ A \to I &: senc(s, k) \end{aligned} I→BB→IA→BI→AA→I:pk(skI):aenc(sign((pk(skB),k),skB),pk(skI)):pk(skA):aenc(sign((pk(skB),k),skB),pk(skA)):senc(s,k)

只要让服务器回传的信息中包含目标客户端的标识（这里是用公钥）就可以防止这种攻击发生了：
A→B:pk(skA)B→A:aenc(sign((pk(skA),pk(skB),k),skB),pk(skA))A→B:senc(s,k)\begin{aligned} A \to B &: pk(skA) \\ B \to A &: aenc(sign((pk(skA),pk(skB),k),skB),pk(skA)) \\ A \to B &: senc(s, k) \end{aligned} A→BB→AA→B:pk(skA):aenc(sign((pk(skA),pk(skB),k),skB),pk(skA)):senc(s,k)

2 声明

用户定义类型，其中t是类型名称：

type t.

定义free的变量（原文是free names），其中n是变量名称，t是类型名：

free n : t.

定义一连串的free names，都是t类型的：

free n1,...,nk : t.

channel c.和free c : channel.是同一个意思，都是声明一个公共信道c，如果要指定不被攻击者获取，使用：

free n : t [private].

构造器（函数）用来构建密码协议使用的建模原语，例如单向哈希、加密、数字签名等：

fun f(t1,...,tn) : t.

其中f是有n个参数的构造器，t是返回值类型，t1到tn是参数。构造器默认是可以被攻击者使用的，如果要禁止攻击者使用，则要：

fun f(t1,...,tn) : t [private].

例如，这种私有的构造可以用在对服务器密钥表的建模上。

密码原语之间的关系由析构器指明，析构函数用于操作构造器组成的项。析构器使用如下的重写规则：

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 .

其中ggg是有k个参数的析构器，项M1,1,...,M1,k,M1,0M_{1,1},...,M_{1,k},M_{1,0}M1,1,...,M1,k,M1,0是将构造器作用于t1,1,...,t1,n1t_{1,1},...,t_{1,n_1}t1,1,...,t1,n1类型的x1,1,...,x1,n1x_{1,1},...,x_{1,n_1}x1,1,...,x1,n1上得到的。上面每一行重写规则，ggg的返回值M1,0M_{1,0}M1,0到Mm,0M_{m,0}Mm,0都应该具有相同的类型，同样的，析构函数里每次传的参数表相应位置上也必须是相同的类型。

每次执行到g(M1,1,...,M1,k)g(M_{1,1},...,M_{1,k})g(M1,1,...,M1,k)或者这一项的实例时，都会找一条合适的重写规则将其变成对应的M1,0M_{1,0}M1,0。如果无法应用重写规则时，析构失败，进程会阻塞（除了let进程）。这和真实世界的密码原语是一致的。

如果多个变量有相同的类型，就只写最后一个的类型就行：

reduc forall x,y : t,z : t'; g(M_1,...,M_k)=M_0.

和构造器类似，析构器也可以加[private]声明为私有的。

3 示例：为握手协议声明加密原语

现在对握手协议中使用的密码学原语进行形式化。

首先是对称加密，这里定义一个密钥类型key，定义了一个对称加密函数senc，传入bitstring（内置的）和key，然后返回一个bitstring：

type key.
fun senc(bitstring, key): bitstring.

再定义一个析构器，来对解密操作进行建模：

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

其中m表示消息，k表示对称密钥。

对于非对称加密，使用一元构造器pk，传入私钥，返回公钥。也可以理解成是传入一个私钥就能生成对应的公钥，从而得到公私钥对。解密的析构器也是和前面类似的做法。

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

对于数字签名，和非对称加密是类似的，需要有签名私钥sskey和签名公钥spkey，用私钥签名、公钥验证。下面是一种带有消息恢复的签名，getmess就是直接从签名后的信息中提取到原信息，而checksign则是用公钥对签名进行验证，只有验证通过时才能返回原信息m。

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

还支持元组，元组是n>=2n>=2n>=2的(M1,...,Mn)(M_1,...,M_n)(M1,...,Mn)。如果允许攻击者访问某个元组，他可以取得其中的任何一项；反过来，如果攻击者有M1,...,MnM_1,...,M_nM1,...,Mn，他就可以构造元组。

元组中的每一项可以是任何类型，但是元组总是bitstring类型的，所以如果某个构造器的某个参数是bitstring类型的，那就可以传个元组进去。

需要注意元组一定是n>=2n>=2n>=2的，只有一个元素的(M1)(M_1)(M1)和M1M_1M1没区别，不是元组。

参考阅读

ProVerif的manual第3~3.1.2章节