检测类型缺陷的形式化构造攻击方法
2021-03-03王建华
王建华, 张 岚
1. 93114 部队, 北京 100195
2. 信息工程大学, 郑州 450001
1 引言
形式化方法用于安全协议分析已有四十多年的发展历史, Dolev-Yao 模型[1]开创了安全协议形式化方法的先河, 定义了协议并发运行环境的形式化模型、密码算法无关的验证以及攻击者行为等, 奠定了安全协议形式化方法研究的基础. 人们在安全协议的设计和分析上投入了大量的精力, 形成了为数众多的研究方法和理论. 逻辑推理方法[2–5]虽然可以发现安全协议设计出错的原因, 但是由于抽象性较高, 不能发现协议存在的攻击且难以反映协议运行整个过程, 有着自身的局限性. 模型检测技术[6–8]是验证有限状态系统的自动化分析技术, 可以发现协议存在的攻击, 但最大的不足就是无法避免状态空间爆炸问题. 定理证明技术是用逻辑符号对安全协议进行模型化, 再用定理证明技术证明安全协议的正确性, 具有代表性有Paulson 的归纳法[9]和串空间模型[10].
密码协议自设计之初就遭受各种各样形式化分析方法[2–6]的检测, 由于协议运行时的高并发性、设计者能力程度的差异性、应用环境的复杂性,导致了诸如消息重放、中间人、并行会话等众多协议缺陷攻击[7]被相继发现. 类型缺陷攻击[8]由于消息格式的相似性而导致部分消息类型重置, 是最不易检测到的一类攻击. 为此各类形式化方法陆续用于检测类型缺陷攻击, 基于定理证明器的Paulson 归纳法[9]分析了ffgg 协议[11]以及Yahalom-Paulson 协议[12], 分析结果显示是安全的, 实则暗含着类型缺陷攻击[13]. 串空间理论构造攻击方法[14]通过密码协议中各个状态的偏序关系构造非空集合, 遍历Dolev-Yao 模型[1]约定的攻击者能力规则集, 分析检测该非空集合的最小元节点是否在攻击者串上, 由于不能识别未知的消息类型属性, 未能发现文献[11,15] 出现的类型缺陷攻击; 文献[16] 改进了串空间理论构造攻击方法, 通过检测含有测试元素的非空集合极小元节点后续的发送和接收情况, 实例化攻击者串, 可用于形式化验证;认证测试理论[17]是基于串空间模型提出来的一种用于证明安全协议认证属性的方法, 虽然简化了协议认证属性的证明过程, 但是对于未知的消息类型属性仍旧不能识别; 文献[18] 改进了认证测试方法, 定义了消息类型属性, 提出若测试元素中随机数类型之前的类型与变换后的组成元素类型一致, 则存在类型缺陷攻击, 该论断仅是一些协议类型缺陷特例, 对于像ffgg* 协议[16]中的类型缺陷仍然发现不了; 文献[19] 通过引入一个多分支标签树, 建立一个强攻击者模型, 并做了分类用以扩展串空间模型, 用于检测密码协议中的类型缺陷攻击. 文献[20,21] 总结了类型缺陷攻击形式, 给出了设计认证协议时检测类型缺陷攻击的方法, 为后续理论研究类型缺陷攻击提供了很好的借鉴. SAT 模型检测器[22]增加了消息类型匹配算法,用于检测类型缺陷攻击. 文献[23—25] 在协议格式中引入类型标签并强制检查, 虽然能检测类型错误攻击,但是会大大增加协议执行的代价. 对于采用CAESAR[26]中带有关联数据认证加密模式的密码协议, 认证码是对报头和报文密文所做的密码处理, 任何数据的改变都会影响认证码的完整性, 但是在选择明文攻击条件下, 攻击者可以对包括认证码在内的指定的协议数据进行修改替换, 进而达到类型缺陷攻击的意图,因此, 只有在设计协议时充分考虑到类型缺陷, 才能从根本上阻止类型缺陷攻击.
类型缺陷攻击自被发现以来, 关于该攻击的类型相似性机理一直没有得到详细研究, 仅仅是停留在表面, 没有从产生该攻击的本质层面考虑, 而且公开相关文献也没有关于消息类型结构的成熟研究. 本文从类型缺陷攻击的消息类型相似性机理入手, 着重研究密码协议原子类加密数据消息类型结构, 指出若密码协议消息序列中存在一组消息类型同态性、相似性、等价性等代数结构的原子类消息加密数据, 则该协议存在类型缺陷, 并给出了设计密码协议时应该遵循的准则; 克服了其它形式化分析方法不能识别消息类型的相似性等结构而导致类型缺陷的不足, 发现了Wide-Mouth Frog 协议[11]的新攻击.
2 基本概念、性质与定理
为了更清晰地阐述检测类型缺陷的形式化构造攻击方法, 便于理解后续章节的符号、名词以及内容,给出了与该形式化构造攻击方法有关的基本概念、性质、引理与定理.
定义1(原子消息集) 原子消息集表示为M0={Nounce,Time,Serial,Key,ID,··· ,Ø},其中Nounce表示随机数, Time 表示时间戳, Serial 表示序列号, ID 表示标识符, Key 表示密钥(公钥、私钥、对称密钥、签名密钥等),Ø表示空消息.
原子消息之间的运算法则由串接和密码运算f(包括加密、解密、签名等) 组成, 使用“x||y” 表示原子消息x与y的串接, 使用“{x1,x2,··· ,xn}k(k ∈Key)” 表示原子消息k对消息序列xi(i=1,2,··· ,n)进行密码运算. 经过串接或密码运算组合合成密码协议中的消息项.
定义2(原子类消息加密数据) 密码协商协议中, 对于消息加密数据t={h}k, 若消息数据序列h中,无形如{···}k的原子消息复合数据, 则称加密数据t为原子类消息加密数据.
定义3(消息类型集) 消息类型集表示为T={R,K,I,Ci(i=1,2,···),Ø,···}, 其中R表示随机因子类,K表示密钥类, 且K/∈KP,KP表示攻击者密钥,I表示主体标识类,Ci(i=1,2,···) 表示第i重密文类,Ø表示空类型,D表示未知原子数据类(密钥、标识、随机因子、密文类、空类型、协商数据等).
消息类型之间的运算法则Tf与原子消息之间的运算法则f相似, 也由串接和密码运算组成, 使用“X||Y” 表示原子消息类型X与Y的串接, 使用“{X1,X2,··· ,Xn}K(K ∈Key)” 表示原子消息密钥类型K对消息类型序列Xi(i=1,2,··· ,n) 进行密码运算. 对于x ∈M,
因此, 根据定义4 可知, 对于∀x,y ∈M,Tf(x)*Tf(y)=Tf(x°y), 即类型映射运算满足同态关系.
定义5(消息-类型同态映射) 密码协议中, 若存在类型映射Tf:M1→T1,M1⊆M,T1⊆T, 对于∀x,y ∈M1, 满足Tf(x°y)=Tf(x)*Tf(y), 则称Tf为从(M1,°) 到(T1,*) 的一种消息-类型同态映射.
定义6(类型缺陷攻击) 通常在认证协议执行过程中, 消息的类型不是显式给出的, 这就意味着无法检查消息是否被加以正确的类型, 由此导致的协议攻击称为类型缺陷攻击.
定义7(消息类型同态结构) 密码协议中的原子类数据Aj={hj|dj,1,··· ,dj,n-1,dj,n}Keyj,j=1,2, 若至少满足以下情形之一:
(1) 若d1,1=d2,1,Tf(d1,2||···||d1,n-1||d1,n)=Tf(d1,2)*···*Tf(d1,n-1)*Tf(d1,n)(首项相同);
(2) 若d1,n=d2,n,Tf(d1,1||···||d1,n-1)=Tf(d1,1)*···*Tf(d1,n-1)(尾项相同);
(3) 若d1,1=d2,1且d1,n=d2,n,Tf(d2,2||···||d2,n-1) =Tf(d2,2)*···*Tf(d2,n-1) =P(∃P ∈T)(首尾相同);
(4) 若d1,1/=d2,1,···,d1,i-1/=d2,i-1,d1,i=d2,i,d1,i+1/=d2,i+1,···,d1,n/=d2,n(中间某一项相同),
则可称Aj(j=1,2) 为具有消息类型同态结构的一组加密数据.
定义 8(消息类型相似性结构) 密码协议中的原子类数据Aj={hj|dj,1,··· ,dj,n-1,dj,n}Keyj,(j=1,2), 若该原子类消息的对应项类型相同, 数据至少有一对不同, 即若Tf(d1,1) =Tf(d2,1),···,Tf(d1,n) =Tf(d2,n), 且至少存在一个i ∈{1,2,··· ,n}, 使i ∈d1,i/=d2,i. 则可判断Aj(j=1,2) 为具有消息类型相似性结构的一组加密数据.
定义 9(消息类型等价性结构) 密码协议中的原子类数据Aj={hj|dj,1,··· ,dj,n-1,dj,n}Keyj,(j=1,2), 若该原子类消息的数据项次序经过排列组合后, 与另一个原子类加密数据相同, 即存在一个位置置换L, 使d1,L(1)=d2,i1,d1,L(2)=d2,i2,···,d1,L(n)=d2,in. 则可称为具有消息类型等价性结构的一组加密数据.
定理1(类型缺陷攻击存在性定理I) 若密码认证协议中存在一组消息类型同态结构的原子类消息加密数据, 则该协议中存在一类类型缺陷攻击.
证明:若该协议存在一组消息类型同态结构的原子类消息加密数据, 由定义7 可知: 该加密数据可表示为:tj={hj|dj,1,··· ,dj,n-1dj,n}Keyj(j=1,2).
(1) 若d1,1=d2,1,Tf(d1,2||···||d1,n-1||d1,n)=Tf(d1,2)*···*Tf(d1,n-1)*Tf(d1,n)(首项相同),Tf(d2,2||···||d2,n)=Tf(d2,2)*···*Tf(d2,n)=P(∃P ∈T), 则令Tf(d1,2||···||d1,n)=Tf(d1,2)*···*Tf(d1,n)=P, 且d1,2||···||d1,n=d2,2||···||d2,n.由定义6 可知, 可以重放消息t1代替t2, 构造类型缺陷攻击.
(2) 若d1,n=d2,n,Tf(d1,1||···||d1,n-1)=Tf(d1,1)*···*Tf(d1,n-1)(尾项相同),Tf(d2,1||···||d2,n-1) =Tf(d2,1)*···*Tf(d2,n-1) =P(∃P ∈T), 令Tf(d1,1||···||d1,n-1) =Tf(d1,1)*···*Tf(d1,n-1)=P, 且d1,1||···||d1,n-1=d2,1||···||d2,n-1. 由定义6 可知, 可以重放消息t1代替t2, 构造类型缺陷攻击.
(3) 若d1,1=d2,1, 且d1,n=d2,n,Tf(d2,2||···||d2,n-1) =Tf(d2,2)*···*Tf(d2,n-1) =P(∃P ∈T)(首尾相同) 令Tf(d1,2||···||d1,n-1) =Tf(d1,2)*···*Tf(d1,n-1) =P,d1,2||···||d1,n-1=d2,2||···||d2,n-1. 由定义6 可知, 可以重放消息t1代替t2, 构造类型缺陷攻击.
(4) 若d1,1/=d2,1,···,d1,i-1/=d2,i-1,d1,i=d2,i,d1,i+1/=d2,i+1,···,d1,n/=d2,n(中间某一项相同),Tf(d2,1||···||d2,i-1)=Tf(d2,1)*···*Tf(d2,i-1)=P1(P1∈T),Tf(d2,i+1||···||d2,n)=Tf(d2,i+1)*···*Tf(d2,n) =P2(P2∈T). 令:Tf(d1,1||···||d1,i-1) =Tf(d1,1)*···*Tf(d1,i-1) =P1,d1,1||···||d1,i-1=d2,1||···||d2,i-1,Tf(d1,i+1||···||d1,n) =Tf(d1,i+1)*···*Tf(d1,n) =P2,d1,i+1||···||d1,n=d2,i+1||···||d2,n. 由定义6 可知, 可以重放消息t1代替t2, 构造类型缺陷攻击.
定理2(类型缺陷攻击存在性定理II) 若密码协议中存在一组消息-类型相似性结构的原子类消息加密数据, 则该协议中存在一类类型缺陷攻击.
证明:若该协议存在一组消息类型相似性结构的原子类消息加密数据, 由定义8 可知: 该加密数据可表示为:tj={hj|dj,1,··· ,dj,n-1dj,n}Keyj(j=1,2).
即若Tf(d1,1) =Tf(d2,1),··· ,Tf(d1,n) =Tf(d2,n), 且至少存在一个i ∈{1,2,··· ,n}, 使d1,i/=d2,i. 即h1与h2之间对应原子消息具有相似性, 由于t1与t2的原子消息类型一致, 而且发送数据的消息格式一致, 通过反复重放该类加密数据消息, 构造类型缺陷攻击. 举例说明如下:t1={h1|r1,i1,k}k,t2={h2|r2,i2,k}k. 其中A为发送方,B为接收方,S为可信第三方.
(1)A →S:{h1|ra,ib,k}kas
(2)S →B:{h2|rs,ia,k}kbs
(1)P(B)→S:{h2|rs,ia,k}kbs
(2)S →A:{h′21|rs1,ib,k}kas
(1)P(A)→S:{h′21|rs1,ib,k′}kas
(2)S →B:{h22|rs2,ia,k′}kbs
该实例通过消息类型的相似性构造类型缺陷攻击, 也可以因为消息类型的相似性借助于重放消息构造类型缺陷攻击, 从而使攻击者与合法主体得到认证或拥有相同密钥.
定理3(类型缺陷攻击存在性定理III) 若密码协议中存在一组消息-类型等价性结构的原子类消息加密数据, 则该协议中存在一类类型缺陷攻击.
证明:若该协议存在一组消息类型等价性结构的原子类消息加密数据, 由定义9 可知: 该加密数据可表示为:tj={hj|dj,1,··· ,dj,n-1dj,n}Keyj(j=1,2). 即存在一个位置置换L, 使d1,L(1)=d2,i1,d1,L(2)=d2,i2,···,d1,L(n)=d2,in. 由于这样的原子类消息数据不变, 仅仅是数据位置发生了平移, 根据此特点, 可以构造类型缺陷攻击. 举例说明如下: 其中A为发送方,B为接收方.
(1)A →B:{r1,r2,k12}k
(2)B →A:{r2,k12,r1}k
(1)P(A)→B:{r1,r2,k12}k
(2)B →P(A):{r2,k12,r1}k
(1)P(B)→A:{r2,k12,r1}k
(2)A →P(B):{k12,r1,r2}k
该实例通过消息类型的等价性构造类型缺陷攻击, 从而使攻击者与合法主体得到认证或拥有相同密钥.
性质1 在密码认证协议中, 对于原子类消息加密数据tj={hj}kj(j=1,2),kj/∈KP, 若h1的形式表示为h1:r1,i1,h2的形式表示为h2:r1,r2, 则h1与h2之间存在一个消息类型同态结构.
证明:对于h1:r1,i1,Tf1(r1) =R,Tf1(i1) =I; 对于h2:r1,r2,Tf2(r2) =Tf2(r1) =R. 令Tf1(i1)=Tf2(r2)=R, 又由于Tf1(r1)=Tf2(r1)=R, 根据定义7,h1与h2之间存在一个消息类型同态结构.
性质2 在密码认证协议中, 对于原子类消息加密数据tj={hj}k(j=1,2),k/∈KP, 若h1的形式表示为h1:i,k,h2的形式表示为h2:i,r1,r2, 则h1与h2之间存在一个消息类型同态结构.
证明:对于h1:i,k,Tf1(i) =I,Tf1(k) =K; 对于h2:i,r1,r2,Tf2(r2) =Tf2(r1) =R. 令Tf2(r1||r2)=K, 可得Tf1(h1)=Tf2(h2)={I,K}. 又由于Tf1(i)=I=Tf2(i), 根据定义7,h1与h2之间存在一个消息-类型同态结构.
性质3 在密码认证协议中, 对于原子类消息加密数据tj={hj}k(j=1,2),k/∈KP, 若h1的形式表示h1:r,d,i1,i2,h2的形式表示为h2:r,k, 则h1与h2之间存在一个消息类型同态结构.
证明:对于h1:r,d,i1,i2,Tf1(r) =R,Tf1(d) =D,Tf1(i1) =Tf1(i2) =I; 对于h2:r,k,Tf2(r) =R,Tf2(k) =K. 令Tf1(d||i1||i2) =K, 可得Tf1(h1) =Tf2(h2) ={R,K}, 又由于Tf1(r) =R=Tf2(r), 根据定义7,h1与h2之间存在一个消息-类型同态结构.
性质4 在密码认证协议中, 对于原子类消息加密数据tj={hj}kj(j=1,2),kj/∈KP, 若h1的形式表示为h1:T1,i1,k12,h2的形式表示为h2:i2,T2,k12, 则h1与h2之间存在一个消息类型同态性结构.
证明:对于h1:T1,i1,k12,Tf1(T1) =R,Tf1(i1) =I,Tf1(k12) =K; 对于h2:i2,T2,k12,Tf2(T2) =R,Tf2(i2) =I,Tf2(k12) =K, 可知Tf1(h1) =Tf2(h2) ={R,I,K}, 且Tf1(k12) =Tf2(k12) =K, 由定义8 可知,h1与h2之间对应原子消息具有同态性,h1与h2之间存在一个消息类型相似性结构.
性质5 在密码认证协议中, 对于原子类消息加密数据tj={hj}kj(j=1,2),kj/∈KP, 若h1形式表示为h1:T1,i1,k12,h2形式表示为h2:T2,i2,k12, 则h1与h2之间存在一个消息类型相似性结构.
证明:对于h1:T1,i1,k12,Tf1(T1) =R,Tf1(i1) =I,Tf1(k12) =K; 对于h2:T2,i2,k12,Tf2(T2)=R,Tf2(i2)=I,Tf2(k12)=K, 可知Tf1(h1)=Tf2(h2)={R,I,K}, 且T1/=T2,i1/=i2, 由定义8 可知,h1与h2之间对应原子消息具有相似性,h1与h2之间存在一个消息类型相似性结构.
性质6 在密码认证协议中, 对于原子类消息加密数据tj={hj}kj(j=1,2),kj/∈KP, 若h1的形式表示为h1:r1,r2,k12,h2的形式表示为h2:r2,k12,r1, 则h1与h2之间存在一个消息类型等价性结构.
证明:对于h1:r1,r2,k12,Tf1(r1)=Tf1(r2)=R,Tf1(k12)=K; 对于h2:r2,k12,r1,Tf2(r2)=R,Tf2(k12) =K,Tf2(r1) =R, 可得Tf1(h1) =Tf2(h2) ={R,K}, 由定义9 可知,h1与h2之间的原子消息具有等价性性,h1与h2之间存在一个消息类型等价性结构.
性质7 在密码认证协议中, 对于原子类消息加密数据tj={hj}kj(j=1,2),kj/∈KP, 若h1的形式表示为h1:r2,k12,r1,h2的形式表示为h2:k12,r1,r2, 则h1与h2之间存在一个消息类型等价性结构.
证明:对于h1:r2,k12,r1,Tf1(r2) =R,Tf1(k12) =K,Tf1(r1) =R; 对于h2:k12,r1,r2,Tf2(k12) =K,Tf2(r1) =R,Tf2(r2) =R, 可得Tf1(h1) =Tf2(h2) ={R,K}, 由定义9 可知,h1与h2之间的原子消息具有等价性性,h1与h2之间存在一个消息类型等价性结构.
性质8 在密码认证协议中, 对于原子类消息加密数据tj={hj}kj(j=1,2),kj/∈KP, 如果h1形式表示为h1:k12,r1,r2,h2形式表示为h2:r1,r2,k12, 则h1与h2之间存在一个消息类型等价性结构.
证明:对于h1:k12,r1,r2,Tf1(k12) =K,Tf1(r1) =R,Tf1(r2) =R; 对于h2:r1,r2,k12,Tf2(r1) =R,Tf2(r2) =R,Tf2(k12) =K, 可得Tf1(h1) =Tf2(h2) ={R,K}, 由定义9 可知,h1与h2之间的原子消息具有等价性,h1与h2之间存在一个消息类型等价性结构.
引理1[27]若C是一个丛, 二元关系≤C是偏序的, 则C的任意非空节点子集都有≤C最小元.
引理2[27]若{h′}K′⊂{h}K且K/=K′, 则{h′}K′⊂h.
引理3[27]自由加密假设: 若{m}k={m′}k′, 则可以推出m=m′,k=k′.
定理4若节点集合S={n ∈C:t ⊂uns-term(n)}有一个最小元节点m, 则它的符号为正.
证明:事实上, 如果m的符号是负的, 那么由丛的定义可知存在一个节点n1, 且n1→m, unsterm(n1) = uns-term(m). 在这种情形下,n1在m之前,t ⊂uns-term(n1), 所以n1∈S, 这与m是集合S的最小元相矛盾.
定理5(随机因子新鲜性) 若随机因子α在协议丛C中是新鲜的, 则存在一个节点n ∈C, 使得α唯一源发于节点n.
证明:由随机因子的新鲜性可知, 该随机因子不可重复, 即在协议丛中不存在两个不同的正节点n1,n2∈C, 使得term(n1)=term(n2)=+α. 即新鲜随机因子在协议丛C中唯一源发.
3 检测类型缺陷的形式化构造攻击方法
密码协议是在不可靠或者敌意的通信环境下, 保障一定安全特性的网络协议. 在这种环境中, 敌手对于协议可以有各种各样的攻击手段, 包括窃听、篡改、截断协议的通信, 甚至加入任何可能的消息, 把协议的消息转向到其它接收者等等. 因此, 这些因素决定了看似完美的协议, 却存在着难以察觉的缺陷. 虽然密码协议的设计过程就那么几步, 然而经过精心设计的协议往往存在一些微妙的漏洞, 这样检测协议的漏洞并加以改进就显得非常重要.
在串空间模型中, 攻击者能力使用两方面的因素来描述: 攻击者所掌握的密钥集合和根据所有已知消息构造新消息的能力. 攻击者所掌握的密钥集合用KP表示. 集合KP包含了攻击者初始知道的所有密钥, 它包括所有的公开密钥和攻击者的私有密钥, 以及根据协议规则所掌握的和其他主体会话的对称密钥,也可能会包括被一些粗心的主体丢失的密钥. 攻击者能力使用攻击串来表示, 攻击者串描述了攻击者拆分、构造、联结和使用已知密钥加解密消息的能力, 属于攻击者串的节点称为攻击者节点(用P表示), 其余称为正规者节点, 攻击者能力使用下面列出的攻击者串[29]来描述.
(a)M.〈+t〉, 其中t ∈T,T为原子消息集合;
(b)F.〈-g〉, 其中g ∈A,A为消息空间;
(c)T.〈-g,+g,+g〉, 其中g ∈A;
(d)C.〈-g,-h,+gh〉, 其中g,h ∈A;
(e)S.〈-gh,+g,+h〉, 其中g,h ∈A;
(f)K.〈+k〉, 其中k ∈KP,KP为攻击者的密钥集;
(g)E.〈-k,-h,+{h}k〉, 其中h ∈A,k ∈KP;
(h)D.〈-k-1,-{h}k,+h〉, 其中k与k-1为互逆密钥,k,k-1∈Kp,h ∈A.
由于攻击者的能力由攻击者的密钥集和攻击者串进行定义, 所以这种能力是独立于任何特定协议的.下述引理给出了攻击者的能力范畴, 符号ST表示集合S与T的差.
引理4[27]若C是一个丛, 密钥k ∈(KKP). 如果k不起源于一个正规节点, 那末对于任意节点n ∈C, 有k/⊂uns-term(n). 特别地, 对于任意攻击者节点p ∈C, 有k/⊂uns-term(p).
3.1 类型形式化构造攻击方法
检测类型缺陷的形式化构造攻击方法, 简称为类型形式化构造攻击方法, 由于其明显的代数结构特征,极易判别, 与其它形式化分析方法相比较, 更适合检测认证协议的类型缺陷. 如表1 所示. 类型形式化构造攻击方法检测是否存在一组消息-类型同态性、相似性、等价性等结构的原子类消息加密数据, 代数特征明显, 易于判别. Paulson 的归纳法基于定理证明器Isabelle 的自动实现, 分析结果安全不代表协议没有攻击, 典型应用如文献[28] 对Yahalom-Paulson 协议的分析, 及文献[11] 对ffgg 协议的分析. 串空间理论构造攻击建立关于测试元素的非空集合S, 基于Dolev-Yao 模型遍历攻击能力规则, 检测S的最小元是否在攻击者串上, 例如文献[9].
表1 协议分析方法对照表Table 1 Comparison of protocol analysis methods
证明:若密码协议原子类消息存在同态性或相似性或等价性等类型数据结构, 由同态性定义7 或相似性定义8 或等价性定义9, 以及类型缺陷攻击的定义6 可知, 该密码协议中存在类型缺陷攻击.
类型构造攻击方法步骤如下:
(1) 检测该密码协议的原子类消息是否存在同态性或相似性或等价性等类型数据结构, 若不存在, 则退出; 若存在, 则该协议存在类型缺陷, 可进入第(2) 步.
(2) 依据协议丛C中节点n的随机数a的原子类加密数据t={h}k(a ∈h) 构造一个非空集合S;根据引理1, 该非空集合S存在最小元节点n1, 遍历Dolev-Yao 攻击者模型, 判断节点n1是否在攻击者原子串上, 若不存在, 则一定在常规者串上; 若节点n1不是I={n:a ⊂n}的入口点,则在该常规者串上节点n1之前还存在另一个节点n2, 使a源发于节点n2.
(3) 由于该常规者串为发送包含随机数a的原子类加密数据t={h}k(a ∈h) 的节点值(n1) 所在串,可知在响应者串上, 根据响应者串的一般形式, 对该常规者串实例化, 得到一个伪正规串S1; 对于收到并解密包含随机数a的原子类加密数据t={h}k(a ∈h) 的节点值所在串, 可知在响应者串上, 根据响应者串的一般形式, 对该常规者串实例化, 得到另一个伪正规串S2.
(4) 若此伪正规串不满足协议规约, 则舍弃; 若满足协议规约, 根据伪正规串S1与S2, 以及随机因子的新鲜性定理和自由加密假设公理, 则可得到一个攻击串.
3.2 类型构造攻击方法的应用
类型形式化构造攻击方法, 已广泛应用于密码认证协议的形式化分析, 而且找出了一系列密码协议的类型缺陷攻击.
(a) Needham-Schroeder[15]简化版本协议如下:
(1)A →B:{Na,A}KB
(2)B →A:{Na,Nb}KA
(3)A →B:{Nb}KB
对Needham-Schroeder 简化版本协议分析如图1 所示. 一方面, 攻击者假冒主体A与B通信,同时又与A通信, 通过重放消息{Na,Nb}KA而导致中间人攻击; 另一方面, 攻击者将主体标识P当做随机数与主体B通信, 同时与主体B正常通信, 导致类型错误攻击. 究其原因存在一组消息-类型同态结构原子类加密数据t1={h1|Na,A}KB与t2={h2|Na,Nb}KA, 只有打破这种结构, 方能制止这类攻击, 如图1 中的Needham-Schroeder-Low 简化版本协议.
图1 N-S 协议及其类型构造攻击Figure 1 N-S protocol and its type construction attack
(b) Yahalom[29]简化版本协议如下:
(1)A →B:A,Na
(2)B →S:B,{A,Na,Nb}KBS
(3)S →A:{B,KAB,Na,Nb}KAS ,{A,KAB}KBS
(4)A →B:{A,KAB}KBS ,{Nb}KAB
对Yahalom 简化版本协议分析如图2 所示, 攻击者通过假冒主体A将消息{A,Na,Nb}KBS,{}NaNb发送给主体B, 并与主体B拥有攻击者构造的会话密钥NaNb, 导致类型错误攻击.
图2 Yahalom 协议及其类型构造攻击Figure 2 Yahalom protocol and its type construction attack
(c) Otway-Rees[30,31]认证协议如下:
(1)A →B:M,A,B,{Na,M,A,B}KAS
(2)B →S:M,A,B,{Na,M,A,B}KAS ,{Nb,M,A,B}KBS
(3)S →B:M,{Na,KAB}KAS ,{Nb,KAB}KBS
(4)B →A:M,{Na,KAB}KAS
对Otway-Rees 认证协议分析如图3 所示, 攻击者假冒主体B发送消息M,{Na,M,A,B}KAS给主体A, 并与主体A拥有攻击者构造的会话密钥M,A,B; 又由于服务器S 产生的会话密钥KAB对于主体B而言, 识别不了它的新鲜性, 因此可诱发重放攻击; 改进后的Otway-Rees认证协议[31], 只是增加了各自的主体标识, 对于会话密钥KAB的新鲜性判别没有帮助, 所以还会导致重放攻击, 可通过添加时间戳Ts来克服这类攻击. 总之, 究其原因Otway-Rees 认证协议存在一组消息-类型同态结构的原子类加密数据:t1={h1|Na,M,A,B}KAS与t2={h2|Na,KAB}KAS, 只有打破这种结构, 才能制止这类攻击, 如图3 中d.Otway-Rees 认证协议.
图3 Otway-Rees 认证协议及其类型构造攻击Figure 3 Otway-Rees authentication protocol and its type construction attack
(d) Wide-Mouth Frog 协议[18]如下:
(1)A →S:A,{Ta,B,KAB}KAS
(2)S →B:{Ts,A,KAB}KBS
对Wide-Mouth Frog 协议分析如图4 所示, 由于主体发送的消息类型与服务器发送的消息类型一致, 导致了攻击者可以在中间不断的重发消息, 从而不断的更新时间戳, 导致诱发了类型缺陷攻击. 主要原因是该协议中存在一组消息类型相似性的加密数据, 即t1={h1|Ta,B,KAB}KAS,t2={h2|Ts,A,KAB}KBS, 只有打破这种结构, 方能制止这类攻击. 由于在改进的Wide-Mouth Frog 协议里, 仍存在一组消息类型同态性的加密数据, 即t1={h1|Ta,B,KAB}KAS,t2={h2|A,TS,KAB}KBS, 由性质4 可知, 存在类型缺陷, 如图5 所示.
图4 大嘴青蛙协议及其类型缺陷攻击Figure 4 Wide-Mouth Frog protocol and its type flaw attack
图5 改进后的大嘴青蛙协议及其类型缺陷攻击Figure 5 Improved Wide-Mouth Frog protocol and its type flaw attack
(e) ffgg 简化版协议[11]如下:
(1)A →B:A,N2
(2)B →A:B,N1,N2
(3)A →B:A,{N1,N2,KAB}P K
(4)B →A:N1,N2,{N2,KAB,N1}P K
对ffgg 协议分析如图6 所示, 该协议的消息(3) 与消息(4) 存在一组消息类型等价性的加密数据,即t1={h1|N1,N2,KAB}P K,t2={h2|N2,KAB,N1}P K, 导致类型缺陷, 使主体A和B之间的共享密钥KAB不仅没有得到彼此确认, 而且共享密钥KAB泄漏了, 如图6(b). 只有打破这种结构, 方能制止这类攻击, 改进后的ffgg 协议如图6(c).
图6 ffgg 协议及其类型缺陷攻击Figure 6 ffgg protocol and its type flaw attack
3.3 密码认证协议的设计准则
针对密码认证协议设计面临的类型缺陷形式化弊端, 给出了无消息-类型同态性、相似性、等价性等密码协议设计准则, 使密码协议设计渐趋精细化、标准化、科学化.
提出在密码协议设计中应遵循的准则: 在密码协商协议中,
(1) 无消息-类型同态性结构: 协议消息序列中原子类消息加密数据项之间无消息-类型同态性结构.(2) 无消息-类型相似性结构: 协议消息序列中原子类消息之间无消息-类型相似性结构.(3) 无消息-类型等价性结构: 协议消息序列中原子类消息之间无消息-类型等价性结构.
4 实例分析
Yahalom-Paulson 协议是由Paulson 在文献[12] 中给出的. 该协议整体框架与原始Yahalom 协议一致, 共三个参与实体: 协议发起者、协议响应者和可信第三方服务器. 协议使用对称密钥加密, 完成协议发起者与响应者之间的相互认证以及会话密钥的秘密分发. 描述如下:
(1)A →B:A,Na
(2)B →S:B,Nb,{A,Na}Kbs
(3)S →A:Nb,{B,K,Na}Kas,{A,B,K,Nb}Kbs
(4)A →B:{A,B,K,Nb}Kbs,{Nb}K
使用检测类型缺陷的构造攻击方法对该协议进行分析.
命题1若Σ 是一个三方协议串空间,C是Σ 的一个丛,Kas/∈KP,Kbs/∈KP,K/∈KP,KP是攻击者已知的密钥集合, 则对所有的节点m ∈C,{Kas,Kbs,K}/⊂uns-term(m).
证明:因为{Kas,Kbs,K}从不在一个常规节点源发, 由引理1 可知,{Kas,Kbs,K}/⊂uns-term(m).
命题2假设Σ 是一个三方协议串空间,C是Σ 的一个丛. 若下面的条件满足:
证明:首先, 根据定义7–9, 检测该密码协议的原子类消息是否存在同态性或相似性或等价性等类型数据结构. 对Yahalom-Paulson 协议进行观察可知, 该协议存在一组消息类型同态性结构的原子类加密数据:t1={h1|A,Na}Kbs与t2={h2|A,B,K,Nb}Kbs, 由定理1 可知, 存在类型缺陷. 由于Nb ⊂term(〈s,2〉), 且Nb在〈s,2〉唯一源发. 令S={n ∈C:{A,Na}Kbs ⊂uns-term(n)}, 由于{A,Na}Kbs ⊂uns-term(〈s,3〉), 所以〈s,3〉 ∈S, 因此S非空. 由引理1 可知, 集合S中有一个最小元n1, 由定理4 可知,n1的符号是正的.n1不可能位于攻击者串上, 因为攻击者串是由攻击者原子行为迹组成的, 所以只需要显示n1不可能位于攻击者原子行为迹上即可. 验证如下:
(1)M串: 若n1在M串上, 则由M串的形式〈+t〉,t ∈M0, 可知{A,Na}Kbs ⊂n1=t, 这与t仅仅是原子消息相矛盾;
(2) 显然,F串、T串、K串均不可能;
(3) 由于Kbs/∈KP, 所以D串也不可能;
(4)C串: 若n1在C串上, 则由C串的形式〈-g,-h,+gh〉, 得n1=gh, 由于{A,Na}Kbs是简单的加密值, 所以{A,Na}Kbs是g或h的子术语, 因此C串上的正节点不可能是集合S中的极小元;
(5)E串: 若n1在E串上, 则由E串的形式〈-K,-m,+{m}K〉, uns-term(n1)={A,Na}Kbs,所以{A,Na}Kbs ⊂{m}K, 由引理2 可知,{A,Na}Kbs={m}K或{A,Na}Kbs ⊂m. 若{A,Na}Kbs ⊂m, 则集合S的极小元不是正节点; 若{A,Na}Kbs={m}K, 由引理3 可知,m={A,Na},K=Kbs, 通过检查丛中常规者串节点的术语, 没有一个节点以明文的形式发送了包含{Kbs}, 因此这种情形不成立.
(6)S串: 若n1在S串上, 则由S串的形式{-gh,+g,+h}, 假定term(n1) = +g, 因为{A,Na}Kbs ⊂g, 所以{A,Na}Kbs ⊂gh, 且在S串上,-gh ≺n1, 这与n1是集合S中的最小元相矛盾.
所以,n1不在攻击者原子行为迹上, 即不在攻击者串上, 因此一定在常规者串上, 又因为节点n1不是I={n:Nb ⊂n}的入口点, 所以在该常规者串上节点n1之前还存在另一个节点n2, 使Nb源发于节点n2, 不妨设此常规者串为T.
由于常规者串T含有包括随机数Nb的最小元节点n1, 且Nb在〈S1,2〉唯一源发. 所以有:
且发送了包含原子类加密数据{C,X1}Kbs的极小元节点值{D,Nb,{C,X1}Kbs}.
对于收到并解密原子类加密数据{C,X1}Kbs的极小元节点值{D,Nb,{C,X1}Kbs}所在串的一般形式为:
由引理3 可得:X2=Nb.
由式(3)和(4)可以刻画出具体的攻击过程, 描述如下:
(1) 攻击者可以成功地冒充协议发起者.
攻击者成功冒充A, 结束时与B拥有攻击者构造的会话密钥KI.
(2) 攻击者可以成功地冒充协议响应者.
其中H为任意加密消息项, 攻击者成功冒充成B, 并与A拥有攻击者构造的会话密钥KI.
对Yahalom-Paulson 简化版本协议分析如图7 所示, 攻击者通过假冒主体A与主体B进行了两次会话, 最后成功将消息{A,B,K,Nb}Kbs,{Nb}K发送给主体B, 并与主体B拥有攻击者构造的会话密钥K; 同理, 攻击者通过假冒主体B与主体A进行了两次会话, 最后成功将消息H,{Nb}K(H为加密的未知消息) 发送给主体B, 并与主体A拥有攻击者构造的会话密钥K. 究其原因在Yahalom-Paulson 协议存在一组消息-类型同态结构的原子类加密数据:t21={h21|A,Na}Kbs与t22={h22|A,B,K,Nb}Kbs,只有打破这种结构, 方能制止这类攻击, 如图7 中Yahalom-Paulson 协议(c), 改进的Yahalom-Paulson协议具体如下:
(1)A →B:A,Na
(2)B →S:B,{A,Na,Nb}KBS
(3)S →A:{B,KAB,Nb,Na}KAS ,{Nb,KAB}KBS
(4)A →B:{Nb.KAB}KBS ,{Nb}KAB
图7 Yahalom-Paulson 协议及其类型构造攻击Figure 7 Yahalom-Paulson protocol and its type construction attack
5 结束语
检测类型缺陷的形式化构造攻击方法总结了密码认证协议中的消息类型特点, 指出了一组消息-类型同态性、相似性、等价性等原子类加密数据是类型缺陷攻击存在的充分条件, 并且结合实例分析了认证协议及其类型缺陷攻击情况, 指出了在密码认证协议设计时应遵循的准则, 为今后密码认证协议设计提供了理论依据. 下一步将继续研究并完善检测类型缺陷的形式化构造攻击方法, 研发基于该方法的密码协议自动化分析工具, 以期实现密码协议的自动化设计与分析.
