可信計算環(huán)境下的WLAN Mesh安全關聯方案

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

（1. 西安郵電大學 物聯網與兩化融合研究院，陜西 西安 710061；2. 西安電子科技大學 綜合業(yè)務網理論與關鍵技術國家重點實驗室，陜西 西安 710071；3.西安電子科技大學 生命科學技術學院，陜西 西安 710071）

1 引言

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

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

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

2 基于改進WAI協(xié)議的WLAN Mesh安全關聯方案

基于改進WAI協(xié)議的WLAN Mesh安全關聯方案如圖1所示。

圖1 基于改進WAI協(xié)議的WLAN Mesh安全關聯方案

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

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

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

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

2.1 證書鑒別過程′

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

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

ECDHparams為AP選擇的ECDH參數，NSTA和NAS分別為STA和AS產生的隨機數，NAP和NAP,2為AP產生的2個隨機數，x·P、y·P和z·P分別為STA、AP和AS產生的密鑰數據，IDSTA、IDAP和IDAS分別為STA、AP和AS的身份標識，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的證書驗證結果，MACSTA為STA的消息鑒別碼且MACSTA=HMAC(MK,NAS||z·P||σAS,2||NSTA||CertSTA||x·P ||σSTA,2)，HMAC()為用于生成消息鑒別碼的 Hash函數，MK=HKD(x·z·P,NSTA||NAS)，HKD()為用于擴展密鑰的Hash函數，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產生的接入結果。

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

2.2 性能對比分析

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

表1 基于WAI協(xié)議的WLAN Mesh安全關聯方案和基于改進WAI協(xié)議的安全關聯方案的性能對比

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

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

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

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

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

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

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

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

其中，a為STA的用戶，α為STA的平臺，b為AP的用戶，β為AP的平臺，IDa和IDb分別為a和b的身份標識，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之間建立的平臺配置保護密鑰，kAP,AS為AP和AS之間建立的平臺配置保護密鑰，σ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的證書驗證結果，ReAIK,α和ReAIK,β分別為Cert(A IKpk,α)和Cert(A IKpk,β)的AIK證書驗證結果，SMLα和SMLβ的正確性分別為PCRα和PCRβ所驗證，ReINT,α和ReINT,β分別為SMLα和SMLβ的平臺完整性評估結果，σα為α的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)。

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

4 安全性分析

由于第3版WAI協(xié)議已經被證明是安全的[11,12]，所以對基于改進WAI協(xié)議的WLAN Mesh安全關聯方案和可信計算環(huán)境下的WLAN Mesh安全關聯方案的安全性分析主要是對2個方案中的證書鑒別過程′和證書鑒別過程′進行安全性分析。下面利用利用串空間模型[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＞，與這類串相關聯的主體為AP；2)響應者串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＞，與類串相關聯的主體為STA；3)服務者串 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 假設如下。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唯一產生于∑中，且x·P≠y·P≠z·P。那么C中存在一個響應者串 t∈Resp[S TA,A P,AS,NSTA,NAP,NAP,2,NAS,x·P,y·P,z·P,CertSTA,CertAP,ReSTA,ReAP,ECDHparams,Reaccess]和一個服務者串r∈Serv[STA,AP,A S,NSTA,NAP,NAP,2,NAS,x·P,y·P,z·P,CertSTA,CertAP,ReSTA,ReAP,ECDHparams]。

證明 由定義1、假設 2）和假設 3）可知，σSTA?term(＜s,4＞)唯一源發(fā)于一個響應者串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、假設2）和假設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']。由假設3）可知，s'=s，所以NAP,2'=NAP,2，y'=y，ReSTA'=ReSTA，ReAP'=ReAP和Reaccess'=Reaccess。

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

定理2 假設如下。1)∑為證書鑒別過程′的串空間，C為∑中含有一個響應者串s的叢，響應者串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唯一產生于∑中，且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]和一個服務者串r∈Serv[S TA,AP,AS,NSTA,NAP,NAP,2,NAS,x·P,y·P,z·P,CertSTA,CertAP,ReSTA,ReAP,ECDHparams]。

證明 由定義1、假設 2）和假設 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中包含一個服務者串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 假設如下。1)∑為證書鑒別過程′的串空間，C為∑中含有一個服務者串s的叢，服務者串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 唯一產生于∑中，且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]和一個響應者串t∈Resp[S TA,AP,AS,NSTA,NAP,NAP,2,NAS,x·P,y·P,z·P,CertSTA,CertAP,ReSTA,ReAP,ECDHparams,Reaccess]。

證明 由定義1、假設2）和假設3）可知，σSTA,2?term(＜s,3＞)唯一源發(fā)于一個響應者串t，從而由假設3）可知，x·P唯一產生于＜t,2＞。由假設1）和假設3）可知，z·P唯一產生于＜s,2＞。因為定義1所述的證書鑒別過程′滿足沉默性和保守性，所以x·z·P不源發(fā)于C中(文獻[14]中的定理9)，從而MK?KP，使得 MACSTA?term(＜s ,3＞)唯一源發(fā)于響應者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ā)于一個服務者串s'∈Serv[S TA,A P,A S,NSTA,NAP',NAP,2',NAS,x·P,y '· P,z·P,CertSTA,CertAP,ReSTA',ReAP',ECDHparams]。由假設3）可知，s'=s，所以NAP'=NAP，NAP,2'=NAP,2，y'=y，ReSTA'=ReSTA和ReAP'=ReAP，進而由定義1可知，Reaccess'=Reaccess。由于C中包含一個響應者串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、假設2）和假設3）可知，證書鑒別過程′是安全的，使得：1)STA和AP實現了它們之間的雙向認證，并建立了它們之間的基密鑰 BK，其中它們實現了對AS的認證并從AS獲得了對對方的證書驗證結果；2)STA和AS實現了它們之間的雙向認證，并建立了它們之間的主密鑰MK。

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

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

定義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＞，與這類串相關聯的主體為AP，它是一個雙身份協(xié)議主體，用b·β表示，前者表示AP的用戶，后者表示 AP的平臺；2)響應者串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＞，與類串相關聯的主體為STA，它是一個雙身份協(xié)議主體，用a·α表示，前者表示STA的用戶，后者表示STA的平臺；3)服務者串 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 假設如下。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唯一產生于∑中，且x·P≠y·P≠z·P 。那么C中存在一個響應者串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,β]和一個服務者串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，那么由假設2）可知，ska?KP。由定義2和假設3）可知，σa?term(＜s,4＞)唯一源發(fā)于一個響應者串t，從而根據假設3）可知：x·P唯一產生于＜t,2＞。由假設1）和假設3）可知，y·P唯一產生于＜s,3＞。因為定義2所述證書鑒別過程′滿足沉默性和保守性，所以x·y·P不源發(fā)于C中(文獻[14]中的定理9)，從而BK?KP，使得MACa?term(＜s ,3＞)源發(fā)于響應者串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,β']。由假設 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和假設 3）可知，σα?term(＜s,4＞)唯一源發(fā)于一個響應者串t' (文獻[15]中的定理1)，從而x·P唯一產生于＜t',2＞。由假設1）和假設3）可知，y·P唯一產生于＜s,3＞。因為定義2所述的證書鑒別過程′滿足沉默性和保守性，所以x·y·P不源發(fā)于C中(文獻[14]中的定理9)，從而BK?KP。因此，由1)的證明可知，t'=t。

由定義2、假設 2）和假設 3）可知，σAS,2?term(＜t,1＞)唯一源發(fā)于一個服務者串r，從而根據假設3）可知，z·P唯一產生于＜r,2＞。因為定義2所述的證書鑒別過程′滿足沉默性和保守性，所以x·z·P 不源發(fā)于C 中(文獻[14]中的定理9)，從而MK?KP，使得 MACAS?term(＜t ,3＞)唯一源發(fā)于服務者串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 假設如下。1)∑為證書鑒別過程′的串空間，C為∑中含有一個響應者串s的叢，響應者串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唯一產生于∑中，且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,β]和一個服務者串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，那么由假設2）可知，skb?KP。由定義2和假設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和假設3）可知，σβ?term(＜s,3＞)唯一源發(fā)于一個發(fā)起串t'(文獻[15]中的定理1)，從而 y·P唯一產生于＜t',3＞。由假設1）和假設3）可知，x·P唯一產生于＜s,2＞。因為定義2所述的證書鑒別過程′滿足沉默性和保守性，所以x·y·P不源發(fā)于C中(文獻[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中包含一個服務者串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 假設如下。1)∑為證書鑒別過程′的串空間，C為∑中含有一個服務者串s的叢，服務者串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 唯一產生于∑ 中，且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,β]和一個響應者串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，那么由假設2）可知，ska?KP。由定義2和假設3）可知，σa,2?term(＜s,3＞)唯一源發(fā)于一個響應者串r，從而根據假設3）可知，x·P唯一產生于＜r,2＞。由假設1）和假設3）可知，z·P唯一產生于＜s,2＞。因為定義2所述的證書鑒別過程′滿足沉默性和保守性，所以x·z·P不源發(fā)于C中(文獻[14]中的定理9)，從而MK? KP，使得 MACa,2?term(＜s,3＞)源發(fā)于響應者串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ā)于一個服務者串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,β']。由假設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,β，進而由定義2可知，Reaccess'=Reaccess。2)如果ska∈Kip，那么由定義2和假設 3）可知，σα,2?term(＜s,4＞)唯一源發(fā)于一個響應者串r'(文獻[15]中的定理1)，從而x·P唯一產生于＜r',2＞。由假設1）和假設3）可知，z·P唯一產生于＜s,2＞。因為定義2所述的證書鑒別過程′滿足沉默性和保守性，所以x·z·P不源發(fā)于C中(文獻[14]中的定理9)，從而MK?KP。因此，由 1)的證明可知，r'=r。

由于C中包含一個響應者串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可知，證書鑒別過程′可以抵抗內部攻擊者和外部攻擊者的攻擊，它是安全的，使得1)STA和AP實現了它們之間的雙向用戶認證和平臺認證，并建立了它們之間的基密鑰 BK，其中它們實現了對AS的認證并從AS獲得了對對方的用戶證書驗證結果、AIK證書驗證結果和平臺完整性評估結果；2)STA和AS實現了它們之間的雙向用戶認證，以及AS對STA的平臺認證，并建立了它們之間的主密鑰MK和平臺配置保護密鑰kSTA,AS。

5 結束語

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

[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網絡可信接入認證協(xié)議[J]. 通信學報，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]中華人民共和國國家標準. GB 15629.11-2003（信息技術 系統(tǒng)間遠程通信和信息交換 局域網和城域網 特定要求 第11部分：無線局域網媒體訪問控制和物理層規(guī)范）[S]. 北京：中國標準出版社，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標準工作組. GB 15629.11-2003（信息技術 系統(tǒng)間遠程通信和信息交換 局域網和城域網 特定要求 第11 部分：無線局域網媒體訪問控制和物理層規(guī)范）和GB 15629.1102-2003（信息技術 系統(tǒng)間遠程通信和信息交換 局域網和城域網 特定要求 第11部分：無線局域網媒體訪問控制和物理層規(guī)范：2.4 GHz頻段較高速物理層擴展規(guī)范）實施指南[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]中華人民共和國國家標準. GB 15629.11-2003/XG1-2006（信息技術系統(tǒng)間遠程通信和信息交換 局域網和城域網 特定要求 第 11 部分：無線局域網媒體訪問控制和物理層規(guī)范，第1號修改單）[S].北京：中國標準出版社，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]. 電子與信息學報,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.