【proverif】proverif的语法-各种密码原语的介绍和具体编码

proverif-系列文章目录

1. 【proverif】proverif的下载安装和初使用
2. 【proverif】proverif的语法-解决中间人攻击-代码详解
3. 【proverif】proverif的语法2-各种密码原语的编码 （本文）

前言

在官方文档中，给出了部分密码原语（例如：对称加密、非对称加密等）的详细编码例子，接下来我们可以通过学习官方例子代码，从而进行仿写并编写出自己需要的协议编码。
官网页数很多，而纵观全网关于proverif的相关学习资料很少，这看似是一块很难啃的骨头，但是没关系，再多的讲解资料都不如官方的使用手册来的详细。所以现在我们已经拿到寻宝图的真经，跟着本博客猪一起遨游proverif的知识海。

铺垫知识

1. 声明：

• type（定义类型） ：用户可以使用 type 定义自定义类型。如定义密钥类型 key，使用type key即可。
• free（自由名称声明）：在一个输入文件中出现的所有自由名称必须使用free进行声明，并且可以通过增加 private 标志来声明该自由名称为秘密的。语法为：free n:t [private]，如声明一个 bitstring类型的自由名称 n，可以通过以下语句实现：free n:bitstring。
• fun（构造函数）：构造函数主要用于建立加密协议所使用的建模原语，如：单项哈希函数、加密和数字签名等。构造函数通过 fun 定义。语法为：fun f(t1,...,tn) : t. 如 fun enc(bitstring, key):bitstring 意味着定义一个名为 enc 的构造函数，该函数的输入有两个参数，分别为 bitstring类型和key类型，输出为bitstring类型。
• reduc（析构函数）：密码学原语之间的关系是通过析构函数进行捕获的。直接从字面意思看不是很好理解，我们可以结合前面的知识，通过定义一个完整的对称加密协议来理解。

3. 宏机制：主要提供了功能宏和进程宏。这里主要讲解功能宏。包含不止一个构造函数或析构函数应用程序的术语会重复多次。ProVerif提供了一种宏机制，以便定义表示该术语的函数符号并避免重复。
4. or fail: 每个参数的类型之后，允许用户在某些参数失败的情况下控制函数宏的行为。果存在or fail并且参数失败，则将失败值传递给函数宏，该函数宏可能会捕获它并返回一些非失败结果。

letfun f(x1:t1 [or fail]，...,xj:tj [or fail])=M.
1

5. 宏机制的应用：非对称加密

type skey.
type pkey.
type coins.
(*格式：fun 函数名（参赛类型）：输出参数的类型*)
fun pk(skey):pkey. （*公钥生成*）
fun internal_aenc(bitstring,pkey,coins):bitstring. (*加密函数*)

reduc 
	forall m:bitstring,k:skey,r:coins; （*参数名：类型*）
	adec(internal_aenc(m,pk
1
2
3
4
5
6
7
8
9