(2)集合K为密钥集合,K与T不相交,K⊆A。 (3)一元运算符 inv: kK。inv(K)为K-1。 (4)二元运算符 encr: K×AA。Encr(k,m)为{m}k。 (5)二元运算符 join: A×AA。join(a,b)为(a,b)。 (6)多元运算符 Hash:A×A…A×AA。
ቤተ መጻሕፍቲ ባይዱ
串空间证明方法-子项
(2)若节点n=<s,i>∈N,有index(n)=i并且strand(n)=s。 term(n)=(tr(s))i,即s的迹中的第i个带符号项+a或-a。定义 uns_term(n)为相应带符号项的无符号部分a。 (3) 存在边n1n2,当且仅当term(n1)=+a且term(n2)=-a,其中
定义5.2: A上的串空间是串集合Σ以及迹映射： tr: Σ (+-A)*
用串集合Σ表示串空间。
串空间证明方法-迹
迹定义:串是一个主体动作的有限序列,该序列若用
带符号项表示的话,就形成一个迹,体现为(+-A)* 的一个元素。
迹s:对串s,其迹记作tr(s),迹的长度为length(tr(s))。 s迹的第i个节点记作
Paulson 归纳法
▉消息可分解为子消息，如主体、Nonce和密钥。密 码算法被限制为Hash和加密(完善加密)。
▉消息集合H操作符：parts,analz和synth。 parts H:消息H中所有子消息的集合。 analz H:parts H子集,使用alalz H 已经存在的解
密密钥,往analz H中递归地增加解密后的子消息。 synth H:对H内的元素组合而成的集合(可用其表示
s(i).1≤i≤length(tr(s))。
记节点n在迹中的序号为index(n)。该点所在的 串为strand(n),该点的项为term(n)。
串空间证明方法-串集合Σ
:对于串集合,用表示消息的发送。
对任意的串s1,s2∈Σ。如两个主体间发送了消息,如 s1(i)=+m, s2(j)=-m,即s1的主体发送消息m给s2 的主体,则记该关系为s1(i)s2(j)。
安全协议理论与方法
定理证明类分析方法
Paulson 归纳法
▉用归纳的方法证明协议的无限状态空间，而不需 要对各个状态一一检测。
▉部分证明可使用自动化定理证明工具Isabelle， 所基于的形式化机制为高阶逻辑，通过对路径的 归纳来自动证明性质的成立。
▉方法：为协议建立形式化模型，然后基于该模型
给出一组假设、公理和引理，用递归方法分析此 协议所有状态以证明协议的正确性。
一个迹上相邻的两个节点表明了该主体的顺序相邻 的两个动作,记s(i)=>s(j),且j=i+1。
串有向图：为Σ中所有串的所有节点之间建立和=> 这样的关系,则串空间可以表示为一个有向图：
<N,(∪=>)>,N代表所有串的所有节点的集合。
串空间证明方法-串集合Σ
定义5.3:给定串空间Σ:
(1) 一个节点node是一个二元组<s,i>,s∈Σ,i为满足1≤i≤length (tr(s))的整数。tr(s)为s的迹,length(tr(s))则为串s的长 度。节点集合记为N,每个节点<s,i>属于唯一的串。
攻击者从消息中获取知识的能力)。
Paulson 归纳法
▉根据前述定义,可写出如下一组公理和引理：
Nonce N∈synth H =>Nonce N∈H {X}k∈parts H => X ∈ H {X}k∈analz H,K-1∈analz H =>X∈analz H
X∈synth H, K∈H => {X}k∈synth H
子项关系⊂递归定义如下：
(1)a ⊂ a。 (2)a ⊂ {g}k,如果a⊂g。 (3)a ⊂ (g,h),如果a⊂g∨a⊂h。 (4)a ⊂Hash(g1,…,gn),如果a⊂g1∨… ∨a⊂gn。
串空间证明方法-带符号项
定义5.1：带符号项是一个二元组<σ,a>,其中 a∈A,σ∈[+,-],记带符号项为+t或-t。（+A）*是一个集合,集合中每个元素都是一个 带符号项的有限序列,该序列可记为 <<σ1,a1>, …, <σn,an>>。
串空间证明方法
▉项及消息交互：安全协议运行时，把协议主体
之间所有可能交换的信息称之为项，如密钥，随 机数以及加密项，Hash等。 ▉项的形式化表示：令集合A中的元素为协议主体间 可能交换的消息。称A的元素为项，特别地，A可 由如下的集合元素和元素间的运算组成。
串空间证明方法-项组成
(1)集合T为原子明文集合,T⊆A。
(5) 一个无符号项t出现在节点n∈N上,当且仅当t⊂term(n)。 (6) 令I为一些无符号项的集合。定义节点n∈N是I的进入点,当且
仅当term(n)=+t,其中i∈I,且对所有的n’=>+n,term(n’)!∈I。 符号!∈表示“不属于”。 (7) 无符号项t产生于节点n∈N,当且仅当n是集合I={t’:t⊂t’} 的进入点。 (8)无符号项t是唯一产生的,当且仅当t产生于N中唯一的节点n。
串空间证明方法
▉串：协议中某个合法主体或攻击者行为事件的一
个序列串，由发送和接收的消息组成。如果某个 主体在一段时间内参与了多轮协议，则用不同的 串表示。不同的主体行为也用不同的串表示。
串空间证明方法
▉串：协议中某个合法主体或攻击者行为事件的一
个序列串，由发送和接收的消息组成。如果某个 主体在一段时间内参与了多轮协议，则用不同的 串表示。不同的主体行为也用不同的串表示。 ▉串空间：是串的集合，分为诚实主体串及攻击者串， 是协议有效时间内所有的事件序列。 ▉丛：串空间的子空间，体现协议一次运行中所有 动作之间的因果关系。
a∈A。意味着节点n1发送消息a,n2接收消息a,是串之间的一种 因果连接。 (4) 若n1=<s,i>∈N, n1=<s,i+1>∈N。则存在边n1=>n2。这里边表 示n1是n2在串s上的直接因果前驱。用n1=>*n2表示n1是n2在同一
串空间证明方法-串集合Σ
定义5.3续
(4) 若n1=<s,i>∈N, n2=<s,i+1>∈N。则存在边n1=>n2。这里边表 示n1是n2在串s上的直接因果前驱。用n1=>*n2表示n1是n2在 同一个串上的因果前驱,此时，n1=<s,i>,n2=<s,j>,i≤j。