唐鄭熠，楊芳，薛醒思

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

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

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

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

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

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

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

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

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

1 DY模型概述

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

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

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

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

·攻擊者可以偽造消息。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

DY模型的構(gòu)建框架明確了在實(shí)現(xiàn)DY模型時(shí)所需要描述的攻擊者要素，并限定了攻擊者所能夠采取的行為以及行為的順序，這為DY模型的實(shí)現(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)鍵，后者則是攻擊者的重要攻擊手段?；凇鞍踩珔f(xié)議底層的密碼體制與算法假定完善”的基本假設(shè)，給出消息分解與構(gòu)造的算法。

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

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

4 實(shí)例驗(yàn)證

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

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

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

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

（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)識(shí)（A與B）和臨時(shí)值（na與nb）向服務(wù)器中心申請(qǐng)會(huì)話密鑰，服務(wù)中心（S）為會(huì)話雙方各生成一個(gè)會(huì)話密鑰包，其中包含：會(huì)話方的臨時(shí)值（用于確認(rèn)證書的有效性）、主體標(biāo)識(shí)（用于標(biāo)識(shí)會(huì)話密鑰的適用對(duì)象）、共享會(huì)話密鑰（K）。會(huì)話密鑰證書適用會(huì)話方與服務(wù)中心的共享密鑰加密（KAS與KBS）。

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

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

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

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

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

通過(guò)對(duì)攻擊軌跡的分析，得出以下攻擊過(guò)程：

（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｝

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

5 結(jié)論

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

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

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

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

［4］陳春玲，田國(guó)良．安全協(xié)議的SPIN建模與分析［J］．南京航空航天大學(xué)學(xué)報(bào)，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語(yǔ)言建模及檢測(cè)［J］．計(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

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

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