可信计算环境下的WLAN Mesh安全关联方案

肖跃雷，王育民，庞辽军，谭示崇

（1. 西安邮电大学 物联网与两化融合研究院，陕西 西安 710061；2. 西安电子科技大学 综合业务网理论与关键技术国家重点实验室，陕西 西安 710071；3.西安电子科技大学 生命科学技术学院，陕西 西安 710071）

1 引言

WLAN Mesh网络作为一种新型的网络结构，成为近年来国内外研究的热点问题之一。在802.11i[1]的基础上，802.11s[2]提出了 EMSA(efficient mesh security association)来建立WLAN Mesh安全关联，包括建立新加入的Mesh节点(MP,mesh point)和Mesh认证器(MA,mesh authenticator)之间的安全关联、新加入的 MP和 Mesh密钥分发器(MKD,mesh key distributor)之间的安全关联、新加入的MP和各个邻居MP之间的安全关联。WLAN Mesh安全关联主要包括4个步骤：第1个步骤是执行一个认证过程，实现对新加入的MP的认证并导出密钥，第2～3个步骤是基于第1个步骤导出的密钥建立新加入的 MP和 MA之间的安全关联、新加入的MP和MKD之间的安全关联、新加入的MP和各个邻居MP之间的安全关联。近年来，随着可信计算技术的产生和发展，使得可信计算技术不仅可以建立终端的可信计算环境，而且可以将终端的可信计算环境扩展至网络，使网络成为一个可信计算环境，从而从源头上遏制住恶意攻击，有效解决日渐突出和复杂的网络安全问题。可信接入认证的目标就是将终端的可信计算环境扩展至网络，它包括用户认证和平台认证，其中平台认证包括平台身份认证和平台完整性验证[3]，平台身份认证可以基于可信第三方(私有 CA)或直接匿名证明 (DAA,direct anonymous attestation)机制来实现。因此， EMSA在可信计算环境下不再适用，因为它不能实现WLAN Mesh可信接入认证。也就是说，EMSA没有实现对新加入的MP的平台认证，从而不能构建可信计算环境 WLAN Mesh网络。可信计算环境WLAN Mesh网络是指每一个新加入的MP在接入WLAN Mesh网络之前都必须对它进行平台认证，以保证每一个新加入的MP处于可信计算环境下的安全状态，从而将每一个新加入的MP的可信计算环境扩展至整个WLAN Mesh网络。于是，马卓等提出了一些 WLAN Mesh可信接入认证协议[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由证书鉴别过程、单播密钥协商过程和组播密钥协商过程组成。虽然最新的WAI协议(即第 3版 WAI协议)被证明是安全的[11,12]，但是它用于建立 WLAN Mesh安全关联时存在以下问题：新加入的MP首先需要与MA、认证服务器(AS,authentication server)执行一次WAI证书鉴别过程和一次单播密钥协商过程来接入WLAN Mesh网络并建立新加入的MP和MA之间的安全关联，然后还需要与WLAN Mesh网络中的n个邻居MP和AS执行n次WAI证书鉴别过程和n次单播密钥协商过程来建立新加入的MP和n个邻居MP之间的安全关联，这使得WLAN Mesh安全关联的性能较差，特别是使AS的负载太重。此外，由于第3版WAI协议没有考虑平台认证，所以它不适用于建立可信计算环境下的WLAN Mesh安全关联，也就是说它不能实现WLAN Mesh可信接入认证。

为了解决上述问题，本文通过对第 3版 WAI协议的改进，提出了一种基于改进 WAI协议的WLAN Mesh安全关联方案，它提高了WLAN Mesh安全关联的性能，特别是降低了AS的负载。然后，通过对第3版WAI协议的进一步改进，在该方案的基础上提出了一种可信计算环境下的WLAN Mesh安全关联方案，它能实现WLAN Mesh可信接入认证，从而增强了WLAN Mesh的安全性。此外，本文利用串空间模型(SSM,strand space model)[13～15]证明了这2个WLAN Mesh安全关联方案是安全的。

2 基于改进WAI协议的WLAN Mesh安全关联方案

基于改进WAI协议的WLAN Mesh安全关联方案如图1所示。

图1 基于改进WAI协议的WLAN Mesh安全关联方案

在图1中，对第3版WAI协议的改进主要体现于证书鉴别过程′，它是对第3版WAI协议中的证书鉴别过程的改进。基于改进WAI协议的WLAN Mesh安全关联方案主要包括以下3个部分。

1)新加入的MP、MA和AS执行证书鉴别过程′来实现新加入的MP与MA之间的双向认证，新加入的MP与AS之间的双向认证，并建立新加入的MP与MA之间的基密钥BK，以及新加入的MP与AS之间的主密钥MK。然后，新加入的MP和MA利用 BK执行单播密钥协商过程建立它们之间的单播密钥，用于保护它们之间的链路层数据通信。

2)AS通过密钥分发消息将MK分发给MKD，其中密钥分发消息是利用AS与MKD之间预置的安全通道进行安全保护的。然后，MKD和新加入的 MP将 MK扩展为2个一级主密钥：FMK1和FMK2。最后，MKD和新加入的MP利用FMK1执行单播密钥协商过程建立它们之间的单播密钥，用于保护后来它们之间交互的密钥传输请求消息和密钥传输响应消息。

3)当新加入的MP在接入WLAN Mesh网络后要与第i个邻居MP建立安全关联时，新加入的MP将FMK2扩展为一个用于它和该邻居MP的二级主密钥SMKi，第i个邻居MP向MKD发送密钥传输请求消息，MKD收到密钥传输请求消息后将FMK2扩展为一个用于新加入的MP和该邻居MP的二级主密钥 SMKi，并通过密钥传输响应消息发送给该邻居 MP，其中密钥传输请求消息和密钥传输响应消息中是利用该邻居MP与MKD之间已建立的单播密钥进行安全保护的。然后，新加入的MP和第i个邻居MP利用SMKi执行单播密钥协商过程建立它们之间的单播密钥，用于保护它们之间的链路层数据通信。

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协议中的证书鉴别过程，证书鉴别过程′中带单下划线的消息和字段是新增加的，而带双下划线的字段做了相应的扩展，目的是实现STA和AS之间的双向认证，并建立它们之间的MK。由于证书鉴别过程′只是新增加了一些消息和字段，以及扩展了一些字段，所以它与第 3版WAI协议中的证书鉴别过程向后兼容。

2.2 性能对比分析

假设：新加入的MP通过MA接入WLAN Mesh网络并建立与MA之间的安全关联后，还需要与n个邻居MP建立安全关联。表1给出了本文引言中所述的基于WAI协议的WLAN Mesh安全关联方案和基于改进WAI协议的安全关联方案的性能对比，其中，E为模指数运算，F为计算签名，M为消息认证码。

表1 基于WAI协议的WLAN Mesh安全关联方案和基于改进WAI协议的安全关联方案的性能对比

在表1中，第1行性能参数是基于WAI协议的WLAN Mesh安全关联方案的交互消息数及相关计算量，第 2行性能参数是基于改进 WAI协议的WLAN Mesh安全关联方案的交互消息数及相关计算量。从表 1可以看出，基于改进 WAI协议的WLAN Mesh安全关联方案比本文引言中所述的基于WAI协议的WLAN Mesh安全关联方案在通信效率和计算量上都具有明显的优势，具体分析如下。

方案通信效率：当n=2时，2个方案中交互的消息数相同，但是，随着n的值增大，与本文引言中所述的基于WAI协议的WLAN Mesh安全关联方案的交互消息数相比，基于改进WAI协议的WLAN Mesh安全关联方案的交互消息数越来越少。

方案计算量：2个方案中MA的计算量相同，而基于改进WAI协议的WLAN Mesh安全关联方案中MKD的计算量比本文引言中所述的基于WAI协议的WLAN Mesh安全关联方案中MKD的计算量增加了1M，但是，随着n的值增大，与本文引言中所述的基于WAI协议的WLAN Mesh安全关联方案中新加入的MP的计算量、n个邻居MP的计算量和AS的计算量相比，基于改进WAI协议的WLAN Mesh安全关联方案中新加入的MP的计算量、n个邻居MP的计算量和AS的计算量越来越小。

3 可信计算环境下的 WLAN Mesh安全关联方案

可信计算环境下的WLAN Mesh安全关联方案如图2所示。

图2 可信计算环境下的WLAN Mesh安全关联方案

图2所示的可信环境下的WLAN Mesh安全关联方案与图1所示的基于改进WAI协议的WLAN Mesh安全关联方案的区别主要体现于证书鉴别过程′，它是对图 1中的证书鉴别过程′的改进。由于证书鉴别过程′引入了平台认证，所以证书鉴别过程′中的认证包含用户认证和平台认证，从而对证书鉴别过程′的形式化描述与上述证书鉴别过程′有所区别。

证书鉴别过程′的具体步骤如下(由于σα中绑定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协议中的证书鉴别过程向后兼容。

4 安全性分析

由于第3版WAI协议已经被证明是安全的[11,12]，所以对基于改进WAI协议的WLAN Mesh安全关联方案和可信计算环境下的WLAN Mesh安全关联方案的安全性分析主要是对2个方案中的证书鉴别过程′和证书鉴别过程′进行安全性分析。下面利用利用串空间模型[13～15]来分析这2个方案中的证书鉴别过程′和证书鉴别过程′的安全性。

4.1 证书鉴别过程′的安全性分析

定义1 证书鉴别过程′的串空间是以下4类串的并集：1)发起者串 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个步骤中所发送的消息。

定理1 假设如下。1)∑为证书鉴别过程′的串空间，C为∑中含有一个发起者串s的丛，发起者串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＞)唯一源发于一个响应者串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＞)唯一源发于一个发起者串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＞)唯一源发于一个服务者串r，从而根据假设3）可知，z·P唯一产生于＜r,2＞。由定义1和假设3）可知，x·P唯一产生于＜t,2＞。因为定义1所述的证书鉴别过程′满足沉默性(silent)和保守性(conservative)，所以x·z·P 不源发于C 中(文献[14]中的定理9)，从而MK∉KP，使得MACAS⊂term(＜t,3＞)唯一源发于服务者串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中存在一个发起者串 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＞)唯一源发于一个发起者串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中包含一个发起者串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中存在一个发起者串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＞)唯一源发于一个响应者串t，从而由假设3）可知，x·P唯一产生于＜t,2＞。由假设1）和假设3）可知，z·P唯一产生于＜s,2＞。因为定义1所述的证书鉴别过程′满足沉默性和保守性，所以x·z·P不源发于C中(文献[14]中的定理9)，从而MK∉KP，使得 MACSTA⊂term(＜s ,3＞)唯一源发于响应者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＞)唯一源发于一个服务者串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中包含一个发起者串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]中所述的针对于可信网络接入协议的串空间模型来分析证书鉴别过程′的安全性。为了分析可信网络接入协议的安全性，文献[15]引入了双身份协议主体、内部攻击者和外部攻击者的定义，并给出了针对于平台认证的定理。双身份协议主体是指具有2个可认证身份的协议主体。内部攻击者是指在一轮协议中进行内部攻击的合法协议主体，它是因双身份协议主体而存在的，其密钥集用Kip表示。外部攻击者是指除内部攻击者以外的攻击者，其密钥集用Kep表示。针对于平台认证的定理是指：对于一个平台的完整性报告[16]，如果该完整性报告显示该平台是可信赖的，那么该完整性报告必然源发于一个常规者串。下面利用这些定义和定理对证书鉴别过程′进行安全性分析。

定义2 证书鉴别过程′的串空间是以下4类串的并集：1)发起者串 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，它是一个双身份协议主体，用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，它是一个双身份协议主体，用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个步骤中所发送的消息。SMLα显示α是可信赖的，而SMLβ显示β是可信赖的。

定理4 假设如下。1)∑为证书鉴别过程′的串空间，C为∑中含有一个发起者串s的丛，发起者串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＞)唯一源发于一个响应者串t，从而根据假设3）可知：x·P唯一产生于＜t,2＞。由假设1）和假设3）可知，y·P唯一产生于＜s,3＞。因为定义2所述证书鉴别过程′满足沉默性和保守性，所以x·y·P不源发于C中(文献[14]中的定理9)，从而BK∉KP，使得MACa⊂term(＜s ,3＞)源发于响应者串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＞)唯一源发于一个 发起者串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＞)唯一源发于一个响应者串t' (文献[15]中的定理1)，从而x·P唯一产生于＜t',2＞。由假设1）和假设3）可知，y·P唯一产生于＜s,3＞。因为定义2所述的证书鉴别过程′满足沉默性和保守性，所以x·y·P不源发于C中(文献[14]中的定理9)，从而BK∉KP。因此，由1)的证明可知，t'=t。

由定义2、假设 2）和假设 3）可知，σAS,2⊂term(＜t,1＞)唯一源发于一个服务者串r，从而根据假设3）可知，z·P唯一产生于＜r,2＞。因为定义2所述的证书鉴别过程′满足沉默性和保守性，所以x·z·P 不源发于C 中(文献[14]中的定理9)，从而MK∉KP，使得 MACAS⊂term(＜t ,3＞)唯一源发于服务者串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中存在一个发起者串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＞)源发于一个发起者串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＞)唯一源发于一个发起串t'(文献[15]中的定理1)，从而 y·P唯一产生于＜t',3＞。由假设1）和假设3）可知，x·P唯一产生于＜s,2＞。因为定义2所述的证书鉴别过程′满足沉默性和保守性，所以x·y·P不源发于C中(文献[14]中的定理9)，从而BK∉KP，使得MACb⊂term(＜s,3＞)源发于发起者串 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中包含一个发起者串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中存在一个发起者串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＞)唯一源发于一个响应者串r，从而根据假设3）可知，x·P唯一产生于＜r,2＞。由假设1）和假设3）可知，z·P唯一产生于＜s,2＞。因为定义2所述的证书鉴别过程′满足沉默性和保守性，所以x·z·P不源发于C中(文献[14]中的定理9)，从而MK∉ KP，使得 MACa,2⊂term(＜s,3＞)源发于响应者串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＞)唯一源发于一个服务者串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＞)唯一源发于一个响应者串r'(文献[15]中的定理1)，从而x·P唯一产生于＜r',2＞。由假设1）和假设3）可知，z·P唯一产生于＜s,2＞。因为定义2所述的证书鉴别过程′满足沉默性和保守性，所以x·z·P不源发于C中(文献[14]中的定理9)，从而MK∉KP。因此，由 1)的证明可知，r'=r。

由于C中包含一个响应者串r，所以C中包含一个发起者串 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协议的改进，本文提出了一种基于改进WAI协议的WLAN Mesh安全关联方案 。然后，在该方案的基础上，通过对第3版WAI协议的进一步改进，本文提出了一种可信计算环境下的WLAN Mesh安全关联方案，它能实现WLAN Mesh可信接入认证，从而增强了WLAN Mesh的安全性。通过性能对比分析，基于改进WAI协议的WLAN Mesh安全关联方案在通信效率和计算量上都具有明显的优势，从而提高了WLAN Mesh安全关联的性能，特别是降低了AS的负载，有效地解决了第3版WAI协议用于建立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网络可信接入认证协议[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（信息技术 系统间远程通信和信息交换 局域网和城域网 特定要求 第11部分：无线局域网媒体访问控制和物理层规范）[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（信息技术 系统间远程通信和信息交换 局域网和城域网 特定要求 第11 部分：无线局域网媒体访问控制和物理层规范）和GB 15629.1102-2003（信息技术 系统间远程通信和信息交换 局域网和城域网 特定要求 第11部分：无线局域网媒体访问控制和物理层规范：2.4 GHz频段较高速物理层扩展规范）实施指南[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（信息技术系统间远程通信和信息交换 局域网和城域网 特定要求 第 11 部分：无线局域网媒体访问控制和物理层规范，第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密钥管理协议的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.