【ProVerif学习笔记】7：基本建模特性

1 constants

常量（constant）可以用参数量为0的函数（fun关键字声明的，在ProVerif里其实应该叫constructor ）来表示，也就是有一个类型名有一个返回值类型（就是常量的类型），也可以直接用const关键字来描绘常量。

const c1, ... , ck : t.

2 data constructors和type conversion

2.1 `[data]`

constructor就是用fun声明的函数，用来对一系列数据做构造。data constructor是一种将构造器用来表示数据的方案，一种就是在后面加一个[data]标记：

fun f(t1, ... , tn) : t [data].

这样声明的data constructor就类型于一个tuple，攻击者能够使用它去构造数据（即从参数里的t1…tn类型的数据去构造t类型的返回数据），还可以去解构（decompose）数据，也就是说相当于默认生成了n个destructor，分别把构造结果f(x1, ..., xn)映射到每个参数xi。

出于上面描述的能被攻击者使用的性质，对于data constructor就不能再使用[private]声明了。

下面是一个对[data]修饰的data constructor解构的例子，首先有这样的声明：

type key.
type host.
fun keyhost(key, host) : bitstring [data].

其中两个参数key和host都是类型变量（variable），在解构的时候可以不写类型，具体是：

let keyhost(k, h) = x in ...

这里x其实就是一个bitstring，然后k和h分别是对keyhost这个data constructor解构出来的key和host。

2.2 `[typeConverter]`

这是一种特殊的data constructor标记，语义是类型转换器（type converter），用来做类型转换（因为有的时候遇到类型不匹配的情况就没法把参数应用到希望使用的函数上去了）。

fun tc(t) : t' [typeConverter].

由于它也是一种data constructor，所以也和前面说的一样，是攻击者可以使用的，而且可以从转换后的类型t'解构得到转换前的类型t。

另外，[typeConverter]标记的data constructor只是一种标记函数（identity function），也就是说除了把类型转换一下之外没有任何其它的影响。

默认情况下，在ProVerif里类型只在做协议的typechecking的阶段用到，在验证的阶段就会忽略类型了，所以在验证的时候会把[typeConverter]标记的data constructor全都移除掉。手册上讲这样做是为了能够检测type flaw attack，可以用set ignoreTypes = ...来强制改变这种行为。

下面是一个对[typeConverter]修饰的data constructor解构（其实就是反向的类型转换，构造的时候是把t类型转换成t'类型，解构的时候就是把t'类型转换回t类型）的例子：

let tc(x) = M in ...

这里M就是t'类型的，结构出来的x就是t类型的，用法其实和2.1是一样的（因为都是data constructor）。

注意，如果有从t到t'的类型转换器tc，那么所有的t类型都能（通过这个转换器）转换成t'类型。但是反过来，对于t'类型的项，只有形如tc(M)的才能转换回t类型。

从这个角度来看，写的时候要考虑一下转换器应该是把哪个类型t转换成哪个类型t'，遵从现实的语义。例如，定义一个type converter来把128-bit key转换成bitstring是合规的，因为所有的128-bit key都能表示成bitstring，但是不是所有的bitstring都能表示成128-bit key。

3 `nat`自然数

在ProVerif里用皮亚诺公理（Peano Axiom）来描述自然数，简单描述就是定义0是一个自然数，然后每个自然数都有一个唯一的后继元素，用一个后继函数来产生，得到的后继元素也是一个自然数。然后ProVerif里的自然数有专门的内置类型nat，并支持一系列的中缀运算：

内置的is_nat(M)函数可以用来判断任意项（arbitrary term）M是不是一个自然数。

从上面的表中可以看出，两个任意项M之间的加法是不允许的。序关系>、<、>=、<=内部是用布尔型的解构器来实现的，如果关系的两边都是自然数那么就按日常理解的关系来做比较返回true或者false，只要有一边不是自然数，那么这个比较就会失败。另外，M - i中如果M < i那么也会失败，因为ProVerif中不允许出现负数。

由于自然数是用Peano Axiom生成的，所以攻击者可以生成所有的自然数。ProVerif不允许自己定义新的自然数，即不能有类似于：

new k : nat

因为这样做就会破坏Peano Axiom。同理，用户自定义的constructor也不能把nat作为返回类型，但是可以作为constructor的参数，所以是可以作为destructor的参数和返回类型的。

下面这个例子展示了对nat类类型的使用，可以注意到解构器idec里可以把nat作为返回值类型。

(* 对称密钥 *)
type key.
(* 公共通道 *)
free c: channel.
(* 秘密消息 *)
free s: bitstring [private].(* constructor：用key对nat加密 *)
fun ienc(nat, key): bitstring.
(* destructor：用key对加密结果解密，如果本来明文是x，现在得到的是x-1 *)
fun idec(bitstring, key): nat
reduc forall x: nat, y: key; idec(ienc(x + 1, y), y) = x.(* 查询秘密消息s是否不会被攻击者获取，即s的保密性 *)
query attacker(s).(* 主进程 *)
process(* 创建一个密钥k，然后 *)new k: key; ((* 将使用k加密的ienc(2, k)从通道c发出去 *)out(c, ienc(2, k))| ((* 从通道c读取nat类型x *)in(c, x: nat);(* 从通道c读取bitstring类型y *)in(c, y: bitstring);(* 尝试对y解密，只要x + 3 大于 解密结果，就把秘密消息s公布到通道c  *)if x + 3 > idec(y, k) then out(c, s)))

因为加密时用的数x + 1是2，所以解密出来的是1，x + 3 > 1是恒成立的，所以攻击者只要随便向通道c里传入一个数就能让这个判定成立，从而让s发送出去完成窃取：

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

另一方面，如果把>号左侧的3移动到右侧变成减法：

(* 尝试对y解密，只要x 大于 解密结果 - 3，就把秘密消息s公布到通道c  *)
if x > idec(y, k) - 3 then out(c, s)

验证结果就变了：

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

这是因为idec(y, k)仅当y是一个合规的构造结果的时候（也就是主进程里发的ienc(2, k)）才能解构成功，所以成功的时候解构结果一定是1，而1 - 3是不合规的（ProVerif里不允许出现负数），所以这个条件到这就直接fail掉了，也就无法完成窃取。

4 enriched terms

为了灵活性，ProVerif将项目（term）扩充定义，如下：

这里大部分的语义都是比较清楚的，比如：

就是先从通道c读取x和y两个bitstring，然后如果x是A或者B就要把z从通道c发出去，但是发的时候，如果y = A那么就让z = (x, n)（其中n是一个新的bitstring），否则就让z = (x, y)。

这个process的一个更清楚的写法是：

加的括号只是为了阅读上更清晰。

5 `table`和key distribution

ProVerif用table来实现持久存储，其定义形如：

table d(t1, ..., tn).

在进程里面对table进行填充和访问，但是没法删除，table不能被攻击者访问（就像数据库里的数据没法直接被攻击者获取一样）。有关table的语法：

第一条是向table d里面插入数据(M1, ..., Mn)，然后执行过程P。

第二条是从table d里获取能够匹配模式(T1, ..., Tn)的数据，如果能获取到相匹配的数据就执行P，否则执行Q。

第三条是从table d里获取能够匹配模式(T1, ..., Tn)的数据，然后获取到的数据还要能够满足条件M，如果成功就执行P，否则执行Q。

上面是用作process的情况，用作enriched term时候也是类似的：

其实就是条件满足的时候这个term就取用in后面的term，否则就取用else后面的term。

table还可以用作密钥管理，在后面学Needham-Schroeder公钥协议的时候能看到case。

6 `phase`相

phase，相，表达的是进行执行的不同“阶段”，是通过给进程指令加入标号来区分不同的阶段的。

默认的不带标号的指令都是在0阶段，所以不能显式的指定0阶段。

阶段的语义是，从000阶段开始执行，当从第iii阶段到第i+1i+1i+1阶段的时候，会去执行第i+1i+1i+1阶段的指令，并且所有≥i+2\geq i + 2≥i+2阶段的指令都会被丢弃。

阶段可以用来证明前向保密（forward secrecy）协议，它是指即使一些秘密被泄露了（一般就是密钥泄露发生的破坏），那么在这种泄露发生之前交换的信息也不会遭受威胁。

例如，在阶段111的时候把密钥泄露，阶段000所交互的信息s仍然是保密的：

(* Symmetric key encryption *)
type key.
fun senc(bitstring, key): bitstring.
reduc forall 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 forall 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 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).let clientA(pkA:pkey,skA:skey,pkB:spkey) = out(c,pkA);in(c,x:bitstring); let y = adec(x,skA) inlet (=pkA,=pkB,k:key) = checksign(y,pkB) inout(c,senc(s,k)).let serverB(pkB:spkey,skB:sskey,pkA:pkey) = in(c,pkX:pkey);new k:key; out(c,aenc(sign((pkX,pkB,k),skB),pkX));in(c,x:bitstring); let z = sdec(x,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)) |(* 这里是阶段1的时候才把skB泄露 *)phase 1; out(c, skB) )

验证结果：

--------------------------------------------------------------
Verification summary:Query not attacker_p1(s[]) is true.--------------------------------------------------------------

如果泄露的是skA不是skB：

(* 这里是阶段1的时候才把skA泄露 *)
phase 1; out(c, skA) )

那么攻击者就能拿着这个密钥去获取之前交互的信息了，所以阶段000的s就会被窃取：

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

7 `sync`同步

关键字sync用来实现process的全局同步，它的功能有点像上面学习的phase。同步有一个等级和一个标记，形如

sync t [tag]

其中t就是同步的等级（level），tag就是同步的标签。具有相同等级和相同标签的同步被视为相同的同步，所以相同的同步只能被用于if、let、let ... suchthat、get的不同分支里，因为同一时刻只能有一个分支在执行，所以同一时刻至多只有一个“相同的同步”能到达。

全局同步是按level升序执行的，在执行level为t的同步的时候，进程会执行到level为t的同步的所有tag都到达的程序点。

比如，假设t就是最小同步等级，然后在这个等级的tag有tag1…tagn，那么进程就会执行到到达tag1…tagn这些程序点（各一个），然后就会一起执行掉这些同步命令，然后再继续往下执行。

和phase不同的是，同步是不会丢弃进程片段的。

同步的tag以下面的方式确定：

用户可以用sync t [tag]来指定，如果用户忽略了tag，只写sync t，那么ProVerif会分配一个新tag。
如果同步被用在process macro里，那么在这个macro展开的地方可以指定tag的前缀（prefix），形如[sync: tag prefix p]，然后在宏展开的时候就会把这个前缀补上，比如：

其实就是把T1和T2这两个前缀加到T前面去了，并且补上下划线变成T1_T和T2_T两个tag。这个功能是有必要的，当一个process macro被复用的时候，特别是多个做并发的时候，按理说这些同步点的tag就应该是不一样的（不然就成了“相同的同步”），所以即使[sync: tag prefix p]被省略了，实际上ProVerif也会自动加入一个新的前缀让它们区分开。如果要强制不加前缀，那么就使用[sync: no tag prefix]。

对于测试分支，不同分支里的同步应该有相同的tag名，不然的话就容易导致同步的阻塞（block），因为两个分支只能走一个但是缺要求同步的时候走到所有的不同的tag标记点。所以应该这样写：

分别对应process macro内和外的写法。