基于串空间认证测试理论的认证协议分析*

翁艳琴 ，石曙东 ，解颜铭

（1.湖北师范学院 数学与统计学院，湖北 黄石 435000；2.湖北师范学院 计算机科学与技术学院，湖北 黄石 435000）

串空间模型[1-2]是由 THAYER、HERZOG和 GUTTMAN三人于1998年提出来的，它吸纳了NRL协议器、Schneider秩函数和Paulson归纳法等方法的思想，将协议的描述和目标安全属性转化为图结构，借助图的理论和算法进行协议安全性分析。认证测试[4-5]理论是在串（Strand）空间模型的基础上发展而来的一种基于挑战-响应概念的协议分析技术。AT概念提供了简洁、强大的协议分析能力，它对协议不正确的判断基于Strand参数的不一致性，可用于协议的分析和设计。增强型认证测试理论是在串空间模型的基础上，借助认证测试理论，运用AT中协议判断分析的思想，通过由果导因的推理模式分析协议的关联性进而对协议的认证性进行验证。

本文对增强型认证测试理论进行简化，使得它对协议的认证性分析更加简洁、高效，将其应用到协议的安全性分析中，同时提出对协议认证性分析的一般模式，并将其应用到对OR协议的分析中，发现协议存在的漏洞，对OR协议进行了改进，并对改进后的协议进行了验证。

1 串空间内认证测试理论

串空间内认证测试理论的基本思想是，如果协议的一个主体发送了包含某个特定值a（明文或者密文形式）的消息，并在之后收到改变了形式后的a值（被加密或者解密），那么可以肯定存在一个持有相应密钥的普通协议主体参与了该协议的执行。本文涉及的相关定义和概念如下：

定义 1（Component）项 t0是 t的组件⇔

当且仅当t、t0不属于级联类型，并且对于任意t1≠t0，如果有t0⊂t1⊂t，那么，t1属于级联类型。消息组件则是原子数据类型或者加密类型。

定义 2 （Transformed Edge和 Transforming Edge）设a∈A，n1和 n2为同一串中的节点，则：边 n1⇒+n2是关于值a的被转换边⇔当且仅当a在节点n1发送，并在节点n2从新组件中接收。边是n1⇒+n2关于值a的转换边⇔当且仅当a在节点n1接收，并在节点n2存在于新组件中发送。

定义 3 （Test Component和 Test）t={h}k是节点 n关于a的测试组件⇔

①a⊂t，并且 t是节点 n的组件；

②t不是串空间中任意其他正常节点的组件的子项。

边n1⇒+n2是a的一个测试⇔

如果值a在节点n1唯一生成，并且边n1⇒+n2是关于 a的Transformed Edge。

对应于挑战方-响应方对值a不同的加解密处理，参考文献 [4]将认证测试划分为 Incoming Test（IT）、Outgoing Test（OT）和 Unsolicited Test（UT）3 种类型。其中，OT和IT测试在增强型认证测试理论中可以进行简化，主要有以下两项：

方法 1 （OT）

边n1⇒+n2是项t={h}k关于值a的输出认证测试（OT），如果：

①边n1⇒+n2是a的一个测试；

②k-1∉Kp；

③a不在节点n1的除t以外的任何其他组件中出现；

④t是节点n1关于a的一个测试组件。

方法 2 （UT）

接收节点 （负节点）n是项t={h}k关于值 a的主动认证测试（UT），如果：

①t是节点n关于a的一个测试组件；

②k∉Kp。

2 AT中Strand参数一致性判断定理

[3]认为Strand参数可以分为Nonce参数、协商数据和主体标志3类，在主体A发起的与主体S之间的认证测试过程中，只有同时满足三类一致性才满足Strand参数的一致性。

（1）A能确定在Nonce类型参数上与S的一致性；

（2）当且仅当认证测试的数据满足表1中的要求，A能确定与S在主体标志参数上的一致性；

（3）当且仅当协商数据包含在测试组件中，A能确定协商数据满足一致性。

表1给出了A发起与S的认证测试时，在不同加密方式下，各Strand的参数在某主体标志X上要达到一致所需满足的条件。

其中符号的含义如下：

id（A，X，S）：主体标志，包含 id（A，A，S）和 id（A，B，S）。在协议 Strand 空间Σ中，id（A，A，S）表示主体 A确定原子数据t∈A是A对于主体S的身份标志，即A可以确认的A相对S的身份标志，则必须有t=A或者t=Ka-1∧t∉P或者 t=Kas∧t∉P或者 t是 A与 S之间共享的秘密才可以满足。 而 id（A，B，S）表示 Strand空间Σ中主体A确定原子数据t∈A是B对于主体S的身份标志，即A可以确认的B相对S的身份标志，则必须有t=B或者t是A能够确认被S所知的A与B之间共享秘密才可满足。C表示主体标志必须包含在挑战（Challenge）内；R 表示必须包含在响应（Response）内；×表示不满足认证测试要求；OK表示在A与S交互中，id（A，A，S）就是作为主体 A能确认的A相对S的标志。表1列中不带方括号的内容给出的是在A与S两方进行交互的过程中的主体标志的参数一致性要满足的条件；带方括号表示A、S、B三方交互时主体标志的参数一致性需要附加的条件。

表1 Strand参数一致性

3 增强型认证测试理论

针对认证测试理论中的认证测试方法，结合Strand参数一致性定理和关联规则，给出增强型认证测试的两种规则。

（1）规则 1

假设C是某协议Strand空间的线束，节点 n2∈C，边 n1⇒+n2是项 t关于值 a的 OT，则必然存在节点 m1、m2∈C满足t是m1的消息组件，并且边m1⇒+m2是值a的Transforming Edge；如果能满足Strand参数的一致性，那么对于AT的发起方来说，n1⇒+n2和m1⇒+m2满足关联性。

（2）规则 2

假设C是某协议Strand空间的线束，节点 n∈C，且n是项t关于值 a的UT，那么必然存在一个常规发送节点m（正节点）∈C满足t是m的消息组件；如果能满足Strand参数的一致性，那么对于AT的发起方来说，n和m满足关联性。

4 关联度理论

定义 4：在 Strand空间中，Corresp（AS）表示协议主体S相对于 A 的关联度，Corresp（AS）≥0。

Corresp（AS）赋初值为 0，按 A的 Strand节点顺序依次考虑与 S的认证测试（OT，以及 S向 A提供的 UT），如果 S 的边

M（A，S）=Corresp（AS），A=S

M（A，S）=Corresp（AS），A≠S

如果 Corresp（AS）=0，表示协议主体 A不能确认与主体 S的关联性；如果 Corresp（AS）=n＞0，表示协议主体A能确认与主体 S的 Strand边

5 增强型认证测试理论对协议的认证性分析

认证性对认证协议来说是其安全性的关键因素。增强型认证测试理论是一种针对协议的认证性进行分析的技术，它集合了基于Strand的认证测试理论、AT中参数一致性理论以及关联性理论的优点，将协议分析规范化和模式化，抽象到数学矩阵的层次，为认证协议的分析提供了很好的工具。一般应用增强型认证测试理论对协议的认证性进行分析的步骤如下：

（1）将协议过程形式化，按照 Strand理论的方法将各个主体之间联系起来构造Strand图；

（2）对协议中的参数按照 AT中的 Nonce、协商数据和参与主体三种类型进行分类；

（3）按照主体的顺序依次分析每个主体与其他主体之间的关联性；

（4）将步骤（3）分析的结果构造成关联矩阵，分析判断协议的整体关联性；

（5）由协议的关联性分析判断协议的认证性是否满足要求，如果不满足则指明原因。

6 分析OR协议

OR协议是一种有可信第三方参与的对称密钥协议，通过第三方S达成一致进行分配共享密钥Kab。按照上面的步骤对OR协议进行分析，协议的过程如下：

（1）A→B：M，A，B，E（Kas：Na，M，A，B）；

（2）B →S：M，A，B，E （Kas：Na，M，A，B），E （Kbs：Nb，M，A，B）；

（3）S→B：M，E（Kas：Na，Kab），E（Kbs：Nb，Kab）；

（4）B→A：M，E（Kas：Na，Kab）。

对应的Strand图如图1所示。

图1 OR协议的Strand图

对协议的参数分类如下：

Nonce 类型参数：Na，Nb；

协商数据参数：M，Kas，Kbs，Kab；

主体标志参数：A，B，S。

应用增强型认证测试理论对协议进行分析。

（1）对于协议的主体A进行分析。

由图1可看出，Na是在Strand空间唯一生成的，term（A，1）={M，A，B，（Na，M，A，B）Kas}，其中，（Na，M，A，B）Kas（Kas∉Kp）是（A，1）节点关于 Na 的测试组件。当其被B转发到 S后，以新组件（Na，Kab）Kas的形式在（A，2）节点接收，根据测试理论知：

（2）对主体 B进行分析。

Nb是在 Strand空间唯一生成的，term（B，2）={M，A，B，（Na，M，A，B）Kas，（Nb，M，A，B）Kbs}，其中，（Nb，M，A，B）Kbs（Kbs∉Kp）是（B，2）节点关于 Nb 的测试组件。根据测试理论可知：

（3）对于主体S进行分析。

在负节点 （S，1）处，S 收到 term （B，2）={M，A，B，（Na，M，A，B）Kas， （Nb，M，A，B）Kbs}，Na 和 Nb 是Strand 空间唯一生成的，且 Kas，Kbs∉Kp，则（S，1）是关于Na和Nb的UT。对于Na来自于A，由表 1知，符合主体标志一致性，结合关联度理论有Corresp（SA）=1。同理，对Nb也满足主体标志一致性，结合关联度理论可得Corresp（SB）=2。结合上面结果构造协议的关联矩阵如图2所示。

图2 OR协议的关联矩阵

由图 2 可知：Corresp（AS）=2，A 能确认（S，1）⇒（S，2）的关联性；Corresp（BS）=2，B 能确认（S，1）⇒（S，2）的关联性 ；而 Corresp（AB）=0，Corresp（BA）=0，则 A 和 B不能互相确认关联性。对协议整体来说，A，B都可以确认与S的共识，但是不能确认S为其分配的共享密钥Kab在A和B之间进行交互时的确认，所以存在一定的安全隐患，可能导致信息的部分重放攻击。通过对OR协议的分析可看出增强型认证测试在对协议的认证性分析的有效性，还可以找出这个漏洞的原因来自于参数类型的不一致性。为了实现A和B之间的认证，针对此漏洞可以将协议作一些修改，修改后协议的Strand图如图3所示。

图3 改进的OR协议的Strand图

协议中 A和 B之间通过 E（Kab：Nb）来实现认证性的关联，为了使得发起方A确认协商数是一致的，A通过比较Kas加密的数据中的部分和Kab加密的数据来确认。可以用同样的方法对改进后的协议进行分析：（A，2）是关于 Nb的 UT，Nb来自于 B，由表 1可得：A、B满足主体参数一致性，在协商数Kab上也满足一致性，由关联规则 2和关联度理论可得出 Corresp（AB）=4。

图4 改进的OR协议的关联矩阵

由图 4 可看出，Corresp（i j）≠0（i=A，B，S，j=A，B，S且 i≠j），故A、B和 S三者之间可实现双向认证，具有认证性，在原协议的基础上进行了完善。

增强型认证测试理论从新的角度对协议进行了验证，推理过程简单，抽象到数学模型的层次，简单易用，为协议的形式化分析提供了新的思路。本文对增强型认证测试理论进行简化，将其应用到协议的安全性分析中，对OR协议进行了分析，发现存在的漏洞并有针对性地进行了改进，并对完善后的协议进行了验证。同时，本文还提出了协议认证性分析的一般模式，将协议分析规范化和模式化。本文提出的理论还存在许多需要完善的地方，如该方法目前只是在认证类协议中应用较多，对其他的协议还要推广扩充，对协议中并发问题的考虑等还需要相关研究者们的共同努力。

参考文献：

[1]Fàbrega F J T， HERZOG J C， GUTTMAN J D.Strand spaces： why is a security protocol correct？[C].Proceedings of the 1998 IEEE Symposium on Security and Privacy，1998：160-171.

[2]Fàbrega F J T， HERZOG J C， GUTTMAN J D.Strand spaces：proving security protocols correct[J].Journal of Computer Security，1999，7（2-3）：191-230.

[3]杨明，罗军舟.基于认证测试的安全协议分析[J].软件学报，2006，17（01）：148-156.

[4]GUTTMAN J D， Fàbrega F J T.Authentication tests[C].Proceedings of the 2000 IEEE Symposium on Security and Privacy， 2000：96-109.

[5]GUTTMAN J D， Fàbrega F J T.Authentication tests and the structure of bundles[J].Theoretical Computer Science，2002，283（2）：333-380.

[6]GUTTMAN J D.Security protocol design via authentication tests[C].Proceedings of the 2002 IEEE Computer Security Foundations Workshop， 2002：92-103.

[7]WOO T Y C， LAM S S.A semantic model for authentication protocols[C].Proceedings of the 1993 IEEE Computer Society Symposium on Research in Security and Privacy，1993：178-194.

[8]Ji Q G， Qing S H， Zhou Y B， et al.Study on strand space model theory[J].Journal of Computer Science and Technology， 2003，18（5）：553-570.

[9]BURROWS M， ABADI M， NEEDHAMR.A logic of authentication[J].ACM Transaction in Computer System，1990，8（1）：18-23.

[10]卿斯汉.安全协议20年研究进展 [J].软件学报，2003，14（10）1740-1752.

[11]董军，杨秀娟，赵艳芹.基于串空间模型安全协议形式化分析方法的研究 [J].计算机技术的发展，2008，18（04）：051-055.