肖躍雷，王育民，龐遼軍，譚示崇

（1. 西安郵電大學(xué) 物聯(lián)網(wǎng)與兩化融合研究院，陜西 西安 710061；2. 西安電子科技大學(xué) 綜合業(yè)務(wù)網(wǎng)理論與關(guān)鍵技術(shù)國家重點(diǎn)實(shí)驗(yàn)室，陜西 西安 710071；3.西安電子科技大學(xué) 生命科學(xué)技術(shù)學(xué)院，陜西 西安 710071）

1 引言

WLAN Mesh網(wǎng)絡(luò)作為一種新型的網(wǎng)絡(luò)結(jié)構(gòu)，成為近年來國內(nèi)外研究的熱點(diǎn)問題之一。在802.11i[1]的基礎(chǔ)上，802.11s[2]提出了 EMSA(efficient mesh security association)來建立WLAN Mesh安全關(guān)聯(lián)，包括建立新加入的Mesh節(jié)點(diǎn)(MP,mesh point)和Mesh認(rèn)證器(MA,mesh authenticator)之間的安全關(guān)聯(lián)、新加入的 MP和 Mesh密鑰分發(fā)器(MKD,mesh key distributor)之間的安全關(guān)聯(lián)、新加入的MP和各個鄰居MP之間的安全關(guān)聯(lián)。WLAN Mesh安全關(guān)聯(lián)主要包括4個步驟：第1個步驟是執(zhí)行一個認(rèn)證過程，實(shí)現(xiàn)對新加入的MP的認(rèn)證并導(dǎo)出密鑰，第2～3個步驟是基于第1個步驟導(dǎo)出的密鑰建立新加入的 MP和 MA之間的安全關(guān)聯(lián)、新加入的MP和MKD之間的安全關(guān)聯(lián)、新加入的MP和各個鄰居MP之間的安全關(guān)聯(lián)。近年來，隨著可信計(jì)算技術(shù)的產(chǎn)生和發(fā)展，使得可信計(jì)算技術(shù)不僅可以建立終端的可信計(jì)算環(huán)境，而且可以將終端的可信計(jì)算環(huán)境擴(kuò)展至網(wǎng)絡(luò)，使網(wǎng)絡(luò)成為一個可信計(jì)算環(huán)境，從而從源頭上遏制住惡意攻擊，有效解決日漸突出和復(fù)雜的網(wǎng)絡(luò)安全問題?？尚沤尤胝J(rèn)證的目標(biāo)就是將終端的可信計(jì)算環(huán)境擴(kuò)展至網(wǎng)絡(luò)，它包括用戶認(rèn)證和平臺認(rèn)證，其中平臺認(rèn)證包括平臺身份認(rèn)證和平臺完整性驗(yàn)證[3]，平臺身份認(rèn)證可以基于可信第三方(私有 CA)或直接匿名證明 (DAA,direct anonymous attestation)機(jī)制來實(shí)現(xiàn)。因此， EMSA在可信計(jì)算環(huán)境下不再適用，因?yàn)樗荒軐?shí)現(xiàn)WLAN Mesh可信接入認(rèn)證。也就是說，EMSA沒有實(shí)現(xiàn)對新加入的MP的平臺認(rèn)證，從而不能構(gòu)建可信計(jì)算環(huán)境 WLAN Mesh網(wǎng)絡(luò)?？尚庞?jì)算環(huán)境WLAN Mesh網(wǎng)絡(luò)是指每一個新加入的MP在接入WLAN Mesh網(wǎng)絡(luò)之前都必須對它進(jìn)行平臺認(rèn)證，以保證每一個新加入的MP處于可信計(jì)算環(huán)境下的安全狀態(tài)，從而將每一個新加入的MP的可信計(jì)算環(huán)境擴(kuò)展至整個WLAN Mesh網(wǎng)絡(luò)。于是，馬卓等提出了一些 WLAN Mesh可信接入認(rèn)證協(xié)議[4～6]來增強(qiáng)EMSA，并證明了它們是通用可組合安全的。

類似于802.11i，我國也推出了WLAN鑒別和保密基礎(chǔ)設(shè)施(WAPI,WLAN authentication privacy infrastructure)[7～9]來解決 IEEE 802.11 標(biāo)準(zhǔn)[10]中存在的安全問題，它包括WLAN鑒別基礎(chǔ)設(shè)施(WAI，WLAN authentication infrastructure)和WLAN保密基礎(chǔ)設(shè)施(WPI,WLAN privacy infrastructure)2個部分，其中，WAI由證書鑒別過程、單播密鑰協(xié)商過程和組播密鑰協(xié)商過程組成。雖然最新的WAI協(xié)議(即第 3版 WAI協(xié)議)被證明是安全的[11,12]，但是它用于建立 WLAN Mesh安全關(guān)聯(lián)時存在以下問題：新加入的MP首先需要與MA、認(rèn)證服務(wù)器(AS,authentication server)執(zhí)行一次WAI證書鑒別過程和一次單播密鑰協(xié)商過程來接入WLAN Mesh網(wǎng)絡(luò)并建立新加入的MP和MA之間的安全關(guān)聯(lián)，然后還需要與WLAN Mesh網(wǎng)絡(luò)中的n個鄰居MP和AS執(zhí)行n次WAI證書鑒別過程和n次單播密鑰協(xié)商過程來建立新加入的MP和n個鄰居MP之間的安全關(guān)聯(lián)，這使得WLAN Mesh安全關(guān)聯(lián)的性能較差，特別是使AS的負(fù)載太重。此外，由于第3版WAI協(xié)議沒有考慮平臺認(rèn)證，所以它不適用于建立可信計(jì)算環(huán)境下的WLAN Mesh安全關(guān)聯(lián)，也就是說它不能實(shí)現(xiàn)WLAN Mesh可信接入認(rèn)證。

為了解決上述問題，本文通過對第 3版 WAI協(xié)議的改進(jìn)，提出了一種基于改進(jìn) WAI協(xié)議的WLAN Mesh安全關(guān)聯(lián)方案，它提高了WLAN Mesh安全關(guān)聯(lián)的性能，特別是降低了AS的負(fù)載。然后，通過對第3版WAI協(xié)議的進(jìn)一步改進(jìn)，在該方案的基礎(chǔ)上提出了一種可信計(jì)算環(huán)境下的WLAN Mesh安全關(guān)聯(lián)方案，它能實(shí)現(xiàn)WLAN Mesh可信接入認(rèn)證，從而增強(qiáng)了WLAN Mesh的安全性。此外，本文利用串空間模型(SSM,strand space model)[13～15]證明了這2個WLAN Mesh安全關(guān)聯(lián)方案是安全的。

2 基于改進(jìn)WAI協(xié)議的WLAN Mesh安全關(guān)聯(lián)方案

基于改進(jìn)WAI協(xié)議的WLAN Mesh安全關(guān)聯(lián)方案如圖1所示。

圖1 基于改進(jìn)WAI協(xié)議的WLAN Mesh安全關(guān)聯(lián)方案

在圖1中，對第3版WAI協(xié)議的改進(jìn)主要體現(xiàn)于證書鑒別過程′，它是對第3版WAI協(xié)議中的證書鑒別過程的改進(jìn)?；诟倪M(jìn)WAI協(xié)議的WLAN Mesh安全關(guān)聯(lián)方案主要包括以下3個部分。

1)新加入的MP、MA和AS執(zhí)行證書鑒別過程′來實(shí)現(xiàn)新加入的MP與MA之間的雙向認(rèn)證，新加入的MP與AS之間的雙向認(rèn)證，并建立新加入的MP與MA之間的基密鑰BK，以及新加入的MP與AS之間的主密鑰MK。然后，新加入的MP和MA利用 BK執(zhí)行單播密鑰協(xié)商過程建立它們之間的單播密鑰，用于保護(hù)它們之間的鏈路層數(shù)據(jù)通信。

2)AS通過密鑰分發(fā)消息將MK分發(fā)給MKD，其中密鑰分發(fā)消息是利用AS與MKD之間預(yù)置的安全通道進(jìn)行安全保護(hù)的。然后，MKD和新加入的 MP將 MK擴(kuò)展為2個一級主密鑰：FMK1和FMK2。最后，MKD和新加入的MP利用FMK1執(zhí)行單播密鑰協(xié)商過程建立它們之間的單播密鑰，用于保護(hù)后來它們之間交互的密鑰傳輸請求消息和密鑰傳輸響應(yīng)消息。

3)當(dāng)新加入的MP在接入WLAN Mesh網(wǎng)絡(luò)后要與第i個鄰居MP建立安全關(guān)聯(lián)時，新加入的MP將FMK2擴(kuò)展為一個用于它和該鄰居MP的二級主密鑰SMKi，第i個鄰居MP向MKD發(fā)送密鑰傳輸請求消息，MKD收到密鑰傳輸請求消息后將FMK2擴(kuò)展為一個用于新加入的MP和該鄰居MP的二級主密鑰 SMKi，并通過密鑰傳輸響應(yīng)消息發(fā)送給該鄰居 MP，其中密鑰傳輸請求消息和密鑰傳輸響應(yīng)消息中是利用該鄰居MP與MKD之間已建立的單播密鑰進(jìn)行安全保護(hù)的。然后，新加入的MP和第i個鄰居MP利用SMKi執(zhí)行單播密鑰協(xié)商過程建立它們之間的單播密鑰，用于保護(hù)它們之間的鏈路層數(shù)據(jù)通信。

2.1 證書鑒別過程′

證書鑒別過程′的具體步驟如下。

其中，STA、AP和AS分別表示站(STA，station)、接入點(diǎn)(AP，access point)和AS，

ECDHparams為AP選擇的ECDH參數(shù)，NSTA和NAS分別為STA和AS產(chǎn)生的隨機(jī)數(shù)，NAP和NAP,2為AP產(chǎn)生的2個隨機(jī)數(shù)，x·P、y·P和z·P分別為STA、AP和AS產(chǎn)生的密鑰數(shù)據(jù)，IDSTA、IDAP和IDAS分別為STA、AP和AS的身份標(biāo)識，CertSTA和CertAP分別為STA和 AP的證書，σAS,2為AS的簽名且σAS,2=[z·P]skAS，skAS為AS的私鑰，σSTA,2為STA的簽名且σSTA,2=[x·P]skSTA，skSTA為STA的私鑰，σAS為AS的簽名且σAS=[ResAS]skAS，ResAS=NAP,2||NSTA||CertSTA||CertAP||ReSTA||ReAP，ReSTA和ReAP分別為CertSTA和CertAP的證書驗(yàn)證結(jié)果，MACSTA為STA的消息鑒別碼且MACSTA=HMAC(MK,NAS||z·P||σAS,2||NSTA||CertSTA||x·P ||σSTA,2)，HMAC()為用于生成消息鑒別碼的 Hash函數(shù)，MK=HKD(x·z·P,NSTA||NAS)，HKD()為用于擴(kuò)展密鑰的Hash函數(shù)，MACAS為AS的消息鑒別碼且MACAS=HMAC(MK,NAS||z·P||σAS,2||NSTA||CertSTA||x·P||σSTA,2||MACSTA||NAP||y·P||ResAS||σAS)，σSTA為STA的簽名且σSTA=[NAP||NSTA||x·P||IDAP||CertSTA||ECDHparams||IDAS||σSTA,2||MACSTA]skSTA，σAP為AP的簽名且σAP=[NSTA||NAP,2||Reaccess||x·P||y·P||IDAP||IDSTA||ResAS||σAS||MACAS]skAP，skAP為AP的私鑰，Reaccess為AP產(chǎn)生的接入結(jié)果。

相對于第3版WAI協(xié)議中的證書鑒別過程，證書鑒別過程′中帶單下劃線的消息和字段是新增加的，而帶雙下劃線的字段做了相應(yīng)的擴(kuò)展，目的是實(shí)現(xiàn)STA和AS之間的雙向認(rèn)證，并建立它們之間的MK。由于證書鑒別過程′只是新增加了一些消息和字段，以及擴(kuò)展了一些字段，所以它與第 3版WAI協(xié)議中的證書鑒別過程向后兼容。

2.2 性能對比分析

假設(shè)：新加入的MP通過MA接入WLAN Mesh網(wǎng)絡(luò)并建立與MA之間的安全關(guān)聯(lián)后，還需要與n個鄰居MP建立安全關(guān)聯(lián)。表1給出了本文引言中所述的基于WAI協(xié)議的WLAN Mesh安全關(guān)聯(lián)方案和基于改進(jìn)WAI協(xié)議的安全關(guān)聯(lián)方案的性能對比，其中，E為模指數(shù)運(yùn)算，F(xiàn)為計(jì)算簽名，M為消息認(rèn)證碼。

表1 基于WAI協(xié)議的WLAN Mesh安全關(guān)聯(lián)方案和基于改進(jìn)WAI協(xié)議的安全關(guān)聯(lián)方案的性能對比

在表1中，第1行性能參數(shù)是基于WAI協(xié)議的WLAN Mesh安全關(guān)聯(lián)方案的交互消息數(shù)及相關(guān)計(jì)算量，第 2行性能參數(shù)是基于改進(jìn) WAI協(xié)議的WLAN Mesh安全關(guān)聯(lián)方案的交互消息數(shù)及相關(guān)計(jì)算量。從表 1可以看出，基于改進(jìn) WAI協(xié)議的WLAN Mesh安全關(guān)聯(lián)方案比本文引言中所述的基于WAI協(xié)議的WLAN Mesh安全關(guān)聯(lián)方案在通信效率和計(jì)算量上都具有明顯的優(yōu)勢，具體分析如下。

方案通信效率：當(dāng)n=2時，2個方案中交互的消息數(shù)相同，但是，隨著n的值增大，與本文引言中所述的基于WAI協(xié)議的WLAN Mesh安全關(guān)聯(lián)方案的交互消息數(shù)相比，基于改進(jìn)WAI協(xié)議的WLAN Mesh安全關(guān)聯(lián)方案的交互消息數(shù)越來越少。

方案計(jì)算量：2個方案中MA的計(jì)算量相同，而基于改進(jìn)WAI協(xié)議的WLAN Mesh安全關(guān)聯(lián)方案中MKD的計(jì)算量比本文引言中所述的基于WAI協(xié)議的WLAN Mesh安全關(guān)聯(lián)方案中MKD的計(jì)算量增加了1M，但是，隨著n的值增大，與本文引言中所述的基于WAI協(xié)議的WLAN Mesh安全關(guān)聯(lián)方案中新加入的MP的計(jì)算量、n個鄰居MP的計(jì)算量和AS的計(jì)算量相比，基于改進(jìn)WAI協(xié)議的WLAN Mesh安全關(guān)聯(lián)方案中新加入的MP的計(jì)算量、n個鄰居MP的計(jì)算量和AS的計(jì)算量越來越小。

3 可信計(jì)算環(huán)境下的 WLAN Mesh安全關(guān)聯(lián)方案

可信計(jì)算環(huán)境下的WLAN Mesh安全關(guān)聯(lián)方案如圖2所示。

圖2 可信計(jì)算環(huán)境下的WLAN Mesh安全關(guān)聯(lián)方案

圖2所示的可信環(huán)境下的WLAN Mesh安全關(guān)聯(lián)方案與圖1所示的基于改進(jìn)WAI協(xié)議的WLAN Mesh安全關(guān)聯(lián)方案的區(qū)別主要體現(xiàn)于證書鑒別過程′，它是對圖 1中的證書鑒別過程′的改進(jìn)。由于證書鑒別過程′引入了平臺認(rèn)證，所以證書鑒別過程′中的認(rèn)證包含用戶認(rèn)證和平臺認(rèn)證，從而對證書鑒別過程′的形式化描述與上述證書鑒別過程′有所區(qū)別。

證書鑒別過程′的具體步驟如下(由于σα中綁定BK，所以步驟3)中需要傳輸y·P且NAP=NAP,2)：

其中，a為STA的用戶，α為STA的平臺，b為AP的用戶，β為AP的平臺，IDa和IDb分別為a和b的身份標(biāo)識，Certa和Certb分別為a和b的證書，PCRα和PCRβ分別為α和β的平臺配置寄存器(PCR，platform configuration register)值，SMLα和SMLβ分別為α和β的存儲度量日志(SML，stored measurement log)[3]，Cert(A IKpk,α)和Cert(A IKpk,β)分別為α和β的平臺身份證明密鑰(AIK，attestation identity key)證書[3]，AIKpk,α和AIKpk,β分別為α和β的AIK公鑰， kSTA,AS為STA和AS之間建立的平臺配置保護(hù)密鑰，kAP,AS為AP和AS之間建立的平臺配置保護(hù)密鑰，σa,2為a的簽名且σa,2=[x·P]ska，ska為a的私鑰，ResAS=NAP,2||NSTA||Certa||Certb||Rea||Reb||PCRα||Cert(A IKpk,α)||ReAIK,α||ReINT,α||PCRβ||Cert(A IKpk,β)||ReAIK,β||ReINT,β，Rea和Reb分別為Certa和Certb的證書驗(yàn)證結(jié)果，ReAIK,α和ReAIK,β分別為Cert(A IKpk,α)和Cert(A IKpk,β)的AIK證書驗(yàn)證結(jié)果，SMLα和SMLβ的正確性分別為PCRα和PCRβ所驗(yàn)證，ReINT,α和ReINT,β分別為SMLα和SMLβ的平臺完整性評估結(jié)果，σα為α的AIK簽名且σα=[HMAC(B K,NAP),PCRα]AIKsk,α，σβ為β的AIK簽名且σβ=[HMAC(B K,NSTA),PCRβ]AIKsk,β，σα,2為α的AIK簽名且σα,2=[HMAC(MK,NAS),PCRα]AIKsk,α，BK為STA和AP之間建立的基密鑰且BK=HKD(xyP,NSTA||NAP,2)，MK||kSTA,AS=HKD(x zP,AIKsk,α和AIKsk,β分別為α和β的 AIK私鑰，MACa,2為a的消息鑒別碼且MACa,2=HMAC(MK,NAS||z·P||σAS,2||NSTA||Certa||x·P||σa,2)，MACAS為AS的消息鑒別碼且MACAS=HMAC(MK ,NAS||z·P||σAS,2||NSTA||Certa||x·P||σa,2||MACa,2||NAP||y·P|| ResAS||σAS)，σa為a的簽名且σa=[NAP||NSTA||x·P||IDAP||Certa||ECDHparams||IDAS||σa,2||MACa,2||y·P||PCRα||{SMLα}kSTA,AS||Cert(A IKpk,α)||σα||σα,2]ska，σb為b的簽名且σb=[NSTA||NAP,2||Reaccess||x·P||y·P|| IDb||IDa||ResAS||σAS||MACAS||PCRβ||Cert(AIKpk,β)||σβ]skb，skb為b的私鑰。MACa為a的消息鑒別碼且MACa=HMAC(B K,NAP||NSTA||x·P||IDAP||Certa||ECDHparams||IDAS||σa,2||MACa,2||y·P||PCRα||{SMLα}kSTA,AS||Cert(A IKpk,α)||σα||σα,2||σa)。MACb為b的消息鑒別碼且MACb=HMAC(B K,NSTA||NAP,2||Reaccess||x·P|| y·P||IDb||IDa||ResAS||σAS||MACAS||PCRβ||Cert(A IKpk,β)||σβ||σb)。

相對于上述證書鑒別過程′和證書鑒別過程′中帶單下劃線的消息和字段是新增加的，而帶雙下劃線的字段做了相應(yīng)的擴(kuò)展，目的是在BK的建立過程中引入了STA和AP之間的雙向平臺認(rèn)證，以及在MK的建立過程中引入了AS對STA的平臺認(rèn)證，從而確保BK和MK的建立過程沒有受到各個平臺的惡意攻擊。此外，對STA的平臺認(rèn)證，可以有效地防止病毒、木馬等通過 STA的平臺帶入 WLAN Mesh網(wǎng)絡(luò)。值得注意的是：STA和AS在導(dǎo)出MK時還導(dǎo)出了它們之間的平臺配置保護(hù)密鑰 kSTA,AS，用于保護(hù)平臺認(rèn)證過程中的SML。由于證書鑒別過程′只是新增加了一些消息和字段，以及擴(kuò)展了一些字段，所以它與證書鑒別過程′向后兼容，從而也與第3版WAI協(xié)議中的證書鑒別過程向后兼容。

4 安全性分析

由于第3版WAI協(xié)議已經(jīng)被證明是安全的[11,12]，所以對基于改進(jìn)WAI協(xié)議的WLAN Mesh安全關(guān)聯(lián)方案和可信計(jì)算環(huán)境下的WLAN Mesh安全關(guān)聯(lián)方案的安全性分析主要是對2個方案中的證書鑒別過程′和證書鑒別過程′進(jìn)行安全性分析。下面利用利用串空間模型[13～15]來分析這2個方案中的證書鑒別過程′和證書鑒別過程′的安全性。

4.1 證書鑒別過程′的安全性分析

定義1 證書鑒別過程′的串空間是以下4類串的并集：1)發(fā)起者串 s∈Init[S TA,A P,A S,NSTA,NAP,NAP,2,NAS,x·P,y·P,z·P,CertSTA,CertAP,ReSTA,ReAP,ECDHparams,Reaccess]，跡為＜+m1,-m2,+m3,-m4,+m5,-m6,+m7＞，與這類串相關(guān)聯(lián)的主體為AP；2)響應(yīng)者串s∈Resp[S TA,A P,A S,NSTA,NAP,NAP,2,NAS,x·P,y·P,z·P,CertSTA,CertAP,ReSTA,ReAP,ECDHparams,Reaccess]，跡為＜-m3,+m4,-m7＞，與類串相關(guān)聯(lián)的主體為STA；3)服務(wù)者串 s∈Serv[S TA,AP,A S,NSTA,NAP,NAP,2,NAS,x·P,y·P,z·P,CertSTA,CertAP,ReSTA,ReAP,ECDHparams]；4)入侵者串s∈P。m1，m2，m3，m4，m5，m6和 m7分別為證書鑒別過程′中7個步驟中所發(fā)送的消息。

定理1 假設(shè)如下。1)∑為證書鑒別過程′的串空間，C為∑中含有一個發(fā)起者串s的叢，發(fā)起者串s的跡為：s∈Init[S TA,A P,A S,NSTA,NAP,NAP,2,NAS,x·P,y·P,z·P,CertSTA,CertAP,ReSTA,ReAP,ECDHparams,Reaccess]。2)skSTA,skAP,skAS? KP。3)x·P、y·P和z·P唯一產(chǎn)生于∑中，且x·P≠y·P≠z·P。那么C中存在一個響應(yīng)者串 t∈Resp[S TA,A P,AS,NSTA,NAP,NAP,2,NAS,x·P,y·P,z·P,CertSTA,CertAP,ReSTA,ReAP,ECDHparams,Reaccess]和一個服務(wù)者串r∈Serv[STA,AP,A S,NSTA,NAP,NAP,2,NAS,x·P,y·P,z·P,CertSTA,CertAP,ReSTA,ReAP,ECDHparams]。

證明 由定義1、假設(shè) 2）和假設(shè) 3）可知，σSTA?term(＜s,4＞)唯一源發(fā)于一個響應(yīng)者串t∈Resp[S TA,A P,A S,NSTA,NAP,NAP,2',NAS,x·P,y'·P,z·P,CertSTA,CertAP,ReSTA',ReAP',ECDHparams,Reaccess']。由定義1、假設(shè)2）和假設(shè)3）可知，σAP?term(＜t,3＞)唯一源發(fā)于一個發(fā)起者串s'∈Init[S TA,A P,AS,NSTA,NAP,NAP,2',NAS,x·P,y'·P,z·P,CertSTA,CertAP,ReSTA',ReAP',ECDHparams,Reaccess']。由假設(shè)3）可知，s'=s，所以NAP,2'=NAP,2，y'=y，ReSTA'=ReSTA，ReAP'=ReAP和Reaccess'=Reaccess。

由定義1、假設(shè) 2）和假設(shè) 3）可知，σAS,2?term(＜t,1＞)唯一源發(fā)于一個服務(wù)者串r，從而根據(jù)假設(shè)3）可知，z·P唯一產(chǎn)生于＜r,2＞。由定義1和假設(shè)3）可知，x·P唯一產(chǎn)生于＜t,2＞。因?yàn)槎x1所述的證書鑒別過程′滿足沉默性(silent)和保守性(conservative)，所以x·z·P 不源發(fā)于C 中(文獻(xiàn)[14]中的定理9)，從而MK?KP，使得MACAS?term(＜t,3＞)唯一源發(fā)于服務(wù)者串r∈Serv[S TA,AP,A S,NSTA,NAP,NAP,2,NAS,x·P,y·P,z·P,CertSTA,CertAP,ReSTA,ReAP,ECDHparams]。

定理2 假設(shè)如下。1)∑為證書鑒別過程′的串空間，C為∑中含有一個響應(yīng)者串s的叢，響應(yīng)者串s的跡為s∈Resp[S TA,A P,A S,NSTA,NAP,NAP,2,NAS,x·P,y·P,z·P,CertSTA,CertAP,ReSTA,ReAP,ECDHparams,Reaccess]。2)skAP,skAS? KP。3)x·P 、y·P 和 z·P唯一產(chǎn)生于∑中，且x·P≠y·P≠z·P 。那么C中存在一個發(fā)起者串 t∈Init[S TA,A P,A S,NSTA,NAP,NAP,2,NAS,x·P,y·P,z·P,CertSTA,CertAP,ReSTA,ReAP,ECDHparams,Reaccess]和一個服務(wù)者串r∈Serv[S TA,AP,AS,NSTA,NAP,NAP,2,NAS,x·P,y·P,z·P,CertSTA,CertAP,ReSTA,ReAP,ECDHparams]。

證明 由定義1、假設(shè) 2）和假設(shè) 3）可知，σAP?term(＜s,3＞)唯一源發(fā)于一個發(fā)起者串t∈Init[S TA,A P,A S,NSTA,NAP,NAP,2,NAS,x·P,y·P,z·P,CertSTA,CertAP,ReSTA,ReAP,ECDHparams,Reaccess]。由于C中包含一個發(fā)起者串t，所以C中包含一個服務(wù)者串r∈Serv[S TA,A P,A S,NSTA,NAP,NAP,2,NAS,x·P,y·P,z·P,CertSTA,CertAP,ReSTA,ReAP,ECDHparams]，與定理1的證明同理。

定理3 假設(shè)如下。1)∑為證書鑒別過程′的串空間，C為∑中含有一個服務(wù)者串s的叢，服務(wù)者串s的跡 為s∈Serv[S TA,A P,A S,NSTA,NAP,NAP,2,NAS,x·P,y·P,z·P,CertSTA,CertAP,ReSTA,ReAP,ECDHparams]。2)skSTA,skAP,skAS? KP。3)x·P、y·P 和z·P 唯一產(chǎn)生于∑中，且x·P≠y·P≠z·P 。那么C中存在一個發(fā)起者串r∈Init[S TA,A P,A S,NSTA,NAP,NAP,2,NAS,x·P,y·P,z·P,CertSTA,CertAP,ReSTA,ReAP,ECDHparams,Reaccess]和一個響應(yīng)者串t∈Resp[S TA,AP,AS,NSTA,NAP,NAP,2,NAS,x·P,y·P,z·P,CertSTA,CertAP,ReSTA,ReAP,ECDHparams,Reaccess]。

證明 由定義1、假設(shè)2）和假設(shè)3）可知，σSTA,2?term(＜s,3＞)唯一源發(fā)于一個響應(yīng)者串t，從而由假設(shè)3）可知，x·P唯一產(chǎn)生于＜t,2＞。由假設(shè)1）和假設(shè)3）可知，z·P唯一產(chǎn)生于＜s,2＞。因?yàn)槎x1所述的證書鑒別過程′滿足沉默性和保守性，所以x·z·P不源發(fā)于C中(文獻(xiàn)[14]中的定理9)，從而MK?KP，使得 MACSTA?term(＜s ,3＞)唯一源發(fā)于響應(yīng)者t∈Resp[S TA,A P,A S,NSTA,NA′P,N′AP,2,NAS,x·P,y'·P,z·P,CertSTA,CertAP,,ECDHparams,。同理，MACAS?term(＜t ,3＞)唯一源發(fā)于一個服務(wù)者串s'∈Serv[S TA,A P,A S,NSTA,NAP',NAP,2',NAS,x·P,y '· P,z·P,CertSTA,CertAP,ReSTA',ReAP',ECDHparams]。由假設(shè)3）可知，s'=s，所以NAP'=NAP，NAP,2'=NAP,2，y'=y，ReSTA'=ReSTA和ReAP'=ReAP，進(jìn)而由定義1可知，Reaccess'=Reaccess。由于C中包含一個響應(yīng)者串t，所以C中包含一個發(fā)起者串r∈Init[S TA,AP,AS,NSTA,NAP,NAP,2,NAS,x·P,y·P,z·P,CertSTA,CertAP,ReSTA,ReAP,ECDHparams,Reaccess]，與定理2的證明同理。

由定理1、假設(shè)2）和假設(shè)3）可知，證書鑒別過程′是安全的，使得：1)STA和AP實(shí)現(xiàn)了它們之間的雙向認(rèn)證，并建立了它們之間的基密鑰 BK，其中它們實(shí)現(xiàn)了對AS的認(rèn)證并從AS獲得了對對方的證書驗(yàn)證結(jié)果；2)STA和AS實(shí)現(xiàn)了它們之間的雙向認(rèn)證，并建立了它們之間的主密鑰MK。

4.2 證書鑒別過程′的安全性分析

由于證書鑒別過程′引入了平臺認(rèn)證，所以需要利用文獻(xiàn)[15]中所述的針對于可信網(wǎng)絡(luò)接入?yún)f(xié)議的串空間模型來分析證書鑒別過程′的安全性。為了分析可信網(wǎng)絡(luò)接入?yún)f(xié)議的安全性，文獻(xiàn)[15]引入了雙身份協(xié)議主體、內(nèi)部攻擊者和外部攻擊者的定義，并給出了針對于平臺認(rèn)證的定理。雙身份協(xié)議主體是指具有2個可認(rèn)證身份的協(xié)議主體。內(nèi)部攻擊者是指在一輪協(xié)議中進(jìn)行內(nèi)部攻擊的合法協(xié)議主體，它是因雙身份協(xié)議主體而存在的，其密鑰集用Kip表示。外部攻擊者是指除內(nèi)部攻擊者以外的攻擊者，其密鑰集用Kep表示。針對于平臺認(rèn)證的定理是指：對于一個平臺的完整性報告[16]，如果該完整性報告顯示該平臺是可信賴的，那么該完整性報告必然源發(fā)于一個常規(guī)者串。下面利用這些定義和定理對證書鑒別過程′進(jìn)行安全性分析。

定義2 證書鑒別過程′的串空間是以下4類串的并集：1)發(fā)起者串 s∈Init[a·α,b·β,AS,NSTA,NAP,NAP,2,NAS,x·P,y·P,z·P,Certa,Certb,Rea,Reb,ECDHparams,Reaccess,Cert(A IKpk,α),Cert(A IKpk,β),ReAIK,α,ReAIK,β,PCRα,PCRβ,S MLα,S MLβ,ReINT,α,ReINT,β]，跡為＜+m1,-m2,+m3,-m4,+m5,-m6,+m7＞，與這類串相關(guān)聯(lián)的主體為AP，它是一個雙身份協(xié)議主體，用b·β表示，前者表示AP的用戶，后者表示 AP的平臺；2)響應(yīng)者串s∈Resp[a·α,b·β,AS,NSTA,NAP,NAP,2,NAS,x·P,y·P,z·P,Certa,Certb,Rea,Reb,ECDHparams,Reaccess,Cert(A IKpk,α),Cert(A IKpk,β),ReAIK,α,ReAIK,β,PCRα,PCRβ,S MLα,S MLβ,ReINT,α,ReINT,β]，跡為＜-m3,+m4,-m7＞，與類串相關(guān)聯(lián)的主體為STA，它是一個雙身份協(xié)議主體，用a·α表示，前者表示STA的用戶，后者表示STA的平臺；3)服務(wù)者串 s∈Serv[a·α,b·β,A S,NSTA,NAP,NAP,2,NAS,x·P,y·P,z·P,Certa,Certb,Rea,Reb,ECDHparams,Cert(A IKpk,α),Cert(A IKpk,β),ReAIK,α,ReAIK,β,PCRα,PCRβ,S MLα,SMLβ,ReINT,α,ReINT,β]；4)入侵者串s∈P 。m1，m2，m3，m4，m5，m6和 m7分別為證書鑒別過程′中7個步驟中所發(fā)送的消息。SMLα顯示α是可信賴的，而SMLβ顯示β是可信賴的。

定理4 假設(shè)如下。1)∑為證書鑒別過程′的串空間，C為∑中含有一個發(fā)起者串s的叢，發(fā)起者串s的跡為s∈Init[a·α,b·β,A S,NSTA,NAP,NAP,2,NAS,x·P,y·P,z·P,Certa,Certb,Rea,Reb,ECDHparams,Reaccess,Cert(A IKpk,α),Cert(A IKpk,β),ReAIK,α,ReAIK,β,PCRα,PCRβ,S MLα,S MLβ,ReINT,α,ReINT,β]。2)ska?Kep且skAS? KP。3)x·P、y·P和z·P唯一產(chǎn)生于∑中，且x·P≠y·P≠z·P 。那么C中存在一個響應(yīng)者串t∈Resp[a·α,b·β,A S,NSTA,NAP,NAP,2,NAS,x·P,y·P,z·P,Certa,Certb,Rea,Reb,ECDHparams,Reaccess,Cert(A IKpk,α),Cert(A IKpk,β),ReAIK,α,ReAIK,β,PCRα,PCRβ,S MLα,S MLβ,ReINT,α,ReINT,β]和一個服務(wù)者串r∈Serv[a·α,b·β,A S,NSTA,NAP,NAP,2,NAS,x·P,y·P,z·P,Certa,Certb,Rea,Reb,ECDHparams,Cert(A IKpk,α),Cert(A IKpk,β),ReAIK,α,ReAIK,β,PCRα,PCRβ,S MLα,SMLβ,ReINT,α,ReINT,β]。

證明 1)如果ska?Kip，那么由假設(shè)2）可知，ska?KP。由定義2和假設(shè)3）可知，σa?term(＜s,4＞)唯一源發(fā)于一個響應(yīng)者串t，從而根據(jù)假設(shè)3）可知：x·P唯一產(chǎn)生于＜t,2＞。由假設(shè)1）和假設(shè)3）可知，y·P唯一產(chǎn)生于＜s,3＞。因?yàn)槎x2所述證書鑒別過程′滿足沉默性和保守性，所以x·y·P不源發(fā)于C中(文獻(xiàn)[14]中的定理9)，從而BK?KP，使得MACa?term(＜s ,3＞)源發(fā)于響應(yīng)者串t∈Resp[a·α,b·β',A S,NSTA,NAP,NAP,2',NAS,x·P,y'· P,z·P,Certa,Certb,Rea',Reb',ECDHparams,Reaccess',Cert(A IKpk,α),Cert(A IKpk,β)',ReAIK,α',ReAIK,β',PCRα,PCRβ',S MLα,S MLβ',ReINT,α',ReINT,β']。同理，MACb?term(＜t ,3＞)唯一源發(fā)于一個 發(fā)起者串s'∈Init[a·α,b·β',A S,NSTA,NAP,NAP,2',NAS,x·P,y'·P,z·P,Certa,Certb,Rea',Reb',ECDHparams,Reaccess',Cert(A IKpk,α),Cert(A IKpk,β)',ReAIK,α',ReAIK,β',PCRα,PCRβ',S MLα,S MLβ',ReINT,α',ReINT,β']。由假設(shè) 3）可知，s'=s，所以β'=β，NAP,2'=NAP,2，y'=y，ReSTA'=ReSTA，ReAP'=ReAP，Reaccess'=Reaccess，Cert(A IKpk,β)'=Cert(A IKpk,β)，ReAIK,α'=ReAIK,α，ReAIK,β'=ReAIK,β，PCRβ'=PCRβ，SMLβ'=SMLβ，ReINT,α'=ReINT,α和ReINT,β'=ReINT,β。2)如果ska∈Kip，那么由定義2和假設(shè) 3）可知，σα?term(＜s,4＞)唯一源發(fā)于一個響應(yīng)者串t' (文獻(xiàn)[15]中的定理1)，從而x·P唯一產(chǎn)生于＜t',2＞。由假設(shè)1）和假設(shè)3）可知，y·P唯一產(chǎn)生于＜s,3＞。因?yàn)槎x2所述的證書鑒別過程′滿足沉默性和保守性，所以x·y·P不源發(fā)于C中(文獻(xiàn)[14]中的定理9)，從而BK?KP。因此，由1)的證明可知，t'=t。

由定義2、假設(shè) 2）和假設(shè) 3）可知，σAS,2?term(＜t,1＞)唯一源發(fā)于一個服務(wù)者串r，從而根據(jù)假設(shè)3）可知，z·P唯一產(chǎn)生于＜r,2＞。因?yàn)槎x2所述的證書鑒別過程′滿足沉默性和保守性，所以x·z·P 不源發(fā)于C 中(文獻(xiàn)[14]中的定理9)，從而MK?KP，使得 MACAS?term(＜t ,3＞)唯一源發(fā)于服務(wù)者串r∈Serv[a·α,b·β,A S,NSTA,NAP,NAP,2,NAS,x·P,y·P,z·P,Certa,Certb,Rea,Reb,ECDHparams,Cert(A IKpk,α),Cert(A IKpk,β),ReAIK,α,ReAIK,β,PCRα,PCRβ,S MLα,SMLβ,ReINT,α,ReINT,β]。

定理5 假設(shè)如下。1)∑為證書鑒別過程′的串空間，C為∑中含有一個響應(yīng)者串s的叢，響應(yīng)者串s的跡 為s∈Resp[a·α,b·β,A S,NSTA,NAP,NAP,2,NAS,x·P,y·P,z·P,Certa,Certb,Rea,Reb,ECDHparams,Reaccess,Cert(A IKpk,α),Cert(A IKpk,β),ReAIK,α,ReAIK,β,PCRα,PCRβ,S MLα,S MLβ,ReINT,α,ReINT,β]。2)skb?Kep且skAS? KP。3)x·P、y·P和z·P唯一產(chǎn)生于∑中，且x·P≠y·P≠z·P 。那么C中存在一個發(fā)起者串t∈Init[a·α,b·β,A S,NSTA,NAP,NAP,2,NAS,x·P,y·P,z·P,Certa,Certb,Rea,Reb,ECDHparams,Reaccess,Cert(A IKpk,α),Cert(A IKpk,β),ReAIK,α,ReAIK,β,PCRα,PCRβ,S MLα,S MLβ,ReINT,α,ReINT,β]和一個服務(wù)者串r∈Serv[a·α,b·β,A S,NSTA,NAP,NAP,2,NAS,x·P,y·P,z·P,Certa,Certb,Rea,Reb,ECDHparams,Cert(A IKpk,α),Cert(A IKpk,β),ReAIK,α,ReAIK,β,PCRα,PCRβ,S MLα,SMLβ,ReINT,α,ReINT,β]。

證明 1)如果skb?Kip，那么由假設(shè)2）可知，skb?KP。由定義2和假設(shè)3）可知，σAP?term(＜s,3＞)源發(fā)于一個發(fā)起者串t∈Init[a·α,b·β,AS,NSTA,NAP,NAP,2,NAS,x·P,y·P,z·P,Certa,Certb,Rea,Reb,ECDHparams,Reaccess,Cert(A IKpk,α),Cert(A IKpk,β),ReAIK,α,ReAIK,β,PCRα,PCRβ,S MLα,S MLβ,ReINT,α,ReINT,β]。2)如果skb∈Kip，那么由定義2和假設(shè)3）可知，σβ?term(＜s,3＞)唯一源發(fā)于一個發(fā)起串t'(文獻(xiàn)[15]中的定理1)，從而 y·P唯一產(chǎn)生于＜t',3＞。由假設(shè)1）和假設(shè)3）可知，x·P唯一產(chǎn)生于＜s,2＞。因?yàn)槎x2所述的證書鑒別過程′滿足沉默性和保守性，所以x·y·P不源發(fā)于C中(文獻(xiàn)[14]中的定理9)，從而BK?KP，使得MACb?term(＜s,3＞)源發(fā)于發(fā)起者串 t'=t∈Init[a·α,b·β,A S,NSTA,NAP,NAP,2,NAS,x·P,y·P,z·P,Certa,Certb,Rea,Reb,ECDHparams,Reaccess,Cert(A IKpk,α),Cert(A IKpk,β),ReAIK,α,ReAIK,β,PCRα,PCRβ,SMLα,S MLβ,ReINT,α,ReINT,β]。

由于C中包含一個發(fā)起者串t，所以C中包含一個服務(wù)者串r∈Serv[a·α,b·β,A S,NSTA,NAP,NAP,2,NAS,x·P,y·P,z·P,Certa,Certb,Rea,Reb,ECDHparams,Cert(A IKpk,α),Cert(A IKpk,β),ReAIK,α,ReAIK,β,PCRα,PCRβ,S MLα,S MLβ,ReINT,α,ReINT,β]，與定理4的證明同理。

定理6 假設(shè)如下。1)∑為證書鑒別過程′的串空間，C為∑中含有一個服務(wù)者串s的叢，服務(wù)者串s的跡 為：s∈S erv[a·α,b·β,A S,NSTA,NAP,NAP,2,NAS,x·P,y·P,z·P,Certa,Certb,Rea,Reb,ECDHparams,Cert(A IKpk,α),ReAIK,β,PCRα,PCRβ,S MLα,Cert(A IKpk,β),ReAIK,α,SMLβ,ReINT,α,ReINT,β]。2)ska?Kep且skb? Kep。3)x·P、y·P 和z·P 唯一產(chǎn)生于∑ 中，且x·P≠y·P≠z·P。那么C中存在一個發(fā)起者串t∈Init[a·α,b·β,A S,NSTA,NAP,NAP,2,NAS,x·P,y·P,z·P,Certa,Certb,Rea,Reb,ECDHparams,Reaccess,Cert(A IKpk,α),Cert(A IKpk,β),ReAIK,α,ReAIK,β,PCRα,PCRβ,S MLα,S MLβ,ReINT,α,ReINT,β]和一個響應(yīng)者串r∈Resp[a·α,b·β,A S,NSTA,NAP,NAP,2,NAS,x·P,y·P,z·P,Certa,Certb,Rea,Reb,ECDHparams,Reaccess,Cert(A IKpk,α),Cert(A IKpk,β),ReAIK,α,ReAIK,β,PCRα,PCRβ,S MLα,S MLβ,ReINT,α,ReINT,β]。

證明 1)如果ska?Kip，那么由假設(shè)2）可知，ska?KP。由定義2和假設(shè)3）可知，σa,2?term(＜s,3＞)唯一源發(fā)于一個響應(yīng)者串r，從而根據(jù)假設(shè)3）可知，x·P唯一產(chǎn)生于＜r,2＞。由假設(shè)1）和假設(shè)3）可知，z·P唯一產(chǎn)生于＜s,2＞。因?yàn)槎x2所述的證書鑒別過程′滿足沉默性和保守性，所以x·z·P不源發(fā)于C中(文獻(xiàn)[14]中的定理9)，從而MK? KP，使得 MACa,2?term(＜s,3＞)源發(fā)于響應(yīng)者串r∈Resp[a·α',b· β',A S,NSTA,NAP',NAP,2',NAS,x·P,y '·P,z·P,Certa,Certb,Rea',Reb',ECDHparams,Reaccess',Cert(A IKpk,α)',Cert(A IKpk,β)',ReAIK,α',ReAIK,β',PCRα',PCRβ',S MLα',S MLβ',ReINT,α',ReINT,β']。同理，MACAS?term(＜r ,3＞)唯一源發(fā)于一個服務(wù)者串s'∈Serv[a·α',b· β',A S,NSTA,NAP',NAP,2',NAS,x·P,y'·P,z·P,Certa,Certb,Rea',Reb',ECDHparams,Cert(A IKpk,α)',Cert(A IKpk,β)',ReAIK,α',ReAIK,β',PCRα',PCRβ',S MLα',SMLβ',ReINT,α',ReINT,β']。由假設(shè)3）可知，s'=s，所以 NAP'=NAP，NAP,2'=NAP,2，y'=y，Rea'=Rea，Reb'=Reb，α'=α，β'=β，Cert(A IKpk,α)'=Cert(A IKpk,α)，ReAIK,α'=ReAIK,α，Cert(A IKpk,β)'=Cert(A IKpk,β)，ReAIK,β'=ReAIK,β，PCRα'=PCRα，PCRβ'=PCRβ，SMLα'=SMLα，SMLβ'=SMLβ，ReINT,α'=ReINT,α和ReINT,β'=ReINT,β，進(jìn)而由定義2可知，Reaccess'=Reaccess。2)如果ska∈Kip，那么由定義2和假設(shè) 3）可知，σα,2?term(＜s,4＞)唯一源發(fā)于一個響應(yīng)者串r'(文獻(xiàn)[15]中的定理1)，從而x·P唯一產(chǎn)生于＜r',2＞。由假設(shè)1）和假設(shè)3）可知，z·P唯一產(chǎn)生于＜s,2＞。因?yàn)槎x2所述的證書鑒別過程′滿足沉默性和保守性，所以x·z·P不源發(fā)于C中(文獻(xiàn)[14]中的定理9)，從而MK?KP。因此，由 1)的證明可知，r'=r。

由于C中包含一個響應(yīng)者串r，所以C中包含一個發(fā)起者串 t∈Init[a·α,b·β,A S,NSTA,NAP,NAP,2,NAS,x·P,y·P,z·P,Certa,Certb,Rea,Reb,ECDHparams,Reaccess,Cert(A IKpk,α),Cert(A IKpk,β),ReAIK,α,ReAIK,β,PCRα,PCRβ,S MLα,S MLβ,ReINT,α,ReINT,β]，與定理5的證明同理。

由定理4～定理6可知，證書鑒別過程′可以抵抗內(nèi)部攻擊者和外部攻擊者的攻擊，它是安全的，使得1)STA和AP實(shí)現(xiàn)了它們之間的雙向用戶認(rèn)證和平臺認(rèn)證，并建立了它們之間的基密鑰 BK，其中它們實(shí)現(xiàn)了對AS的認(rèn)證并從AS獲得了對對方的用戶證書驗(yàn)證結(jié)果、AIK證書驗(yàn)證結(jié)果和平臺完整性評估結(jié)果；2)STA和AS實(shí)現(xiàn)了它們之間的雙向用戶認(rèn)證，以及AS對STA的平臺認(rèn)證，并建立了它們之間的主密鑰MK和平臺配置保護(hù)密鑰kSTA,AS。

5 結(jié)束語

通過對第3版WAI協(xié)議的改進(jìn)，本文提出了一種基于改進(jìn)WAI協(xié)議的WLAN Mesh安全關(guān)聯(lián)方案 。然后，在該方案的基礎(chǔ)上，通過對第3版WAI協(xié)議的進(jìn)一步改進(jìn)，本文提出了一種可信計(jì)算環(huán)境下的WLAN Mesh安全關(guān)聯(lián)方案，它能實(shí)現(xiàn)WLAN Mesh可信接入認(rèn)證，從而增強(qiáng)了WLAN Mesh的安全性。通過性能對比分析，基于改進(jìn)WAI協(xié)議的WLAN Mesh安全關(guān)聯(lián)方案在通信效率和計(jì)算量上都具有明顯的優(yōu)勢，從而提高了WLAN Mesh安全關(guān)聯(lián)的性能，特別是降低了AS的負(fù)載，有效地解決了第3版WAI協(xié)議用于建立WLAN Mesh安全關(guān)聯(lián)時所存在的問題。最后，利用串空間模型證明了這2個WLAN Mesh安全關(guān)聯(lián)方案是安全的。

[1]IEEE Supplement to Standard for Information Technology - Telecommunications and Information Exchange Between Systems -LAN/MAN Specific Requirements - Part 11: Wireless LAN Medium Access Control (MAC)and Physical Layer (PHY)Specifications:Specification for Enhanced Security[S]. IEEE 802.11i,2004.

[2]IEEE Draft Amendment to Standard for Information Technology–Telecommunications and Information Exchange Between Systems -LAN/MAN Specific Requirements - Part 11: Wireless LAN Medium Access Control (MAC)and Physical Layer (PHY)Specifications:Amendment to ESS Mesh Networking[S]. IEEE P802.11s/D1.0,2007.

[3]Trusted computing group. TCG trusted network connect architecture for interoperability specification version 1.4[EB/OL]. http://www.trustedcomputinggroup.org/.

[4]馬卓，馬建峰，曾勇等. 通用可組合安全的WLAN Mesh網(wǎng)絡(luò)可信接入認(rèn)證協(xié)議[J]. 通信學(xué)報，2008，29(10):126-134.MA Z,MA J F,ZHENG Y,et al. Universally composable secure trusted access protocol for WLAN Mesh networks[J]. Journal on Communications,2008,29(10):126-134.

[5]MA Z,MA J F,SHEN Y L. Provably secure trusted access protocol for WLAN Mesh networks[A]. 2008 IEEE 5th International Conference on Embedded and Ubiquitous Computing[C]. Shanghai,China,2008.43-48.

[6]MA Z,MA J F,SHEN Y L. An efficient authentication protocol for WLAN Mesh networks in trusted environment[J]. IEICE Transactions on Information and Systems,2010,E93-D(3): 430-437.

[7]中華人民共和國國家標(biāo)準(zhǔn). GB 15629.11-2003（信息技術(shù) 系統(tǒng)間遠(yuǎn)程通信和信息交換 局域網(wǎng)和城域網(wǎng) 特定要求 第11部分：無線局域網(wǎng)媒體訪問控制和物理層規(guī)范）[S]. 北京：中國標(biāo)準(zhǔn)出版社，2003.National Standard of the People’s Republic of China. GB 15629.11-2003(Information Technology - Telecommunications and Information Exchange Between Systems-LAN/MAN Specific Requirements-Part 11: Wireless LAN Medium Access Control (MAC)and Physical Layer (PHY)Specifications)[S]. Beijing: Chinese Standard Publishing House,2003.

[8]中國寬帶無線IP標(biāo)準(zhǔn)工作組. GB 15629.11-2003（信息技術(shù) 系統(tǒng)間遠(yuǎn)程通信和信息交換 局域網(wǎng)和城域網(wǎng) 特定要求 第11 部分：無線局域網(wǎng)媒體訪問控制和物理層規(guī)范）和GB 15629.1102-2003（信息技術(shù) 系統(tǒng)間遠(yuǎn)程通信和信息交換 局域網(wǎng)和城域網(wǎng) 特定要求 第11部分：無線局域網(wǎng)媒體訪問控制和物理層規(guī)范：2.4 GHz頻段較高速物理層擴(kuò)展規(guī)范）實(shí)施指南[EB/OL]. http://www. chinabwips.org/.China broadband wireless ip standard group. Guide for GB 15629.11-2003(information technology-telecommunications and information exchange between systems - LAN/MAN specific requirements - part 11: wireless LAN medium access control (MAC)and physical layer (PHY)specifications)and GB 15629.1102-2003 (information technology - telecommunications and information exchange between systems - LAN/MAN specific requirements - part 11: wireless LAN medium access control (MAC)and physical layer (PHY)specifications: higher-speed physical layer extension in the 2.4 GHz band)[EB/OL]. http://www.chinabwips.org/.

[9]中華人民共和國國家標(biāo)準(zhǔn). GB 15629.11-2003/XG1-2006（信息技術(shù)系統(tǒng)間遠(yuǎn)程通信和信息交換 局域網(wǎng)和城域網(wǎng) 特定要求 第 11 部分：無線局域網(wǎng)媒體訪問控制和物理層規(guī)范，第1號修改單）[S].北京：中國標(biāo)準(zhǔn)出版社，2006.National Standard of the People’s Republic of China. GB 15629.11-2003/XG1-2006(Information Technology - Telecommunications and Information Exchange Between Systems - LAN/MAN Specific Requirements - Part 11: Wireless LAN Medium Access Control(MAC)and Physical Layer (PHY)Specifications: Amendment 1)[S].Beijing: Chinese Standard Publishing House,2006.

[10]IEEE Standard for Information Technology - Telecommunications and Information Exchange Between Systems - LAN/MAN Specific Requirements - Part 11: Wireless LAN Medium Access Control (MAC)and Physical Layer (PHY)Specifications[S]. IEEE 802.11,1999.

[11]TANG Q. On the security of three versions of the WAI protocol in Chinese WLAN implementation plan[A]. CHINACOM’07 Proceedings of the Second International Conference on Communications and Networking in China,2007 Conference[C]. Shanghai,China,2007.333-339.

[12]鐵滿霞,李建東,王育民. WAPI密鑰管理協(xié)議的PCL證明[J]. 電子與信息學(xué)報,2009,31(2):444-447.TIE M X,LI J D,WANG Y M. A correctness proof of WAPI key management protocol based on PCL[J]. Journal of Electronics & Information Technology,2009,31(2):444-447.

[13]FABREGA F J T,HERZOG J C,GUTTMAN J D. Strand spaces:proving security protocols correct[J]. Journal of Computer Security,1999,7(2/3):191-230.

[14]HERZOG J C. The Diffie-Hellman key-agreement scheme in the strand space model[A]. 2003 IEEE 16th IEEE Computer Security Foundations Workshop[C]. Pacific Grove,USA,2003.234-247.

[15]XIAO Y L,WANG Y M,PANG L J. Verification of trusted network access protocols in the strand space model[J]. IEICE Transactions on Fundamentals of Electronics,Communications and Computer Sciences,2012,E95-A(3): 665-668.

[16]SAILER R,ZHANG X L,JAEGER T,et al. Design and implementation of a TCG-based integrity measurement architecture[A]. 2004 ACM 13th USENIX Security Symposium[C]. California,USA,2004.223-238.