【ProVerif学习笔记】6：握手协议（handshake protocol）建模

这节先不继续往下看，巩固一下对ProVerif建模握手协议的理解。

握手协议的流程如下：

ex_handshake.pv（只验证保密性）

手册里在引入security性质之前，握手协议的模型如下：

(* ------------------------对称加密相关------------------------ *)
(* 对称密钥 *)
type key.
(* 对称加密：传入要加密的内容和密钥，返回加密结果 *)
fun senc(bitstring, key): bitstring.
(* 对称解密：用于析构对称加密，传入加密结果senc(m,k)，用同一个密钥k可解密出原始信息m *)
reduc forall m: bitstring, k: key; sdec(senc(m,k),k) = m.(* ------------------------非对称加密相关------------------------ *)
(* 非对称加密-私钥 *)
type skey.
(* 非对称加密-公钥 *)
type pkey.
(* 从私钥获取公钥：可以用于密钥配对 *)
fun pk(skey): pkey.
(* 非对称加密：传入要加密的内容和公钥，返回加密结果 *)
fun aenc(bitstring, pkey): bitstring.
(* 非对称解密：用于析构非对称加密，传入加密结果aenc(m,pk(sk))，用其私钥sk可解密出原始信息m *)
reduc forall m: bitstring, sk: skey; adec(aenc(m,pk(sk)),sk) = m.(* ------------------------数字签名相关------------------------ *)
(* 数字签名-私钥 *)
type sskey.
(* 数字签名-公钥 *)
type spkey.
(* 从私钥获取公钥：可以用于密钥配对 *)
fun spk(sskey): spkey.
(* 数字签名：传入要签名的内容和私钥，返回签名结果 *)
fun sign(bitstring, sskey): bitstring.
(* 获取消息：无视签名用的私钥ssk，直接获取其中的消息m *)
reduc forall m: bitstring, ssk: sskey; getmess(sign(m,ssk)) = m.
(* 验证签名后获取消息：使用公钥spk(ssk)方能对使用ssk签名的消息验证，并成功取出m *)
reduc forall m: bitstring, ssk: sskey; checksign(sign(m,ssk),spk(ssk)) = m.(* ------------------------全局声明相关------------------------ *)
(* 通信信道c，是一个公有的信道 *)
free c:channel.
(* 要传输的保密消息s，由于使用[private]修饰，所以攻击者无法直接获取 *)
free s:bitstring [private].(* ------------------------查询相关------------------------ *)
(* 查询攻击者能否窃取s，即关于s的保密性 *)
query attacker(s).(* ------------------------进程相关------------------------ *)
(* 客户端进程A：A公钥、A私钥、B公钥 *)
let clientA(pkA:pkey,skA:skey,pkB:spkey) =(* 将A公钥发送到通道c *)out(c,pkA);(* 从通道c取回B传来的结果x *)in(c,x:bitstring);(* 用自己的私钥skA对结果x解密得到y *)let y = adec(x,skA) in(* 用B的公钥pkB对y验证，验证结果需是(pkB, k)，第二项k即是对称密钥 *)let (=pkB,k:key) = checksign(y,pkB) in(* 使用对称密钥k对消息明文s加密并发送 *)out(c,senc(s,k)).(* 服务器进程B：B公钥、B私钥 *)
let serverB(pkB:spkey,skB:sskey) =(* 从通道c取出公钥，是A的公钥 *)in(c,pkX:pkey);(* 新建一个对称密钥k *)new k:key;(* 将(pkB,k)用B的私钥skB签名，然后用A的公钥pkX加密，发到通道c *)out(c,aenc(sign((pkB,k),skB),pkX));(* 从通道c拿到A发来的消息x *)in(c,x:bitstring);(* 使用对称密钥k解密即可得到消息明文z *)let z = sdec(x,k) in0.(* 总的进程 *)
process(* A的私钥 *)new skA:skey;(* B的私钥 *)new skB:sskey;(* A的公钥，生成后发到通道c上，攻击者可获取 *)let pkA = pk(skA) in out(c,pkA);(* B的公钥，生成后发到通道c上，攻击者可获取 *)let pkB = spk(skB) in out(c,pkB); (* 实际行为是无限个客户端A和无限个服务器B的并发执行 *)( (!clientA(pkA,skA,pkB)) | (!serverB(pkB,skB)) )

整体就是两类进程，客户端clientA和服务器serverB。认为一个服务器B的进程实体是可以服务任何一个具体的客户端的，所以在它的macro里只传入了自己签名用的公钥和私钥。而一个客户端A的进程实体只会找一个具体的服务器，所以是在自己的macro里传入了想要服务自己的服务器B的公钥，在这里定死了。

这里希望有无数的进程在并发执行，对客户端和服务器都是做了replication（符号!）然后再并发。

还有要注意的就是之前学习的解构器（destructor） 和模式匹配（pattern matching） 的使用。

解构器本身如果传入的东西不匹配就会解构失败，解构失败会走let-in-else的else路线，如果else被省略掉（像上面一样）就会把进程直接halt掉，所以一般解构器本身就能检查传过来的东西是不是按期望的合规的。

模式匹配可以和解构器一起用，这样不仅要求解构成功，还需要模式匹配成功才能走let-in-else的in路线，否则一律走else路线。比如

let (=pkB,k:key) = checksign(y,pkB)

这一行，不仅要求y是用pkB对应的私钥skB签名的（这样才能解构成功），而且要求解构后的内容能匹配到一个二元组形式（分别是签名方公钥和签名方提供的对称密钥），还要求二元组的第二项能匹配到一个key类型（对称密钥），二元组的第一项能匹配到公钥pkB上（和自己期望的pkB是相同的，这块只是签名方自己声明自己的身份，其实在密码学上还不够强，比如第二节里学习到可能遭受中间人攻击）。

这个是最原始的握手协议，因为可能遭受中间人攻击，所以验证结果是不通过的：

--------------------------------------------------------------
Verification summary:Query not attacker(s[]) is false.--------------------------------------------------------------

ex_handshake_annotated.pv（加入对认证性的验证）

手册里3.2节讲security性质的时候引用了这个case，这里“annotated”意思就是如果要证明authentication（一种security性质，表达认证关系，包括用correspondence断言和injective correspondence断言两种声明），那么是需要用event来标记程序点的：

To reason with correspondence assertions, we annotate processes withevents, which markimportant stages reached by the protocol but do not otherwise affect behavior.

因为correspondence断言就是用来捕获事件先后关系的：

“if an event e has been executed, then event e′ has been previously executed.”

这种标记不会影响进程本身的行为，也不会让攻击者的知识有任何的增加或者减少。添加了事件标记的模型如下：

type key.
fun senc(bitstring, key): bitstring.
reduc forall m: bitstring, k: key; sdec(senc(m,k),k) = m.type skey.
type pkey.
fun pk(skey): pkey.
fun aenc(bitstring, pkey): bitstring.
reduc forall m: bitstring, sk: skey; adec(aenc(m,pk(sk)),sk) = m.type sskey.
type spkey.
fun spk(sskey): spkey.
fun sign(bitstring, sskey): bitstring.
reduc forall m: bitstring, ssk: sskey; getmess(sign(m,ssk)) = m.
reduc forall m: bitstring, ssk: sskey; checksign(sign(m,ssk),spk(ssk)) = m.free c:channel.
free s:bitstring [private].
query attacker(s).(* 客户端认为自己在使用key对称密钥和服务器进行协议交互 *)
event acceptsClient(key).
(* 服务器认为自己在使用key对称密钥和pkey公钥标识的客户端进行协议交互 *)
event acceptsServer(key,pkey).
(* pkey标识的客户端认为自己使用key和服务器进行协议交互结束 *)
event termClient(key,pkey).
(* 服务器认为自己使用key对称密钥和客户端进行协议交互结束 *)
event termServer(key).(*
对于每个以对称密钥x和服务器交互结束的客户端y
前面总是存在认定以对称密钥x和客户端y交互的服务器
*)
query x:key,y:pkey; event(termClient(x,y))==>event(acceptsServer(x,y)).
(*
对于每个以对称密钥x交互结束的服务器
前面总是存在一个区别于其它的“以对称密钥x和服务器交互的客户端”
即单射关系
*)
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) inlet (=pkB,k:key) = checksign(y,pkB) in(* 客户端解密成功+验证成功后即认为接受了使用密钥k通信 *)event acceptsClient(k);out(c,senc(s,k));(* 客户端运行结束，本次是使用k通信，自己的公钥是pkA *)event termClient(k,pkA).let serverB(pkB:spkey,skB:sskey,pkA:pkey) = in(c,pkX:pkey);new k:key;(* 服务器收到客户端公钥pkX，并创建了密钥k，即认为接受了使用密钥k和客户端pkX通信 *)event acceptsServer(k,pkX);out(c,aenc(sign((pkB,k),skB),pkX));in(c,x:bitstring);let z = sdec(x,k) in(* 如果接收到的pkX确实是pkA，即认为服务器使用对称密钥k运行结束 *)if pkX = pkA then event termServer(k).processnew 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)) )

注意这一版不仅加入了event，而且在serverB的macro中传入了pkA，这是因为termServer本身需要判断自己交互的pkX是pkA。

这一版只是加了认证性质的验证，但是还是没有解决中间人攻击问题。

--------------------------------------------------------------
Verification summary:Query not attacker(s[]) is false.Query event(termClient(x_2,y_1)) ==> event(acceptsServer(x_2,y_1)) is false.Query inj-event(termServer(x_2)) ==> inj-event(acceptsClient(x_2)) is true.--------------------------------------------------------------

结果第一条表明，对消息s还是不满足的。

结果第二条表明，从B（服务器）到A（客户端）的认证是不满足的，也就是说如果客户端觉得自己和服务器完成了协议流程，不一定真的有这个服务器在和客户端走协议，这个也是因为中间人可以冒充服务器来和客户端通信。

结果第三条表明，从A（客户端）到B（服务器）的认证是满足的，也就是说如果服务器觉得自己走完了协议流程，一定至少有一个客户端是在和自己走协议的。

ex_handshake_annotated_fixed.pv（解决中间人攻击）

这里主要就是像第二节里说的那样，让服务器回传的信息中包含目标客户端的标识（这里是用公钥）来防止中间人攻击发生。

type key.
fun senc(bitstring, key): bitstring.
reduc forall m: bitstring, k: key; sdec(senc(m,k),k) = m.type skey.
type pkey.
fun pk(skey): pkey.
fun aenc(bitstring, pkey): bitstring.
reduc forall m: bitstring, sk: skey; adec(aenc(m,pk(sk)),sk) = m.type sskey.
type spkey.
fun spk(sskey): spkey.
fun sign(bitstring, sskey): bitstring.
reduc forall m: bitstring, ssk: sskey; getmess(sign(m,ssk)) = m.
reduc forall 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(acceptsClient(x)).let clientA(pkA:pkey,skA:skey,pkB:spkey) = out(c,pkA);in(c,x:bitstring); let y = adec(x,skA) in(* 这里检查一下这个包确实是要发给自己pkA的 *)let (=pkA,=pkB,k:key) = checksign(y,pkB) inevent 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);(* 这里把要通信的客户端标识pkX放进去 *)out(c,aenc(sign((pkX,pkB,k),skB),pkX));in(c,x:bitstring); let z = sdec(x,k) inif 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)) )

现在三条性质就都能验证通过了：

--------------------------------------------------------------
Verification summary:Query not attacker(s[]) is true.Query event(termClient(x_2,y_1)) ==> event(acceptsServer(x_2,y_1)) is true.Query inj-event(termServer(x_2)) ==> inj-event(acceptsClient(x_2)) is true.--------------------------------------------------------------