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

金大鵬， 林宏剛

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

0 引言

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

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

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

1 擴展的串空間模型理論

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

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

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

設(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，當且僅當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反應了結(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的集合到非負實數(shù)R的映射，其中邊n1→m1到非負實數(shù)R的映射用函數(shù)f表示，若n1發(fā)送消息a給m1，則fa表示n1產(chǎn)生并發(fā)送消息a所付出的代價值;邊m1?m2到非負實數(shù)R的映射用函數(shù)g表示，若結(jié)點m1接收了來自另一個串的消息a后，由事件m1變?yōu)槭录2，則ga表示接收并對消息a進行處理所付出的代價值。

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

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

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

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

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

(1)O是空集;

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

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

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

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

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

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

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

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

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

IEEEE802.11i標準在無限局域網(wǎng)中具有更好的認證性和機密性，認證過程包括3個實體:認證服務器(AS)，認證者(AP)，申請者(STA)。完整過程包括STA和AP之間的握手，AP和AS之間的握手，以及STA和AP之間的握手。經(jīng)過握手，STA和AS相互認證并形成一個主會話密鑰(MSK)，AS將MSK安全的傳輸給 AP。STA和 AP，分別用 MSK生成相同的PMK，當作握手協(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 的隨機數(shù)，Sn，Sn+1為重放計數(shù)值，m1，m2，m3，m4為其他不同的信息，kck用來計算消息完整性驗證碼。具體過程如下:首先AP向STA發(fā)送M1，STA收到M1后，驗證重放計數(shù)值，通過則產(chǎn)生隨機數(shù)Ns，以及其他信息，利用這些信息計算臨時密鑰PTK以及完整性驗證碼{Ns，Sn，m2}kck，然后生成消息M2發(fā)送給AP，AP收到M2后，計算PTK，并驗證完整性驗證碼，然后生成消息M3，發(fā)送給STA。STA收到M3后，進行消息完整性驗證，驗證成功，則生成M4發(fā)送給AP，安裝PTK。AP收到M4后，進行完整性驗證，成功則安裝PTK，4步握手完成。

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

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

3.1.1 抗服務中止型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，可認為是同樣的子項。

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

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

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是可認證的，根據(jù)規(guī)則1，不存在針對AP的服務中止型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)生隨機數(shù)Na，重放計數(shù)值Sn，并和自己的MAC地址一同生成M1發(fā)給STA，付出的代價值為fM1;STA接收到M1后，首先取出Na，然后產(chǎn)生隨機數(shù)Ns，之后再利用PMK，算出PTK并存儲，然后計算完整性校驗碼MIC，發(fā)送消息M2給AP，付出的代價是 gM1。比較 fM1和 gM1，可知 gM1大于fM1，根據(jù)規(guī)則2，存在對STA的DoS攻擊，但是由于STA并不會同時發(fā)起多個認證，所以只存儲一個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主要應用在C/S模式，能夠保護發(fā)起者的身份;JFKr主要適用于P2P模式，每一個響應者都能夠保護自己的身份信息。

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é)議符號說明

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

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

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

3.2.1 抗服務中止型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}。

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

3.2.2 抗資源消耗型DoS分析

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

4 結(jié)束語

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

［1］ 衛(wèi)劍釩，陳鐘，段云所，等.一種認證協(xié)議防御拒絕服務攻擊的設(shè)計方法［J］.電子學報，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］.中國電子科學研究院學報，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é)議抗拒絕服務攻擊性自動化證明［J］.通信學報.2012，(3).

［12］ 卿斯?jié)h.安全協(xié)議20年研究進展［J］.軟件學報，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］.北京:機械工業(yè)出版社，2010.

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