【Proverif语法学习（一）】

1.声明（declaration）

1.1 声明变量

格式：type t.

free n:t. 表示n的类型是t，free是关键词，表示公开的，是可以被攻击者获取的。
如果不想被攻击者获取，则需要声明为私密的，关键词为private，格式如下：
free n:t [private].

1.2 声明函数

格式：fun f(t1,…,tn):t.

f是关于n的函数构造器，t是该函数f的返回值类型，t1…tn是函数f的自变量。
fun f(t1,…,tn):t [private]. 表示攻击者无法获取由函数f生成的t。**
fun senc(bitstring, key):bitstring.** 表示用类型key加密bitstring类型明文，生成的密文是bitstring类型值。

1.3 析构函数

格式： reduc forall x1,1 : t1,1,…,x1,n1 : t1,n1;g(M1,1,…,M1,k)=M1,0;
…
forall xm,1 : tm,1,…,xm,nm : tm,nm; g(Mm,1,…,Mm,k)=Mm,0.

作用：将密码学原语中的关系连接起来。
例子：reduc forall m : bitstring, k : key; sedc(senc(m,k),k) = m.
m表示明文；k表示系统密钥；senc(m,k) 用密钥 k加密明文m生成密文；sedc(senc(m,k),k)=m用密钥k解密密文senc(m,k)生成明文m。

1.4 子进程

格式：let R(x1 : t1,…,xn : tn) = P.

R是宏**（macros）**的名字，P是定义的子进程，t1,…,tn类型x1,…,xn。

1.5 主进程

格式：process A

process是关键字，相当于编程语言中的main()函数。

1.6 术语语法

假设M和N都是多项式表达式；

格式：**M = N **表示M和N相等；M<>N表示M和N不相等。
等式和不等式都是一个等式理论的模，它们接受相同类型的两个参数，并返回bool类型的结果。

格式：M&&N表示M和N是布尔连接的；M || N表示M和N是非布尔连接即布尔断开。

格式：**not(M)**表示布尔否定

例子：M || N，如果M是真的，那么N不需要计算，这个表达式的结果是真的。

1.7 进程语法

假设P和Q都是进程；

格式：P | Q表示进程P和Q是并行组成的；!P表示P | P | …,表示进程P有无限个。

格式：new n : t; P 表示在进程P中绑定类型为t的n，相当于编程语言中在类中（或函数）设置新的局部变量。

格式：in(M, x : t); P表示等待来自通道M的类型为t的消息，然后表现为P，其中接收的消息绑定到变量x，P中每次出现x都是指收到的消息，当P为0时，P可以省略不写。

格式：out(M, N); P表示在通道M发送N，然后运行进程P，当P为0时，P可以省略不写。

格式：if M then P else Q表示当M的值为真时，运行进程P；当M的值为其他值时，运行进程Q。当术语M失败时它不执行任何操作（例如，当M包含不适用重写规则的析构函数时）。

例子1：if M=N then P else Q表示如果M=N，执行P，或者执行Q
例子2：if x=M then P else Q表示如果对于M中的所有析构函数没有失败，那么x被绑定到M中，并执行P，否则执行Q。

1.8 模式匹配语法

格式：x : t表示将类型t的任何术语绑定到x。
格式：M = N表示相等测试。

1.9 关键词、注释和标识符

关键词：among, channel, choice, clauses, const, def, elimtrue, else, equation, equivalence, event, expand, fail, forall, free, fun, get, if, in, inj-event, insert, let, letfun, new, noninterf, not, nounif, or, otherwise, out, param, phase, pred, proba, process, proof, putbegin, query, reduc, set, suchthat, table, then, type, weaksecret, yield。

注释：用英文括号加星号组成，将星号放在括号内；
标识符：包括字母、数字、单引号、下划线等，第一个字符是字母，区分大小写，关键词不可做标识符。
内置类型：bitsring, bool。bool类型分为true和false。