協(xié)議抗拒絕服務(wù)攻擊性自動(dòng)化證明

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

（中南民族大學(xué) 計(jì)算機(jī)科學(xué)學(xué)院，湖北 武漢 430074）

1 引言

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

對(duì)拒絕服務(wù)攻擊的形式化建模，目前有2類主要方法，一類是以用戶合約為基礎(chǔ)的 Yu-Gligor形式化建模方法[1]，另一類是以代價(jià)為基礎(chǔ)的Meadows形式化建模方法[2]，后者受到了人們的重點(diǎn)關(guān)注。

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

在拒絕服務(wù)攻擊中非常重要的一類攻擊就是利用了協(xié)議狀態(tài)而產(chǎn)生的，例如，利用協(xié)議狀態(tài)的保持來耗盡系統(tǒng)資源，產(chǎn)生資源消耗型拒絕服務(wù)攻擊；修改協(xié)議狀態(tài)，使其前后狀態(tài)不一致而產(chǎn)生協(xié)議中止型拒絕服務(wù)攻擊。因此，本文脫離以用戶合約為基礎(chǔ)的 Yu-Gligor形式化建模方法與以代價(jià)為基礎(chǔ)的Meadows形式化建模方法，從協(xié)議狀態(tài)的角度，對(duì)協(xié)議抗拒絕服務(wù)攻擊性進(jìn)行建模，分析與驗(yàn)證協(xié)議抗拒絕服務(wù)攻擊性。由于標(biāo)準(zhǔn)應(yīng)用PI演算[8]不能夠?qū)f(xié)議狀態(tài)進(jìn)行建模，為了能夠使用基于應(yīng)用PI演算ProVerif來自動(dòng)化分析與驗(yàn)證協(xié)議抗拒絕服務(wù)攻擊性，必須對(duì)標(biāo)準(zhǔn)應(yīng)用PI演算進(jìn)行擴(kuò)展。首先從2個(gè)方面：一個(gè)是攻擊者上下文，另外一個(gè)是進(jìn)程表達(dá)式對(duì)標(biāo)準(zhǔn)應(yīng)用PI演算進(jìn)行擴(kuò)展，然后應(yīng)用擴(kuò)展后的應(yīng)用 PI演算對(duì)協(xié)議抗拒絕服務(wù)攻擊性進(jìn)行建模，提出一個(gè)基于定理證明支持一階定理證明器ProVerif的抗拒絕服務(wù)攻擊性自動(dòng)化證明方法，最后應(yīng)用ProVerif來分析與驗(yàn)證協(xié)議的抗拒絕服務(wù)攻擊性。

2 相關(guān)的工作

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

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

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

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

3 擴(kuò)展的應(yīng)用PI演算

為了對(duì)協(xié)議狀態(tài)及抗拒絕服務(wù)攻擊性進(jìn)行建模，從2個(gè)方面對(duì)標(biāo)準(zhǔn)應(yīng)用PI演算進(jìn)行擴(kuò)展：一個(gè)是攻擊者上下文，另外一個(gè)是進(jìn)程表達(dá)式。擴(kuò)展應(yīng)用PI演算語義與標(biāo)準(zhǔn)應(yīng)用PI演算相同。

3.1 攻擊者上下文

按照攻擊者對(duì)消息的攻擊能力將攻擊者所處的上下文分為現(xiàn)實(shí)上下文和理想上下文。

現(xiàn)實(shí)上下文形式化表示為

3.2 項(xiàng)

應(yīng)用PI演算[5]是一個(gè)用來描述并發(fā)進(jìn)程的語言。它繼承了PI演算的通信與并發(fā)結(jié)構(gòu)，增加了函數(shù)和等價(jià)理論。消息不僅是原子名，還可以是通過名字和函數(shù)構(gòu)成的項(xiàng)。

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

圖1 項(xiàng)的定義

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

3.3 擴(kuò)展后的進(jìn)程

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

圖2 擴(kuò)展后的進(jìn)程

3.4 進(jìn)程上下文

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

圖3 進(jìn)程上下文

4 定義和符號(hào)說明

定義1 帶注解Alice-and-Bob 規(guī)范描述。

定義2 消息Ml認(rèn)證性。

定義3 操作一致性。

定義41γ邏輯先于2γ。

P為協(xié)議帶注解Alice-and-Bob 規(guī)范描述，S為P中操作的集合。對(duì)于S中的任意操作1γ和2γ，1γ邏輯先于2γ當(dāng)且僅當(dāng)：

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

定義5 關(guān)聯(lián)集合。

協(xié)議中的任意消息 Mi和 Mj的關(guān)聯(lián)集合 ω 為中驗(yàn)證操作v的數(shù)據(jù)項(xiàng)集合?和 Mi的數(shù)據(jù)項(xiàng)的集合Ψ的交集，即 ω=?∩Ψ。其中 i, j∈[1 , n]且i＜j。

關(guān)聯(lián)集合ω反映了消息之間互相影響的程度：ω為空集，消息之間互不影響，是獨(dú)立的，關(guān)聯(lián)度為零；ω包含的數(shù)據(jù)項(xiàng)越多，消息之間互相影響的程度就越高，關(guān)聯(lián)度越高。

定義6 抗拒絕服務(wù)攻擊性。

P為協(xié)議帶注解Alice-and-Bob 規(guī)范描述，B具有抗拒絕服務(wù)攻擊性，當(dāng)且僅當(dāng) ()Recv B中的任意一對(duì)消息iM和jM 的關(guān)聯(lián)集合ω滿足：

1) ω是空集?；

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

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

如果協(xié)議 P中任意一對(duì)消息 Mi和 Mj之間互不關(guān)聯(lián)，那么處理這兩條消息的下文是互相獨(dú)立的，則B具有抗拒絕服務(wù)攻擊性；如果消息 Mi和Mj相關(guān)聯(lián)，則對(duì)消息 Mj的處理依賴于對(duì)消息 Mi的處理，那么處理這2條消息的上下文是狀態(tài)關(guān)聯(lián)的，則消息 Mi和 Mj關(guān)聯(lián)集合ω必須是可認(rèn)證的才使B具有抗拒絕服務(wù)攻擊性。

5 自動(dòng)化證明抗拒絕服務(wù)攻擊性方法

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

圖4 可達(dá)進(jìn)程

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

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

如果攻擊者能夠從公開信道c上獲得秘密S，則攻擊者可以通過對(duì)消息1M 進(jìn)行攻擊使協(xié)議產(chǎn)生拒絕服務(wù)攻擊。

圖5 消息M1的形式化模型

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

圖6 消息Mi的形式化模型

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

證明

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

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

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

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

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

至此，可以使用擴(kuò)展后的應(yīng)用PI演算對(duì)抗拒絕服務(wù)攻擊進(jìn)行形式化描述，基于給出的定理，應(yīng)用ProVeif自動(dòng)化證明協(xié)議的抗拒絕服務(wù)攻擊性。

6 一階定理證明器ProVerif

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

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

處理部分負(fù)責(zé)根據(jù)安全協(xié)議的形式化描述對(duì)要證明的安全屬性進(jìn)行邏輯推導(dǎo)證明。它包括自動(dòng)翻譯模塊和邏輯推導(dǎo)模塊。當(dāng)輸入語言為應(yīng)用 PI演算或本文提出的擴(kuò)展的應(yīng)用PI演算時(shí)，自動(dòng)翻譯模塊主要負(fù)責(zé)實(shí)現(xiàn)安全協(xié)議的應(yīng)用PI演算或本文提出的擴(kuò)展的應(yīng)用PI演算形式化描述到一階邏輯規(guī)則的轉(zhuǎn)換，邏輯推導(dǎo)模塊則基于一階邏輯規(guī)則對(duì)要證明的安全屬性進(jìn)行推理和驗(yàn)證。當(dāng)輸入語言為Horn子句時(shí)，處理部分為邏輯推導(dǎo)模塊，不需要自動(dòng)翻譯模塊。

結(jié)果輸出部分主要負(fù)責(zé)輸出處理結(jié)果。從輸出結(jié)果可以得知該協(xié)議是否滿足相應(yīng)的安全屬性，供用戶進(jìn)一步分析，但是ProVerif不輸出詳細(xì)的證明過程。如果不滿足某安全屬性，則ProVerif會(huì)給出詳細(xì)的攻擊方式。

圖7 ProVerif結(jié)構(gòu)

7 JFK與IEEE 802.11四步握手協(xié)議抗拒絕服務(wù)攻擊性

7.1 JFK協(xié)議

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

JFKr協(xié)議涉及2個(gè)角色：協(xié)議的發(fā)起者Alice和協(xié)議的響應(yīng)者Bob。攻擊者建模為Dolev-Yao模型中的攻擊者，既可以在公開信道上監(jiān)聽、攔截、修改，刪除和插入消息，又可以偽裝成誠(chéng)實(shí)的參與者。

JFKr協(xié)議的Alice-and-Bob 規(guī)范描述如圖8所示，符號(hào)說明見文獻(xiàn)[17]。

圖8 JFKr協(xié)議的Alice-and-Bob 規(guī)范描述

JFKr協(xié)議有4條消息組成，消息1和消息2通過Diffie-Hellman密鑰交換協(xié)議建立共享密鑰。首先Alice生成公鑰Alicex和隨機(jī)數(shù)AliceN，發(fā)送給Bob。Bob生成公鑰Bobx、隨機(jī)數(shù)BobN，認(rèn)證cookieBobt。tBob是狀態(tài)信息的MAC值。是Bob成功收到消息1準(zhǔn)備發(fā)送消息2時(shí)的自己環(huán)境狀態(tài)。消息3和消息4提供認(rèn)證性。消息3和消息4包含加密隨機(jī)數(shù)、Diffie-Hellman指數(shù)及其他信息的簽名。Alice生成消息3發(fā)送給Bob，Bob驗(yàn)證消息3中狀態(tài)信息的MAC值tBob的正確性。如果驗(yàn)證成功，Bob用及eK生成加密后的身份標(biāo)識(shí)eBob及其MAC值hBob組成消息4發(fā)送給Alice。

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

圖9 JFKr的ProVerif輸出結(jié)果

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

7.2 IEEE 802.11 i四步握手協(xié)議

IEEE 802.11標(biāo)準(zhǔn)是無線局域網(wǎng)中廣泛采用的標(biāo)準(zhǔn)。由于IEEE 802.11標(biāo)準(zhǔn)被證明在實(shí)體認(rèn)證和有線等價(jià)保密方面是不安全的，IEEE 802.11i標(biāo)準(zhǔn)[21]被提出來增強(qiáng)IEEE 802.11的安全性。IEEE 802.11i除了引入了新的密鑰管理和生成算法，還改進(jìn)了加密和認(rèn)證算法。它定義了一個(gè)基于IEEE 802.1X認(rèn)證和4步握手的強(qiáng)安全網(wǎng)絡(luò)關(guān)聯(lián)。Bicakcia與Tavli[24]對(duì)IEEE 802.11的拒絕服務(wù)攻擊與防范措施進(jìn)行了深入研究。

四步握手協(xié)議簡(jiǎn)化了的Alice-and-Bob 規(guī)范描述如圖10所示。

圖10 四步握手協(xié)議的Alice-and-Bob 規(guī)范描述

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

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

應(yīng)用提出的自動(dòng)化抗拒絕服務(wù)攻擊性證明方法，ProVerif給出了兩個(gè)拒絕服務(wù)攻擊：拒絕服務(wù)攻擊1，如圖11和圖12所示。拒絕服務(wù)攻擊2，如圖13和圖14所示。其中拒絕服務(wù)攻擊2是應(yīng)用我們提出的方法發(fā)現(xiàn)的。。

根據(jù)四步握手協(xié)議規(guī)范，由于請(qǐng)求者Bob對(duì)消息M3的驗(yàn)證依賴于臨時(shí)密鑰PTK，而臨時(shí)密鑰PTK的生成取決于Anonce和Snonce，Snonce的產(chǎn)生又依賴于對(duì)消息M1的重放計(jì)數(shù)值Replay_Counter的有效性驗(yàn)證，所以攻擊者只要成功篡改或重放Anonce與計(jì)數(shù)值Replay_Counter，就可以使請(qǐng)求者Bob對(duì)合法的消息M3的驗(yàn)證失敗，從而產(chǎn)生拒絕服務(wù)攻擊。

根據(jù)消息M1形式化模型，請(qǐng)求者Bob處理消息M1和消息M3的操作Recv(Bob){act(Bob)其中，v是驗(yàn)證操作，。所以M1和M3的關(guān)聯(lián)集合ω=｛Anonce1｝。由于四步握手協(xié)議沒有對(duì)Anonce1進(jìn)行驗(yàn)證，Anonce1是不可認(rèn)證的，由定義6可知四步握手協(xié)議中的請(qǐng)求者Bob不能防止拒絕服務(wù)攻擊。

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

圖11 針對(duì)拒絕服務(wù)攻擊1的ProVerif輸出

圖12 ProVerif輸出的拒絕服務(wù)攻擊1

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

圖13 針對(duì)拒絕服務(wù)攻擊2的ProVerif輸出

圖14 ProVerif輸出的拒絕服務(wù)攻擊2

針對(duì)拒絕服務(wù)攻擊1，He[25]提出請(qǐng)求者Bob除了存儲(chǔ) PTK，另外為每一個(gè)消息M1存儲(chǔ)一個(gè)TPTK(temporary PTK )，在收到消息M1時(shí)，僅更新TPTK，在收到正確的消息M3時(shí)才更新PTK。但是，當(dāng)攻擊者大量發(fā)送偽造的消息M1時(shí)，Bob就會(huì)存儲(chǔ)大量的 TPTK，產(chǎn)生存儲(chǔ)資源消耗型的拒絕服務(wù)攻擊。

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

如果只防止拒絕服務(wù)攻擊 2，那么請(qǐng)求者 Bob可以存儲(chǔ)其在一定時(shí)間內(nèi)收到的Anonce，并且在進(jìn)行下一步處理前，檢查Anonce是否是在一定時(shí)間內(nèi)是重放的，則可以防止這種攻擊。

8 結(jié)束語

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

[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的電子商務(wù)協(xié)議分析[J]. 通信學(xué)報(bào),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] 周世健, 蔣睿, 楊曉輝. 安全協(xié)議DoS攻擊的形式化分析方法研究[J].中國(guó)電子科學(xué)研究院學(xué)報(bào).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.