Proverif分析handshake协议

1. proverif简介

Proverif用来验证密码协议，密码协议是利用互联网等公共通信渠道进行交互以实现一些与安全相关的目标的并发程序。Proverif是在Dolev-Yao模型下进行密码协议验证的。在Dolev-Yao模型下，攻击者可以完全控制通信信道，可以读取、修改、删除以及注入消息，攻击者还可以操纵数据，例如：计算元组的莫个参数，使用密钥解密信息。Proverif还将检测不诚实的参与者行为，只有诚实的参与者会被建模。
Proverif允许密码术语和相关安全性目标以形式化的方式输入，允许自动验证声明的安全性目标。假设密码是完美的，只有攻击者拥有所需的密钥才能执行密码操作。运用对等原理或者重写规则来获取密码术语之间的关系。
使用Proverif语言，需要分三步，第一步声明；第二步进程宏；第三步主进程。

2. 握手（handshake）协议描述

假设client A和server B都有一对公私钥，client A知道server B的公钥(skB)。握手协议的目标就是，client A和server B分享密钥s。client A向server B发送请求，即【A→B:pk(skA)】；server B产生新的对称密钥k作为会话密钥，B把会话密钥和它的身份(pk(skB))相配对，用私钥skB进行签名，即【sign((pk(skB),k),skB)】；再用A的公钥进行加密，即【B→A: aenc(sign((pk(skB),k),skB),pk(skA))】。当client A收到消息后，A用自己的私钥进行解密，验证B的签名使用B的公钥，并提取会话密钥k。

A→B:pk(skA)
B→A: aenc(sign((pk(skB),k),skB),pk(skA))
A→B：senc(s,k)
1
2
3

我们希望这个协议提供三个属性：
- 安全性：会话密钥只有client A和server B知道；
- A对B的认证：如果B达到协议的末尾时，它相信已经和A分享了密钥k，那么A确实是它的对话者，也分享了k。
- B对A的认证：如果A用共享密钥k到达了协议的末尾，那么B提出k供A使用。
这个协议是不能抵抗中间人攻击的。如果一个不诚实的参与者D和B开始一场会话，那么D随后就可以假冒B和A进行会话。在会话结束后，A认为自己已经和B分享了私钥s，而实际上是和D分享了私钥s。

3. proverif模拟握手协议

 (*Symmetric key encryption*)
 type key.
 fun senc(bitstring, key):bitstring.
 reduc formall 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 formall m:bitstring, sk: skey; adec(aenc(m, pk(sk)), sk) = m. 
  
  
 (*Digital signatures*)
  
 type sskey.
 type spkey.
 
 fun spk(sskey): spkey.
 fun sign(bitstring, sskey): bitstring.
  
 reduc foamall m: bitstring, skk:sskey; getmess(sign(m,ssk)) = m.
 reduc foramll 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(acceptClient(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
  	event acceptsClient(k);
  	out(c,senc(s,k)).
   	event termClient(k,pkA).
   
 let serverB(pkB:spkey, skB:sskey) =
   	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))|(!server(pkB,skB)))
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66

4. proverif代码分析

4.1 声明
type----类型、free----自由名称、fun----构造函数；自由名称和构造函数可以声明公开或者私有，如果声明为私有，则攻击者无法获取。
在握手协议中，定义了三种type，分别是key，skey，pkey，sskey，spkey。key是密钥；skey是私钥；pkey是公钥，由skey生成；sskey是签名使用的私钥，spkey是签名使用的公钥，由sskey生成。
定义了9种函数，分别是senc()【加密函数，使用密钥对明文进行加密】，adec()【解密函数，使用密钥对密文进行解密，与senc()函数的关系使用析构函数进行说明（第5行）】，pk()【公钥生成函数，由私钥产生公钥的过程】，aenc() 【加密函数，使用密钥对明文加密】，denc()【解密函数，使用密钥对密文进行解密，与aenc()函数的关系使用析构函数进行说明（第16行）】，spk()【由签名私钥生成签名公钥】， sign()【使用私钥进行签名】， getmess()【得到签名的明文，与签名函数sign()的关系由析构函数决定（第27行）】， checksign()【使用签名者的公钥，验证签名，与签名函数sign()的关系由析构函数决定（第28行）】。
第31行定义了公共通信信道c。
第33行定义了s为私有的，不公开的。
第34行定义了攻击者想要获取的参数s。
第36—39行，是为了认证clientA和serverB的合法性，定义了4个事件的发生。分别是acceptsClient(key)【被client记录它已经接受与serveB运行协议并接收对称密钥key】、acceptsServer(key,pkey)【server接受与client运行协议，接收密钥key和client的公钥pkey】、termClient(key,pkey)【client相信它已经终止了一个协议，第一个参数是对称密钥key，第二个参数是client的公钥pkey】、termServer(key)【server相信它已经终止了与client的协议，参数是对称密钥key】。
client只能和server进行密钥协商，而server可以和多个client进行密钥协商。如果在协议的最后，如果server确认clientA是他的对话者，server只希望A→B的认证保持，所以当pkX=pkA时，执行termServer(x)。
第41、42行用来实现认证属性的。第41行不是inj-even是因为握手协议不允许client验证收到的信息是否是新鲜的。

5. ProVerif模拟结果