一種協(xié)議抗拒絕服務(wù)的形式化分析方法研究

金大鵬， 林宏剛

(成都信息工程大學(xué)信息安全工程學(xué)院，四川成都610225)

0 引言

DoS攻擊是一種常見的網(wǎng)絡(luò)攻擊方式［1］，是通過各種手段使提供服務(wù)的主機(jī)無法提供正常服務(wù)的一種攻擊，按照攻擊方式可分為:物理破壞型、服務(wù)中止型、資源消耗型。傳統(tǒng)的形式化分析方法，如BAN類邏輯等，往往注重的是協(xié)議的認(rèn)證性、秘密性等，忽略了協(xié)議的可用性，無法及時發(fā)現(xiàn)協(xié)議存在的DoS攻擊。隨著互聯(lián)網(wǎng)的飛速發(fā)展，DoS攻擊帶來的危害越來越大，因此，已經(jīng)有專家學(xué)者對DoS攻擊的形式化建模方法進(jìn)行了深入研究。

Meadows提出的基于代價的形式化分析方法［2-4］，適合對資源消耗型DoS攻擊進(jìn)行建模，該建模方法通過設(shè)置容忍關(guān)系，比較產(chǎn)生一個數(shù)據(jù)和驗證這個數(shù)據(jù)所要花費的代價大小，判斷協(xié)議是否存在DoS攻擊。基于Meadows的形式化分析模型，Minea與Groza分析了JFK與STS協(xié)議［5］，指出 JFK協(xié)議能夠抵抗DoS攻擊，而STS協(xié)議不具有抗DoS攻擊能力。基于時態(tài)邏輯，Yu和Gligor引入用戶合約，提出一種對共享服務(wù)DoS攻擊的形式化規(guī)范與驗證方法［6］，該方法的核心思想是以訪問控制策略為基礎(chǔ)，對DoS攻擊進(jìn)行建模，所以不能處理發(fā)生在認(rèn)證之前的DoS攻擊。周世健等［7］在基本串空間的基礎(chǔ)上［8-10］，進(jìn)行了擴(kuò)展，提出了判斷安全協(xié)議DoS攻擊分析的2條檢驗規(guī)則，并利用這兩條規(guī)則，分析了IEEE802.11i 4步握手協(xié)議，發(fā)現(xiàn)其存在的DoS攻擊，并針對此提出了改進(jìn)辦法。這些規(guī)則是基于代價，能夠較好地分析資源消耗型DoS攻擊，但是對服務(wù)中止型DoS攻擊卻無能為力。孟博等［11］從進(jìn)程表達(dá)式和攻擊者上下文2個方面擴(kuò)展了標(biāo)準(zhǔn)應(yīng)用PI演算，并且從協(xié)議狀態(tài)的角度，建立安全協(xié)議抗DoS攻擊分析模型，并驗證了模型的有效性。由于該方法主要是從協(xié)議狀態(tài)的角度分析抗DoS攻擊性，因此可以分析由于協(xié)議的狀態(tài)保持而產(chǎn)生的資源消耗型DoS攻擊，以及服務(wù)中止型DoS攻擊，但是在分析其他原因產(chǎn)生的資源消耗型DoS攻擊時還存在不足。

提出一種擴(kuò)展的串空間模型，在基本串空間模型中引入消息相關(guān)度集合，代價函數(shù)，使串空間模型能夠全面、有效地分析安全協(xié)議是否存在DoS攻擊。

1 擴(kuò)展的串空間模型理論

以基本串空間模型為基礎(chǔ)，參考Meadows提出的基于代價的DoS攻擊形式化建模方法，在串空間模型中引入消息相關(guān)度集合，使模型能夠分析服務(wù)中止型DoS攻擊;引入代價函數(shù)，使模型能夠分析資源消耗型DoS攻擊。新的模型保留了串空間模型原有的分析協(xié)議安全性的優(yōu)點，同時具有對協(xié)議是否能夠抵抗DoS攻擊進(jìn)行全面分析的能力。

1．1 串空間模型基本概念

Fabrega，Herzog和Guttman在1998年提出了串空間模型理論，用于分析認(rèn)證協(xié)議。串空間包含誠實主體的串和攻擊者的串，利用串空間模型，能夠證明協(xié)議的認(rèn)證性與機(jī)密性，以下為詳細(xì)的串空間模型介紹。

設(shè)集合A中的元素為協(xié)議主體交換的消息，則稱A為項集合，A的元素為項。

定義1 集合{+，-}是串空間的動作集，其中“+”表示發(fā)送消息的動作，“-”表示接收消息的動作。

定義2 二元組＜σ，a＞表示一個事件，其中σ∈{+，-}，a∈A。用+a和-a代表一個事件.TIF，+a和-a稱為帶符號的消息。(±A)*為帶符號項的有限序列集合。

定義3 串是協(xié)議參與者所執(zhí)行事件的序列，令∑表示串的集合，定義跡映射tr:∑→(±A)*，將一個串映射到有限消息序列的集合。

定義4 串空間的其他基本概念:

(1)結(jié)點，假設(shè)串s∈∑，s中的每個事件稱為串s的一個結(jié)點，用n=＜s，i＞表示，其中i是結(jié)點n在串中序號。結(jié)點n屬于串s，記為n∈s，結(jié)點的集合記為N。

(2)結(jié)點 n= ＜s，i＞ ∈s，定義 index(n)=i，strand(n)=s，若結(jié)點n代表的實體動作為(tr(s))i=σa，定義 term(n)=σa，uns-term(n)=((tr(s))i)2=a，sign(n)=σ，稱term為結(jié)點事件函數(shù)，uns-term(n)為結(jié)點消息函數(shù)，sign為結(jié)點符號函數(shù)。

(3)結(jié)點 n1，n2∈N，存在一個邊 n1→n2，當(dāng)且僅當(dāng)term(n1)=+a，term(n2)=-a，稱 n1發(fā)送消息 a給n2，或者n2從n1接收消息a。

(4)若 n1= ＜s，i＞，n2= ＜ s，i+1 ＞，則存在邊 n1?n2，稱作事件相繼發(fā)生，表示事件n2在事件n1之后發(fā)生，稱n1是n2在同一個串上的因果前驅(qū)。

1．2 消息相關(guān)度集合

若結(jié)點 ni，nj屬于 N，Mi為 term(ni)的所有子項構(gòu)成的集合，Mj為term(nj)的所有子項構(gòu)成的集合，則結(jié)點ni，nj的消息相關(guān)度集合定義為集合Mi與集合Mj的交集O，集合O反應(yīng)了結(jié)點ni和nj的消息相關(guān)程度，若O為空集，表明ni和nj是不相關(guān)的，反之，若集合O中包含的元素越多，表明結(jié)點ni和nj的消息相關(guān)程度越高。

1．3 代價函數(shù)

如圖1所示，定義代價函數(shù)為邊n1→m1及m1?m2的集合到非負(fù)實數(shù)R的映射，其中邊n1→m1到非負(fù)實數(shù)R的映射用函數(shù)f表示，若n1發(fā)送消息a給m1，則fa表示n1產(chǎn)生并發(fā)送消息a所付出的代價值;邊m1?m2到非負(fù)實數(shù)R的映射用函數(shù)g表示，若結(jié)點m1接收了來自另一個串的消息a后，由事件m1變?yōu)槭录2，則ga表示接收并對消息a進(jìn)行處理所付出的代價值。

圖1 代價函數(shù)串空間模型

2 基于擴(kuò)展的串空間模型的DoS攻擊分析方法

利用上文提出的消息相關(guān)度集合和代價函數(shù)，提出兩條檢驗規(guī)則，分析安全協(xié)議抗服務(wù)中止型DoS攻擊和資源消耗型DoS攻擊的能力。

服務(wù)中止型DoS攻擊產(chǎn)生的原因是協(xié)議本身存在缺陷，當(dāng)攻擊者篡改請求者數(shù)據(jù)，或者發(fā)送偽造的虛假數(shù)據(jù)時，響應(yīng)者卻不能及時發(fā)現(xiàn)，仍然當(dāng)作正常的數(shù)據(jù)處理，導(dǎo)致認(rèn)證失敗，協(xié)議不能繼續(xù)向下執(zhí)行，造成DoS。基于此，提出如下規(guī)則1。

規(guī)則1:設(shè)s是協(xié)議的響應(yīng)者串，ni，nj是s中滿足sign(ni)=-，sign(nj)=-的任意兩個結(jié)點，其中i＜j，O為ni和nj的消息相關(guān)度集合，若O滿足以下條件之一:

(1)O是空集;

(2)O中每一個元素都是可認(rèn)證的。

則協(xié)議的響應(yīng)者能夠抵抗服務(wù)中止型DoS攻擊。

如果O是空集，說明這兩條消息的處理的數(shù)據(jù)是互不相關(guān)的，響應(yīng)者能夠抵抗服務(wù)中止型DoS攻擊;如果O不為空集，說明ni中的數(shù)據(jù)和nj中的數(shù)據(jù)是相關(guān)的，集合O中的數(shù)據(jù)必須是可認(rèn)證的，響應(yīng)者才具有抗服務(wù)中止型DoS攻擊的能力，

不同于服務(wù)中止型DoS攻擊，資源消耗型DoS攻擊的實質(zhì)是攻擊者向響應(yīng)者發(fā)送大量偽造的請求信息，使響應(yīng)者在對這些消息進(jìn)行認(rèn)證以及維持連接的過程中用盡自身資源，造成DoS。因此，要想防止資源消耗型DoS攻擊，必須使協(xié)議發(fā)起者付出比協(xié)議響應(yīng)者更多的資源，基于此，提出如下規(guī)則2。

規(guī)則2:如圖 2 所示，設(shè)結(jié)點 n1，m1，m2，邊 n1→m1，m1?m2，n1屬于發(fā)起者串，m1，m2屬于響應(yīng)者串，若邊m1?m2的代價函數(shù)ga小于邊n1→m1的代價函數(shù)fa，那么協(xié)議由n1運行到m2，能夠抵抗資源消耗型DoS攻擊。

圖2 規(guī)則2串空間模型

可以用上面的兩條規(guī)則形成形式化分析方法檢測安全協(xié)議的抗DoS攻擊能力，如果一個安全協(xié)議的響應(yīng)者串滿足規(guī)則1，則響應(yīng)者能夠抵抗服務(wù)中止型DoS攻擊;如果響應(yīng)者串滿足規(guī)則2，則能夠抵抗資源消耗型DoS攻擊。

3 IEEE802．11i 4步握手協(xié)議與 JFK協(xié)議抗DoS攻擊性分析

3．1 IEEE802．11i 4 步握手協(xié)議

IEEEE802.11i標(biāo)準(zhǔn)在無限局域網(wǎng)中具有更好的認(rèn)證性和機(jī)密性，認(rèn)證過程包括3個實體:認(rèn)證服務(wù)器(AS)，認(rèn)證者(AP)，申請者(STA)。完整過程包括STA和AP之間的握手，AP和AS之間的握手，以及STA和AP之間的握手。經(jīng)過握手，STA和AS相互認(rèn)證并形成一個主會話密鑰(MSK)，AS將MSK安全的傳輸給 AP。STA和 AP，分別用 MSK生成相同的PMK，當(dāng)作握手協(xié)議生成臨時密鑰(PTK)的材料。

4步握手可簡化為如下描述:

消息 M1:AP→STA:Na，Sn，m1

消息 M2:STA→AP:Ns，Sn，m2，{Ns，Sn，m2}kck

消息 M3:AP→ STA:Na，Sn+1，m3，{Na，Sn+1，m3}kck

消息 M4:STA → AP:Ns，Sn+1，m4，{Ns，Sn+1，m4}kck

其中，Na，Ns分別是 AP和 STA 的隨機(jī)數(shù)，Sn，Sn+1為重放計數(shù)值，m1，m2，m3，m4為其他不同的信息，kck用來計算消息完整性驗證碼。具體過程如下:首先AP向STA發(fā)送M1，STA收到M1后，驗證重放計數(shù)值，通過則產(chǎn)生隨機(jī)數(shù)Ns，以及其他信息，利用這些信息計算臨時密鑰PTK以及完整性驗證碼{Ns，Sn，m2}kck，然后生成消息M2發(fā)送給AP，AP收到M2后，計算PTK，并驗證完整性驗證碼，然后生成消息M3，發(fā)送給STA。STA收到M3后，進(jìn)行消息完整性驗證，驗證成功，則生成M4發(fā)送給AP，安裝PTK。AP收到M4后，進(jìn)行完整性驗證，成功則安裝PTK，4步握手完成。

4步握手協(xié)議擴(kuò)展的串空間模型，如圖3所示，其中AP和STA是協(xié)議的參與雙方，fM1、fM3分別為AP生成并發(fā)送消息M1、M3所付出的代價值，fM2、fM4分別為STA生成并發(fā)送消息M2、M4所付出的代價值，gM1、gM3分別為STA接收并處理消息M1、M3所付出的代價值。

圖3 4步握手協(xié)議擴(kuò)展串空間模型

3.1.1 抗服務(wù)中止型DoS分析

消息 M1的所有子項組成的集合 O1:{Na，Sn，m1}，消息 M2的所有子項組成的集合 O2:{Ns，Sn，m2，{Ns，Sn，m2}kck}，消息 M3的所有子項組成的集合 O3:{Na，Sn+1，m3，{Na，Sn+1，m3}kck}，消息 M4的所有子項組成的集合 O4:{Ns，Sn+1，m4，{Ns，Sn+1，m4}kck}，其中，Sn與Sn+1只相差數(shù)值1，可認(rèn)為是同樣的子項。

STA收到的M1，M3的消息相關(guān)度集合O13:{Na，Sn}，M1是明文傳輸，其中的 Na，Sn都是明文，AP接收到M1后，并不能確定M1的準(zhǔn)確來源，所以Na和Sn都是不可認(rèn)證的，根據(jù)規(guī)則1，存在針對STA的服務(wù)中止型DoS攻擊。

事實上已經(jīng)被證實存在針對STA的服務(wù)中止型DoS攻擊，由于消息M1是明文傳輸，攻擊者很容易截取M1并得到其中STA和AP的MAC地址，之后單獨偽造 Na＇或 Sn＇，或者同時偽造 Na'和 Sn'，且 Na'和 Sn＇均是有效值，在STA收到合法的消息M3前，發(fā)送偽造的M1＇給STA，STA在收到 M1＇后，重新計算生成新的PTK＇，此時STA收到合法的M3后，將導(dǎo)致STA無法通過對M3的MIC校驗，根據(jù)協(xié)議規(guī)則，M3將被丟棄，STA將繼續(xù)等待，在超過一段間隔后，AP沒有接收到來自STA的M4，就會重新發(fā)送M3，但同樣不能通過MIC校驗，導(dǎo)致握手失敗。根據(jù)協(xié)議規(guī)則，AP再一次發(fā)起對STA的認(rèn)證請求。

AP收到的消息M2，M4的消息相關(guān)度集合O24:{Ns，Sn}，Ns和Sn在消息M2，M4也是明文形式出現(xiàn)，但是因為完整性校驗碼MIC，AP收到消息M2和M4后，先提取Ns，計算PTK，然后驗證MIC碼，因為只有STA具有相同的PTK，所以如果驗證MIC成功，則可確定M2和M4來自STA，且未經(jīng)篡改，否則不是來自STA。因此，M2和M4的消息相關(guān)度集合O24是可認(rèn)證的，根據(jù)規(guī)則1，不存在針對AP的服務(wù)中止型DoS攻擊。

3.1.2 抗資源消耗型DoS分析

對于STA，結(jié)點 ＜AP，1＞，＜STA，1＞，＜STA，2＞構(gòu)成叢一，結(jié)點 ＜AP，3＞，＜STA，3＞，＜STA，4＞構(gòu)成叢二。在叢一中，AP產(chǎn)生隨機(jī)數(shù)Na，重放計數(shù)值Sn，并和自己的MAC地址一同生成M1發(fā)給STA，付出的代價值為fM1;STA接收到M1后，首先取出Na，然后產(chǎn)生隨機(jī)數(shù)Ns，之后再利用PMK，算出PTK并存儲，然后計算完整性校驗碼MIC，發(fā)送消息M2給AP，付出的代價是 gM1。比較 fM1和 gM1，可知 gM1大于fM1，根據(jù)規(guī)則2，存在對STA的DoS攻擊，但是由于STA并不會同時發(fā)起多個認(rèn)證，所以只存儲一個STA，所以不會產(chǎn)生資源消耗型DoS攻擊。同樣分析叢二，也不會出現(xiàn)針對STA的資源消耗型DoS。

對于AP，結(jié)點結(jié)點 ＜STA，2＞，＜AP，2＞，＜AP，3＞構(gòu)成叢三。叢三中，STA產(chǎn)生并發(fā)送M2的代價是fM2，AP接收到并處理M2，付出的代價是gM2，fM2大于gM2，根據(jù)規(guī)則2，AP在此處能夠防止資源消耗型DoS。

3．2 JFK 協(xié)議

JFK協(xié)議是一種新的Internet密鑰交換協(xié)議，分為JFKr和JFKi兩種變種協(xié)議，其中JFKi主要應(yīng)用在C/S模式，能夠保護(hù)發(fā)起者的身份;JFKr主要適用于P2P模式，每一個響應(yīng)者都能夠保護(hù)自己的身份信息。

JFKr協(xié)議可簡化為如下描述，符號說明見表1。

消息 M1:I→R:Ni，xi

消息 M1:R→I:Ni，Nr，xr，tr

消息 M1:I→R:Ni，Nr，xi，xr，tr，ei，hi

消息 M1:R→I:er，hr

表1 JFKr協(xié)議符號說明

接下來，采用擴(kuò)展后的串空間模型對JFKr協(xié)議進(jìn)行建模，如圖4所示。

JFKr協(xié)議包含4條消息，消息M1和消息M2建立共享密鑰，首先發(fā)起者產(chǎn)生公開密鑰xi，和隨機(jī)數(shù)Ni，發(fā)送給響應(yīng)者。響應(yīng)者產(chǎn)生公開密鑰xr，隨機(jī)數(shù)Nr，認(rèn)證信息 tr，其中 tr是狀態(tài)信息(xr，Nr，Ni)的 MAC值。(xr，Nr，Ni)是響應(yīng)者成功接收消息M1，準(zhǔn)備發(fā)送消息M2時的環(huán)境狀態(tài)。消息M3和消息M4提供認(rèn)證性，包含Diffie-Hellman指數(shù)、加密隨機(jī)數(shù)和其他信息的簽名。發(fā)起者生成消息M3發(fā)送給響應(yīng)者，響應(yīng)者驗證M3中狀態(tài)信息的MAC值tr的正確性，如果驗證通過，響應(yīng)者生成加密后的身份標(biāo)識符er及其MAC值hr組成消息M4發(fā)送給協(xié)議發(fā)起者。

圖4 JFKr協(xié)議擴(kuò)展串空間模型

3.2.1 抗服務(wù)中止型DoS分析

JFKr協(xié)議中，消息 M1的所有子項組成的集合O1:{Ni，xi}，消息M2的所有子項組成的集合O2:{Ni，Nr，xi，xr}，消息 M3的所有子項組成的集合 O3:{Ni，Nr，xi，xr}，消息 M4的所有子項組成的集合 O4:{Ni，Nr，xi，xr}。

響應(yīng)者收到的消息 M1，M3的消息相關(guān)讀集合O13:{Ni，xi}，發(fā)起者收到的 M2，M4的消息相關(guān)度集合O24:{Ni，Nr，xi，xr}，因為 M3和 M4中，雙方的身份信息都被加密，且進(jìn)行了MAC值計算，且雙方的私鑰都由自身保管，不被泄漏，因此保證了消息相關(guān)度集合O13和O24中的項都是可認(rèn)證的，根據(jù)規(guī)則1，JFKr協(xié)議能夠防止服務(wù)中止型DoS攻擊。

3.2.2 抗資源消耗型DoS分析

對于響應(yīng)者，付出的資源消耗主要是gM1和gM3，發(fā)起者對應(yīng)付出的代價是fM1和fM3。首先，發(fā)起者產(chǎn)生隨機(jī)數(shù)Ni，之后計算公鑰xi，并存儲Ni和 xi，付出代價是fM1。響應(yīng)者接收M1后，生成隨機(jī)數(shù)，計算MAC值作為Cookie，最多的資源消耗就是計算MAC值，但是在不確定發(fā)起者的合法身份前，不會保留發(fā)起者有關(guān)的狀態(tài)信息，沒有存儲資源消耗，因此滿足fM1大于gM1。發(fā)起者收到M2后，利用Ke和Ka對身份信息加密，并計算其MAC值hi，連同收到的Cookie值以及雙方的隨機(jī)數(shù)，公開密鑰等信息，組成消息M3，發(fā)給響應(yīng)者，此過程中發(fā)起者付出的代價值是fM3。響應(yīng)者接收到M3后，首先再次計算Cookie值，并和M3中的Cookie比較，只有驗證通過，才進(jìn)行后續(xù)操作，之后再計算生成身份標(biāo)識符er及其MAC值hr，此過程中響應(yīng)者付出代價是gM3小于發(fā)起者付出的代價fM3。經(jīng)過以上分析，根據(jù)規(guī)則2，JFKr協(xié)議能夠防止資源消耗型DoS攻擊。

4 結(jié)束語

針對安全協(xié)議中存在的DoS攻擊，對基本的串空間模型進(jìn)行擴(kuò)展，提出一種形式化的分析方法，能夠較為全面地分析安全協(xié)議存在的服務(wù)中止型以及資源消耗型DoS攻擊，并且利用該模型對IEEEE802.11i協(xié)議中的4步握手協(xié)議以及JFK協(xié)議進(jìn)行分析，發(fā)現(xiàn)IEEEE802.11i 4步握手協(xié)議中存在的DoS攻擊，驗證了JFK協(xié)議具有抗DoS攻擊的能力。不足的是，模型只能夠分析在攻擊者和響應(yīng)者系統(tǒng)資源相當(dāng)情況下的資源消耗型攻擊，當(dāng)有大量的攻擊者發(fā)起分布式DoS攻擊時，還需要更好的辦法進(jìn)行應(yīng)對，在接下來的研究中將以此為重點。

［1］ 衛(wèi)劍釩，陳鐘，段云所，等.一種認(rèn)證協(xié)議防御拒絕服務(wù)攻擊的設(shè)計方法［J］.電子學(xué)報，2005，33(2):288-293.

［2］ Meadows C.A formal framework and evaluation method for，network denial of service［C］//Proceedings of 12th IEEE Computer，Security Foundations Workshop，1999:4-13.

［3］ Meadows C.A cost-based framework for analysis of denial of service networks［J］.Journal of Computer Security，2001，9:143-164.

［4］ Meadows C.Formal Methods for Cryptographic Protocol Analysis:Emerging Issues and Trends［J］.IEEE Journal on Selected Areas，in Communications，2003，21(1):44-54.

［5］ GROZA B，MINEA M.Formal modelling and automatic detection of resource exhaustion attacks［A］.Proc of 6th ACM Symposium on Information，Computerand Communications Security(ASIACCS)［C］.HongKong，China，2011.

［6］ YU C，GLIGOR V.A formal specification and verification method for the prevention of denial of service［J］.IEEE Transactions on Software Engineering，1990，16(6):581-592.

［7］ 周世健，蔣睿，楊曉輝.安全協(xié)議 DoS攻擊的形式化分析方法研究［J］.中國電子科學(xué)研究院學(xué)報，2008，3(6):592-598.

［8］ Fabregaf，Herzog，Guttmanj.Strand space:Why is a Security Protocol Correct［C］//Proceedings of，the 1998 IEEE Symposium on Security and Privacy，IEEE，Computer Society Press.1998:160-171.

［9］ Thayer FJ，Herzog JC，Guttman JD.Strand spaces:Proving security protocols correct［J］.Journal of Computer Security，1999，7(2-3):191-230.

［10］ Thayer FJ，Herzog JC，Guttman JD.Strand spaces:Honest ideals on strand spaces［C］.In:Proceedings of the 1998 IEEE Computer Security Foundations Workshop.LosAlamitos:IEEE Computer Society Press，1998:66-77.

［11］ 孟博，黃偉，王德軍，等.協(xié)議抗拒絕服務(wù)攻擊性自動化證明［J］.通信學(xué)報.2012，(3).

［12］ 卿斯?jié)h.安全協(xié)議20年研究進(jìn)展［J］.軟件學(xué)報，2013，14.

［13］ Ramachandran V.Analyzing DoS-Resistance of Protocols Using a Cost-based Framework［R］.Technical Report DCS/TR-1239，Yale University，2002.

［14］ 李建華.網(wǎng)絡(luò)安全協(xié)議的形式化分析與驗證［M］.北京:機(jī)械工業(yè)出版社，2010.

［15］ 馮登國.網(wǎng)絡(luò)安全原理與技術(shù)［M］.北京:科學(xué)出版社，2003.