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

金大鵬， 林宏剛

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

0 引言

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

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

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

1 擴展的串空間模型理論

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

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

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

設集合A中的元素為協議主體交換的消息，則稱A為項集合，A的元素為項。

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

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

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

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

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

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

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

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

1．2 消息相關度集合

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

1．3 代價函數

如圖1所示，定義代價函數為邊n1→m1及m1?m2的集合到非負實數R的映射，其中邊n1→m1到非負實數R的映射用函數f表示，若n1發送消息a給m1，則fa表示n1產生并發送消息a所付出的代價值;邊m1?m2到非負實數R的映射用函數g表示，若結點m1接收了來自另一個串的消息a后，由事件m1變為事件m2，則ga表示接收并對消息a進行處理所付出的代價值。

圖1 代價函數串空間模型

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

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

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

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

(1)O是空集;

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

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

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

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

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

圖2 規則2串空間模型

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

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

3．1 IEEE802．11i 4 步握手協議

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

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

圖3 4步握手協議擴展串空間模型

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只相差數值1，可認為是同樣的子項。

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

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

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

3.1.2 抗資源消耗型DoS分析

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

對于AP，結點結點 ＜STA，2＞，＜AP，2＞，＜AP，3＞構成叢三。叢三中，STA產生并發送M2的代價是fM2，AP接收到并處理M2，付出的代價是gM2，fM2大于gM2，根據規則2，AP在此處能夠防止資源消耗型DoS。

3．2 JFK 協議

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

JFKr協議可簡化為如下描述，符號說明見表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協議符號說明

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

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

圖4 JFKr協議擴展串空間模型

3.2.1 抗服務中止型DoS分析

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

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

3.2.2 抗資源消耗型DoS分析

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

4 結束語

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

［1］ 衛劍釩，陳鐘，段云所，等.一種認證協議防御拒絕服務攻擊的設計方法［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］ 周世健，蔣睿，楊曉輝.安全協議 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］ 孟博，黃偉，王德軍，等.協議抗拒絕服務攻擊性自動化證明［J］.通信學報.2012，(3).

［12］ 卿斯漢.安全協議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］ 李建華.網絡安全協議的形式化分析與驗證［M］.北京:機械工業出版社，2010.

［15］ 馮登國.網絡安全原理與技術［M］.北京:科學出版社，2003.