知新_RL

这个屌丝很懒，什么也没留下！

热门标签

【ProVerif学习笔记】2：协议建模中的声明_proverif工作原理

作者：知新_RL | 2024-05-30 11:54:24

踩

proverif工作原理

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

1 握手协议

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

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

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

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

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

整个过程如下：

\begin{aligned} A \to B & : p k (s k A) \\ B \to A & : a e n c (s i g n ((p k (s k B), k), s k B), p k (s k A)) \\ A \to B & : s e n c (s, k) \end{aligned}

$\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 \to B B \to A A \to B : p k (s k A) : a e n c (s i g n ((p k (s k B), k), s k B), p k (s k A)) : s e n c (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通信：

\begin{aligned} I \to B & : p k (s k I) \\ B \to I & : a e n c (s i g n ((p k (s k B), k), s k B), p k (s k I)) \\ A \to B & : p k (s k A) \\ I \to A & : a e n c (s i g n ((p k (s k B), k), s k B), p k (s k A)) \\ A \to I & : s e n c (s, k) \end{aligned}

$\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 \to B B \to I A \to B I \to A A \to I : p k (s k I) : a e n c (s i g n ((p k (s k B), k), s k B), p k (s k I)) : p k (s k A) : a e n c (s i g n ((p k (s k B), k), s k B), p k (s k A)) : s e n c (s, k)

只要让服务器回传的信息中包含目标客户端的标识（这里是用公钥）就可以防止这种攻击发生了：

\begin{aligned} A \to B & : p k (s k A) \\ B \to A & : a e n c (s i g n ((p k (s k A), p k (s k B), k), s k B), p k (s k A)) \\ A \to B & : s e n c (s, k) \end{aligned}

$\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 \to B B \to A A \to B : p k (s k A) : a e n c (s i g n ((p k (s k A), p k (s k B), k), s k B), p k (s k A)) : s e n c (s, k)

2 声明

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

type t.
1

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

free n : t.
1

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

free n1,...,nk : t.
1

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

free n : t [private].
1

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

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

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

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

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

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

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 .
1
2
3

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

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

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

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

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

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

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

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

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

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

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

其中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.
1
2
3
4
5
6
7

对于数字签名，和非对称加密是类似的，需要有签名私钥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.
1
2
3
4
5
6
7
8

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

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

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

参考阅读

ProVerif的manual第3~3.1.2章节

声明：本文内容由网友自发贡献，不代表【wpsshop博客】立场，版权归原作者所有，本站不承担相应法律责任。如您发现有侵权的内容，请联系我们。转载请注明出处：https://www.wpsshop.cn/w/知新_RL/article/detail/646842