唐鄭熠，楊芳，薛醒思

（1．福建工程學(xué)院信息科學(xué)與工程學(xué)院，福建福州350118；2．湖南大學(xué)信息科學(xué)與工程學(xué)院，湖南長沙410082；3．湖南醫(yī)藥學(xué)院圖書館，湖南懷化418000）

安全協(xié)議驗證中DY模型的構(gòu)建框架

唐鄭熠1，楊芳2，3，薛醒思1

（1．福建工程學(xué)院信息科學(xué)與工程學(xué)院，福建福州350118；2．湖南大學(xué)信息科學(xué)與工程學(xué)院，湖南長沙410082；3．湖南醫(yī)藥學(xué)院圖書館，湖南懷化418000）

攻擊者建模是安全協(xié)議驗證工作的一個重要部分，直接影響到驗證的效率與質(zhì)量，但目前卻還沒有一個可遵循的形式化框架，影響了建模工作的準(zhǔn)確性與客觀性。針對這一問題，通過對在安全協(xié)議驗證中具有廣泛影響的DY模型進(jìn)行形式化，建立了一個DY模型的構(gòu)建框架，刻畫了攻擊者的構(gòu)成要素、行為規(guī)則以及行為模式，從而保證了攻擊者具有合理的行為與能力，并能在攻擊過程中獲取新的知識，不斷增強(qiáng)攻擊能力。最后，將該工作運用到Otway-Rees協(xié)議的驗證中，找出了該協(xié)議中所存在的漏洞，從而證明了該構(gòu)建框架的有效性。

安全協(xié)議；形式化；DY模型；攻擊者；Otway-Rees協(xié)議

安全協(xié)議又稱為密碼協(xié)議，是以密碼學(xué)為基礎(chǔ)的信息交換協(xié)議，其目的是在一個開放的網(wǎng)絡(luò)環(huán)境中，提供保密的信息交換和傳遞服務(wù)。它解決了包括主體認(rèn)證、保障消息完整、防止消息偽造、防止消息抵賴等一系列關(guān)鍵的安全問題，并成為目前最重要的通信安全保障手段。然而設(shè)計高質(zhì)量的安全協(xié)議是十分困難且容易出錯的，即使是最簡單的、只包括若干有限主體和消息的認(rèn)證協(xié)議，迄今也沒有一種技術(shù)能夠保障所設(shè)計的協(xié)議能夠絕對正確、符合需求。

形式化方法是目前最有效的安全協(xié)議分析技術(shù)，它將協(xié)議主體、攻擊者與協(xié)議環(huán)境進(jìn)行抽象，建立數(shù)學(xué)模型，通過模型所支持的計算技術(shù)驗證模型所具有的性質(zhì)，從而發(fā)現(xiàn)協(xié)議中所存在的缺陷。這種分析技術(shù)的一個關(guān)鍵問題在于攻擊者的建模，不恰當(dāng)?shù)墓粽吣Ｐ蜔o法有效找出協(xié)議的漏洞。迄今為止的大部分相關(guān)工作，都是以Dolev與Yao所提出的DY模型［1］作為攻擊者建模的依據(jù)。

盡管DY模型在實際的安全協(xié)議驗證中具有重要的作用與意義，并被許多研究工作所引用，但基本都集中于用不同的語言或工具對其進(jìn)行實現(xiàn)［2-6］，而鮮有對其進(jìn)行形式刻畫、為具體實現(xiàn)提供框架。這導(dǎo)致當(dāng)研究人員在用不同的方法實現(xiàn)DY攻擊者模型時，缺乏一個可遵循的統(tǒng)一而精確的框架，從而造成不同的實現(xiàn)之間可能存在差異，并可能偏離DY模型的真實行為與能力。針對這一問題，本文構(gòu)建了一個DY模型的形式化框架，定義了DY模型的構(gòu)成要素、行為規(guī)則以及行為模式，為攻擊者的建立提供了可遵循的統(tǒng)一標(biāo)準(zhǔn)，可作為安全協(xié)議自動驗證技術(shù)的基礎(chǔ)。

1 DY模型概述

DY模型是Dolev與Yao在1983年提出的，它基于安全協(xié)議的分層次分析的思想，即先研究安全協(xié)議本身的行為邏輯是否存在缺陷，然后再考慮實現(xiàn)方法是否存在問題（如所采用的密碼算法）。

因此，對安全協(xié)議的驗證，都建立在假定完善的底層密碼體制及算法的基礎(chǔ)之上，攻擊者被認(rèn)為不具有攻破密碼算法的能力。具體來說，就是在未掌握對應(yīng)密鑰的情況下，攻擊者無法獲知加密消息中的信息。在這個前提下，DY模型規(guī)定了攻擊者可以具有以下行為與能力：

·攻擊者可以在不被協(xié)議主體察覺的情況下，竊聽到通訊網(wǎng)絡(luò)中的所有消息。

·攻擊者可以在不被協(xié)議主體察覺的情況下，攔截并存儲通訊網(wǎng)絡(luò)中的所有消息。

·攻擊者可以偽造消息。

·攻擊者可以發(fā)送消息。

·攻擊者也可以作為合法的協(xié)議主體，參與協(xié)議的運行。

DY模型下的攻擊者具有控制整個網(wǎng)絡(luò)的能力，協(xié)議的整個執(zhí)行過程都可能暴露在攻擊者的監(jiān)視之下，并且攻擊者還能夠隨時干擾或參與協(xié)議的執(zhí)行過程。

盡管DY模型對攻擊者的行為進(jìn)行了限定，但卻并沒有給出必要的規(guī)則，例如行為執(zhí)行的順序、偽造消息的方法、如何成為合法主體等，這導(dǎo)致在建模過程中DY模型難以被精確實現(xiàn)，并且在不同的驗證工作中存在差異性。

2 DY模型的構(gòu)建框架

依據(jù)有關(guān)DY模型研究的相關(guān)文獻(xiàn)［7-8］，本節(jié)將首先給出DY模型的形式化定義，即總體的構(gòu)建框架。

在安全協(xié)議中，主體之間是通過網(wǎng)絡(luò)交換消息來進(jìn)行交互，因此首先給出消息的形式化定義。本文的工作基于非對稱密鑰體制，但也可以運用在對稱密鑰體制上。

定義1（消息） 安全協(xié)議的主體之間交換的消息M符合以下形式之一：

·M＝m：m是不可再分的原子消息，如主體標(biāo)識、臨時值等．

·M＝｛M1，M2…Mn｝：由多個消息構(gòu)成的普通消息．

·M＝KX｛M1，M2…Mn｝：使用主體X的公鑰加密的消息．

·M＝KX-1｛M1，M2…Mn｝：使用主體X的私鑰簽名的消息

遵循DY模型的攻擊者在運行時，需要使用到一些自身掌握或在運行過程中獲取的信息，稱為知識。

定義2（知識） DY模型中的知識指的是偽造消息時所用到信息，包括各種類型的原子消息、密鑰以及簽名消息等。

攻擊者所采取的行為需遵循一定的順序，稱為行為模式。為了描述行為模式，需要用到以下行為模式運算符：

定義3（行為模式運算符） 在DY模型的行為模式中，包含以下行為模式運算符：

·→：順序運算符，描述兩個行為的執(zhí)行具有先后順序，形如act1∨act2．

·∨：隨機(jī)運算符，描述隨機(jī)選取兩個行為中的一個執(zhí)行，形如act1∨act2．

·R（φ）：重復(fù)運算符，描述一個行為重復(fù)執(zhí)行，形如R（φ）［act］；φ是重復(fù)條件，可用邏輯公式表示，當(dāng)它的取值為假時，行為act中止．

下面給出DY模型的形式化構(gòu)建框架：

定義4（DY模型的構(gòu)建框架） DY＝（KN，ACT，BS，MD，NET），其中：

·KN＝kn1∪kn2∪…knn：是攻擊者的知識庫，kni表示不同類型的知識庫。

·ACT＝｛Intercept，Resolve，F(xiàn)orge，Choose，Send｝：是攻擊者的行為集合。

·BS＝R（true）［（Intercept→Resolve）∨（（Forge∨Choose）→Send）］：是攻擊者的行為模式，刻畫了攻擊者的行為執(zhí)行順序。

·MD＝＜M1，M2，…Mn＞：是攻擊者的消息庫，用于存放攻擊者所需保存的消息。

·NET＝＜M1，M2，…Mn＞：是攻擊者所監(jiān)聽的網(wǎng)絡(luò)，同時也是協(xié)議的其他主體所使用的網(wǎng)絡(luò)；攻擊者能夠從中攔截一條消息，也能夠向其中添加一條消息。

DY模型的構(gòu)建框架限定了攻擊者可以具有的5種行為，同時通過行為模式限定了這5種行為的執(zhí)行順序：

·Intercept：攻擊者執(zhí)行Intercept行為時，會從其所監(jiān)聽的網(wǎng)絡(luò)中攔截并存儲一條消息。

·Resolve：攻擊者執(zhí)行Resolve行為時，會運用知識庫中的知識，將一條消息進(jìn)行分解，并擴(kuò)充自己的知識庫。

·Forge：攻擊者執(zhí)行Forge行為時，會運用知識庫中的知識，構(gòu)造一條消息。

·Choose：攻擊者執(zhí)行Choose行為時，會從消息庫中隨機(jī)選取一條以前攔截過的消息。

·Send：攻擊者執(zhí)行Send行為時，會將一條消息發(fā)送到其所監(jiān)聽的網(wǎng)絡(luò)中。

攻擊者通過Intercept行為獲取通訊網(wǎng)絡(luò)中所傳輸?shù)南ⅲ瑢⑵浯鎯Σ⒎纸?，從而擴(kuò)充消息庫與知識庫。而隨著消息庫與知識庫的擴(kuò)充，攻擊者的能力將會不斷增強(qiáng)，并能夠通過發(fā)送不同來源的消息干擾或參與協(xié)議的運行，并可能最終攻破協(xié)議。各行為之間的關(guān)系如圖1所示。

DY模型的構(gòu)建框架明確了在實現(xiàn)DY模型時所需要描述的攻擊者要素，并限定了攻擊者所能夠采取的行為以及行為的順序，這為DY模型的實現(xiàn)提供了依據(jù)與準(zhǔn)則。

圖1 DY模型行為之間的關(guān)系Fig．1 The relationship among the behaviours in DY model

3 消息分解與構(gòu)造

在DY模型的5種行為中，Resolve（分解消息）行為與Forge（構(gòu)造消息）行為是最為重要的，前者是攻擊者的攻擊能力不斷增強(qiáng)的關(guān)鍵，后者則是攻擊者的重要攻擊手段。基于“安全協(xié)議底層的密碼體制與算法假定完善”的基本假設(shè)，給出消息分解與構(gòu)造的算法。

對于一條非加密的消息，攻擊者可以直接進(jìn)行分解；而對于加密消息，則要根據(jù)知識庫中的知識判定是否能夠分解。消息分解的過程如算法1所述。

攻擊者可以運用知識庫中的知識，構(gòu)造一條新的消息。但對于具體的安全協(xié)議，構(gòu)造該協(xié)議中不存在的消息類型是沒有意義的。為了避免這個問題，通過參數(shù)來指定構(gòu)造消息的類型。消息構(gòu)造的過程如算法2所述。

4 實例驗證

SPIN模型檢測是一種實現(xiàn)安全協(xié)議自動驗證的有效技術(shù)，屬于形式化方法的一類。使用SPIN技術(shù)驗證安全協(xié)議的過程如圖2所示。

圖2 基于SPIN的安全協(xié)議自動驗證過程Fig．2 The autom atic verification process based on SPIN safety protocol

建模工作包括三個部分：協(xié)議主體的建模、攻擊者的建模以及協(xié)議目標(biāo)的形式化。然后，將模型直接輸入模型檢查器，由其進(jìn)行自動驗證。最終，模型檢測器將給出驗證結(jié)果：協(xié)議目標(biāo)滿足，或者攻擊者攻破協(xié)議的軌跡。

為了驗證前文所構(gòu)建的攻擊者建?？蚣艿挠行?，本節(jié)對一個密鑰協(xié)商協(xié)議——Otway-Rees協(xié)議［9］進(jìn)行驗證。OR協(xié)議的目的，是為會話雙方，建立一個相同的會話密鑰。OR協(xié)議本身存在缺陷，因此之后又出現(xiàn)了它的改進(jìn)版本［10］，本文以這個改進(jìn)版本作為驗證的實例：

（1）A→B：A，B，na

（2）B→S：A，B，na，nb

（3）S→B：KAS｛na，A，B，K｝，KBS｛nb，A，B，K｝

（4）B→A：KAS｛na，A，B，K｝

協(xié)議主體使用主體標(biāo)識（A與B）和臨時值（na與nb）向服務(wù)器中心申請會話密鑰，服務(wù)中心（S）為會話雙方各生成一個會話密鑰包，其中包含：會話方的臨時值（用于確認(rèn)證書的有效性）、主體標(biāo)識（用于標(biāo)識會話密鑰的適用對象）、共享會話密鑰（K）。會話密鑰證書適用會話方與服務(wù)中心的共享密鑰加密（KAS與KBS）。

協(xié)議主體的建模遵循上述的描述，而攻擊者的建模則遵循前文所構(gòu)建的形式化框架。OR協(xié)議的目標(biāo)有兩個：

（1）保證服務(wù)中心S分發(fā)的會話密鑰K，不會被除A和B外的第三方獲知。

（2）保證A和B所獲得的會話密鑰是一致的。

驗證結(jié)果表明，本文所構(gòu)建的攻擊者無法破壞OR協(xié)議的第一個目標(biāo)，即無法獲得會話密鑰K。但對于第二個目標(biāo)，在攻擊者（P）的干擾下，則無法達(dá)成。攻擊者攻破協(xié)議的軌跡如圖3所示。

圖3 攻破協(xié)議的軌跡Fig．3 The trail of breaking through the protocol

通過對攻擊軌跡的分析，得出以下攻擊過程：

（1）A→B：A，B，na

（2）B→P：A，B，na，nb

（3）P→S：A，B，na，nb

（4）S→P：KAS｛na，A，B，K1｝，KBS｛nb，A，B，K1｝

（5）P→S：A，B，na，nb

（6）S→P：KAS｛na，A，B，K2｝，KBS｛nb，A，B，K2｝

（7）P→B：KAS｛na，A，B，K1｝，KBS｛nb，A，B，K2｝

（8）B→A：KAS｛na，A，B，K1｝

由于會話雙方的臨時值是不加密的，因此攻擊者可以使用臨時值申請到多個不同的會話密鑰包，并進(jìn)行組合，從而讓會話雙方得到不一致的會話密鑰。在這個攻擊過程中，攻擊者所用到的操作包括：攔截消息、發(fā)送消息、分解消息、構(gòu)造消息。這些都是本文所構(gòu)建的攻擊者所具備的能力。

5 結(jié)論

本文分析了安全協(xié)議驗證工作具有重大影響的DY模型，給出了構(gòu)建該模型的形式化框架，定義了遵循DY模型的攻擊者所應(yīng)具有的要素、行為以及行為模式，并給出了消息分解與構(gòu)造的算法。同時，通過對Otway-Rees協(xié)議的實例驗證，證明了該構(gòu)建框架的有效性。這一工作可以運用在安全協(xié)議驗證工作中的攻擊者建模的部分，使得攻擊者的建模工作更為客觀，并保證在不同的驗證工作中，攻擊者能夠具有一致的行為與能力。

［1］Dolev D，Yao A．On the security of public key protocols［J］．IEEE Transactions on Information Theory，1983，29（2）：198-208．

［2］鐘軍，吳雪陽，江一民，等．一種安全協(xié)議的安全性分析及攻擊研究［J］．計算機(jī)工程與科學(xué)，2014，36（6）：1077-1082．

［3］冉俊鐵，吳盡昭．基于SPIN的安全協(xié)議形式化驗證技術(shù)［J］．計算機(jī)應(yīng)用，2014：34（S2）：85-90．

［4］陳春玲，田國良．安全協(xié)議的SPIN建模與分析［J］．南京航空航天大學(xué)學(xué)報，2009，41（5）：672-676．

［5］Fu Yulong，Ousmane K．A finite transitionmodel for security protocol verification［C］／／Proc of6th International Conference on Security of Information and Networks．Aksaray，Turkey，2013．

［6］龍士工，王巧麗，李祥．密碼協(xié)議的Promela語言建模及檢測［J］．計算機(jī)應(yīng)用，2005，25（7）：1548-1550．

［7］Kanovich M，Kiriginc T B，Nigamd Vi，et al．Bounded memory Dolev-Yao adversaries in collaborative systems［J］．Information and Computation，2014，238：233-261．

［8］Mazare L．Satisfiability of Dolev-Yao constraints［J］．Electronic Notes in Theoretical Computer Science，2005，125（1）：109-124．

［9］Otway D，Rees O．Efficient and timelymutual authentication［J］．ACM Operating Systems Review，1987，21（1）：8-10．

［10］AbadiM，Needham R．Prudent engineering practice for cryptographic protocols［J］．IEEE Transactions on Software Engineering，1996，22（1）：6-15．

（責(zé)任編輯：肖錫湘）

A framework for constructing DY model in security protocol verification

Tang Zhengyi1，Yang Fang2，3，Xue Xingsi1
（1．College of Information Science and Engineering，F(xiàn)ujian University of Technology，F(xiàn)uzhou 350118，China；2．College of Computer Science and Electronic Engineering，Hunan University，Changsha 410082，China；3．Library of Hunan University of Medicine，Huaihua 418000，China）

Themodelling of intruders is an important partof security protocol verification，which directly affects the efficiency and correctness of verification．There is no available formal framework of introdersmodelling，which is a disadvantage formodelling work．A framework for formalizing／constructing DY model that has extensive influence on security protocol verification was proposed．The framework can depict the components，behaviours and behaviourmodel of the intruders，which ensures that the intruder has reasonable behaviours and ability and can acquire new knowledges in the attacking process to enhance contantly the attacking ability．The effectiveness of the framework was confirmed in the verification of Otway-Rees protocol in which a fault in the protocolwas found．

security protocol；formalization；Dolev and Yao（DY）model；intruder；Otway-Rees protocol

TP393．08

A

1672-4348（2015）03-0239-05

10．3969／j．issn．1672-4348．2015．03．007

2015-04-20

福建省中青年教師教育科研項目（JB14069）；福建工程學(xué)院科研啟動基金項目（GY-Z13112）

唐鄭熠（1984-），男，福建福州人，博士，講師，研究方向：形式化方法。