【ProVerif学习笔记】3：进程宏和进程书写的语法规则

1 进程宏

进程宏(Process Macros)用来定义子进程，因为在用ProVerif对协议进行建模时，直接一个大的主进程比较混乱，进程宏的形式为：
l e t R ( x 1 : t 1 , . . . , x n : t n ) = P . \bold{let} \ \ R(x_1:t_1,...,x_n:t_n)=P. let R(x1:t1,...,xn:tn)=P.

其中 R R R是宏的名字， P P P是子进程， x 1 , . . . , x n x_1,...,x_n x1,...,xn是 P P P里面的free变量，当使用这个宏时（原文叫macro expansion）就把使用时的参数传进去了。

例如：

free c:channel.free Cocks:bitstring [private].
free RSA:bitstring [private].
query attacker(Cocks).let R(x:bitstring) = out(c,x);0.let R'(y:bitstring) = 0.process R(RSA) | R'(Cocks)

第7行和第9行定义了两个过程宏R和R'，R将参数x从通道c输出，R'什么都不做。

第11行进行macro expansion，分别将定义的两个free变量作为参数传入，两个进程并发执行。

2 进程书写的语法规则

2.1 项和进程的语法

这里大部分都能和编程语言里的概念对应上，只有几个特别的部分需要说明。

P ∣ Q P \ | \ Q P ∣ Q表示进程 P P P和进程 Q Q Q的并发组合执行，即parallel composition。

! P !P !P表示无限个 P P P进程的并发组合执行，即infinite parallel composition，称为replication。

n e w n : t ; P \bold{new} \ \ n:t;P new n:t;P表示绑定进程 P P P中类型为 t t t的name n n n，即name restriction。

i f M t h e n P e l s e Q \bold{if} \ M \ \bold{then} \ P \ \bold{else} \ Q if M then P else Q是条件选择， M M M必须是一个计算布尔值的项，条件为真时执行P，假时执行Q，但是要注意 M M M执行失败的情况，例如 M M M中存在一个析构器，并且找不到与之对应的重写规则(rewrite rules)，这个时候就是执行失败了，那么整个都不会执行。

l e t x = M i n P e l s e Q \bold{let} \ \ x=M \ \bold{in} \ P \ \bold{else} \ Q let x=M in P else Q是项求值，如果 M M M能执行成功，它的值会赋给 x x x（ x x x进行自动类型推导，和 M M M的类型一致），然后执行 P P P。如果 M M M执行失败，那么执行 Q Q Q。

2. 2 模式匹配的语法

变量模式 x : t x:t x:t匹配类型为 t t t的任何模式，然后绑定给 x x x，常用在有显式或者隐式赋值的地方。

变量模式 x x x也是一样，但是要求 x x x的类型必须能通过上下文推导出来才行。

元组模式 ( T 1 , . . . , T n ) (T_1,...,T_n) (T1,...,Tn)匹配的就是和每个位置类型一致的元组 ( M 1 , . . . , M n ) (M_1,...,M_n) (M1,...,Mn)。

= M =M =M模式匹配的是一个与项 M M M相等的项 N N N。

2.3 作用域和绑定

这里主要讲了加括号和优先级的问题， P ∣ Q P \ | \ Q P ∣ Q是最先结合的，然后是if-then-else和let-in-else，最后是一元操作，如 ! P !P !P。所以 ! P ∣ Q !P \ | \ Q !P ∣ Q将被视为 ! ( P ∣ Q ) !(P \ | \ Q) !(P ∣ Q)，这个和编程语言有挺大区别的。

还有就是省略 e l s e 0 else \ 0 else 0的习惯导致的意义不清晰，比如：
i f M = M ′ t h e n i f N = N ′ t h e n P e l s e Q \bold{if} \ M = M' \ \bold{then} \ \bold{if} \ N = N' \ \bold{then} \ P \ \bold{else} \ Q if M=M′ then if N=N′ then P else Q

它将被视为：
i f M = M ′ t h e n ( i f N = N ′ t h e n P e l s e Q ) \bold{if} \ M = M' \ \bold{then} \ (\bold{if} \ N = N' \ \bold{then} \ P \ \bold{else} \ Q) if M=M′ then (if N=N′ then P else Q)

即 e l s e else else总是和最近的没有匹配的 i f if if匹配，对于let-in-else也是一样。

2.4 标识符和注释

对于构造器和析构器，没有什么类型上的限制，只要是标识符就行。标识符是用字母、数字、下划线、单引号组成的序列，区分大小写，避开保留字，且必须以字母开头。

注释是用(*和*)括起来的部分，不支持嵌套注释。

2.5 保留字

among, axiom, channel, choice, clauses, const, def, diﬀ, do, elimtrue, else, equation, equivalence, event, expand, fail, for, forall, foreach, free, fun, get, if, implementation, in, inj-event, insert, lemma, let, letfun, new, noninterf, not, nounif, or, otherwise, out, param, phase, pred, proba, process, proof, public vars, putbegin, query, reduc, restriction, secret, set, suchthat, sync, table, then, type, weaksecret, yield.

另外，ProVerif有内置类型bitstring、bool、time，以及逻辑量true、false，它们不属于保留字，可以被当作标识符，但是不建议这样做。

3 示例：书写握手协议

这里实际要用到上一章示例中定义的对称加密、非对称加密和签名的内容，这里把那些部分省略了没有写出来。

free c:channel.free s:bitstring [private].
query attacker(s).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) inout(c,senc(s,k)).let serverB(pkB:spkey,skB:sskey) =in(c,pkX:pkey);new k:key;out(c,aenc(sign((pkB,k),skB),pkX));in(c,x:bitstring);let z = sdec(x,k) in0.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)) )

在process处开始的是主进程，可以看到为A生成了非对称加密用的私钥，为B生成了签名用的私钥，然后为它们都生成公钥，把公钥都从公共通道c发送出去（以使得攻击者能访问这些公钥），再调用两个进程宏clientA和serverB来实现两个进程的并发执行，这里用replication的方式让两个主体都以无限数量会话并发执行。

协议流程和笔记2里学习的一样。即A把自己公钥pkA发出去。B则是接收到这个公钥pkX，然后B创建了一个对称密钥k（起到会话密钥的作用），和自己的公钥pkB一起打包成元组，先用自己的私钥skB签名，再用收到的公钥pkX加密，然后发出去。A接受到这个发来的bitstring，然后用自己私钥解密，解密成功之后得到y，然后用B的公钥pkB验证签名，如果验证通过了那么第一项就是pkB（这里用=pkB来匹配），第二项就是对称密钥k了，A再用这个k给消息s进行对称加密然后发出去。B接收到发来的bitstring之后，用自己刚刚创建的对称密钥k解密就得到了内容z，这应该和s是一样的内容。

参考阅读

ProVerif的manual第3.1.3~3.1.5章节