用户认证协议的安全分析*

齐爱琴

（西北民族大学数学与计算机科学学院，甘肃 兰州 730000）

用户认证协议的安全分析*

齐爱琴

（西北民族大学数学与计算机科学学院，甘肃 兰州 730000）

认证是网络安全中最重要的一个安全目标，所有其他的安全属性例如完整性、不可否认性、可信性等都依赖于通信双方的认证。因此，很多安全认证协议被提出。而判断协议是否有效的方法主要是模拟。模拟只能证明协议在制定的模拟环境下是否可以达到安全目标。而对于正常真实的各种情况无法真正反应。本文提出了模型检测的方法来对其中一种用户认证协议进行了验证，通过模型检测协议的安全属性可以检测系统能达到的任何状态,比模拟的结果更有效。

Needham-Schroeder协议;规范化;Casper和FDR2

1 概述

当今，企业、政府或个人每天都需要通过网络进行信息交换。随着网络的普及，安全问题也日益突出。认证是安全通信的基础，也是网络安全中最重要的一个安全目标，所有其他的安全属性例如完整性、不可否认性、可信性等都依赖于通信双方的认证。因此，很多安全认证协议被提出。但协议的设计极其容易出错，使之不能正常工作。在实现和使用这些协议前，他们声称的安全属性应该被验证，而普通的常用的方法是模拟。模拟只能证明模拟的协议在特定的模拟环境下可以达到的安全目标。而对于正常的各种情况无法真实反应。需要一个更有效的方法来完成这个功能。模型检测就是其中之一。通过模型检测协议的安全属性可以在系统能达到的任何状态被验证。常用的工具是Ban logic[5，6], CAPl-es[2]和SPIN[3，4],安全协议的正式验证仍然是一个新的领域。文献1和文献7采用BAN逻辑对特定协议进行了验证和分析。但由于BAN逻辑存在着初始假设没有明确依据的方法、协议理想化、语义定义不明确、对协议的攻击探测能力较弱等问题，使得协议分析的结果还有待进一步验证。在这篇论文中，我们采用Casper和FDR2工具对一种经典的用户认证协议进行了模型检测和验证。这种方法不是新的，只是将这种方法应用在用户认证中是之前没有的。

2 协议描述

经典的Needham-Schroeder用户认证协议是基于对称加密和第三方仲裁机构的。整个系统的结构包括申请发起用户、第三方仲裁机构和目标用户三个部分。每个用户都有与第三方仲裁机构共享的秘密密钥。当用户之间要进行通信时，需先通过第三方仲裁机构完成用户之间的认证。认证过程如图1所示：

图1 认证过程图

A、B是用户的身份，S是第三方仲裁机构的身份，Na是用户A产生的随机数，Nb是用户B产生的随机数。Kas是用户A与第三方机构S的共享密钥，Kbs是用户B与第三方机构的共享密钥，Kab是第三方机构为用户A和B通信产生的会话密钥。我们给出对应的协议描述如下：

第一步中，用户A向第三方第三方仲裁机构S发出申请自己想和用户B通信的请求，第二步：收到消息的第三方仲裁机构查找与用户的共享密钥Kas，并产生用户A、B之间通信的会话密钥Kab，用与用户B的共享密钥Kbs加密信息Kab，A即 {Kab，A}Kbs，然后将Na，B，Kab，{Kab，A}Kbs信息用Kas加密之后发送给用户A，在第三步中，用户A用Kas解密收到的信息，得到与用户B的会话密钥Kab，将{Kab，A}Kbs发送给用户B。第四步：用户B用与第三方仲裁机构的共享密钥解密收到的信息得到Kab，A，然后生成一个随机数Nb，用得到的会话密钥Kab加密之后发送给用户A。第五步：用户A收到B的信息后，用Kab解密得到随机数Nb，计算Nb-1，并用会话密钥加密后发给用户B，用户B收到信息后，得到A是合法用户，从而认证A的身份，认证过程结束。

3 协议的形式化验证

根据协议中用户的工作方式，我们选择模型检查器FDR2来验证模型的安全性，这是一个基于并发理论和CSP的模型检测器。它主要用来检查系统的安全属性例如访问控制、认证、电子商务、移动代理、web服务、AXML文档等。FDR2中的规范化语言是CSP。但使用这种语言来模型化系统是耗时的并且易于出错。所以我们使用Casper产生CSP模型。Casper传递安全协议的规范给CSP以便于被FDR2分析。它也可以用于传递输出消息到可读格式。

验证认证协议的第一步是用Casper模型化协议。协议的模型化包括两部分：带有形式变量的模板参数的协议描述和协议实际使用的场景描述。形式变量最终会被实际变量所替代。

关于用户认证协议的模板如下：

协议的描述用来规范化消息交换。第1步对应协议中的第1步，用户将自己的身份A、用户B的身份B和随机数Na发给第三方机构。第2步对应协议第2步，第三方机构回复信息给用户A，用户A用密钥Kas解密消息得到Na，B，Kab，{Kab，A}Kbs，与自己存储的Na比较看是否相等，若相等证实信息是第三方机构发来的。第3步对应协议第3步，用户A将{Kab，A} Kbs发送给用户B，用户B解密信息，得到Kab，A，从而知道是用户A要与自己通信。第4步对应协议第4步，用户B生成一个随机数Nb并用Kab加密之后发送给用户A来验证A的身份的真实性。用户A解密得到Nb。第5步对应协议第5步，用户A将得到的随机数减一，用Kab加密之后发送给用户B，用户B比较自己存储的随机数与收到随机数之间是否差一，若是，认证通过。

我们只给出了一对用户之间认证的模型，事实上，所有用户之间的通信都是相同的，因此检测一对用户结点的安全属性是足够的。如果对一对用户结点有效，那么对所有用户节点都有效。这对FDR2的验证也是非常有益的。如果有很多个用户结点同时验证的话，机器的内存会全部耗尽，检查无法终止。

定义了协议的模板后，需要检测的安全属性也就规范化了。在用户认证协议中，安全属性是用户之间的认证。相应的输入文件是#specification。这个认证规范可以用下面的声明来完成：Agreement[A，B，[Nb]]协议规定A被B认证，Agreement[B，A，[Nb]]协议规定B被A认证。

正如我们之前提到的，协议的安全验证不是在协议的模板上来完成，而是在一个特定的场景中。对用户认证协议来说，场景包括二个部分：协议的初始方（想去被认证的用户）和响应方（第三方仲裁机构和执行认证的用户）。场景的定义使用真实变量来给出：

在模型化协议的最后一步是关于恶意分子的规范说明，恶意分子可以破坏协议，它知道所有用户和第三方的身份，由于本协议是建立在第三方仲裁机构是可信的、公平的基础上的。如果第三方机构与恶意分子勾结来产生对应的会话密钥Kis，并产生一个随机数am，那相应的恶意分子的场景描述如下：

完成输入文件后，Casper用来生成协议的CSP规范，这个规范用作FDR2的输入。完成协议的模型化之后,在linux环境中采用FDR2进行验证，FDR2验证的第一步是构造模型化系统的状态。然后指定的属性在每种状态下被验证。如果在每个状态下都可以通过验证，则协议的属性是安全的。否则被认为是无效的。在正常的状态下即只有用户和第三方仲裁机构的情况下，协议运行正常，认证安全属性得到验证。在有恶意分子存在情况下或者第三方仲裁机构与恶意分子勾结情况下，协议的认证安全属性验证错误。由此可以分析出Needham-Schroeder协议的安全性有待改进，可以对第三方仲裁机构设置可信值来评估他的真实可信性或者采用公钥基础设施来进一步完善协议，从而提高协议的认证安全。

4 总结

在这篇论文中，我们演示了如何用规范化验证技术来检测一个安全协议的有效性。使用的工具是Casper和FDR2。这个方法也可以适用于任何模型检测。首先，使用验证工具的规范化语言明确规定协议的各个部分。转换成一个验证执行的实际协议。这步很重要，如果模型错误或者与实际协议比较缺少相关限制条件的话，验证结果将会出错。接下来制定需要验证的安全属性。在这里我们只验证了认证属性，其他的属性也可以被验证。最后一步是实际执行的验证情况。FDR2证明了该协议的安全性有待提高，没有达到安全目标。接下来我们可以完成对称密钥的建立或者公钥基础设施的改进等工作，协议的使用范围可以进一步扩展。

[1] 田建波,王育民.认证协议的形式分析[J].通信保密,1998, 76(4)：8-12.

[2] John D.Aprshall,an analysis of the secure routing protocol for mobile ad hoc network route discovery：using intuitive. reasoning and formal verification to identify flaws,Msc thesis, Florida State University,2003.

[3] Davor Obradovic,Formal Analysis of convergence of routing protocols,PH.Dthesis,university of pensylvania,2000.

[4] Todd R.Andel,Formal Security Evaluation of ad hoc routing protocols,PH.Dthesis,,Florida State University,2007.

[5] 张玉清,李继红，肖国镇.密码协议分析工具—BAN逻辑及其缺陷[J].西安电子科技大学学报,1999,26(3)：376-378.

[6] 张玉清,吴建平，李星.BAN类逻辑的由来与发展[J].清华大学学报,2002,42(1)：96-99.

[7] 王正才,许道云,王晓峰,等.BAN逻辑的可靠性分析与改进[J].计算机工程,2012,38(17)：110-115.

TN915.04

中央高校科研项目(x31920150079)。