当前位置 : 主页 > 大数据 > 区块链 >

Scyther-Semantics and verification of Security Protocol 翻译 (第二章 2.2.2)

来源:互联网 收集:自由互联 发布时间:2021-06-22
2.2.2 事件顺序 协议中的每个角色对应于事件列表,换句话说, 在属于角色 R 的协议事件集上施加结构,总的排序表示为 $ \prec $ , 如此任何角色 R∈Role 和 $\varepsilon 1$ ,$\varepsilon 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 视为通信顺序过程的集合。每一个顺序组件由特定的角色承载。通信由装饰事件的标签管理,因为标签直接决定了通信的关系  ?。

定义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}$ )

网友评论