【ProVerif学习笔记】4：信息安全性质(Security Property)
1 Reachability和Secrecy
证明Reachability是最基本的能力，因为需要知道攻击者能访问到哪些term，而Secrecy就可以根据这个来评估——能访问到的term不满足Secrecy。要测试项 M M M在模型中是否满足Secrecy，在主进程前使用：
q u e r y a t t a c k e r ( M ) . \bold{query} \ \ attacker(M). query attacker(M).
其中 M M M是一个最基本的项，即不包含析构器， M M M可以包含free定义的名称，当然也可以设置为[private]，这样攻击者最开始是不知道它的。
2 事件(event)相关
Correspondence Assertions就是说某个程序点执行了，另一个点一定在之前执行过了，要定义这种性质就需要引入事件(event)。事件也可以包含参数，以研究参数之间的关系。定义的事件只是标记进程中的一个重要位置，并不对进程的行为产生任何影响，事件按如下方式定义：
e v e n t e ( M 1 , . . . , M n ) ; P \bold{event} \ \ e(M_1,...,M_n); \ P event e(M1,...,Mn); P
因为事件不产生任何影响，所以这里面的项 M 1 , . . . , M n M_1,...,M_n M1,...,Mn也不会扩展这个进程的知识。事件必须在使用前以 e v e n t e ( t 1 , . . . , t n ) . event \ \ e(t_1,...,t_n). event e(t1,...,tn).的形式声明，其中的 t 1 , . . . , t n t_1,...,t_n t1,...,tn是参数类型。
2.1 Correspondence断言
查询Correspondence的语法如下：
q u e r y x 1 : t 1 , . . . , x n : t n ; e v e n t ( e ( M 1 , . . . , M j ) ) = = > e v e n t ( e ′ ( N 1 , . . . , N k ) ) . \bold{query} \ \ x_1 : t_1,...,x_n : t_n ; \ \bold{event}(e(M_1,...,M_j)) ==> \bold{event}(e'(N_1,...,N_k)). query x1:t1,...,xn:tn; event(e(M1,...,Mj))==>event(e′(N1,...,Nk)).
这个查询成立的条件是，对于每次事件 e ( M 1 , . . . , M j ) e(M_1,...,M_j) e(M1,...,Mj)发生，都能在此前找到一个位置有事件 e ′ ( N 1 , . . . , N k ) e'(N_1,...,N_k) e′(N1,...,Nk)发生。更进一步，事件的参数必须满足所定义的关系，也就是说变量 x 1 , . . . , x n x_1,...,x_n x1,...,xn在 M 1 , . . . , M j M_1,...,M_j M1,...,Mj和 N 1 , . . . , N k N_1,...,N_k N1,...,Nk中是有相同的值的。
注意，在 = = > ==> ==>之前的事件中出现的参数相当于是被全称量词修饰的；而在 = = > ==> ==>之后的事件中出现，且在前面没有出现的的参数是被存在量词修饰的。例如：
q u e r y x : t 1 , y : t 2 , z : t 3 ; e v e n t ( e ( x , y ) ) = = > e v e n t ( e ′ ( y , z ) ) . \bold{query} \ \ x : t_1,y : t_2,z : t_3 ; \bold{event}(e(x,y)) ==> \bold{event}(e'(y,z)). query x:t1,y:t2,z:t3;event(e(x,y))==>event(e′(y,z)).
这表示对于 x , y x,y x,y的每次出现 e ( x , y ) e(x,y) e(x,y)，总是存在一个 z z z使得 e ′ ( y , z ) e'(y,z) e′(y,z)出现。
2.2 Injective Correspondence断言
如果期望协议双方的时间是只发生一次的（即one-to-one的），那么2.1中学习的Correspondence不足以表达Authentication（认证关系）。比如服务器向客户端请求缴费，客户端缴费一次应该对应服务器收费一次，否则客户端缴费一次对应服务器收费多次这样就不正确了。Injective Correspondence断言可以表达这种一对一关系，其语法如下：
q u e r y x 1 : t 1 , . . . , x n : t n ; i n j − e v e n t ( e ( M 1 , . . . , M j ) ) = = > i n j − e v e n t ( e ′ ( N 1 , . . . , N k ) ) . \bold{query} \ \ x_1 : t_1,...,x_n : t_n ; \ \bold{inj−event}(e(M_1,...,M_j)) ==> \bold{inj−event}(e'(N_1,...,N_k)). query x1:t1,...,xn:tn; inj−event(e(M1,...,Mj))==>inj−event(e′(N1,...,Nk)).
这个意思是 = = > ==> ==>之后的 e ′ e' e′的发生次数大于等于 = = > ==> ==>之前的 e e e的发生次数的。另外要注意， = = > ==> ==>之前写 i n j − e v e n t inj-event inj−event或者写 e v e n t event event都行，只有箭头之后写什么才重要。
3 示例：握手协议中的保密性和认证性
握手协议中是涉及认证性质的，如客户端A认为她在和服务器B通信，那么性质就要求确实是在和B通信，反过来也是一样。这里的【A认为】意思就是A所接收到的信息表明了这件事，因此可以声明如下这些事件：
event acceptsClient(key)：客户端接受了【使用收到的key和服务器交互】这件事。event acceptsServer(key,pkey)：服务器接受了【使用key和公钥为pkey的客户端交互】这件事。event termClient(key,pkey)：客户端认为已经完成了【使用key为会话密钥以及pkey作为客户端公钥，和服务器运行协议】这件事。event termServer(key)：服务器认为已经完成了【使用key作为会话密钥，和客户端运行协议】这件事。
对客户端A而言，她只想和服务器B分享自己的加密信息，所以如果她执行完协议，B对A的认证就应该保持。
对服务器B而言，他可以和很多客户端交互，所以在运行完协议之后，如果B认为A是他的对话者（ p k X = = p k A pkX==pkA pkX==pkA），那么A对B的认证就应该保持。
将上面两条认证性质形式化，书写为：
q u e r y x : k e y , y : s p k e y ; e v e n t ( t e r m C l i e n t ( x , y ) ) = = > e v e n t ( a c c e p t s S e r v e r ( x , y ) ) . q u e r y x : k e y ; i n j − e v e n t ( t e r m S e r v e r ( x ) ) = = > i n j − e v e n t ( a c c e p t s C l i e n t ( x ) ) . \begin{aligned} \bold{query} \ \ & x:key,y:spkey; \ \bold{event}(termClient(x,y))==>\bold{event}(acceptsServer(x,y)). \\ \bold{query} \ \ & x:key; \ \bold{inj-event}(termServer(x))==>\bold{inj-event}(acceptsClient(x)). \end{aligned} query query x:key,y:spkey; event(termClient(x,y))==>event(acceptsServer(x,y)).x:key; inj−event(termServer(x))==>inj−event(acceptsClient(x)).
这两条形式上有差异的原因是客户端和服务器所期望的身份验证方式是不同的，其中第一条不是单射(injective)的，因为服务器没有允许客户端知道她收到的消息是否是新的，从服务器向客户端可能发多个消息，就会导致单个服务器session对应多个客户端session。
加入这两条认证性质的握手协议如下：
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 (=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,pkA:pkey) = 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)) | (!serverB(pkB,skB,pkA)) ) 注意客户端和服务器的accepts*事件和term*事件的位置要在各自的进程宏中写出来。通常事件放置的位置按照它的语义也不是唯一的，对于上面的两条认证性质涉及的四个事件，整个逻辑就是（可以分成这样两类部分来看）：
绿色的部分就是【服务器给客户端发消息n-1】，所以【服务器接受关系建立acceptsServer】应该放在这个发送之前，另外按照它的语义还应该在【获取到客户端发来的公钥】之后；【客户端协议确认termClient】可以放在客户端运行末尾，按照图上一定要在【接收到消息】之后。
蓝色的部分就是【客户端给服务器回消息n】，所以【客户端接受关系建立acceptsClient】应该是在拿到key、验证身份之后，而且是回发消息之前；【服务器协议确认termServer】也可以放在末尾，但是一定要在【收到刚刚的客户端发来的消息】之后，所以代码里要检查pkX==pkA才行。
手册里给出了一些技巧，即通常而言==>前面的事件可以放在进程末尾，而==>后面的事件（在另一个进程）的位置后面至少应该有一个发送消息的地方。
设e==>e'即不同进程中的两个事件达成认证关系，通常e比较靠后，e'比较靠前，但是让e尽量往上，e'尽量往下，可以强化这种认证关系。还有就是添加事件的参数来进行限定也可以强化这种认证关系。
参考阅读
ProVerif的manual第3.2~3.2.3章节
