協議抗拒絕服務攻擊性自動化證明

孟博，黃偉，王德軍，邵飛

（中南民族大學 計算機科學學院，湖北 武漢 430074）

1 引言

拒絕服務攻擊具有威害巨大及難以有效防御的特點，越來越受到網絡安全專家與用戶的關注。拒絕服務攻擊是通過各種手段使提供服務的主機無法提供服務的一種攻擊，本質是對分布式系統的可用性進行攻擊。按照攻擊方式可以分為：資源消耗型、服務中止型和物理破壞型。這種攻擊簡單有效，如攻擊者可以發送大量垃圾信息給服務器，造成服務器處理大量無效的數據，從而無法向合法用戶提供正常的服務，而產生拒絕服務攻擊；此外拒絕服務攻擊很難甚至無法確定攻擊者，并且能夠通過這種攻擊產生其他攻擊，例如，中間人攻擊，會話攔截攻擊等。目前的 TCP/IP協議架構從鏈路層到應用層都存在拒絕服務攻擊，例如，鏈路層的ARP Flooding攻擊、ARP poisoning攻擊，網絡層的ICMP攻擊，傳輸層的SYN Floods攻擊，應用層的session flooding攻擊、buffer overflow攻擊等。

對拒絕服務攻擊的形式化建模，目前有2類主要方法，一類是以用戶合約為基礎的 Yu-Gligor形式化建模方法[1]，另一類是以代價為基礎的Meadows形式化建模方法[2]，后者受到了人們的重點關注。

安全協議的形式化分析與驗證方法主要有定理證明、模型檢測、邏輯推理、類型檢測等。代表性的定理證明方法有 Paulson的歸納證明法和Thayer等學者提出的串空間模型。基于定理證明的方法在自動化工具支持方面雖然無法與模型檢測方法比擬，但是它克服了模型檢測固有的缺陷——狀態空間爆炸的問題，能夠處理無窮狀態系統。定理證明可以通過自動化的定理證明器協助完成證明過程。主要的定理證明器有 ProVerif、Isabelle、HOL、ACL2、PVS等，其中ProVerif是Blanchet[3]開發的基于Dolev-Yao模型的一階定理證明器，它可以分析和驗證使用Horn子句或應用PI演算描述的安全協議的秘密性、強秘密性、認證性等。ProVerif已經成功分析了很多復雜的協議，如電子商務協議[4]、網絡投票協議[5,6]、JFK協議[7]等。

在拒絕服務攻擊中非常重要的一類攻擊就是利用了協議狀態而產生的，例如，利用協議狀態的保持來耗盡系統資源，產生資源消耗型拒絕服務攻擊；修改協議狀態，使其前后狀態不一致而產生協議中止型拒絕服務攻擊。因此，本文脫離以用戶合約為基礎的 Yu-Gligor形式化建模方法與以代價為基礎的Meadows形式化建模方法，從協議狀態的角度，對協議抗拒絕服務攻擊性進行建模，分析與驗證協議抗拒絕服務攻擊性。由于標準應用PI演算[8]不能夠對協議狀態進行建模，為了能夠使用基于應用PI演算ProVerif來自動化分析與驗證協議抗拒絕服務攻擊性，必須對標準應用PI演算進行擴展。首先從2個方面：一個是攻擊者上下文，另外一個是進程表達式對標準應用PI演算進行擴展，然后應用擴展后的應用 PI演算對協議抗拒絕服務攻擊性進行建模，提出一個基于定理證明支持一階定理證明器ProVerif的抗拒絕服務攻擊性自動化證明方法，最后應用ProVerif來分析與驗證協議的抗拒絕服務攻擊性。

2 相關的工作

目前，協議拒絕服務攻擊形式化建模主要有 2類方法。

Yu和 Gligor基于時態邏輯，引入用戶合約，提出了一個對共享服務拒絕服務攻擊的形式化規范和驗證方法。他們把拒絕服務攻擊歸結為新鮮性與安全性問題。Yu-Gligor形式化建模方法的核心思想是以訪問控制策略為基礎對拒絕服務攻擊進行形式化建模，因此不能夠處理在認證發生之前產生的拒絕服務攻擊，如 SYN Floods攻擊。此外 Yu-Gligor形式化建模方法不支持自動化工具。Millen[9]通過對時間逝去的明確度量對 Yu-Gligor形式化建模方法進行了擴展，使得它可以處理最大等待時間策略。Cuppens與 Saurel[10]應用模態邏輯和道義邏輯也對Yu和Gligor框架的可用性策略進行了形式化建模。

Meadows提出了基于代價的拒絕服務攻擊形式化建模方法，該形式化建模方法通過設置容忍關系靈活的判斷協議是否會產生拒絕服務攻擊，適合對協議的資源消耗型拒絕服務攻擊進行建模。Meadows聲明其框架支持NRL協議分析器，但是沒有給出具體例子。基于代價的形式化建模方法存在一個問題：在任何時候產生一個偽造的數據比驗證它要花費的代價要小，按照Meadows形式化建模方法，那么所有的協議都不能夠抵抗拒絕服務攻擊。Ramachandran[11]應用 Meadows 形式化建模方法分析并指出 JFK協議具有抗拒絕服務攻擊性。Smith[12]等應用 Meadows 形式化建模方法分析了JFK協議，聲稱在允許攻擊者IP地址保密或者協議雙方的DH協議的公鑰可以重用的情況下，JFK協議存在2個拒絕服務攻擊，但是我們認為他們的結論是值得商榷的。基于Meadows 形式化建模方法，Groza與 Minea[13]應用支持 ASLan規范語言的AVANTSSAR自動化工具對資源消耗型的拒絕服務攻擊進行了建模，分析STS與JFK協議，指出STS協議不能抵抗拒絕服務攻擊，JFK協議具有抗拒絕服務攻擊性；Abadi和Blanchet[7]應用觀察等價關系對抗拒絕服務攻擊性進行建模，且應用PI演算分析并證明JFKr協議具有抗拒絕服務攻擊性；Lafrance和 Mullins[14]應用安全進程代數 SPPA與容許干擾來對安全協議中的拒絕服務攻擊進行建模，具體是通過引入“Impassivity”來描述攻擊者通過利用低代價的行為來產生對協議另外一方的高代價行為的干擾，適合對資源消耗型拒絕服務攻擊進行建模，并且分析證明1KP支付協議不能夠抵抗拒絕服務攻擊；周世健等學者[15]對串空間模型進行了擴展，分析了IEEE 802．11i四步握手協議抗拒絕服務攻擊性，發現其存在拒絕服務攻擊；Tritilanunt等[16,17]指出Meadows基于代價的形式化建模方法存在2個主要的問題：1) 僅僅考慮到誠實的協議參加方；2) 代價的分類方式太粗糙而不具有實用性。故他們應用著色Petri網提出了一個基于時間和代價的形式化拒絕服務形式化建模方法，分析了HIP協議，指出在攻擊者為類型3（攻擊者選擇正確的客戶端難題答案（client puzzle solution））和類型4（攻擊者偽造客戶端難題答案（client puzzle solution））情況下，存在拒絕服務攻擊。

除了上述2類主要的形式化建模方法之外，Agha等[18]應用概率重寫理論PMAUDE對拒絕服務攻擊進行了形式化建模，應用CSL邏輯形式化描述拒絕服務攻擊成功的概率，并且應用基于統計的模型檢查器VESTA對TCP三步握手協議進行了分析，指出TCP三步握手協議不具有抗拒絕服務攻擊性。Mahimkar和Shmatikov[19]基于博弈的ATL邏輯，對資源消耗與帶寬消耗抗拒絕服務攻擊性進行了建模，應用MOCHA模型檢查器分析并證明JFKr協議具有抗拒絕服務攻擊性。

3 擴展的應用PI演算

為了對協議狀態及抗拒絕服務攻擊性進行建模，從2個方面對標準應用PI演算進行擴展：一個是攻擊者上下文，另外一個是進程表達式。擴展應用PI演算語義與標準應用PI演算相同。

3.1 攻擊者上下文

按照攻擊者對消息的攻擊能力將攻擊者所處的上下文分為現實上下文和理想上下文。

現實上下文形式化表示為

3.2 項

應用PI演算[5]是一個用來描述并發進程的語言。它繼承了PI演算的通信與并發結構，增加了函數和等價理論。消息不僅是原子名，還可以是通過名字和函數構成的項。

項的定義如圖1所示。用a、b、c、m、n等標識符及其組合表示名字，用x、y、z表示變量；也使用原語言變量u、v、w表示名字和變量；用f、g、h表示函數項，每個函數項都帶有固定元數的參數，例如，encrypt（ m, k）表示函數encrypt有參數m和k。函數項是用來構造項的。因此，項M、N、T、V是變量，名字和函數項。

圖1 項的定義

如果項M=f( M1,…,Mn)，則項M有子項Mi, i∈[1,n]。項Mi, i∈[1,n]也可能包含子項，不包含任何子項的項叫作原子項。項M用來描述協議中參與者之間相互交換的消息。變量可以描述任何消息或值，名字用來描述原子值，函數項用來描述從已知消息和值構造新的消息和值。

3.3 擴展后的進程

擴展后的進程如圖2所示，空進程0不做任何操作；并行復合進程|P Q同時運行進程P和Q；復制進程!P并發執行無數個P進程；受限進程.n Pν首先產生一個新的私有名字n，然后執行P進程；條件進程分為2種：理想上下文中的條件進程if M =N then P else C和現實上下文中的條件進程if M = N then P else Q 。理想上下文中的條件進程if M =N then P else C.Q首先判斷條件M N= 是否為真，如果為真，則執行P進程，否則執行C.Q 進程；現實上下文中的條件進程if M = N then P else Q 首先判斷條件M = N 是否為真，如果為真，則執行P進程，否則執行Q進程；消息輸入進程 u( x). P準備從通道u接受消息，并將接收到的消息與P中的x綁定，然后執行P進程；消息輸出進程. P準備從通道u輸出消息N，然后執行P進程。閉進程P從通道c輸出消息M，當且僅當存在進程 P '和 P ''，使得

圖2 擴展后的進程

3.4 進程上下文

進程上下文C是帶洞([_])的進程表達式，如圖3所示。if M = Nthen C else Q 表示如果項M與項N匹配，那么執行進程上下文C，則C是可驗證上下文。if M = N then PelseC 表示如果項M與項N不匹配，那么執行進程上下文C，則C是不可驗證上下文。

圖3 進程上下文

4 定義和符號說明

定義1 帶注解Alice-and-Bob 規范描述。

定義2 消息Ml認證性。

定義3 操作一致性。

定義41γ邏輯先于2γ。

P為協議帶注解Alice-and-Bob 規范描述，S為P中操作的集合。對于S中的任意操作1γ和2γ，1γ邏輯先于2γ當且僅當：

3) 存在操作3γ，使得3γ邏輯先于2γ，1γ邏輯先于3γ。

定義5 關聯集合。

協議中的任意消息 Mi和 Mj的關聯集合 ω 為中驗證操作v的數據項集合?和 Mi的數據項的集合Ψ的交集，即 ω=?∩Ψ。其中 i, j∈[1 , n]且i＜j。

關聯集合ω反映了消息之間互相影響的程度：ω為空集，消息之間互不影響，是獨立的，關聯度為零；ω包含的數據項越多，消息之間互相影響的程度就越高，關聯度越高。

定義6 抗拒絕服務攻擊性。

P為協議帶注解Alice-and-Bob 規范描述，B具有抗拒絕服務攻擊性，當且僅當 ()Recv B中的任意一對消息iM和jM 的關聯集合ω滿足：

1) ω是空集?；

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

其中， R ecv( B)為協議P中參與者B所有處理消息的操作按邏輯先于組成的集合， i, j ∈[1,n]且i＜j。

如果協議 P中任意一對消息 Mi和 Mj之間互不關聯，那么處理這兩條消息的下文是互相獨立的，則B具有抗拒絕服務攻擊性；如果消息 Mi和Mj相關聯，則對消息 Mj的處理依賴于對消息 Mi的處理，那么處理這2條消息的上下文是狀態關聯的，則消息 Mi和 Mj關聯集合ω必須是可認證的才使B具有抗拒絕服務攻擊性。

5 自動化證明抗拒絕服務攻擊性方法

首先，應用擴展后的應用PI演算對協議帶注解Alice-and-Bob規范描述進行精確的形式化建模。假設協議由 2n條消息組成，協議參加者為 Alice和Bob，Alice分別發送消息Mii∈[1,n]和接收消息Mi'i∈[1,n]，Bob分別接收消息Mii∈[1,n]和發送接收消息Mi'i∈[1,n]。協 議 進 程PP≡νn.（!A lice|!Bob）是封閉進程，由任意的發起者進程Alice和響應者進程Bob并行復合組成。根據擴展后的應用PI演算，進程Alice和Bob可以經過一系列的規約到達如圖4所示某一個進程。

圖4 可達進程

為了應用ProVerif對Bob的抗拒絕服務攻擊性進行形式化分析，需要對 Bob收到的消息Mii∈[1,n -1]進行形式化建模，如果攻擊者能夠從公開信道c上獲得秘密S，則攻擊者可以通過對消息 Mi進行攻擊使協議產生拒絕服務攻擊。

首先對消息 M1進行建模。如圖 5所示。在現實上下文中交換和處理消息 M1，在理想上下文中交換和處理消息協議進程PP， 其中，c1,c是公開信道，ci, i∈[2,n]是Bob接收消息Mi的隱私通道,

如果攻擊者能夠從公開信道c上獲得秘密S，則攻擊者可以通過對消息1M 進行攻擊使協議產生拒絕服務攻擊。

圖5 消息M1的形式化模型

采用類似的方法對消息 Mi, i ∈[2,n -1]分別建立如圖6所示的模型。在現實上下文中交換和處理消息 Mi，在理想上下文中交換和處理消息。協議進程PP為為PP≡ν（!Alicei|!Bobi），其中，ci, i∈[2,n-1],c是公開信道，cj,j∈[2,n-1]∩j≠i 是Bob接收消息Mi的隱私通道,。如果攻擊者能夠從公開信道c上獲得秘密S，則攻擊者可以通過對消息iM進行攻擊使協議產生拒絕服務攻擊。

圖6 消息Mi的形式化模型

定理 抗拒絕服務攻擊性。協議進程PP的響應者Bob具有抗拒絕服務攻擊性當且僅當對Bob收到的所有消息Mi, i∈[1,n]的形式化模型，PP都不能從公共通道c輸出秘密消息S，即不存在進程P'，P''和攻擊者進程Attacker，使得。

證明

Bob具有抗拒絕服務攻擊性，依據定義6，?Mi, Mj∈Recv（ Bob），i, j∈[1,n]，Mi邏輯先于Mj，驗證操作v是進程ifM=NthenP else，則對消息iM的形式化模型：

1) ω=?即在協議規范描述中MN=的值與消息Mi無關，那么不論在理想上下文還是現實上下文中交換Mi，MN=的值恒為真，協議進程PP（→ ∪ ≡）*P ；

所以，對響應者Bob收到的所有消息Mi, i∈[1,n]的形式化模型，PP都不能從公共通道c輸出秘密消息S。

如果對于響應者Bob收到的消息Mi, i∈[1,n]的形式化模型，PP能從公共通道c輸出秘密消息S，即存在進程P'，P''和攻擊者進程Attacker，使得，則攻擊者Attacker可以通過篡改與v關聯的邏輯先于Mj的消息，使M=N的值為假。那么關聯集合ω存在不可認證項m'，所以協議進程PP的響應者Bob不具備防止拒絕服務攻擊性。 證畢。

由定理可知如果攻擊者能夠獲得秘密消息S，那么它能夠構造一個拒絕服務攻擊：在不影響其他消息正常交互的情況下，篡改消息iM的內容并使其不被接收者察覺，產生拒絕服務攻擊。

至此，可以使用擴展后的應用PI演算對抗拒絕服務攻擊進行形式化描述，基于給出的定理，應用ProVeif自動化證明協議的抗拒絕服務攻擊性。

6 一階定理證明器ProVerif

ProVerif[3]是Blanchet開發的基于重寫逼近的一階定理證明器。它基于Prolog語言，能夠分析與驗證使用Horn子句、應用PI演算及本文提出的擴展的應用PI演算描述的安全協議的安全性。同時，它克服了模型檢測方法固有的缺陷－狀態空間爆炸問題，能夠處理無窮狀態系統。ProVerif已經成功分析了很多復雜的安全協議，如電子商務協議[4]、網絡投票協議[5,6]等。

ProVerif的體系結構如圖7所示，由協議輸入、處理和輸出3部分組成。協議輸入部分主要包括安全協議形式化描述和安全屬性的形式化定義。ProVerif對輸入的協議形式化描述進行初始處理，主要是語法檢查。輸入語言為應用 PI演算、Horn子句或者本文提出的擴展的應用PI演算。

處理部分負責根據安全協議的形式化描述對要證明的安全屬性進行邏輯推導證明。它包括自動翻譯模塊和邏輯推導模塊。當輸入語言為應用 PI演算或本文提出的擴展的應用PI演算時，自動翻譯模塊主要負責實現安全協議的應用PI演算或本文提出的擴展的應用PI演算形式化描述到一階邏輯規則的轉換，邏輯推導模塊則基于一階邏輯規則對要證明的安全屬性進行推理和驗證。當輸入語言為Horn子句時，處理部分為邏輯推導模塊，不需要自動翻譯模塊。

結果輸出部分主要負責輸出處理結果。從輸出結果可以得知該協議是否滿足相應的安全屬性，供用戶進一步分析，但是ProVerif不輸出詳細的證明過程。如果不滿足某安全屬性，則ProVerif會給出詳細的攻擊方式。

圖7 ProVerif結構

7 JFK與IEEE 802.11四步握手協議抗拒絕服務攻擊性

7.1 JFK協議

JFK(just fast keying)協議是一個密鑰交換協議，主要有JFKr和JFKi 2個版本，主要區別是對協議雙方提供不同的身份保護。JFKr基于Sign-and-MAC協議[20]，能夠在有主動攻擊者的環境中保護響應者的身份，在被動攻擊者的環境中保護發起者的身份。JFKi基于ISO 9798-3 密鑰交換協議[21]，能夠在有主動攻擊者的環境中保護發起者的身份。Abadi和Blanchet[7]應用應用PI演算分析了對JFKr協議的秘密性、認證性、可否認性，同時用手工的方式分析了JFKr抗拒絕服務攻擊性，指出JFKr協議可以抵抗拒絕服務攻擊。Aiello等學者[22,23]采用非形式化的方法分析了JFK協議的安全性。這里主要應用提出的自動化抗拒絕服務攻擊方法分析JFKr協議的抗拒絕服務攻擊性。

JFKr協議涉及2個角色：協議的發起者Alice和協議的響應者Bob。攻擊者建模為Dolev-Yao模型中的攻擊者，既可以在公開信道上監聽、攔截、修改，刪除和插入消息，又可以偽裝成誠實的參與者。

JFKr協議的Alice-and-Bob 規范描述如圖8所示，符號說明見文獻[17]。

圖8 JFKr協議的Alice-and-Bob 規范描述

JFKr協議有4條消息組成，消息1和消息2通過Diffie-Hellman密鑰交換協議建立共享密鑰。首先Alice生成公鑰Alicex和隨機數AliceN，發送給Bob。Bob生成公鑰Bobx、隨機數BobN，認證cookieBobt。tBob是狀態信息的MAC值。是Bob成功收到消息1準備發送消息2時的自己環境狀態。消息3和消息4提供認證性。消息3和消息4包含加密隨機數、Diffie-Hellman指數及其他信息的簽名。Alice生成消息3發送給Bob，Bob驗證消息3中狀態信息的MAC值tBob的正確性。如果驗證成功，Bob用及eK生成加密后的身份標識eBob及其MAC值hBob組成消息4發送給Alice。

基于提出的抗拒絕服務攻擊性自動化證明方法，應用擴展的應用PI演算對JFKr協議響應者Bob收到的消息1進行建模，然后轉換成ProVerif的輸入語言，最后應用ProVerif對JFKr協議進行分析。由于空間的限制，只給出了ProVerif的分析結果，如圖9所示。圖9表明公開通道c沒有輸出秘密信息dos。

圖9 JFKr的ProVerif輸出結果

根據消息1形式化模型，得知Bob處理收到的消息1和消息3的操作是Recv( Bob){ act( Bob)驗證操作v是對的驗證，其中，。所以消息1和消息3的關聯集合ω為空集。這和ProVerif在公開通道c的輸出是一致的。由定義6可知JFKr中的響應者Bob能夠防止拒絕服務攻擊。

7.2 IEEE 802.11 i四步握手協議

IEEE 802.11標準是無線局域網中廣泛采用的標準。由于IEEE 802.11標準被證明在實體認證和有線等價保密方面是不安全的，IEEE 802.11i標準[21]被提出來增強IEEE 802.11的安全性。IEEE 802.11i除了引入了新的密鑰管理和生成算法，還改進了加密和認證算法。它定義了一個基于IEEE 802.1X認證和4步握手的強安全網絡關聯。Bicakcia與Tavli[24]對IEEE 802.11的拒絕服務攻擊與防范措施進行了深入研究。

四步握手協議簡化了的Alice-and-Bob 規范描述如圖10所示。

圖10 四步握手協議的Alice-and-Bob 規范描述

其中，Anonce和Snonce分別為認證者Alice和請求者Bob生成的隨機數，它用來生成PTK（Pairwise Transient Key）。m1、m2、m3、m4分別為不同的消息，其中，m1、m2、m3、m4都包含有重放計數值Replay_Counter。MIC2=MIC（Snonce,m2）,MIC3=MIC（Anonce,m3）,MIC4=MIC（m4），MIC（message integrity code）值為消息完整性碼。

四步握手協議運行過程如下：首先認證者Alice首先發送消息1M給請求者Bob，請求者Bob收到消息M1后，首先驗證重放計數值_ReplayCounter的有效性，驗證通過則產生一個隨機數Snonce，然后應用偽隨機函數PRF(pseudo random functions)生成臨時密鑰PTK。偽隨機函數PRF輸入為Anonce、Snonce與其他信息。請求者Bob生成MIC值，把消息M2發送給認證者Alice。認證者Alice收到消息2M后，計算臨時密鑰PTK值，驗證M2中的MIC值，生成消息3M給請求者Bob。請求者Bob收到消息M3對MIC值進行驗證，如果成功，生成并發送消息M4給認證者Alice，安裝PTK。認證者Alice在收到M4后對MIC值進行驗證，如果驗證成功，安裝PTK。至此四步握手結束，產生并安裝PTK。

應用提出的自動化抗拒絕服務攻擊性證明方法，ProVerif給出了兩個拒絕服務攻擊：拒絕服務攻擊1，如圖11和圖12所示。拒絕服務攻擊2，如圖13和圖14所示。其中拒絕服務攻擊2是應用我們提出的方法發現的。。

根據四步握手協議規范，由于請求者Bob對消息M3的驗證依賴于臨時密鑰PTK，而臨時密鑰PTK的生成取決于Anonce和Snonce，Snonce的產生又依賴于對消息M1的重放計數值Replay_Counter的有效性驗證，所以攻擊者只要成功篡改或重放Anonce與計數值Replay_Counter，就可以使請求者Bob對合法的消息M3的驗證失敗，從而產生拒絕服務攻擊。

根據消息M1形式化模型，請求者Bob處理消息M1和消息M3的操作Recv(Bob){act(Bob)其中，v是驗證操作，。所以M1和M3的關聯集合ω=｛Anonce1｝。由于四步握手協議沒有對Anonce1進行驗證，Anonce1是不可認證的，由定義6可知四步握手協議中的請求者Bob不能防止拒絕服務攻擊。

拒絕服務攻擊1，如圖11和圖12所示。圖11表明公開通道c輸出秘密信息S。ProVerif構造的拒絕服務攻擊1如圖12所示：在協議的一次運行中，請求者Bob收到消息M3前，攻擊者偽造一個隨機數Anonce'和重放計數值Replay_Counter（'使Replay_Counter'的值為有效值），并生成消息M1發送給請求者Bob，根據四步握手協議規范，請求者Bob重新生成PTK，此時Bob收到合法的消息M3，將不能通過對 MIC值驗證。根據四步握手協議規范，認證者Alice在將重新發送M3，但仍然不能通過驗證，n次這樣的驗證后，認證者Alice將和請求者Bob重新開始認證。從而產生拒絕服務攻擊。

圖11 針對拒絕服務攻擊1的ProVerif輸出

圖12 ProVerif輸出的拒絕服務攻擊1

拒絕服務攻擊2，如圖13和圖14所示。圖13表明公開通道c輸出秘密信息S。ProVerif構造的拒絕服務攻擊2如圖14所示。拒絕服務攻擊2與拒絕服務攻擊1基本上是相同的，區別是攻擊者只偽造重放計數值 Replay _ C ounter'，使Replay _ C ounter'的值為有效值。

圖13 針對拒絕服務攻擊2的ProVerif輸出

圖14 ProVerif輸出的拒絕服務攻擊2

針對拒絕服務攻擊1，He[25]提出請求者Bob除了存儲 PTK，另外為每一個消息M1存儲一個TPTK(temporary PTK )，在收到消息M1時，僅更新TPTK，在收到正確的消息M3時才更新PTK。但是，當攻擊者大量發送偽造的消息M1時，Bob就會存儲大量的 TPTK，產生存儲資源消耗型的拒絕服務攻擊。

基于以上分析， 為了防止拒絕服務攻擊1和2，我們認為使消息M1可認證即可。具體方案是應用認證者 Alice的簽名密鑰對M1進行簽名或使用MSK對M1進行加密。這樣就使消息1是可認證的，來防止拒絕服務攻擊1和2。在通過認證以后再分配資源。

如果只防止拒絕服務攻擊 2，那么請求者 Bob可以存儲其在一定時間內收到的Anonce，并且在進行下一步處理前，檢查Anonce是否是在一定時間內是重放的，則可以防止這種攻擊。

8 結束語

拒絕服務攻擊具有威害巨大及難以有效防御的特點，受到網絡安全專家與用戶的重點關注。形式化方法是分析協議安全性強有力的工具。本文沒有遵循Yu-Gligor形式化建模方法和Meadows形式化建模方法，而是從協議狀態的角度，應用形式化方法對拒絕服務攻擊性進行建模。首先從攻擊者上下文與進程表達式2個方面對標準應用PI演算進行擴展，然后應用擴展后的應用PI演算對協議的抗拒絕服務攻擊性進行建模，提出了一個基于定理證明的支持一階定理證明器ProVerif的抗拒絕服務攻擊性自動化證明方法，最后應用ProVerif分析與驗證了JFK協議與IEEE 802.11四步握手協議抗拒絕服務攻擊性，證明JFK協議能夠抵抗拒絕服務攻擊，而IEEE 802.11四步握手協議的確存在拒絕服務攻擊，同時也發現了IEEE 802.11四步握手協議的一個新的拒絕服務攻擊。針對IEEE 802.11四步握手協議存在的攻擊提出了2種改進方法。由于提出的抗拒絕服務攻擊性自動化證明方法主要從協議狀態來分析協議抗拒絕服務攻擊性，因此既可以分析利用協議狀態的保持產生的資源消耗型拒絕服務攻擊，又可以分析協議中止型拒絕服務攻擊，但是在分析由其他原因產生的存儲資源消耗型的拒絕服務攻擊方面還有欠缺，可以作為下一步的工作方向。同時在未來的工作中，計劃應用提出的基于定理證明的支持一階定理證明器ProVerif的抗拒絕服務攻擊性自動化證明方法對復雜的電子商務、電子投票協議的抗拒絕服務攻擊性進行深入的研究，驗證其抗拒絕服務攻擊性。

[1] 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.

[2] MEADOWS C. A cost-based framework for analysis of denial of service networks[J]. Journal of Computer Security, 2001,9(1/2):143-164.

[3] BLANCHET B. An efficient cryptographic protocol verifier based on prolog rules[A]. Proc of the 14th IEEE Workshop on Computer Security Foundations Workshop (CSFW)[C]. Cape Breton, Nova Scotia,Canada, 2001.82-96.

[4] 郭云川, 丁麗, 周淵等. 基于 ProVerif的電子商務協議分析[J]. 通信學報,2009,30(3):125-129.GUO Y C, DING L, ZHOU Y, et al. E-commerce protocol analysis based on ProVerif[J]. Journal on Communications, 2009, 30(3):125-129.

[5] MENG B, HUANG W, LI Z M, et al. Automatic verification of security properties in remote Internet voting protocol with applied pi cal-culus[J]. International Journal of Digital Content Technology and its Applications, 2010, 4(7):88-107.

[6] MENG B. Refinement of mechanized proof of security properties of remote Internet voting protocol in applied PI calculus with ProVerif[J].Information Technology Journal, 2011, 10(2):293-334.

[7] ABADI M, BLANCHET B, FOURNET C. Just fast keying in the pi calculus[J]. ACM Transactions on Information and System Security,2007, 10(3):1-59.

[8] ABADI M, FOURNET C. Mobile values, new names, and secure communication[A]. Proc of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)[C]. London,UK, 2001.104-115.

[9] MILLEN J K. A resource allocation model for denial of service protection[J]. Journal of Computer Security, 1993, 2(2-3):89-106.

[10] CUPPENS F, SAUREL C. Towards a formalization of availability and denial of service[A]. Proc of Information Systems Technology Panel Symposium on Protecting Nato Information Systems in the 21st Century[C]. Washington, 1999.

[11] RAMACHANDRAN V. Analyzing DoS-Resistance of Protocols Using a Cost-based Framework[R]. Technical Report DCS/TR-1239,Yale University, 2002.

[12] SMITH J,GONZALEZ-NIETO J M,BOYD C. Modelling denial of service attacks on JFK with Meadows's cost-based framework[A]. Proc of the 2006 Australasian Workshops on Grid Computing and E-Research(ACSW Frontiers)[C]. Darlinghurst, Australia, 2006. 125-134.

[13] GROZA B, MINEA M. Formal modelling and automatic detection of resource exhaustion attacks[A]. Proc of 6th ACM Symposium on Information, Computer and Communications Security (ASIACCS)[C].HongKong,China, 2011.

[14] LAFRANCE S, MULLINS J. Using admissible interference to detect denial of service vulnerabilities[A]. Proc of the Sixth International Workshop in Formal Methods (IWFM)[C]. Ireland,2003.

[15] 周世健, 蔣睿, 楊曉輝. 安全協議DoS攻擊的形式化分析方法研究[J].中國電子科學研究院學報.2008, 3(6):592-598.ZHOU S J, JING R, YANG X H. DoS attacks on security protocols of the formal analysis[J]. Journal of Research Institute of China Electronics, 2008, 3(6):592-598.

[16] TRITILANUNT S,BOYD C,FOO E, et al. Cost-based and time-based analysis of DoS-resistance in HIP[A]. Proc of the Thirtieth Australasian Conference on Computer Science (ACSC '07)[C]. Darlinghurst,Australia, 2007.191-200.

[17] TRITILANUNT S. Protocol Engineering for Protection Against Denial of Service Attacks[D]. Brisbane Australia, Queensland University of Technology, 2009.

[18] AGHA G, GREENW ALD M, GUNTER C A, et al. Formal modeling and analysis of DoS using probabilistic rewrite theories[A]. Proc of International Workshop on Foundations of Computer Security(FCS)[C].Chicago IL,2005.

[19] MAHIMKAR A, SHMATIKOV V. Game-based analysis of denial-of-service prevention protocols[A]. Proc of the 18th IEEE workshop on Computer Security Foundations (CSFW)[C]. Aix-en-Provence,France, 2005.287-301.

[20] KRAWCZYK H. Invited talk, SIGMA: the SIGn-and-MAc approach to authenticated diffie Hellman and its use in the IKE protocols[A].Proc of the 23rd Annual International Cryptology Conference(CRYPTO)[C]. Santa Barbara, California, USA, 2003.400-425.

[21] CANETTI R , KRAWCZYK H. Analysis of key-exchange protocols and their use for building secure channels[A]. Proc of the International Conference on the Theory and Application of Cryptographic Techniques: Advances in Cryptology (EUROCRYPT)[C]. Innsbruck, Austria, 2001.453-474.

[22] AIELLO W, BELLOVIN S M, BLAZE M, et al. Efficient,DoS-resistant, secure key exchange for Internet protocols[A]. Proc of the 9th ACM Conference on Computer and Communications Security(CCS)[C]. Washington, DC, USA, 2002.48-58.

[23] AIELLO W, BELLOVIN S M, BLAZE M, et al. Just fast keying: key agreement in a hostile internet[J]. ACM Transactions on Information and System Security, 2004, 7(2):242-273.

[24] BICAKCIA K, TAVLI B. Denial-of-service attacks and countermeasures in IEEE 802.11 wireless networks[J].Computer Standards & Interfaces, 2009, 31(5):931-941.

[25] HE C, MITCHELL J C. Analysis of the 802.11i 4-way handshake[A].Proc of the 3rd ACM Workshop on Wireless Security (WiSe '04)[C].ACM, New York, NY, USA, 2004.43-50.