tamarin manual总结笔记5（使用流程的模型规格）

使用流程的模型规格

在本节中，我们提供了一个非正式的描述过程演算现在集成在Tamarin。它被称为SAPIC，即“状态应用PI-Calculus”。该模型的全部细节可以在(Kremer and k nnemann 2016)和(Backes et al 2017)中找到。

可以根据规则或作为(单个)流程对协议进行建模。过程被转换成一组遵守过程演算语义的规则。甚至可以将流程声明和一组规则混合在一起，尽管不建议这样做，因为规则和流程之间的交互取决于如何精确地定义这种转换.

SAPIC演算是应用pi演算的一种方言，具有用于存储、检索和修改全局状态的附加功能。

标准应用pi特性

建模协议的主要成分是网络通信和并行性。我们从网络通信和其他为本地操作建模的构造开始。

过程out(m,n);P和in(m,n);P分别表示通道m上消息n的输出和输入。与应用的pi演算(Abadi和Fournet 2001)相反，SAPiC的输入构造执行模式匹配而不是变量绑定。

如果通道被忽略，则假定公共通道’c’，这是我们大多数示例中的情况。这正是In(m)和Out(m)所表示的。进程也可以分支:如果Pred，则执行P，否则Q将执行P或Q，这取决于Pred是否保持。到目前为止，只实现了相等性检查，因此对于项t和t’， Pred总是具有t = t’的形式。

构造new a;P绑定了P中的新鲜名称a。与Fr(a)类似，它模拟了一个新鲜的随机值的生成。

事件构造类似于规则中的操作。事实上，它将被转化为行动。与规则一样，事件对流程的某些部分进行注释，对于声明安全属性非常有用。这些结构中的每一个都可以被认为是“局部”计算。它们用分号分隔;并以0结束，即终止进程或null进程。这是一个什么都不做的过程。允许省略末尾的0进程和由0进程组成的else分支。

现在我们来看看操作的并行性建模。P | Q是进程P和进程Q的并行执行。它被用来模拟协议中的两个参与者。

!P是P的复制，它允许在协议执行中无限数量的会话。它可以被认为是无穷多个进程P |…P并行运行。如果P描述了一个回答单个查询的web服务器，那么!P是无限期回答查询的web服务器。P+Q表示外部非确定性选择，可用于对备选方案进行建模。从这个意义上说，它更接近于一个条件，而不是两个并行运行的进程:P+Q减少为P’或Q’，后续进程或P或Q分别。

操纵全局状态

其余的构造用于操作全局状态

• 结构插入m,n;P将值n绑定到键m。后续插入将覆盖此绑定。存储是全局的，但由于m是一个术语，因此可以使用它来定义名称空间。例如，如果一个web服务器是由名称w_id标识的，那么它可以为它的store添加如下前缀:

 insert <'webservers'，w_id，'store'>， data;  P.

• 构造delete m;P“取消定义”绑定。
• 在P else Q中查找m为x的构造允许检索与m相关的值，并在输入P时将其绑定到变量x。如果m的映射未定义，则过程表现为Q。
• lock和unlock结构用于获得或放弃对资源m的独占访问权，采用Dijkstra二进制信号量的风格:如果项m已被锁定，则任何后续锁定m的尝试将被阻塞，直到m已被解锁。这对于编写并行进程可以读取和更新公共内存的协议至关重要。

对于专家来说有一个隐藏的特性:内联多集重写规则:[l]–[a]-> r; P是一个有效过程。如果预置条件适用(即，左侧的事实存在)，则应用嵌入式规则，并且将流程简化为此规则。如果规则适用于当前状态，则流程减少到p。我们建议尽可能避免使用这些规则，因为它们与SAPIC的目标背道而驰:为协议建模提供清晰、可证明正确的高级抽象。还请注意，状态操作将查找x构造为v，插入x,y和删除x通过发出IsIn(x,y’)， insert (x,y)和delete (x)操作来管理状态，并通过限制强制其正确的语义。例如:表示查找成功的操作IsIn(x,y)要求操作Insert(x,y)先前已经发生，并且在此期间，没有其他Insert(x,y’)或Delete(x)操作更改了位置x的全局存储。因此，全局存储不同于当前状态下的事实集。

强制本地进度(可选)

可以修改来自进程的转换，使其执行不同的语义。在这个语义中，跟踪集只包含那些进程已经尽可能减少的跟踪集。进程可以减少，除非它正在等待一些输入，它正在复制，或者除非它已经减少到0进程。

选择:translation-progress

这可用于对超时进行建模。以下过程必须减少到P或out(‘help’);0:

( in(x); P) + (out('help');0)

如果接收到输入消息，它将产生规则，在这个例子中:p。如果没有接收到输入，除了右边没有其他方法可以进行。但进步是必须的，这样右手边的人才能制定恢复方案。

在翻译后的规则中，添加了ProgressFrom_p和ProgressTo_p事件。这里p标记了一个位置，当到达该位置时，需要出现相应的ProgressTo事件。这是通过限制来实现的。注意，工艺可能需要加工到一个以上的位置，例如:

new a; (new b; 0 | new c; 0)

进展到两个跟踪0进程。

它也可以加工成许多位置中的一个，例如这里

in(x); if x='a' then 0 else 0

更多细节可以在相应的论文中找到(Backes et al . 2017)。注意，本地进程本身并不能保证消息到达。恢复协议通常依赖于受信任的第三方，该第三方可能大部分时间都处于离线状态，但可以使用内置的可靠通道理论进行访问。

建模孤立的执行环境

IEEs或enclave允许在安全环境中运行代码，并提供enclave当前状态(包括已执行的程序)的证书。在(JKS-eurosp17?)中定义并包含在SAPIC中的应用微积分的本地化版本允许对此类环境进行建模。

进程可以被赋予一个唯一的标识符，我们称之为location:

let A = (...)@loc

位置可以是任何项(这可能取决于之前的输入)。位置是一个标识符，它允许谈论它的进程。在一个location中，可以生成一个关于某个值的报告:

(...
let x=report(m) in
...)@loc

然后，一些外部用户可以通过使用check_rep函数来验证某个值是否在特定位置产生，即由特定进程或程序产生:

if input=check_rep(rep,loc) then

只有当前面的指令产生了rep, m=input时，这才有效。

关于enclave的重要一点是，任何用户(例如攻击者)都可以使用enclave，从而为自己的进程或位置生成报告。但是，如果攻击者可以为任何位置生成报告，他就可以破坏与该位置相关的所有安全属性。为此，用户可以通过定义一个内置的Report谓词来定义一组不受信任的位置，这相当于定义一组他不信任的进程:

predicates:
Report(x,y) <=> phi(x,y)

如果phi(m,loc)为真，攻击者可以生成任意report(m)@loc。

更多细节可以在相应的论文(JKS-eurosp17?)和示例中找到。

语法糖

使用let处理声明

建议围绕流程所代表的协议角色来构建流程。这些可以使用let结构声明:

let Webserver = in(<'Get',identity..>); ..
let Webbrowser = ..
(! new identity !Webserver) | ! Webbroser
These can be nested, i.e., this is valid:
let A = ..
let B = A | A
!B

其他过程演算，例如，ProVerif的应用-pi演算方言，只允许输入变量。虽然在letblock中编写模式有时更清晰，但它可能会让期望in构造绑定变量的用户感到困惑:

let pat_m1 = <x,y> in
in(pat_m1)

为了避免意外行为，我们只允许let表达式应用于in中的单变量项，如果该变量以pat_为前缀，如上面的示例所示。

在进程中使用“let”绑定

let foo1 = h(bar)
  foo2 = <'bars', foo1>
  ...
  var5 = pk(~x)
    in
    in(<'test',y>); let response = <foo2,y> in out(response)

流程中的let绑定遵循与规则中的let绑定相同的规则。