梅映天 吳尚青

(1池州職業(yè)技術(shù)學(xué)院 安徽池州 247100；2江西省機(jī)場集團(tuán)公司九江機(jī)場分公司 江西九江 332000)

IEEE 802.11是自1997年以來，無線局域網(wǎng)絡(luò)使用的通用標(biāo)準(zhǔn)，隨著信息時(shí)代的不斷發(fā)展，IEEE 802.11標(biāo)準(zhǔn)也在不斷地修改和完善，從而增強(qiáng)數(shù)據(jù)安全和用戶認(rèn)證機(jī)制[1]。最初，管理框架不包含敏感信息，因此不太需要對其進(jìn)行保護(hù)，但是隨著新的無線網(wǎng)絡(luò)管理方案的更新以及管理幀中敏感信息未加密問題的日益嚴(yán)重，IEEE工作組提出了一個(gè)新的IEEE 802.11w修正案，旨在保護(hù)無線連接和管理幀中交換的網(wǎng)絡(luò)敏感信息[2]。IEEE 802.11w標(biāo)準(zhǔn)基于IEEE 802.11i無線網(wǎng)絡(luò)管理框架[3]，是一種在原始框架下增加管理幀保護(hù)的標(biāo)準(zhǔn)，致力于改進(jìn)IEEE 802.11通用標(biāo)準(zhǔn)中的MAC層從而增加管理幀的安全性[4-5]，可以對抗攻擊者在無線局域網(wǎng)中基于管理幀的攻擊[6]。

形式化方法被廣泛應(yīng)用于驗(yàn)證密碼協(xié)議的不同安全屬性，如協(xié)議交互過程中密文機(jī)密性的證明，不同主體之間認(rèn)證性的證明，或是電子商務(wù)協(xié)議中不可否認(rèn)性的證明，從而保證協(xié)議執(zhí)行過程中的正確性[7]。事件邏輯[8]屬于定理證明一類，是形式化方法的一種，不僅可以形容各類分布式系統(tǒng)中出現(xiàn)的狀態(tài)遷移事件，同樣也可以對密碼協(xié)議的各種屬性進(jìn)行描述[9]。事件邏輯理論可以將安全協(xié)議表述為事件序和事件類的語言，并且使用原子Atom來表示nonce,key,signature,ciphertexts，給出簡單的公理化理論[10]，通過這些定義，安全協(xié)議可以被正式定義，其強(qiáng)認(rèn)證屬性也可以通過定義進(jìn)行進(jìn)一步的證明。

文章組織結(jié)構(gòu)如下：第2節(jié)介紹IEEE 802.11w無線網(wǎng)絡(luò)認(rèn)證協(xié)議；第3節(jié)介紹事件邏輯理論，并提出隨機(jī)數(shù)引理；第4節(jié)使用事件邏輯理論對IEEE 802.11w無線網(wǎng)絡(luò)認(rèn)證協(xié)議認(rèn)證性進(jìn)行證明；第5節(jié)為文章的結(jié)論部分。

1 IEEE802.11w無線認(rèn)證協(xié)議

在IEEE 802.11w無線網(wǎng)絡(luò)認(rèn)證協(xié)議正式通過確立之前，只有數(shù)據(jù)幀能夠被加密保護(hù)[11]，而對管理幀和控制幀等所有其他幀都沒有任何保護(hù)[12]。IEEE 802.11w在協(xié)議的交互過程中，有別于其他標(biāo)準(zhǔn)的一處就是允許使用一些具有保護(hù)的管理幀，通過四次握手完成秘鑰協(xié)商從而保護(hù)管理幀。

IEEE 802.11w無線認(rèn)證協(xié)議通過四次握手過程驗(yàn)證STA(Station，工作站)是否知道PMK(Pre-Shared Key，預(yù)共享密鑰)[13]。其中AP(Acess point，接入點(diǎn))可以理解為無線網(wǎng)絡(luò)的創(chuàng)建方，提供無線網(wǎng)絡(luò)接入的服務(wù)，STA是任何可以連接并且加入到當(dāng)前無線局域網(wǎng)的終端。

根據(jù)完美密碼假設(shè)，假定密碼系統(tǒng)是完善的，從而對協(xié)議本身進(jìn)行剖析，可得到主要認(rèn)證交互信息如圖1所示，首先AP發(fā)送包含NonceA的信息，然后STA發(fā)送給AP新生成的隨機(jī)數(shù)NonceS和基于NonceA的消息完整性驗(yàn)證。在接收到第二條消息之后，AP能夠?qū)С鯬TK，通過發(fā)送經(jīng)PTK加密的GTK，IGTK，NonceS的消息完整性驗(yàn)證來檢查消息的正確性并繼續(xù)認(rèn)證，最后STA發(fā)送給AP一個(gè)只包含GTK，IGTK的完整性確認(rèn)。

圖1 IEEE 802.11w中主要交互信息描述

2事件邏輯理論

事件邏輯是定理證明方法中的一種，使用嚴(yán)格的數(shù)學(xué)規(guī)則和邏輯方法對密碼協(xié)議的性質(zhì)進(jìn)行證明分析，是一種描述并發(fā)與分布式系統(tǒng)下協(xié)議和算法的邏輯。

2.1基本語義

該部分介紹事件邏輯基本語義[8，14-15]，用于刻畫IEEE 802.11w無線網(wǎng)絡(luò)認(rèn)證協(xié)議交互過程中的不同安全屬性，基本符號(hào)定義具體如表1所示。

表1 事件邏輯基本符號(hào)

在對IEEE 802.11w無線網(wǎng)絡(luò)認(rèn)證協(xié)議進(jìn)行形式化證明之前，首先需要使用事件邏輯理論對IEEE 802.11w無線網(wǎng)絡(luò)認(rèn)證協(xié)議的交互過程進(jìn)行建模，建立包含事件點(diǎn)的模型，主要通過三種類型布爾值、標(biāo)識(shí)符、原子(Atom)，其中原子表示不可預(yù)測的數(shù)據(jù)值[6-7]，即任何無法猜測的內(nèi)容，比如密文和挑戰(zhàn)數(shù)。x:T||a表示類型T不包含原子a。當(dāng)x屬于類型T時(shí)，x和a相互獨(dú)立。

事件類是事件邏輯中另一個(gè)基本概念，將密碼協(xié)議中會(huì)發(fā)生的主要事件進(jìn)行分類，包括信息的發(fā)送，信息的接受，不同主體隨機(jī)數(shù)的生成，明文的加密，密文的解密，信息的簽名以及簽名的驗(yàn)證，其中不同事件的類型由此決定。事件類包含Atom，可以使用一個(gè)二叉樹Data≡defTree(Id+Atom)來定義所有事件類，七個(gè)協(xié)議動(dòng)作類型可定義如下：

2.2公理系統(tǒng)

2.2.1因果公理 因果公理包括AxiomR,AxiomV,AxiomD，將任何的接收，驗(yàn)證以及解密事件之間發(fā)生前后相互關(guān)聯(lián)起來。

2.2.2不相交公理 不相交公理定義任何主體，其產(chǎn)生的隨機(jī)數(shù)nonce與自身持有的私鑰，簽名以及密文是不相交的。

2.2.3誠實(shí)公理 誠實(shí)主體在任何情況下都不會(huì)釋放自己的私鑰，并且任何的簽名事件、加密事件以及解密事件，如果需要使用到主體私鑰，這些事件都必須發(fā)生在誠實(shí)主體上。

2.2.4秘鑰公理 對稱密鑰只能匹配自身，而分配給主體的私有秘鑰只匹配相對的公鑰，協(xié)議交互過程中沒有任何兩個(gè)主體會(huì)擁有相同的私鑰。

2.2.5隨機(jī)數(shù)公理 隨機(jī)數(shù)公理主要包含三部分，主要定義簽名、密文以及包含事件之間的相似關(guān)系。如果存在沒有經(jīng)過假設(shè)的簽名消息或者加密信息，那么一定與獨(dú)立事件有關(guān)，所以如果存在一個(gè)事件包含簽名消息或者加密過的信息，只能推斷出部分的消息簽名或加密事件。

2.2.6流關(guān)系 流關(guān)系公理定義事件與事件之間的因果順序，假設(shè)Atom類型的a從e1流入到e2，只能以有限的方式發(fā)生。第一種方式是e1和e2位于同一主體；第二種是存在發(fā)送和接收事件，將a通過明文發(fā)送；第三種情況為a位于加密事件，并流入匹配的解密事件。

2.3推理規(guī)則

線程thr是主體A中已知bss基本序列的其中之一，記作thr=oneof(bss,A)。關(guān)系inoneof(e,thr,bss,A)用協(xié)議的形式化定義為：e∈thr∧thr=oneof(bass,A)[14-15]。

線程thr1和thr2構(gòu)成一個(gè)長度為n的匹配會(huì)話，如果它們包含至少n個(gè)消息，且當(dāng)線程中前n個(gè)消息成對存在，每對滿足m1|m2∨m2|m1。此時(shí)強(qiáng)匹配會(huì)話定義為如果每對只滿足m1～m2∨m2～m1，得到一個(gè)弱匹配會(huì)話，記作

2.4隨機(jī)數(shù)引理

如果協(xié)議Protocol(bss)是合法的。A是誠實(shí)主體并且屬于協(xié)議Protocol(bss)，且thr屬于基本序列bssthr[j]、n∈E(New)、e=thr[j]，和j

3 IEEE802.11w無線認(rèn)證協(xié)議分析

使用事件邏輯理論對IEEE802.11w無線認(rèn)證協(xié)議的認(rèn)證性進(jìn)行分析，首先需要對該協(xié)議的基本序列進(jìn)行描述，定義I1,I2,I3,I4,I5為協(xié)議認(rèn)證方產(chǎn)生的基本序列，R1,R2,R3,R4為協(xié)議被認(rèn)證方產(chǎn)生的基本序列，圖2所示為IEEE 802.11w無線網(wǎng)絡(luò)認(rèn)證協(xié)議的交互過程描述。

圖2 IEEE802.11w無線認(rèn)證協(xié)議序列描述

通過事件邏輯理論形式化分析在協(xié)議交互過程中需要滿足的安全屬性，來驗(yàn)證IEEE802.11w無線網(wǎng)絡(luò)認(rèn)證協(xié)議是否存在未知風(fēng)險(xiǎn)，還需要對協(xié)議交互中的基本序列進(jìn)行排序。圖3所示為IEEE802.11w無線網(wǎng)絡(luò)認(rèn)證協(xié)議交互過程中每個(gè)主體間基本序列的排序。

圖3 IEEE802.11w無線認(rèn)證協(xié)議基本序列

如果IEEE802.11w無線認(rèn)證協(xié)議可以保證不同時(shí)間的兩個(gè)線程間具有強(qiáng)匹配會(huì)話，則IEEE802.11w無線網(wǎng)絡(luò)認(rèn)證協(xié)議滿足協(xié)議交互過程中的強(qiáng)認(rèn)證屬性。所以分析基本序列，使用事件邏輯理論將IEEE802.11w無線網(wǎng)絡(luò)認(rèn)證協(xié)議定義為Protocol([I1，I2，I3，I4，I5，R1，R2，R3，R4])，需要驗(yàn)證的強(qiáng)身份認(rèn)證性質(zhì)為：

Nse╞auth(I5，4)∧Nse╞auth(R4，3)

首先對Nse╞auth(I5，4)進(jìn)行證明，假設(shè)誠實(shí)主體AP≠STA，且雙方都遵循IEEE802.11w無線認(rèn)證協(xié)議，根據(jù)事件邏輯理論中對于協(xié)議中基本序列的定義，線程作為基本序列的實(shí)例存在，則令thr1是基本序列I5的一個(gè)實(shí)例，定義 e0

由驗(yàn)證公理AxiomV和誠實(shí)公理AxiomS可知，存在某個(gè)事件e′并且e′能夠使得式子e′

故而可以排除I2,I3,I4,I5，即意味著R2,R3,R4中存在一個(gè)基本序列可能與I5構(gòu)成匹配會(huì)話.

假設(shè)e′為R2中的一個(gè)實(shí)例，那么對于Atom類型的NonceS′,NonceA′,s1′以及主體A，在主體STA上存在事件e0′,e1′,e2′,e3′有：

通過上式發(fā)現(xiàn)，R2中簽名事件e2′與驗(yàn)證事件e8不匹配，所以排除e′是R2中一個(gè)實(shí)例的可能性，同理排除R3。

可發(fā)現(xiàn)滿足：

則可知有e7′=e′,B=AP,GTK′=GTK,IGTK′=IGTK,s4′=s4，可得出：

在已知e7′=e′，e′一定為R4中的某個(gè)實(shí)例后，必須存在某個(gè)事件e″，并且這個(gè)事件能夠令e″,AP,s3>。

因此，事件e″必然為協(xié)議基本序列中的實(shí)例成員，在基本序列中，包含Sign( )動(dòng)作的有I2,I3,I4,I5,R2,R3,R4。可以排除I4,I5，同樣為了保證事件發(fā)生的有效性，所以AP和STA參與的事件類不能是單方的，可以排除R2,R3,R4，也就得出I2,I3中存在一個(gè)基本序列包含序列e″。

假設(shè)e″是I2上的實(shí)例，對于Atom類型的NonceS″,NonceA″,s1″和主體C，在主體AP存在事件e0″,e1″,e2″,e3″有：

從上式可得出I2中的簽名事件e1″與解密事件e5′不匹配，所以排除e″是I2中的一個(gè)實(shí)例的可能性.

由上式可以發(fā)現(xiàn)，滿足：

則可知有e6″=e″,NonceS″=NonceS,D=STA,s3″=s3，可以得到：

當(dāng)e″為I3中的實(shí)例后，則必須再存在某個(gè)事件e?并且這個(gè)事件可以使得如下表達(dá)式e?,STA,s1>。

如果e?存在，那么事件e?必然為IEEE802.11w無線認(rèn)證協(xié)議基本序列中的某一個(gè)實(shí)例成員，其中包含Sign( )動(dòng)作的有I2,I3,I4,I5,R2,R3,R4。對于未發(fā)生的事件將不納入考慮范圍，則可以排除R3,R4,I4,I5，即R2中可能存在一個(gè)基本序列包含序列e?。

假設(shè)e?是R2上的一個(gè)實(shí)例，那么對于Atom類型的NonceS?,NonceA?,s1?和主體E，在主體STA上存在事件e0?,e1?,e2?,e3?,e4?,e5?有：

可以發(fā)現(xiàn)滿足：

則由上式可知存在e?，故有e4?=e?,E=AP,NonceA?=NonceA,s1?=s1，由此可以得到：

根據(jù)以上證明結(jié)果，可以得到：

所以在協(xié)議的交互過程中，存在一個(gè)弱匹配會(huì)話，并且其長度為3。

下一步對協(xié)議交互過程中的強(qiáng)匹配會(huì)話進(jìn)行證明，根據(jù)事件邏輯理論定義，首先需要證明e3′進(jìn)行簽名，而不包括STA的名稱，若攻擊者擁有足夠的能力[16]，則在證明步驟中無法得出D=STA的結(jié)論，并且證明失敗，即存在中間人的攻擊。

類似的，可證明Nse╞auth(R4，3)。

通過證明，可知IEEE802.11w無線網(wǎng)絡(luò)認(rèn)證協(xié)議的交互主體同時(shí)滿足需要證明的兩個(gè)強(qiáng)認(rèn)證性質(zhì)，所以在協(xié)議交互過程中不存在消息重放的可能性，但是在攻擊者擁有足夠能力的情況下，存在中間人攻擊，IEEE802.11w無線網(wǎng)絡(luò)認(rèn)證協(xié)議交互過程中的認(rèn)證性無法得證。

4結(jié)語

文章基于事件邏輯理論對IEEE802.11w無線網(wǎng)絡(luò)認(rèn)證協(xié)議交互過程中的認(rèn)證性進(jìn)行驗(yàn)證，結(jié)合事件邏輯基本公理以及推理規(guī)則并提出隨機(jī)數(shù)引理對IEEE 802.11w標(biāo)準(zhǔn)交互過程中認(rèn)證性進(jìn)行驗(yàn)證，證明得出IEEE 802.11w無線認(rèn)證協(xié)議能夠抵抗重放攻擊但是存在中間人攻擊。研究表明，事件邏輯理論適用于類似無線認(rèn)證協(xié)議的證明。