这节先不继续往下看，巩固一下对ProVerif建模握手协议的理解。
握手协议的流程如下：
手册里在引入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) in
0.
(* 总的进程 *)
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.
--------------------------------------------------------------
手册里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) in
let (=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).
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)) )
注意这一版不仅加入了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（服务器）的认证是满足的，也就是说如果服务器觉得自己走完了协议流程，一定至少有一个客户端是在和自己走协议的。
这里主要就是像第二节里说的那样，让服务器回传的信息中包含目标客户端的标识（这里是用公钥）来防止中间人攻击发生。
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) 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);
(* 这里把要通信的客户端标识pkX放进去 *)
out(c,aenc(sign((pkX,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)) )
现在三条性质就都能验证通过了：
--------------------------------------------------------------
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.
--------------------------------------------------------------