一种新的认证协议自动验证方法

肖跃雷，朱志祥，张勇

一种新的认证协议自动验证方法

肖跃雷，朱志祥，张勇

为了实现对认证协议的自动验证，首先，通过对认证协议的协议主体行为分析，给出了驱动模型（Driving Module，DM）的定义。然后，根据串空间模型中的常规者串和攻击者串分别构建了常规者DM和攻击者DM。最后，提出了基于常规者DM和攻击者DM的自动验证算法。实例分析和定理证明表明，该算法的搜索过程不仅是全面和正确的，而且能有效地避免状态空间爆炸问题。

自动验证；驱动模型；串空间模型；认证协议

0 引言

认证协议是许多信息系统的安全基础，因而确保认证协议的正确性是至关重要的。但是，设计一个正确的认证协议是一项十分困难的任务。目前许多公布的认证协议太多都存在着各种各样的安全漏洞。为了验证认证协议的正确性，研究者们提出了许多形式化分析方法。这些形式化分析方法可以分为3类：（1）基于知识逻辑与信念的方法，如BAN逻辑[1]；（2）验证工具，如Murφ[2]、FDR[3]、NRL[4]和Athena[5]；（3）定理证明的方法，如串空间模型[6-11]。自动验证工具的优点是不需要使用人员是安全专家，而且从验证结果中可以直观地看到认证协议是如何被攻击的。但是，自动验证工具通常无法避免状态空间爆炸问题。

为了解决这一问题，本文首先分析了认证协议的协议主体行为，并定义了驱动模块（Driving Module，DM），然后，利用串空间模型（Strand Space Model，SSM）构建了常规者DM和攻击者DM，最后，提出了基于DM的认证协议自动验证算法。通过定理证明和对NSPK协议[12]的实例分析可知，该自动验证算法不仅能很快地搜索到认证协议的安全漏洞，而且能有效地避免状态空间爆炸问题。

1 新自动验证方法

1.1 符号定义

为了分析认证协议，需要对认证协议的消息符号进行了一般化定义，本文用到的消息符号为：

Xi：表示协议主体；

N*：表示未知协议主体产生的随机数；

*：表示仅能验证其长度的值；

其中，i =1,2,3……。

1.2 驱动模块

认证协议是各个协议主体之间进行的一些事件序列。认证协议执行过程中的协议主体行为主要为发送消息和接收消息。任何一个认证协议都有始发点和终止点，始发点发送消息驱动协议的进行，终止点接收消息而结束整个协议执行过程。对于认证协议执行过程的中间部分，协议主体接收消息之后必然发送新的消息给其他协议主体，这显然构成了一个驱动过程。根据以上对认证协议执行过程的分析，本文给出了驱动模块（Driven Module）的定义如下：

定义1协议主体X接收消息或不接收消息而发送新的消息给其他协议主体的协议执行过程为一个驱动模块（Driving Module，DM），X称为DM的主体。

对于一个认证协议而言，该协议的合法参与者称为常规者，而非法参与者便称为攻击者。若DM的主体为常规者，则该DM为常规者DM；否则，该DM为攻击者DM。

（1）常规者DM构建

由于常规者DM的主体为常规者，而常规者的协议执行过程必须遵守正常协议的执行规则，所以常规者DM可以根据正常协议的执行过程得到，即可以根据文献[6]所述的常规者串得到。如图1所示：

图1 NPSK协议的常规串和常规者DM

例如，NPSK协议[12]的常规者串如图1中的(a)所示，而得到的相应常规者DM图1中的(b)所示。

从图1可知，协议主体A的常规者串由常规者DM①和常规者者 DM③构成，而协议主体 B的常规者串由常规者DM②和常规者DM④构成，从而NPSK协议是由常规者DM①、常规者DM②、常规者DM③和常规者DM④按序列构成和执行的，其中常规者DM①称为NPSK协议的始发常规者DM，常规者DM④称为NPSK协议的终止常规者DM，常规者DM②和常规者DM③称为NSPK协议的过程常规者DM。

（2）攻击者DM构建

攻击者的能力主要由两方面因素来描述：一是攻击者获得它可掌握的消息；二是攻击者由它所能掌握的消息产生新消息的能力。根据文献[6]所述的攻击者串，可以得到如下攻击者DM：

①发送文本项：<+t>；

②发送密钥项：<+K>；

③级联各组件为消息：<-h1，-h2，-…， +h>；

④分割消息为各组件：<-h，+h1，+h2，+…>；

⑤加密消息：<-K，-h，+{h}K>；

⑥解密消息：<-{h}K，- K-1，+ h>。

其中，h1、h2、…为h的各个组件[7]，h为消息，K为加密密钥，K-1为解密密钥。本文用到的组件是指文本项、密钥项或加密项。

1.3 自动验证算法

由DM的定义可知，任何协议过程都可以描述成一系列DM过程。因此，不管是正常协议还是攻击协议（通常称为攻击剧本），都可利用以上定义的DM描述出来。为了得到这些攻击剧本，本文基于DM对协议过程执行自底向上的自动验证。自动验证机理如图2所示：

图2 自动验证机理

其中m1、m2、m、r1、r2、s1、s2为消息项，①表示父结点DM的接收消息都由常规者DM发送，②表示父结点DM的接收消息都由攻击者DM发送，③表示父结点DM的接收消息由常规者DM和攻击者DM共同发送。

按照图2所示的自动检验机理，对安全协议的自动检验可以形成一个DM结点搜索树。DM结点搜索树的每一条搜索路径称为DM结点路径。这些DM结点路径包括正常协议的DM结点路径和攻击协议的DM结点路径(攻击剧本的过程)。自动验证算法的具体过程如下：

以认证协议的终止常规者DM为根结点DM，依据根结点DM中接收消息的格式分别搜索该协议的常规者DM集和攻击者DM集，并按自动验证机理生成各个子结点DM，然后以可得到的各子结点DM为父结点DM再作类似的搜索，直至生成的子结点DM数为零，其中搜索过程必须满足以下条件：

（1）协议的假设条件；

（2）搜索攻击者DM中的④或⑥时，要保证它们的接收消息在分割消息集和解密消息集中；

（3）同一条DM结点路径上不能出现两个相同的DM；

（4）同一条DM结点路径上不能出现两个互成逆过程的攻击者DM。

分割消息集是指各常规者 DM的发送消息经过直接分割或分割和解密组合的间接分割过程可获得到消息集。解密消息集是指各常规者 DM的发送消息经过直接解密或分割和解密组合的间接解密过程可获得到消息集。

最后，根据文献[6]中的协议正确性定义判定哪些 DM结点路径是正常协议执行过程，哪些DM结点路径是攻击剧本执行过程，哪些DM结点路径是无效攻击过程。

2 应用实例

其中， A和B表示常规者（发起者和响应者），P表示攻击者。由于认证协议的终止常规DM在自动验证算法中是明确描述的根结点 DM，所以上述 NSPK协议的终止常规DM是明确描述的。

本文利用 C语言实现上述自动验证算法，通过输入NSPK协议的假设条件和各个常规DM的一般化描述，最终得到NSPK协议的DM结点搜索树，如图3所示：

图3 NPSK协议的DM结点搜索树

在图3的DM结点搜索树中，各个DM结点值为：1. <-

分析图3可知，DM结点①的最左边的分支树为NSPK协议的正常协议过程，而右边的 3条分支树分别构成了NSPK协议的3个攻击剧本。这3个攻击剧本的攻击效果是一致的，与文献[3]中分析结果相同，从而说明该自动验证算法是有效的。

3 分析与讨论

下面将证明该自动验证算法的搜索过程不仅是全面和正确的，而且能够有效地避免状态空间爆炸问题。

定理1 对某个接收消息搜索常规DM就是搜索常规者可以发送该消息的能力。

证明：由于常规DM是根据常规者串而得到的，所以常规DM代表了常规者发送消息的能力。常规DM空间是由各个常规DM构成的，而常规者串空间是各个常规者串构成的，所以搜索各个常规DM就相当于搜索各个常规者串，即搜索常规者可以发送该消息的能力。因此，对某个接收消息搜索常规DM就是搜索常规者可以发送该消息的能力。

定理2对某个接收消息搜索攻击DM就是搜索攻击者可以发送该消息的能力。

证明：由于攻击 DM是根据文献[6]中的攻击者串而得到的，其中攻击DM①与文献[6]中的攻击者串M相同，攻击DM②与文献[6]中的攻击者串K相同，攻击DM③与文献[6]中的攻击者串C等价，攻击DM④与文献[6]中的攻击者串S等价，攻击DM⑤与文献[6]中的攻击者串E相同，攻击DM⑥与文献[6]中的攻击者串D相同，而文献[6]中的攻击迹F和T直接隐含在DM搜索过程中，所以对某个接收消息搜索攻击DM就是搜索攻击者可以发送该消息的能力。

定理3 自动验证算法是全面的和正确的。

证明：自动验证算法是对每个接收消息搜索常规DM和攻击DM，从定理1和定理2可知该自动验证算法是全面的。搜索条件（1）是协议的假设条件，搜索条件（2）是根据协议常规DM能力来描述攻击者分割和解密消息的能力，搜索条件（3）和（4）是用于避免循环搜索的。这些搜索条件都是合理和正确的。因此，自动验证算法是全面的和正确的。

定理4 自动验证算法能有效地避免状态空间爆炸。

证明：自动验证算法采用自底向上的搜索方式，而每一条搜索路径总是收敛于搜索条件（1）～（4），所以可有效地避免了状态空间爆炸问题。

4 总结

本文提出了一种新的认证协议自动验证方法。首先，通过对认证协议的协议主体行为分析，给出了DM的定义。然后，根据串空间模型中的常规者串和攻击者串分别构建了常规者DM和攻击者DM，它们分别代表了认证协议的常规者能力和攻击者能力。最后，提出了基于常规者DM和攻击者DM的自动验证算法，并基于串空间模型中的正确性定义判定哪些DM结点路径是正常协议执行过程，哪些DM结点路径是攻击剧本执行过程，哪些DM结点路径是无效攻击过程。此外，通过定理证明和对NSPK协议的实例分析可知，该方法的搜索过程是全面和正确的，而且能够有效地避免了状态空间爆炸问题。

[1] Burrows M, Abadi M, Needham R. A logic of authentication[J]. ACM Transactions on Computer System, 1990, 8(1):18-36.

[2] Mitchell J, Mitchell M, Stern U. Automated analysis of cryptographic protocols using Murφ[A]. Proceedings of the 1997 IEEE Symposium on Security and Privacy[C]. USA: IEEE Computer Society Press, 1997：141-151.

[1] Lowe G. Breaking and fixing the Needham-Schroeder public-key protocol using FDR[A]. Tools and Algorithms for the Construction and Analysis of Systems, volume 1055 of Lecture Notes in Computer Science[C]. Beilin: Springer Verlag, 1996：147-166.

[2] Meadows C. The NRL Protocol Analyzer: an overview [J]. Journal of Logic Programming, 1996, 26(2):113-131.

[3] Song D. Athena: A new efficient automated checker for security protocols analysis [A]. Proceedings of the 12th IEEE Computer Security Foundations Workshop[C]. IEEE Computer Society Press, 1999：192-202.

[4] Thayer F. Herzog J C. Guttman J D. Strand space: why is a security protocol correct?[A]. Proceedings of the 1998 IEEE Symposium on Security and Privacy[C]. New York: IEEE Computer Press, 1998：160-171.

[5] Guttman JD, Thayer FJ. Authentication tests [A]. Proceedings of the 2000 IEEE Symposium on Security and Privacy[C].IEEE Computer Society Press, 2000：150～164.

[6] 董学文,马建峰,牛文生,等. 基于串空间的 Ad Hoc安全路由协议攻击分析模型[J]. 软件学报，2011，22(7)：1641-1651.

[7] 泰彬彬,王俊芳. 基于串空间认证测试的 DTLS协议认证性分析[J]. 计算机与网络，2014，40(496)：51-55.

[8] 吴名欢,程小辉. Casper/FDR和串空间在物联网通信协议中的形式化分析[J]. 桂林理工大学学报，2014，34(2)：338-344.

[9] Xiao Y L, Wang Y M, Pang L J. A Verification of trusted networkaccess protocols in the strand space model[J]. IEICE Transactions onFundamentals of Electronics, Communications and Computer Sciences, 2012, E95-A(3)：665-668.

[10] NeedhamR, Schroeder M. Using encryption for authenticationin large networks of computers [J]. Communicationsof the ACM, 1978，21(12)：993-999.

TP393.08文献标志码：A

2015.04.11）

1007-757X (2015)08-0004-03

国家自然科学基金（61402367）；陕西省信息化技术研究项目（2013-008）；西安邮电大学青年教师科研基金项目（401-1201）

肖跃雷（1979-），男，汉族，江西吉安人，西安邮电大学，物联网与两化融合研究院，讲师，博士后，研究方向：可信计算、安全协议分析与设计、无线网络安全，西安，710061；朱志详（1959-），男，,汉族，西安邮电大学，物联网与两化融合研究院，教授，博士，研究方向：多媒体通信，信息化应用，网络安全，西安，710061；张勇（1974-），男，,汉族，西安邮电大学，物联网与两化融合研究院，高工，博士，研究方向：信息安全，云计算与储存技术，西安，710061；