Scyther-Semantics and verification of Security Protocol 翻译 (第二章 2.2.2)
2.2.2 事件顺序
协议中的每个角色对应于事件列表，换句话说， 在属于角色 R 的协议事件集上施加结构，总的排序表示为 $ \prec $ , 如此任何角色 R∈Role 和 $\varepsilon 1$ ,$\varepsilon 2$ ∈ RoleEvent,这样 Role($\varepsilon 1$)=R 和 role($\varepsilon 2$)=R 我们有 这样的表达：$ \varepsilon 1 \prec \varepsilon 2\vee \varepsilon 1=\varepsilon 2\vee \varepsilon 1\succ R\varepsilon 2$ 我们认为一个抽象安全协议P 视为通信顺序过程的集合。每一个顺序组件由特定的角色承载。通信由装饰事件的标签管理，因为标签直接决定了通信的关系 ↝。
SRE实战 互联网时代守护先锋，助力企业售后服务体系运筹帷幄！一键直达领取阿里云限量特价优惠。定义2.10 （通信关系）： 所有的 $\imath $∈Label ， m1, m2 ∈ Role ×Role ×RoleTerm , 通信关系 ↝ 表示为 ：
$\varepsilon 1$ ↝ $\varepsilon 2\Leftrightarrow \exists \imath $ m1,m2:$\varepsilon 1=send \imath (m1) \Lambda \varepsilon 2=read \imath (m2)$ . 该关系规定了发送协议事件和协议接受事件如何对应，
例子： 2.1.1 （事件角色和 通信关系）： 比方说 NS 协议， 角色顺序 $\prec$ i 和 $\prec$ r 是角色 i 和 r ，分别如下表示：
通信关系 ↝ 给出如下表示：
2.2.3 静态要求
在之前的章节中我么解释了抽象的协议规范语法。适当的协议规范必须满足许多良好的形式要求，并不是任何发送、声明、读取事件序列被认为是安全的协议，比方说，我们要求代理必须能够构建他发出的术语条款，如果他不知道秘钥则不能检查加密术语的内容。
良好的角色： 对于每一个角色，我么要求他符合基本的某些标准，这些范围相当的明显，例如：角色定义中的每个事件都具有相同的角色执行它（被称为该事件的参与者），关于消息的更加微小的要求。对于消息，我们要求发着的消息实际上可以有发送者构造，如果消息在发送角色中，则满足此要求。对于变量我们要求首先出现在一个读取事件中， 在该事件中被实力化，然后才能出现在发送事件中。
对于读取事件，情况要复杂的多，从上面的列子中可以看出，我们描述协议 Needham-Schroeder 初始角色，读取事件对传入的消息施加结构，以这种模式的形式，如果接受者的知识满足某些要求，那么他只能将消息与这种预期的模式相匹配。
我们介绍一种预测形式 WF （Well- Formed） 表示角色定义满足这些一致性要求，使用辅助预测 RD （Readable）和一个推论知识关系$ \vdash $ : RoleKnow × RoleTerm
角色可以组成和分解术语对，如果代理知道加密秘钥则可以加密术语，如果代理知道解密秘钥则同样可以解密加密的术语。
定义 2.12 （知识推理操作）
使用 M 作为角色知识集，知识推理关系$ \vdash $ : RoleKnow × RoleTerm 定义归纳如下： 针对所欲的角色术语 rt 、 rt1 、 rt2 、k
列子 2.13 （推理和加密）
从一个包含 {/m/}k术语的术语集，不包含$k^{-1}$ 不能够推断出 m 或者 k ,i ,e
给定术语表达式 {/m/}k 和 $k^{-1}$ ，我们能够推断 m , 如果 k 是非对称秘钥（这就是说 k 不等于$k^{-1}$ ），给定{/m/}k 和 $k^{-1}$ 不可能推断 k
例子 2.14 （推论和子项）：给定两个术语 m1 和 m2 关系是 {m1}$\vdash $m2 ,通常并不是这种 m2$ \sqsubseteq $ m1 ,给出一个反例： m1 =( rt1, rt2) 和 m2=(rt2, rt1) 当 rt1不等于 rt2的时候。反过来也没有。例如 因为给定术语 k 和 m 以及 
，我们有 k $\sqsubseteq $ {/m/}k 还有
例子 2.15 （推论和函数）给定术语 f(rt) 且 f ∈Func , 没有适用的进一步推理规则，如此推断 rt 是不可能的，在这方面，我们框架中的函数充当散列函数。我们可以放心的安全建模秘钥 （列如：k(rt1,rt2),sk(rt1)） 作为散列函数在相同的地方。正如我们后面将看到的，代理名称最初被代理和入侵者所知。建模
， 因此不会增加任何相关方的可推断条款。
（在模型中，应用推理运算符的所有集合都包括 rt1 、 rt2）
