基于串空間認(rèn)證測(cè)試?yán)碚摰恼J(rèn)證協(xié)議分析*

翁艷琴 ，石曙東 ，解顏銘

（1.湖北師范學(xué)院 數(shù)學(xué)與統(tǒng)計(jì)學(xué)院，湖北 黃石 435000；2.湖北師范學(xué)院 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，湖北 黃石 435000）

串空間模型[1-2]是由 THAYER、HERZOG和 GUTTMAN三人于1998年提出來(lái)的，它吸納了NRL協(xié)議器、Schneider秩函數(shù)和Paulson歸納法等方法的思想，將協(xié)議的描述和目標(biāo)安全屬性轉(zhuǎn)化為圖結(jié)構(gòu)，借助圖的理論和算法進(jìn)行協(xié)議安全性分析。認(rèn)證測(cè)試[4-5]理論是在串（Strand）空間模型的基礎(chǔ)上發(fā)展而來(lái)的一種基于挑戰(zhàn)-響應(yīng)概念的協(xié)議分析技術(shù)。AT概念提供了簡(jiǎn)潔、強(qiáng)大的協(xié)議分析能力，它對(duì)協(xié)議不正確的判斷基于Strand參數(shù)的不一致性，可用于協(xié)議的分析和設(shè)計(jì)。增強(qiáng)型認(rèn)證測(cè)試?yán)碚撌窃诖臻g模型的基礎(chǔ)上，借助認(rèn)證測(cè)試?yán)碚摚\(yùn)用AT中協(xié)議判斷分析的思想，通過(guò)由果導(dǎo)因的推理模式分析協(xié)議的關(guān)聯(lián)性進(jìn)而對(duì)協(xié)議的認(rèn)證性進(jìn)行驗(yàn)證。

本文對(duì)增強(qiáng)型認(rèn)證測(cè)試?yán)碚撨M(jìn)行簡(jiǎn)化，使得它對(duì)協(xié)議的認(rèn)證性分析更加簡(jiǎn)潔、高效，將其應(yīng)用到協(xié)議的安全性分析中，同時(shí)提出對(duì)協(xié)議認(rèn)證性分析的一般模式，并將其應(yīng)用到對(duì)OR協(xié)議的分析中，發(fā)現(xiàn)協(xié)議存在的漏洞，對(duì)OR協(xié)議進(jìn)行了改進(jìn)，并對(duì)改進(jìn)后的協(xié)議進(jìn)行了驗(yàn)證。

1 串空間內(nèi)認(rèn)證測(cè)試?yán)碚?/h2>

串空間內(nèi)認(rèn)證測(cè)試?yán)碚摰幕舅枷胧?，如果協(xié)議的一個(gè)主體發(fā)送了包含某個(gè)特定值a（明文或者密文形式）的消息，并在之后收到改變了形式后的a值（被加密或者解密），那么可以肯定存在一個(gè)持有相應(yīng)密鑰的普通協(xié)議主體參與了該協(xié)議的執(zhí)行。本文涉及的相關(guān)定義和概念如下：

定義 1（Component）項(xiàng) t0是 t的組件?

當(dāng)且僅當(dāng)t、t0不屬于級(jí)聯(lián)類型，并且對(duì)于任意t1≠t0，如果有t0?t1?t，那么，t1屬于級(jí)聯(lián)類型。消息組件則是原子數(shù)據(jù)類型或者加密類型。

定義 2 （Transformed Edge和 Transforming Edge）設(shè)a∈A，n1和 n2為同一串中的節(jié)點(diǎn)，則：邊 n1?+n2是關(guān)于值a的被轉(zhuǎn)換邊?當(dāng)且僅當(dāng)a在節(jié)點(diǎn)n1發(fā)送，并在節(jié)點(diǎn)n2從新組件中接收。邊是n1?+n2關(guān)于值a的轉(zhuǎn)換邊?當(dāng)且僅當(dāng)a在節(jié)點(diǎn)n1接收，并在節(jié)點(diǎn)n2存在于新組件中發(fā)送。

定義 3 （Test Component和 Test）t={h}k是節(jié)點(diǎn) n關(guān)于a的測(cè)試組件?

①a?t，并且 t是節(jié)點(diǎn) n的組件；

②t不是串空間中任意其他正常節(jié)點(diǎn)的組件的子項(xiàng)。

邊n1?+n2是a的一個(gè)測(cè)試?

如果值a在節(jié)點(diǎn)n1唯一生成，并且邊n1?+n2是關(guān)于 a的Transformed Edge。

對(duì)應(yīng)于挑戰(zhàn)方-響應(yīng)方對(duì)值a不同的加解密處理，參考文獻(xiàn) [4]將認(rèn)證測(cè)試劃分為 Incoming Test（IT）、Outgoing Test（OT）和 Unsolicited Test（UT）3 種類型。其中，OT和IT測(cè)試在增強(qiáng)型認(rèn)證測(cè)試?yán)碚撝锌梢赃M(jìn)行簡(jiǎn)化，主要有以下兩項(xiàng)：

方法 1 （OT）

邊n1?+n2是項(xiàng)t={h}k關(guān)于值a的輸出認(rèn)證測(cè)試（OT），如果：

①邊n1?+n2是a的一個(gè)測(cè)試；

②k-1?Kp；

③a不在節(jié)點(diǎn)n1的除t以外的任何其他組件中出現(xiàn)；

④t是節(jié)點(diǎn)n1關(guān)于a的一個(gè)測(cè)試組件。

方法 2 （UT）

接收節(jié)點(diǎn) （負(fù)節(jié)點(diǎn)）n是項(xiàng)t={h}k關(guān)于值 a的主動(dòng)認(rèn)證測(cè)試（UT），如果：

①t是節(jié)點(diǎn)n關(guān)于a的一個(gè)測(cè)試組件；

②k?Kp。

2 AT中Strand參數(shù)一致性判斷定理

[3]認(rèn)為Strand參數(shù)可以分為Nonce參數(shù)、協(xié)商數(shù)據(jù)和主體標(biāo)志3類，在主體A發(fā)起的與主體S之間的認(rèn)證測(cè)試過(guò)程中，只有同時(shí)滿足三類一致性才滿足Strand參數(shù)的一致性。

（1）A能確定在Nonce類型參數(shù)上與S的一致性；

（2）當(dāng)且僅當(dāng)認(rèn)證測(cè)試的數(shù)據(jù)滿足表1中的要求，A能確定與S在主體標(biāo)志參數(shù)上的一致性；

（3）當(dāng)且僅當(dāng)協(xié)商數(shù)據(jù)包含在測(cè)試組件中，A能確定協(xié)商數(shù)據(jù)滿足一致性。

表1給出了A發(fā)起與S的認(rèn)證測(cè)試時(shí)，在不同加密方式下，各Strand的參數(shù)在某主體標(biāo)志X上要達(dá)到一致所需滿足的條件。

其中符號(hào)的含義如下：

id（A，X，S）：主體標(biāo)志，包含 id（A，A，S）和 id（A，B，S）。在協(xié)議 Strand 空間Σ中，id（A，A，S）表示主體 A確定原子數(shù)據(jù)t∈A是A對(duì)于主體S的身份標(biāo)志，即A可以確認(rèn)的A相對(duì)S的身份標(biāo)志，則必須有t=A或者t=Ka-1∧t?P或者 t=Kas∧t?P或者 t是 A與 S之間共享的秘密才可以滿足。 而 id（A，B，S）表示 Strand空間Σ中主體A確定原子數(shù)據(jù)t∈A是B對(duì)于主體S的身份標(biāo)志，即A可以確認(rèn)的B相對(duì)S的身份標(biāo)志，則必須有t=B或者t是A能夠確認(rèn)被S所知的A與B之間共享秘密才可滿足。C表示主體標(biāo)志必須包含在挑戰(zhàn)（Challenge）內(nèi)；R 表示必須包含在響應(yīng)（Response）內(nèi)；×表示不滿足認(rèn)證測(cè)試要求；OK表示在A與S交互中，id（A，A，S）就是作為主體 A能確認(rèn)的A相對(duì)S的標(biāo)志。表1列中不帶方括號(hào)的內(nèi)容給出的是在A與S兩方進(jìn)行交互的過(guò)程中的主體標(biāo)志的參數(shù)一致性要滿足的條件；帶方括號(hào)表示A、S、B三方交互時(shí)主體標(biāo)志的參數(shù)一致性需要附加的條件。

表1 Strand參數(shù)一致性

3 增強(qiáng)型認(rèn)證測(cè)試?yán)碚?/h2>

針對(duì)認(rèn)證測(cè)試?yán)碚撝械恼J(rèn)證測(cè)試方法，結(jié)合Strand參數(shù)一致性定理和關(guān)聯(lián)規(guī)則，給出增強(qiáng)型認(rèn)證測(cè)試的兩種規(guī)則。

（1）規(guī)則 1

假設(shè)C是某協(xié)議Strand空間的線束，節(jié)點(diǎn) n2∈C，邊 n1?+n2是項(xiàng) t關(guān)于值 a的 OT，則必然存在節(jié)點(diǎn) m1、m2∈C滿足t是m1的消息組件，并且邊m1?+m2是值a的Transforming Edge；如果能滿足Strand參數(shù)的一致性，那么對(duì)于AT的發(fā)起方來(lái)說(shuō)，n1?+n2和m1?+m2滿足關(guān)聯(lián)性。

（2）規(guī)則 2

假設(shè)C是某協(xié)議Strand空間的線束，節(jié)點(diǎn) n∈C，且n是項(xiàng)t關(guān)于值 a的UT，那么必然存在一個(gè)常規(guī)發(fā)送節(jié)點(diǎn)m（正節(jié)點(diǎn)）∈C滿足t是m的消息組件；如果能滿足Strand參數(shù)的一致性，那么對(duì)于AT的發(fā)起方來(lái)說(shuō)，n和m滿足關(guān)聯(lián)性。

4 關(guān)聯(lián)度理論

定義 4：在 Strand空間中，Corresp（AS）表示協(xié)議主體S相對(duì)于 A 的關(guān)聯(lián)度，Corresp（AS）≥0。

Corresp（AS）賦初值為 0，按 A的 Strand節(jié)點(diǎn)順序依次考慮與 S的認(rèn)證測(cè)試（OT，以及 S向 A提供的 UT），如果 S 的邊

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

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

如果 Corresp（AS）=0，表示協(xié)議主體 A不能確認(rèn)與主體 S的關(guān)聯(lián)性；如果 Corresp（AS）=n＞0，表示協(xié)議主體A能確認(rèn)與主體 S的 Strand邊

5 增強(qiáng)型認(rèn)證測(cè)試?yán)碚搶?duì)協(xié)議的認(rèn)證性分析

認(rèn)證性對(duì)認(rèn)證協(xié)議來(lái)說(shuō)是其安全性的關(guān)鍵因素。增強(qiáng)型認(rèn)證測(cè)試?yán)碚撌且环N針對(duì)協(xié)議的認(rèn)證性進(jìn)行分析的技術(shù)，它集合了基于Strand的認(rèn)證測(cè)試?yán)碚?、AT中參數(shù)一致性理論以及關(guān)聯(lián)性理論的優(yōu)點(diǎn)，將協(xié)議分析規(guī)范化和模式化，抽象到數(shù)學(xué)矩陣的層次，為認(rèn)證協(xié)議的分析提供了很好的工具。一般應(yīng)用增強(qiáng)型認(rèn)證測(cè)試?yán)碚搶?duì)協(xié)議的認(rèn)證性進(jìn)行分析的步驟如下：

（1）將協(xié)議過(guò)程形式化，按照 Strand理論的方法將各個(gè)主體之間聯(lián)系起來(lái)構(gòu)造Strand圖；

（2）對(duì)協(xié)議中的參數(shù)按照 AT中的 Nonce、協(xié)商數(shù)據(jù)和參與主體三種類型進(jìn)行分類；

（3）按照主體的順序依次分析每個(gè)主體與其他主體之間的關(guān)聯(lián)性；

（4）將步驟（3）分析的結(jié)果構(gòu)造成關(guān)聯(lián)矩陣，分析判斷協(xié)議的整體關(guān)聯(lián)性；

（5）由協(xié)議的關(guān)聯(lián)性分析判斷協(xié)議的認(rèn)證性是否滿足要求，如果不滿足則指明原因。

6 分析OR協(xié)議

OR協(xié)議是一種有可信第三方參與的對(duì)稱密鑰協(xié)議，通過(guò)第三方S達(dá)成一致進(jìn)行分配共享密鑰Kab。按照上面的步驟對(duì)OR協(xié)議進(jìn)行分析，協(xié)議的過(guò)程如下：

（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）。

對(duì)應(yīng)的Strand圖如圖1所示。

圖1 OR協(xié)議的Strand圖

對(duì)協(xié)議的參數(shù)分類如下：

Nonce 類型參數(shù)：Na，Nb；

協(xié)商數(shù)據(jù)參數(shù)：M，Kas，Kbs，Kab；

主體標(biāo)志參數(shù)：A，B，S。

應(yīng)用增強(qiáng)型認(rèn)證測(cè)試?yán)碚搶?duì)協(xié)議進(jìn)行分析。

（1）對(duì)于協(xié)議的主體A進(jìn)行分析。

由圖1可看出，Na是在Strand空間唯一生成的，term（A，1）={M，A，B，（Na，M，A，B）Kas}，其中，（Na，M，A，B）Kas（Kas?Kp）是（A，1）節(jié)點(diǎn)關(guān)于 Na 的測(cè)試組件。當(dāng)其被B轉(zhuǎn)發(fā)到 S后，以新組件（Na，Kab）Kas的形式在（A，2）節(jié)點(diǎn)接收，根據(jù)測(cè)試?yán)碚撝?A，1＞?

（2）對(duì)主體 B進(jìn)行分析。

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）節(jié)點(diǎn)關(guān)于 Nb 的測(cè)試組件。根據(jù)測(cè)試?yán)碚摽芍?B，2＞?

（3）對(duì)于主體S進(jìn)行分析。

在負(fù)節(jié)點(diǎn) （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）是關(guān)于Na和Nb的UT。對(duì)于Na來(lái)自于A，由表 1知，符合主體標(biāo)志一致性，結(jié)合關(guān)聯(lián)度理論有Corresp（SA）=1。同理，對(duì)Nb也滿足主體標(biāo)志一致性，結(jié)合關(guān)聯(lián)度理論可得Corresp（SB）=2。結(jié)合上面結(jié)果構(gòu)造協(xié)議的關(guān)聯(lián)矩陣如圖2所示。

圖2 OR協(xié)議的關(guān)聯(lián)矩陣

由圖 2 可知：Corresp（AS）=2，A 能確認(rèn)（S，1）?（S，2）的關(guān)聯(lián)性；Corresp（BS）=2，B 能確認(rèn)（S，1）?（S，2）的關(guān)聯(lián)性 ；而 Corresp（AB）=0，Corresp（BA）=0，則 A 和 B不能互相確認(rèn)關(guān)聯(lián)性。對(duì)協(xié)議整體來(lái)說(shuō)，A，B都可以確認(rèn)與S的共識(shí)，但是不能確認(rèn)S為其分配的共享密鑰Kab在A和B之間進(jìn)行交互時(shí)的確認(rèn)，所以存在一定的安全隱患，可能導(dǎo)致信息的部分重放攻擊。通過(guò)對(duì)OR協(xié)議的分析可看出增強(qiáng)型認(rèn)證測(cè)試在對(duì)協(xié)議的認(rèn)證性分析的有效性，還可以找出這個(gè)漏洞的原因來(lái)自于參數(shù)類型的不一致性。為了實(shí)現(xiàn)A和B之間的認(rèn)證，針對(duì)此漏洞可以將協(xié)議作一些修改，修改后協(xié)議的Strand圖如圖3所示。

圖3 改進(jìn)的OR協(xié)議的Strand圖

協(xié)議中 A和 B之間通過(guò) E（Kab：Nb）來(lái)實(shí)現(xiàn)認(rèn)證性的關(guān)聯(lián)，為了使得發(fā)起方A確認(rèn)協(xié)商數(shù)是一致的，A通過(guò)比較Kas加密的數(shù)據(jù)中的部分和Kab加密的數(shù)據(jù)來(lái)確認(rèn)?？梢杂猛瑯拥姆椒▽?duì)改進(jìn)后的協(xié)議進(jìn)行分析：（A，2）是關(guān)于 Nb的 UT，Nb來(lái)自于 B，由表 1可得：A、B滿足主體參數(shù)一致性，在協(xié)商數(shù)Kab上也滿足一致性，由關(guān)聯(lián)規(guī)則 2和關(guān)聯(lián)度理論可得出 Corresp（AB）=4。

圖4 改進(jìn)的OR協(xié)議的關(guān)聯(lián)矩陣

由圖 4 可看出，Corresp（i j）≠0（i=A，B，S，j=A，B，S且 i≠j），故A、B和 S三者之間可實(shí)現(xiàn)雙向認(rèn)證，具有認(rèn)證性，在原協(xié)議的基礎(chǔ)上進(jìn)行了完善。

增強(qiáng)型認(rèn)證測(cè)試?yán)碚搹男碌慕嵌葘?duì)協(xié)議進(jìn)行了驗(yàn)證，推理過(guò)程簡(jiǎn)單，抽象到數(shù)學(xué)模型的層次，簡(jiǎn)單易用，為協(xié)議的形式化分析提供了新的思路。本文對(duì)增強(qiáng)型認(rèn)證測(cè)試?yán)碚撨M(jìn)行簡(jiǎn)化，將其應(yīng)用到協(xié)議的安全性分析中，對(duì)OR協(xié)議進(jìn)行了分析，發(fā)現(xiàn)存在的漏洞并有針對(duì)性地進(jìn)行了改進(jìn)，并對(duì)完善后的協(xié)議進(jìn)行了驗(yàn)證。同時(shí)，本文還提出了協(xié)議認(rèn)證性分析的一般模式，將協(xié)議分析規(guī)范化和模式化。本文提出的理論還存在許多需要完善的地方，如該方法目前只是在認(rèn)證類協(xié)議中應(yīng)用較多，對(duì)其他的協(xié)議還要推廣擴(kuò)充，對(duì)協(xié)議中并發(fā)問(wèn)題的考慮等還需要相關(guān)研究者們的共同努力。

參考文獻(xiàn)：

[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]楊明，羅軍舟.基于認(rèn)證測(cè)試的安全協(xié)議分析[J].軟件學(xué)報(bào)，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]卿斯?jié)h.安全協(xié)議20年研究進(jìn)展 [J].軟件學(xué)報(bào)，2003，14（10）1740-1752.

[11]董軍，楊秀娟，趙艷芹.基于串空間模型安全協(xié)議形式化分析方法的研究 [J].計(jì)算機(jī)技術(shù)的發(fā)展，2008，18（04）：051-055.