一种改进的安全协议认证测试分析方法*

2014-02-10彭代渊

通信技术 2014年8期

关键词：发起者结点测试方法

熊玲,彭代渊

(1.保密通信重点实验室,四川成都610041;2.西南交通大学,四川成都610041)

一种改进的安全协议认证测试分析方法*

熊玲1,2,彭代渊2

(1.保密通信重点实验室,四川成都610041;2.西南交通大学,四川成都610041)

认证测试方法是以串空间模型为基础的一种形式化分析方法。该方法在协议形式化分析过程中具有简洁、清晰等优点,然而,认证测试方法不能检测类型缺陷攻击,文中着力于研究认证测试方法的定义、输出测试定理、输入测试定理以及主动测试定理,以ISO/IEC9798-3协议的安全性分析为例指出认证测试方法的局限,在此基础上重新修改认证测试方法的相关定义,提出新的改进方案,新的认证测试方法扩大了认证测试理论的应用范围。

安全协议认证测试串空间

0 引言

串空间理论因为其简单清晰的证明过程被广泛应用于协议安全形式化分析中[1]。2000年,Guttman和Thayer在文献[2]中首次提出了基于串空间理论的认证测试方法。随后Guttman于2002年对认证测试理论作了进一步的研究,为认证测试定理开辟了新的空间[3]。认证测试方法以挑战-应答机制来验证协议安全属性,具有简洁、清晰等优点,然而,目前认证测试方法不能有效检测类型缺陷攻击。国内学者杨明和罗军周提出了一种增强型的认证测试方案,该方案解决了安全协议关联属性问题[4],使协议分析人员可以比较方便的进行手动分析,更利于自动化工具的实现。刘家芬和周明天在文献[5]的基础上改进了认证测试方案,突破了认证测试元素在整个协议消息中不能被多重加密的限制,扩展了认证测试理论的应用[6]。

本文着力于研究认证测试方法的测试定理,通过分析ISO/IEC9798-3协议的安全性来说明认证测试不能抵抗类型缺陷攻击的局限,在此基础上提出了一种改进的认证测试方法,新的方法具有更广泛的应用。

1 认证测试

1.1 符号与约定

本文使用的符号说明如下:

A、B表示协议的参与方。

K表示密钥。

RA和RB分别表示为A和B的随机数。

CertA和CertB分别表示为A和B的公钥证书,证书中包含了公钥,身份识别码等信息。

{M}K表示用密钥K加密消息M。

P表示攻击者可能获得的所有消息的集合。

1.2 基本概念和定理

下面介绍认证测试中基本概念和定理[1]:

定义1 组成元素(Component)：项t0称为项t的组成元素,当且仅当t0不属于级联类型,且对任何t0≠t1,均有t0⊂t1⊂t。即组成元素或者是原子项,或者是密文,简称元素。

定义2 新元素(New Component)：若t0是结点＜S,i＞的新元素,当且仅当t0是＜S,i＞的组成元素,且不是其他任意结点＜S,j＞,(j＜i)的组成元素。

定义3 变换边(Transformed Edge)/变换进行边(Transforming Edge)：若＜S,i＞圯+＜S,j＞是关于值a的变换边,当且仅当a在结点＜S,i＞发送,且a在结点＜S,j＞以新元素形式接收。若＜S,i＞圯+＜S,j＞是关于值a的变换进行边,当且仅当a在结点＜S,i＞接收,且a在结点＜S,j＞以新元素形式发送。

定义4 测试元素(Test Component)/测试(Test)：t={h}k是结点n关于a的测试元素,如果a⊂t,且t是结点n的组成元素,t不是串空间∑中其它常规结点的组成元素的子项。

如果值a在唯一起源于结点n0,且边n0圯+n是关于a的转换边,则称边n0圯+n是a的一个测试。

定义5 输出测试(Outgoing Test)：边n0圯+n1是元素t={h}k关于a的输出测试,如果①边n0圯+n1是a的一个测试;②K∉KP;③a不在结点n0的除t以外的任何其他元素中出现;④t是结点n0关于a的一个测试元素。

定义6 输入测试(Incoming Test)：边n0圯+n1是元素t={h}k关于a的输入测试,如果①边n0圯+n1是a的一个测试;②K∉KP;③t是结点n1关于a的一个测试元素。

定义7 主动测试(Unsolicited Test)：接收结点n是元素t={h}k关于a的主动测试,如果①t是结点n1关于a的一个测试元素;②K∉KP。

定理1 输出测试定理：假设丛C中,n0,n1∈C,边n0圯+n1是元素t关于a的输出测试,则:①必然存在结点m,m′∈C满足t是m的组成元素,并且边m圯+m′是a的测试进行边;②若a在结点m′的元素t={h}k中出现,t不是任何其它常规结点的元素,且K∉KP,则必然存在一个包含t为组成元素的常规结点,且该结点为负结点。

定理2 输入测试定理：假设丛C中,n0,n1∈C,边n0圯+n1是元素t关于a的输入测试,则必然存在常规结点m,m′∈C满足t是m′的组成元素,并且m圯+m′是a的测试进行边;

定理3 主动测试定理：假设丛C中,n∈C,且n是元素t关于a的主动测试,则必然存在常规正结点m∈C,使得t是m的组成元素。

2 认证测试的局限性研究

下面通过利用ISO/IEC9798-3协议的分析来说明认证测试的局限。

2.1 ISO/IEC9798-3协议

目标:A和B完成双向认证。

交互过程:

其中交互传递过程中的A和B表示身份识别码,SA和SB分别为A和B的私钥。

定义8设(∑,P)是一个渗透串空间,如果∑由下述3种串组成,就称它为ISO/IEC9798-3串空间:

1)攻击者串。

2)发起者串Init[A,B,RA,RB],其迹为:

3)响应者串Resp[A,B,RA,RB],其迹为:

图1 ISO/IEC9798-3协议串空间模型Fig.1 Strand space model of ISO/IEC9798-3

2.2 发起者对响应者的认证

发起者保障:假设

1)ISO/IEC9798-3协议的串空间∑中,C为包含发起者串Si∈Init[A,B,RA,RB]的丛,并且发起者串的C-height为3。

2)SA∉KP,SB∉KP。

3)RA在∑中唯一源发。

需要证明的是丛C中一定包含响应串Sr∈Resp[A,B,RA,RB],且该响应者串的C-height为2。

证明：根据ISO/IEC9798-3协议的丛图,RA在∑中唯一源发于节点＜Si,1＞,并且＜Si,1＞圯＜Si,2＞构成变换边,又因SB∉KP,则边＜Si,1＞圯＜Si,2＞构成{RB‖RA‖A}SB关于RA输入测试,{RB‖RA‖A}SB为RA的测试元素。根据输入测试定理,丛C中存在常规结点m和m′,使得{RB‖RA‖A}SB为m′的组成元素,并且边m圯+m′为RA的变换进行边。

根据输入测试定理,结点m′为正结点,且m′为响应者串Sr中的结点,m′=＜Sr,2＞,且{RB‖RA‖A}SB为m′的组成元素。由于常规正结点中包含{RB‖RA‖A}SB形式的只有＜Sr,2＞,且该串的C-height为2。所以C中必然存在一个响应者串Resp[A,B,RA,RB]。

根据上面的分析,发起者A能够对响应者B的身份进行成功认证。

2.3 响应者对发起者的认证

响应者保障:假设

1)ISO/IEC9798-3协议的串空间∑中,C为包含响应者串Sr∈Resp[A,B,RA,RB]的丛,并且响应者串的C-height为3。

2)SA∉KP,SB∉KP。

3)RA≠RB,且RB在∑中唯一源发。

需要证明的是丛C中一定包含发起者串Si∈Init[A,B,RA,RB],且发起者串的C-height为3。

证明：根据协议丛图RA≠RB,且RB唯一起源于＜Sr,2＞,由于SA∉KP,所以边＜Sr,2＞圯＜Sr,3＞构成{RA‖RB‖B}SA关于RB输入测试,{RA‖RB‖B}SA为RB的测试元素。根据输入测试定理,丛C中存在常规结点m和m′,{RA‖RB‖B}SA为m′的组成元素,并且边m圯+m′为RB的变换进行边。

常规正结点中包含{RA‖RB‖B}SA形式的只有＜Si,3＞,且{RA‖RB‖B}SA为m′的组成元素,且该串的C-height为3。故C中必然存在一个发起者串Si∈Init[A,B,RA,RB]。

根据上面的分析,发起者B能够对响应者A的身份进行成功认证。

2.4 安全性分析

根据认证测试分析得出ISO/IEC9798-3协议满足双向认证,然而实际上ISO/IEC9798-3协议中响应者对发起者认证测试存在漏洞,图2是该协议的攻击过程。这是由于认证测试理论对测试元素的定义有局限,2.3节丛C中存在常规结点m和m′, {RA‖RB‖B}SA为m′的组成元素,并且边m圯+m′为RB的变换进行边。如果针对测试元素{RA‖RB‖B}SA,这种方法并没有问题,然而实际上响应者B并没有将RA与前一轮使用的RA进行一致性验证,现有的认证测试方法并没有考虑该种情况,攻击者可以冒充发起者A将{R′A‖RB‖B}SA发送给相应者B,B认为是A,从而攻击成功。

图2 ISO/IEC9798-3协议串空间攻击模型Fig.2 Attack strand space model of ISO/IEC9798-3

3 改进的认证测试方案

基于以上分析,重新定义认证测试相关定义。

定义9 新输入测试(incoming test)：边n0圯+n1是元素t′={h′}k关于a的输入测试,如果①边n0圯+n1是a的一个测试;②K∉KP;③h′∩h={…a…},其中t={h}k是结点n1关于a的一个测试元素。

定理4 新输入测试定理：假设丛C中,n0,n1∈C,边n0圯+n1是元素t′关于a的输入测试,则必然存在常规结点m,m′∈C满足t′={h′}k,a⊂t′是m′的组成元素,并且m圯+m′是a的测试进行边。

4 结语

本文通过认证测试方法对ISO/IEC9798-3协议进行形式化实例分析,指出现有的认证测试不能抵抗类型缺陷攻击,在此基础上重新定义了认证测试方法的相关定义,并提出改进的方案,显然改进的方案扩大了协议的形式化分析范围。

认证测试方法具有简洁、清晰的优点,但是目前认证测试方法主要对密码协议的认证属性进行形式化分析,下一步工作将继续研究认证测试方法对密码其它安全属性的形式化分析,其次是安全协议形式化分析自动化工具的实现。

[1] 高悦翔,李敏.基于串空间模型的WAI密钥协商协议分析[J].通信技术,2008,41(12):313-315.

GAO Yue-Xiang,LI Ming.Analysis of WAI Key Agreement Protocol based on the Strand Space Model,Communication Technology.2008,41(12):313-315.

[2] GUTTMAN JD,FABREGA FJT.Authentication Tests [C]//Proc.of the 2000 IEEE Symp on Security and Privacy.Los Amitoses:IEEE Computer Society Press, 2000.96-109.

[3] GUTTMAN JD,FABREGA FJT.Authentication tests and the structure of bundles[J].Theoretical Computer Science.2002,283(02):333-380.

[4] 杨明,罗军舟.基于认证测试的安全协议分析[J].软件学报,2006,17(01):148-156.

YANG Ming,LUO Jun-zhou.Analysis of Security Protocols Based on Authentication Test.Journal of Software, 2006,17(1):148-156.

[5] PERRIG A,SONG D.Looking for Diamonds in the Desert -Extending Automatic Protocol Generation to Three-Party Authentication and Key Agreement[C]//Proc.of the 13th IEEE Computer Security Foundations Workshop.Los Amitoses:IEEE Computer Society Press,2000.64-76.

[6] 刘家芬,周明天.突破认证测试方法的局限性[J].软件学报,2009,20(10):2799-2809.

LIU Jia-fen,ZHOU Ming-tian.Overcome the Limitation on Authentication Test[J].Journal of Software,2009, 20(10):2799-2809.

XIONG Ling(1983-),female,M.Sci., engineer,majoring in cryptography theory.

彭代渊(1955—),男,博士,教授,主要研究方向为编码理论,信息安全。

PENG Dai-yuan(1955-),male,Ph.D.,professor, mainly working at coding theory and information security.

An Improved Authentication Test for Security Protocol Analysis

XIONG Ling1,2,PENG Dai-yuan2
(1.Key Laboratory of Confidential Communication,Chengdu Sichuan 610041,China; 2.Southwest Jiaotong University,Chengdu Sichuan 610041,China)

Authentication test is a new type of formal analysis based on strand space model.Compared with strand space model,authentication test is simpler and clearer.However,authentication test cannot detect type flaw attack.This paper focuses on the definition of authentication test,outgoing test theorems,incoming theorems and unsolicited test theorems,and takes ISO/IEC9798-3 protocol as an example,then points out deficiency of authentication test.It modifies the definition of authentication test,and proposes an improved authentication test theory.Compared with original method,the new approach could expand the application scale of the authentication test theory.

security protocol;authentication test;strand space

TP393

1002-0802(2014)08-0951-04

10.3969/j.issn.1002-0802.2014.08.022