一種基于狀態(tài)擴展的安全協(xié)議驗證機制

摘 要:基于模型檢測驗證協(xié)議的方法存在狀態(tài)空間爆炸問題，其中基于目標綁定搜索狀態(tài)空間的方法有效控制了狀態(tài)空間，但不能完全給出協(xié)議的運行情況。針對這一問題，提出了一種基于狀態(tài)擴展的安全協(xié)議自動化驗證機制，首先對協(xié)議狀態(tài)進行初始搜索，給出協(xié)議運行需要的事件，得到協(xié)議基本狀態(tài)，然后進行擴展搜索，考慮基本狀態(tài)與其他協(xié)議運行的關(guān)系，形成協(xié)議擴展狀態(tài)。該機制能夠有效反映出協(xié)議的運行情況，且能夠同時對多種安全性質(zhì)進行驗證。

關(guān)鍵詞:安全協(xié)議; 自動化驗證; 基本搜索; 擴展搜索

中圖分類號:TP309文獻標志碼:A

文章編號:1001-3695(2010)06-2327-04

doi:10.3969/j.issn.10013695.2010.06.095

Stateextended based verification mechanism for security protocols

HUANG Qing1， WANG Yadi1， HAN Jihong1， FAN Yudan1， HUANG He2

(1.School of Electronic Technology， PLA Information Engineering University， Zhengzhou 450004，China; 2.61983 Unit of PLA， Beijing 100840， China)

Abstract:The tools for cryptographic protocols analysis based on state exploration had the problem of state exploration， among them， the goal binding could deduce the states effectively， but if it couldn’t give the runs of protocol wholly. To solve this problem， this article proposed a state extendedbased verification mechanism， which got the basic states with necessary events through basic search， and then proceeded with extended search in order to get the connections between basic states and the other runs， which formed the extended states. This mechanism can give the runs of protocol effectively， and under which can verified security properties synchronously.

Key words:security protocol; automatic verification; basic search; extended search

0 引言

安全協(xié)議自動化驗證一直是協(xié)議分析的熱點和難點，其中基于模型檢測的方法[1~3]被證明是一種比較成功的方法，但它存在著狀態(tài)空間爆炸問題。其中，Athena[1]是一個基于后向搜索的驗證器，它用串[4]來描述協(xié)議和攻擊者，基于目標綁定進行狀態(tài)搜索，大大減少了狀態(tài)中運行實例的數(shù)目，有效控制了狀態(tài)空間。但其得到的狀態(tài)空間不完全，不能完全反映出協(xié)議的運行情況，進而影響了對一些安全性質(zhì)的驗證，如對單射性而言，從接收事件出發(fā)，它只有擴展得到其對應的發(fā)送事件，卻不能給出發(fā)送事件是否對應著其他接收事件。

為進一步提高協(xié)議自動化驗證的質(zhì)量和效率，支持協(xié)議多種安全性質(zhì)的驗證，本文提出了一種基于狀態(tài)擴展的安全協(xié)議自動化驗證機制，它首先通過對協(xié)議狀態(tài)的初始搜索，給出協(xié)議運行需要的事件，得到協(xié)議基本狀態(tài)，然后進行擴展搜索，考慮基本狀態(tài)與協(xié)議其他運行的關(guān)系，給出協(xié)議的擴展狀態(tài)，從而有效地給出了協(xié)議運行的情況。該驗證機制有協(xié)議狀態(tài)推理、攻擊者模型和安全性質(zhì)驗證耦合度小的優(yōu)點，不僅有利于各部分的擴展，而且能夠同時對多種安全性質(zhì)進行驗證，大大提高了驗證效率。

1 相關(guān)工作

近年來出現(xiàn)了大量的安全協(xié)議自動化驗證工具，其各有優(yōu)缺點，文獻[5]給出了具體的比較分析。本文基本搜索過程的思想來自于Athena[1]，但有以下幾點不同:

a)Athena用串描述攻擊者，形成的協(xié)議狀態(tài)與攻擊者串密切相關(guān)，且安全特性驗證在狀態(tài)推理的每一步進行。本文將攻擊者推理、協(xié)議驗證機制和安全性質(zhì)分開，減小了耦合度，有利于攻擊者能力的擴展，且提高了整體的驗證效率。

b)采取了不同的消息合一化方式。 Athena采用內(nèi)項合一來進行事件綁定，但該合一算法具有不完備和不可終止問題。文獻[3]中通過規(guī)定協(xié)議中出現(xiàn)的變量均為原子變量來對其進行解決，但這一規(guī)定本身就使得合一不完備。本文驗證機制中合一化是消息的直接合一化，與消息的內(nèi)項無關(guān)，避免了這一問題。

c)擴展了協(xié)議事件，可以處理更多類型的協(xié)議。

除此之外，從驗證思想上來說，還有一個最大的不同:本文在基本搜索的基礎上，給出了擴展搜索，解決了Athena狀態(tài)空間不完全、不能驗證單射性等安全性質(zhì)的問題。

2 安全協(xié)議形式化模型

2.1 協(xié)議模型

定義1 項。它用于描述協(xié)議消息，它由常量、變量和函數(shù)項組成。

定義2 置換、合一化、實例化。令s， t為兩個項，若存在置換σ滿足σ(s)=σ(t)，則稱s和t可以合一化。將置換σ作用于s的過程稱做s的置換過程，若置換σ將一個變量置換為一個常量，則該過程也叫實例化過程。

定義3 事件。它包括消息的發(fā)送、接收和匹配事件，分別用send(t)、receive(t)、match(t，t′)來表示。

事件e的主動主體、被動主體、消息及事件類型分別用函數(shù)aprinc(e)、pprinc(e)、msg(e)、type(e)表示。

定義4 角色(role)。它是一個帶參數(shù)的事件序列。主體依據(jù)角色來運行協(xié)議，角色的一次具體運行形成一個角色實例，用運行標志RID來區(qū)分不同的角色運行。

定義5 初始角色實例。創(chuàng)建的一個初始角色具體實例稱為初始角色實例。在初始角色實例中的參數(shù)除隨機數(shù)外，都用變量表示。

定義6 協(xié)議。它由角色組成，將其定義為Prt=(role1，role2，role3，…)。

在協(xié)議中，事件之間存在著兩種關(guān)系，一種是事件之間的收發(fā)關(guān)系，記做e1→e2;另一種是同一角色實例中事件之間的前趨關(guān)系，記做e1e2。如果事件滿足e1(|→)*e2，則稱事件e1在e2之前發(fā)生，記做e1e2。

2.2 攻擊者模型

本文基于DolevYao模型[6]來描述攻擊者，攻擊者由初始知識和攻擊者能力構(gòu)成。假設攻擊者控制著整個網(wǎng)絡，并將攻擊者能力抽象為從網(wǎng)絡獲取消息、進行消息推理和向網(wǎng)絡插入消息這三個事件，用take、compute和insert表示。為實現(xiàn)insert事件，攻擊者可能需通過take事件來獲取消息，然后調(diào)用compute事件通過各種密碼學運算、代數(shù)運算等來計算消息。

本文省略消息計算過程，將攻擊者用take和insert事件表示，攻擊者的具體能力體現(xiàn)在take和insert事件消息項的關(guān)系上，攻擊者能力不同，相同的insert事件對應不同的take事件或者不能實現(xiàn)。

本文的驗證機制支持DolevYao及其擴展模型，這一抽象使得驗證機制與攻擊者模型的耦合度較小，既有利于攻擊者模型的擴展，也便于在不同攻擊者模型下驗證協(xié)議。

3 驗證機制

驗證機制基于狀態(tài)擴展來進行狀態(tài)轉(zhuǎn)移，即從包含一個完整的初始角色實例的狀態(tài)出發(fā)，根據(jù)事件和驗證的需要不斷進行狀態(tài)的擴展和實例化，從而得到代表協(xié)議運行的最終驗證狀態(tài)。

規(guī)定初始狀態(tài)包含一個完整的角色實例，其意義在于:

在協(xié)議所有可能的攻擊中，一定存在協(xié)議的一個完整的角色實例，如果任何主體都沒有依照角色完成自己的運行，那就相當于該協(xié)議沒有運行，協(xié)議攻擊也是沒有意義的。

下面首先給出一些基本概念，然后給出具體的驗證過程。

定義7 未滿足事件。該事件指還不具有實現(xiàn)條件的事件。從協(xié)議模型可以看出，協(xié)議運行過程中可能出現(xiàn)五類事件，在滿足事件前趨關(guān)系的條件下，可認為send是可實現(xiàn)的，receive和take事件則還要滿足事件收發(fā)關(guān)系，insert事件可能需要相應的take事件，match事件中含有的項需要滿足一定的內(nèi)容要求。

定義8 協(xié)議狀態(tài)。定義協(xié)議狀態(tài)為一個四元組state=(event，σ，，US)。其中:event表示狀態(tài)中含有的事件集合;→表示事件收發(fā)關(guān)系，σ表示項的置換操作;US表示狀態(tài)中的未滿足事件;表示事件前趨關(guān)系，且e1e，e∈event，e1∈event，即協(xié)議狀態(tài)滿足事件前趨關(guān)系。

驗證機制分為基本搜索和擴展搜索兩個階段。

3.1 基本搜索

基本搜索階段從實現(xiàn)狀態(tài)中未滿足事件的需要出發(fā)，給出實現(xiàn)初始狀態(tài)必須存在的事件，形成協(xié)議的基本狀態(tài)集。狀態(tài)轉(zhuǎn)移過程如下:

設state=(event，σ，，US)，e∈US，根據(jù)e的事件類型轉(zhuǎn)移到不同的狀態(tài):

a)e=match(t，t′)。將match事件看做是項的合一化操作，設σ′(t)=σ′(t′)，形成下一狀態(tài)state′=(event′，σ，，US′):event′=σ′(event)，US′=US/match(t，t′)。

b)e=receive(t)。合法主體的接收事件有兩種實現(xiàn)方式，一是合法主體的發(fā)送事件，二是攻擊者的插入消息事件:

(a)合法主體的send事件實現(xiàn)又有兩種可能:一種是event中已經(jīng)存在的send事件，另一種是event中還未包含的send事件，需要創(chuàng)建新的事件實例或角色實例:

由event中已存在的send(t1)事件實現(xiàn)形成狀態(tài)state1=(event1，→1，，US1)，event1=σ1(event)，→1=→∪(send(t1)σ1receive(t))，US1=US/receive(t)，其中σ(t1)=σ(t)。

由Event中還未包含但在所有角色實例已經(jīng)存在的send(t2)事件實現(xiàn)，形成狀態(tài)state2，→2=→∪send(t2)σ2receive(t)，esend(t2)，eevent，event2=σ(event∪e)，US進行相應的改變。

由event中還未包含且其所有角色實例也不存在的send(t3)事件實現(xiàn)，形成狀態(tài)state3:首先創(chuàng)建一個包含send(t3)的初始角色實例，并將其中的事件加入event3中，規(guī)定基本搜索中創(chuàng)建的角色實例RID>0，→2=→∪send(t3)σ3receive(t)，和US進行相應的改變。

(b)由insert(t)實現(xiàn)，形成狀態(tài)state4，event4=event∪insert(t)，US4=US/receive(t)∪insert(t)，→4=→∪(insert(t)→receive(t))。

Insert事件是攻擊者的插入消息事件，需要調(diào)用compute事件，若攻擊者知識不夠，則返回take事件，形成狀態(tài)state′=(event′，σ，′，US′)，event′=event∪take(t1)∪take(t2)∪…，′=∪take(t1)take(t2)…insert(t′)，US′=US/insert(t′)∪take(t1)∪take(t2)∪…;若不需要take事件，event′=event，US′=US/insert(t′)。

Take事件是攻擊者的接收事件，只能由合法主體的發(fā)送事件實現(xiàn)，與合法主體接收事件綁定的方法類似，不再給出，不同之處在于如果take事件可以由已經(jīng)存在的send事件實現(xiàn)，則不再擴展其他send事件。已經(jīng)存在的send事件相當于攻擊者已經(jīng)擁有的消息，所以不再創(chuàng)建新的發(fā)送事件。

3.2 擴展搜索

基本搜索得到的基本狀態(tài)包含了為實現(xiàn)初始狀態(tài)必須存在的事件，這些事件與協(xié)議其他的運行可能有關(guān)系，攻擊者可能利用這些事件對其他的運行形成攻擊或得到更多的知識。因此，本文給出擴展搜索，考慮基本狀態(tài)所含有的事件與協(xié)議其他運行的關(guān)系，對基本狀態(tài)進行擴展，給出協(xié)議的擴展狀態(tài)集，該階段主要是根據(jù)狀態(tài)擴展的需要，考慮發(fā)送事件與協(xié)議其他運行的關(guān)系，對基本狀態(tài)進行擴展。

擴展搜索與基本搜索不同，不能直接對擴展的未滿足事件進行處理，如果得到的基本狀態(tài)與協(xié)議其他運行沒有任何關(guān)系，那就相當于另一次基本搜索。為避免這一情況，本文將擴展搜索分為兩步:a)基本狀態(tài)綁定，找到基本狀態(tài)中的事件與協(xié)議其他運行的關(guān)系;b)擴展狀態(tài)形成，處理擴展的其他未滿足事件，形成協(xié)議擴展狀態(tài)。如果第一階段返回空值，那么不再進行第二階段。

為區(qū)分基本狀態(tài)與擴展狀態(tài)中的事件，規(guī)定擴展搜索中新擴展的角色實例RID<0。

1)基本狀態(tài)綁定

為得到基本狀態(tài)與以后事件的所有可能關(guān)系，需要依次向基本狀態(tài)中加入各個協(xié)議角色的一個新創(chuàng)建的角色實例，用該角色實例代表該角色參與的一次會話，因為依次考慮了各個角色的一個角色實例，所以基本狀態(tài)綁定階段考慮了基本狀態(tài)與協(xié)議其他所有可能運行的聯(lián)系。下面給出對其中的一個角色實例進行處理的過程:

該步只考慮基本狀態(tài)與協(xié)議其他運行的關(guān)系，只對部分事件進行處理，所以會出現(xiàn)一些在本步進行了綁定，但事實上并不能綁定的情況。本文在該步采用了組合的方法，對所有可能由初始狀態(tài)實現(xiàn)的事件進行組合，從而避免了這一情況。

在基本狀態(tài)綁定時，US表示可能與基本狀態(tài)有關(guān)系的未滿足事件集，在初始時只包含receive事件。

e∈US進行處理，分析可知，在基本狀態(tài)綁定過程中，e只可能為receive或take事件。

1)e=receive(t) 合法主體的接收事件有三種實現(xiàn)方式，即RID>0的發(fā)送事件、攻擊者的插入消息事件、新擴展的事件。

a)由RID>0的send(t1)事件實現(xiàn)，形成狀態(tài)state1，event1=σ1(event)。其中σ(t1)=σ(t)，→1=→∪(send(t1)σ1receive(t))，US1=US/receive(t)。

b)由insert(t)實現(xiàn)，形成狀態(tài)state2，event2=event∪insert(t)，US2=US/receive(t)∪insert(t)，→3=→∪(insert(t)→receive(t))。

c)由擴展的事件實現(xiàn)，形成state3，state3與state的區(qū)別在于US3=US/receive(t)，表明receive(t)由擴展的事件完成。

2)e=take(t) 攻擊者的接收事件有兩種實現(xiàn)方式，即RID>0的發(fā)送事件和新擴展的事件。

a)由RID>0的send(t1)實現(xiàn)形成state4，與上面receive事件相同。

b)由擴展的事件實現(xiàn)，形成state5，state5與state的區(qū)別在于US5=US/receive(t)。

重復以上過程，不斷對狀態(tài)進行處理，直到US為空，然后對得到的狀態(tài)進行檢查，如果在所有新加入的綁定關(guān)系→中，不包含由已經(jīng)存在的事件實現(xiàn)的綁定，那么說明基本狀態(tài)與該角色實例不存在直接關(guān)系，刪除該狀態(tài)。

對各個角色的角色實例也進行類似處理。

這樣，擴展搜索的第一階段就給出了基本狀態(tài)與協(xié)議其他會話的關(guān)系，且保證了狀態(tài)中至少存在一個事件與基本狀態(tài)中的事件有關(guān)，狀態(tài)中的其他未滿足事件由擴展的事件實現(xiàn)。

2)擴展狀態(tài)形成

擴展狀態(tài)形成階段處理其他不能由基本狀態(tài)中的事件實現(xiàn)的擴展事件，即US表示由擴展事件實現(xiàn)的事件。在狀態(tài)處理前，首先需要將狀態(tài)中的未滿足事件加入到US中，然后采用與基本搜索中相同的方法進行處理，不再復述，但需要指出，當由已經(jīng)存在的事件實現(xiàn)時，只能與RID<0的事件綁定。

擴展搜索階段形成協(xié)議的擴展狀態(tài)集。基本狀態(tài)集與擴展狀態(tài)集共同形成協(xié)議的最終狀態(tài)，它們都包含了協(xié)議的初始狀態(tài)，也都是協(xié)議可能的運行，但兩者的側(cè)重點不同:初始搜索的目的在于找到初始狀態(tài)的實現(xiàn)方式，基本狀態(tài)包含的是實現(xiàn)初始狀態(tài)必需的事件，給出的是協(xié)議運行過程中一些關(guān)鍵的事件。協(xié)議的一些安全性質(zhì)，如存在性等，其驗證目標與基本搜索的目標是一致的;擴展搜索的目的在于找到協(xié)議運行與其他運行的聯(lián)系，擴展狀態(tài)包含的是與初始狀態(tài)有關(guān)的事件，一些攻擊，如不滿足單射性的協(xié)議就是通過以前的會話來實現(xiàn)現(xiàn)在的會話，再如猜測攻擊，攻擊者的目的就是盡可能多地獲取相關(guān)消息以進行猜測值的驗證，但這并不表示在基本狀態(tài)中就不存在猜測攻擊。因此，在進行安全性質(zhì)驗證時，需要考慮形成的所有最終狀態(tài)。

3.3 有效狀態(tài)檢驗

狀態(tài)推理過程中采用以下一些策略對形成的狀態(tài)進行有效性檢驗:

a)無環(huán)性，即協(xié)議狀態(tài)是一個有向無環(huán)圖。

b)e，e′∈event，若e→e′，則在e之前不存在滿足type(e″)=send|insert，msg(e″)=msg(e)的事件e″，即事件由最早出現(xiàn)的事件來實現(xiàn)。

c)if US=， thene，e′∈event， if msg(e)=msg(e′)∧e∧e′e， then e=e′，即消息最早出現(xiàn)的事件是惟一的。

d)未滿足事件可滿足性。

3.4 驗證機制分析

驗證機制首先通過實現(xiàn)未滿足事件來對協(xié)議狀態(tài)進行擴展，擴展過程考慮了所有可能的實現(xiàn)方法，且通過狀態(tài)有效性策略對得到的狀態(tài)進行了檢查，從而保證了得到的協(xié)議狀態(tài)的正確性和完備性。

在擴展搜索中的基本狀態(tài)綁定中，它首先在基本狀態(tài)中加入各個角色的一個初始實例，初始實例只實例化了事件中的隨機數(shù)，因此，可以代表其他所有可能的實例運行。

在處理未滿足事件時，match事件不進行協(xié)議交互，不能直接與基本狀態(tài)產(chǎn)生聯(lián)系，只能從receive事件入手，通過receive和take事件來與基本狀態(tài)產(chǎn)生聯(lián)系，該步采用了組合的方法，對所有可能由初始狀態(tài)實現(xiàn)的事件進行組合，從而給出了所有可能由基本狀態(tài)實現(xiàn)的情況。協(xié)議的角色數(shù)是有限的，含有的接收事件也是有限的，其組合數(shù)也是有限的，所以該過程需要考慮的情況也是有限的。

基本狀態(tài)綁定也給出了基本狀態(tài)與協(xié)議其他運行的所有可能的關(guān)系，該擴展也是正確完備的。

4 安全性質(zhì)驗證

上一章給出了協(xié)議的驗證機制，從得到的最終狀態(tài)中可以得到協(xié)議具體的運行過程，因此，本文的驗證機制支持所有基于跡的協(xié)議安全性質(zhì)的驗證。下面以單射一致性為例進行說明，據(jù)本文所知，在相關(guān)算法中，還沒有對單射性進行過驗證，這也在一方面說明了本文驗證機制的意義。

另外，本文驗證機制不依賴于安全性質(zhì)，從而可以同時對多種安全性質(zhì)進行驗證，避免重復的狀態(tài)推理，提高了證效率。

下面首先給出單射一致性和猜測攻擊的定義，然后在下節(jié)中用具體實例進行說明。

4.1 單射一致性

單射一致性要求角色A的每一次運行對應著角色B的惟一一次運行，且兩者在參數(shù)上達到了一致。

因為協(xié)議主體是通過其通信事件來確定雙方數(shù)據(jù)是否達到了一致，所以可通過通信事件的消息內(nèi)容來判斷參數(shù)的一致性。形式化定義單射一致性為

state，s∈state，aprinc(s)=p，pprinc(s)=p′:

if type(s)=send，thenunique one r∈tr:

aprinc(r)=p′∧pprinc(r)=p∧type(t)=receive∧msg(s)=msg(r)，

if type(s)=receive， thenuniqueone r∈tr:

aprinc(r)=p′∧pprinc(r)=p∧type(t)=send∧msg(r)=msg(s)

一致性由事件的消息內(nèi)容保證，單射性由事件執(zhí)行的次數(shù)保證。

4.2 猜測攻擊

猜測攻擊是指攻擊者通過窮舉得到秘密項，然后通過某種方式對猜測值進行驗證的一類攻擊[9]。

可實施猜測攻擊的攻擊者具有消息猜測能力，它從協(xié)議運行中獲得相關(guān)消息項，猜測秘密項的值，猜測值的驗證過程也是通過攻擊者推導。因此，本文也對猜測攻擊進行了研究，攻擊者的猜測能力由消息驗證時攻擊者的知識表示。

設IKsm是攻擊者利用知識IKs∪m推導得到的新知識集合，IKs是攻擊者在狀態(tài)s下具有的知識集，在只考慮離線猜測攻擊的情況下，可形式化定義針對m的猜測攻擊為

state，IKs∩{m}=∧IKsm∩{IKs∪m}=∧t1，t2∈IKsm，t1≠t2

下面對其進行解釋:

a)IKs∩{m}=。若該條件不成立，說明攻擊者可以直接推導得到m，m就是驗證項。

b)IKsm∩{IKs∪m}=。設v∈IKsm∩{IKs∪m}，這說明攻擊者通過協(xié)議運行或猜測具有了項v，在猜測m的值后又可以得到v，v是m的驗證項。

c)t1，t2∈IKsm，t1≠t2。若IKsm中有兩個相同的項，說明攻擊者在猜測m后，可以通過兩種不同的方式推導得到驗證項，相同的項即猜測值的驗證項。

如果協(xié)議狀態(tài)滿足以上三條，那么就排除了攻擊者所有可能的驗證方式[9]，從而可以保證協(xié)議狀態(tài)不存在猜測攻擊。

5 實例分析

Lomas、Gong、Saltzer 和Needham給出了如下協(xié)議:

a→s:{a，b，na1，na2，ca，{ta}passwd(a)}pks;s→b:a，b;b→s:{b，a，nb1，nb2，cb，{tb}passwd(b)}pks;s→a:{na1，k⊕na2}passwd(a);s→b:{nb1，k⊕nb2}passwd(b);b→a:{rb}k;a→b:{rb+1，ra}k;b→a:{ra+1}k;

其中:pks是s的公鑰; na1、na2、nb1、nb2、ra、rb、ca和cb是隨機數(shù); ta和tb是時戳。

從S的一個實例出發(fā)進行驗證，初始搜索可得到代表協(xié)議正常運行的前五步。驗證可知，此狀態(tài)滿足單射一致性，沒有猜測攻擊。進行狀態(tài)擴展，依次加入?yún)f(xié)議各個角色的一個運行實例，得到如下擴展狀態(tài):

(1)A→S:{A，I，Na1，Na2，Ca，{0}passwd(A)}pks

(2)S→I:A，I

(3)I→S:{I，A，Ni，Ni，Ci，{1}passwd(I)}pks

(4)S→IA:{Na1，K1⊕Na2}passwd(A)

(5)S→I:{Ni1，K1⊕Ni2}passwd(A)

(1.1)IA→S:{A，I，Na1，Na2，Ca，{0}passwd(A)}pks

(1.2)S→I:A，I

(1.3)I→S:{I，A，Ni，Ni，Ci，{1}passwd(I)}pks

(1.4)S→IA:{Na1，K2⊕Na2}passwd(A)

(1.5)S→I:{Ni1，K2⊕Ni2}passwd(A)

利用安全性質(zhì)進行驗證可知，該協(xié)議不滿足S的單射一致性，S的二次運行對應著A的一次運行，且該協(xié)議具有針對passwd(A)的猜測攻擊:在IKs中，攻擊者具有消息{Na1，K1⊕Na2}passwd(A)和{Na1，K2⊕Na2}passwd(A)，猜測passwd(A)后，分別解密這兩條消息攻擊者都可以得到Na1，進行比較可驗證猜測值。驗證時IKsm中具有了兩個相同項，可直接得到存在猜測攻擊，Na1是驗證項。

6 結(jié)束語

本文給出了一種基于狀態(tài)擴展的安全協(xié)議自動化驗證機制，通過基本搜索和擴展搜索得到了協(xié)議可能的運行，然后給出了單射一致性和猜測攻擊的定義，用具體實例說明了驗證機制的有效性和驗證效率。該驗證機制既有效避免了狀態(tài)空間爆炸問題，又能夠反映出協(xié)議可能的運行情況，有利于攻擊者能力的擴展，便于實現(xiàn)高效的安全性質(zhì)自動化驗證，同時由于該機制支持多協(xié)議目標的驗證，從而大大提高了協(xié)議驗證的效率。下一步將重點研究攻擊者模型，并通過大量實例對該機制進行測試。

參考文獻:

[1]SONG D X. Athena: a new efficient automatic checker for security protocol analysis[C]//Proc of the 12th IEEE Computer Security Foundations Workshop. Los Alamitos: IEEE Computer Society Press，1999.

[2]劉東喜.安全協(xié)議的自動驗證技術(shù)研究[D]. 上海:上海交通大學，2002.

[3]CREMERS C J F. Unbounded verification of security protocols， Technical Report No.572[R]. 2006.

[4]FABREGA F J T， GUTTMAN J. Strand spaces: why is a security protocol correct?[C]//Proc of IEEE Symposium on Security and Privacy. 1998.

[5]CHEMINOD M， BERTOLOTTI I C， DURANTE L ， et al. Experimental comparison of automatic tools for the formal analysis of cryptographic protocols[C]//Proc of the 2nd International Conference on Dependability of Computer Systems. 2007.

[6]DOLEV D， YAO A C. On the security of public key protocols[J]. IEEE Trans on Information Theory， 1983， 29(2): 198-208.

[7]LOWE G. A hierarchy of authentication specifications[C]//Proc of CSFW’97. 1997:31-44.

[8]CORIN R. Analysis models for security protocols[D]. The Netherlands:University of Twente， 2006:41-45.

[9]CREMERS C J F. Unbounded verification， falsification， and characterization of security protocols by pattern refinement[C]//Proc of the 15th ACM Conference on Computer and Communictions Security. New York:ACM Press， 2008:119-128.

[10]LOWE G. Analyzing protocols subject to guessing attacks[J]. Journal of Computer Security， 2004，12(1):83-89.