—10—
李谢华，李建华，杨树堂，诸鸿文
(上海交通大学电子工程系，上海 200030)
摘 要：WAPI 协议是我国自行制定的无线局域网国家标准。该文在研究WAPI 接入鉴别过程的基础上，使用BAN 逻辑对其进行了形式化的分析和验证，证明了接入鉴别过程能够达到信息安全所要求的身份认证、数据完整性和机密性目标。 关键词：WAPI ；接入鉴别；密钥协商 Formal Analysis and Verification for Authentication Process of WAPI
LI Xiehua, LI Jianhua, YANG Shutang, ZHU Hongwen
(Dept of Electronic Engineering, Shanghai Jiaotong Univ., Shanghai 200030)
【Abstract 】WAPI is the WLAN national standard designed by China. Based on the thorough researches on authentication process of WAPI, this paper analyzes and verifies this process with BAN l
ogic. The result of formal analysis indicates that the authentication process of WAPI can achieve the goal of identification, data integrity and confidentiality. 【Key words 】WAPI; Authentication; Session key negotiation
计 算 机 工 程Computer Engineering 第32卷 第22期
Vol.32 No.22 2006年11月
November 2006
·博士论文·
文章编号：1000—3428(2006)22—0010—04
文献标识码：A 中图分类号：TN913.2
1概述
随着网络通信的快速发展，无线通信业务以其方便、灵
活的特点得到了越来越广泛的应用。与此同时，无线网络的安全问题也显得越发突出[1,2]。
针对当前无线局域网(WLAN)中存在的安全问题，我国自行制定了无线局域网鉴别和保密基础结构(WLAN Authen- tication and Privacy Infrastructure ，WAPI)无线局域网国家标准[3,4]。虽然WAPI 在国际化的过程中遇到很多困难，但是作为我国自行研发的第1个无线局域网国际标准，其对我国信息产业的作用和影响是巨大的。因此，WAPI 标准是否能够满足无线通信中的身份认证、数据完整性和机密性[5]等安全目标显得尤为重要。
WAPI 由无线局域网鉴别基础结构WAI(WLAN Authentication Infrastructure)和无线局域网保密基础结构WPI(WLAN Privacy Infrastructure)组成，WAI 负责对用户进行身份鉴别，是实现WAPI 的基础；WPI 负责对传输数据进行加密处理。在BSS(basic service set)中，WAI 采用公钥密码技术实现STA(station)与AP(access point)之间的相互身份鉴别；在IBSS(independent basic service set)中，WAI 采用共享密钥完成STA 之间的相互身份鉴别。WAI 中最为重要的组成部分是鉴别服务单元(Authentication Service Unit ，ASU)，它作为可信任和具有权威的第三方，保证公钥体系中证书的合法性，并负责生成、颁发、吊销、更新所有参与网上信息交换的各方在数据传输中所需要的数字证书。ASU 对管理范围内的AP 与STA 进行管理并提供服务，在同一ASU 的管理范围内，STA 和AP 之间需要通过ASU 实现证书的双向鉴别。
WPI 保密基础结构采用国家密码管理委员会办公室批准的用于WLAN 的对称密码算法实现数据保护，对MAC 子层的MSDU 进行加、解密处理。
WAPI 协议作为新推出的无线局域网国家标准，还在不断地改进和完善当中。BAN 逻辑作为一种简单有效的形式化分析方法被广泛地应用与安全协议的分析和验证，本文针对
WAPI 中与安全接入控制相关的鉴别接入过程，使用BAN 逻辑对协议的安全性能进行了全面详尽的分析和验证。
2 WAPI 接入鉴别过程
2.1 协议中采用的符号说明
E(K;m)：采用密钥K 对消息m 进行加密； K a ：STA 的公钥，与之相应K a -1为STA 的私钥； K b ：AP 的公钥，与之相应K b -1为AP 的私钥； K asu ：ASU 的公钥，与之相应K asu -1为ASU 的私钥； Cert_A: STA 的证书； Cert_B ：AP 的证书； staCertAuthInfo ：ASU 对STA 证书的鉴别结果； apCertAuthInfo ：ASU 对AP 证书的鉴别结果； Sig(X;m)：用密钥X 对消息m 进行签名； ukeyIdx ：单播密钥索引； mIDap ：密钥协商标识；
nextmIDsta ：下一次密钥协商标识； SPI ：安全参数索引；
R1：单播密钥协商中AP 产生的随机数； R2：单播密钥协商中STA 产生的随机数； algIdentifier ：会话算法标识(会话算法响应标识)； MAC ：消息鉴别码； gkeyIdx ：组播密钥索引；
gNonce ：组播密钥通告标识； gsn ：组播数据序号。
noticeData ：组播密钥通告数据；
2.2 STA 接入鉴别过程分析
当STA 关联或重新关联至AP 时，AP 和STA 必须进行
基金项目：国家“863”计划基金资助项目(2002AA145090) 作者简介：李谢华(1977－)，女，博士生，主研方向：网络安全协议；李建华，教授、博导；杨树堂，副教授；诸鸿文，教授、博导 收稿日期：2005-12-08 E-mail ：beverly@
—11—
双向证书鉴别。在BSS 中只有鉴别成功后，AP 才允许STA 接入，同时STA 也才允许通过该AP 收发数据。接入鉴别过程由证书鉴别、单播密钥协商和组播密钥通告3部分组成，鉴别过程如图1所示。
图1 WAPI 鉴别接入过程
证书鉴别过程如下： 消息1 接入鉴别请求
STA AP: Cert_A, Ta →
AP 向STA 发送鉴别激活以启动整个鉴别过程，然后STA 将自己的证书Cert_A 和接入鉴别请求时间Ta
一同发送给AP 。
消息2 证书鉴别请求
-1b AP ASU: Sig( K ; Cert_A, Ta, Cert_B)→ AP 首先检查自己的当前状态，如果符合要求则记录Ta ，再用自己的私钥将Cert_A 、Ta 和Cert_B 进行签名发送给ASU 。
消息3 证书鉴别响应
-1asu ASU AP: Sig(K ; {Cert_A, staCertAuthInfo}, {Cert_B, apCertAuthInfo, Ta})
→ ASU 首先验证AP 的签名和Cert_B 的有效性，
如果有效则进一步验证Cert_A 。验证完毕，ASU 将STA 证书鉴别结果信息(包括Cert_A 和StaCertAuthInfo)、AP 证书鉴别结果信
息(包括Cert_B 、
ApCertAuthInfo 以及Ta)和ASU 对它们的签名构成证书鉴别响应发回给AP 。
信息4 接入鉴别响应
-1asu AP STA: Sig(K ;{Cert_A, staCertAuthInfo}, {Cert_B,apCertAuthInfo, Ta})
→
AP 通过检查当前的状态，Ta 和ASU 的签名验证该报文的有效性，然后查看STA 证书的鉴别结果，根据此结果对STA 进行接入控制。
同时AP 根据证书鉴别响应报文生成接入鉴别响应分组回送至STA 。STA 收到接入鉴别响应分组后通过验证当前状态、Ta 和ASU 的签名确定分组的有效性，并且根据AP 证书的鉴别结果决定是否接入该AP 。
证书鉴别成功后，AP 向STA 发送密钥协商请求分组开始与STA 协商单播密钥。
单播密钥协商过程：
消息5密钥协商请求：
1b AP STA: Sig K ;algIdentifier, ukeyIdx, mIDap, SPI, E(Ka;R1))
→-（ STA 首先检查当前状态、SPI 和AP 签名的有效性。然后
查看该分组是证书鉴别成功后的首次密钥协商还是密钥更新协商请求，并且相应地对mIDap 字段值进行比较。最后使用Ka -1解密得到R1，STA 产生R2，将R1⊕R2的结果进行扩展得到单播会话密钥，计算nextmIDsta 、MAC ，构造密钥协商响应分组发送到AP ，同时保存mIDap 和密钥协商响应分组。
消息6密钥协商响应：
STA AP: {algIdentifier, ukeyIdx, nextmIDsta, SPI E Kb R2)MAC}
→，(;， AP 首先检查当前状态、SPI 和ukeyIdx 字段的有效性。
然后使用Kb -1解密得到R2，扩展R1⊕R2得到单播会话密钥和消息鉴别密钥，计算MAC ，将其和响应分组中的MAC 字段进行比较。最后比较algIdentifier ，判断nextmIDsta 是否单调递增，保存nextmIDsta 作为下次单播密钥更新时的密钥协商标识。
在单播密钥协商成功后，开始组播密钥协商过程。AP 首先向STA 发送组播密钥通告分组通告组播密钥。
消息7组播密钥通告：
AP STA: {gkeyIdx, ukeyIdx,gNonce gsn E Ka noticeData)MAC}
→，，(;， STA 首先检查当前状态，用ukeyIdx 标识的消息鉴别密钥生成MAC 与分组中的MAC 进行比较，以确定分组的有 效性。
若该分组不是证书鉴别成功后的首次组播密钥通告，则比较gNonce 和STA 保存的上次组播通告中的gNonce 字段值，相同则重传上次的组播密钥响应分组；若该分组是证书鉴别成功后的首次组播密钥通告或者gNonce 字段严格单调递增，则利用Ka -1解密得到组播主密钥，并且将其扩展得到组播会话密钥，STA 在本地保存gNonce 。最后生成并保存组播密钥响应分组发送给AP 。
消息8组播密钥响应：
STA AP: {gkeyIdx, ukeyIdx,gNonce MAC}→， AP 通过ukeyIdx 中标识的消息鉴别密钥计算MAC ，并与分组中的MAC 值进行比较，然后比较响应分组与通告分组中的gNonce 、gkeyIdx 字段，若相同则表示组播密钥通告成功。
由于MAC 字段值是利用当前密钥协商计算出的消息鉴别密钥对消息鉴别码字段之前的所有协议数据字段内容计算得到。因此MAC 的值只有STA 和AP 可以计算得到。为方便协议分析，可以将MAC 等价于STA 和AP 之间的共享密钥。消息6、消息7、消息8可转化为以下形式：
消息6转化为
STA AP: E(MAC;algIdentifier, ukeyIdx, nextmIDsta, SPI E Kb R2))
→，(; 消息7转化为
AP STA: E(MAC;gkeyIdx, ukeyIdx,gNonce gsn E Ka noticeData))
→，，(; 消息8转化为
STA AP: E(MAC;gkeyIdx, ukeyIdx,gNonce)→
3 STA 接入鉴别过程的安全性验证
BAN 逻辑[6]是由Burrows 、Abadi 和Needham 在1990年提出的，它由一系列命题和逻辑规则组成，命题表示主体对消息的知识或信念，应用推理规则可以从已知的知识和信念推导出新的知识和信念[7]，最后通过推导的结果证明协议安全目标是否能够达到。
—12—
BAN 逻辑成功地发现了一些安全协议中存在的安全漏洞，并且以其简单直观的特点得到了广泛的应用。它同样适用于无线安全协议的分析验证，文献[8,9]中使用BAN 逻辑验证了无线认证协议的安全性，
因此本文也使用BAN 逻辑对WAPI 协议的接入鉴别过程进行分析和验证。在分析过程中假设只有私钥的合法拥有者才能使用该私钥，并且STA 和AP 的证书是新鲜的。
3.1 协议的形式化描述
为方便协议分析，协议的形式化描述中只保留和安全性分析直接相关的消息字段内容。由于ASU 只对STA 和AP 的证书进行鉴别，因此可以省略ASU 对证书的鉴别过程。协议的形式化描述如下，其中A 代表STA ，B 代表AP ：
消息1: -1
Ka
K
asu A B :[A],Ta
→a
消息2: -1
-
1-1Ka
K asu Kb
K asu K asu
CertAuthInfo CertAuthInfo, Ta B A :{{[A],
sta }, {[B], ap }}→a a 消息3：-1
Ka Kb B A: {mIDap, {R1}}→
消息4：Kb MAC A B: { nextmIDsta,{R2}}→ 消息5：Ka MAC B A: {gNonce noticeData}}→，{ 消息6：MAC A B: {gkeyIdx gNonce}→， 初始假设：
(1)B A |B R1
↔≡ (2)B A |A R2
↔≡ (3)Kasu
A |ASU ≡a (4)Kasu
B |ASU ≡a (5)MAC
A |A
B ≡↔ (6)MAC
B |A B ≡↔
(7)A |(ASU|X)≡⇒ (8)B |(ASU|X)≡⇒ (9)R1
B |A B ≡↔ (10)R2
A |A
B ≡↔ (11)A |A Ka
a ≡ (12)B |B Kb
a ≡ (13)R1
A |(B|A B)≡⇒↔ (14)R2
B |(A|A B)≡⇒↔ (15)noticeData
B |A B ≡↔ 协议安全目标：
A|apCertAuthInfo ≡，B|staCertAuthInfo ≡，R1
A |A
B ≡↔，
R2
B |A B ≡↔，noticeData
A |A
B ≡↔
3.2 协议的形式化验证过程
3.2.1 AP 端的验证过程
ASU 发送证书鉴别响应到B ：
-1-1
-1
Ka
K asu Kb
K
asu
K
asu
ASU B:{{[A], staCertAuthInfo}, {[B], apCertAuthInfo, Ta}}→a a
-1-1
-
1
Ka
K asu Kb
K
asu
K
asu
B {{[A], staCertAuthInfo}, {[B], apCertAuthInfo, Ta}}<a a
由假设(4)以及BAN 逻辑中的消息意义规则： -1
K
K P|Q P {X}P|Q|~X
≡≡a <，
其中P 、Q 为通信主体，X 为消息主体，K －1为Q 的私钥。得到
-1-1
Ka
K asu Kb
K
asu
B|ASU|~{[A], staCertAuthInfo}, {[B], apCertAuthInfo, Ta}
≡a a
B 通过验证Ta ，可以判断该消息是否是新鲜的，如果是，则进行进一步验证，否则，停止验证。如果该条消息是新鲜的，即B|#Ta ≡（），则使用BAN 逻辑中的随机数验证规则：
P|#X P|Q|~X P|Q|X
≡≡≡≡（），
得到
-1-1
Ka
K asu Kb
K
asu
B|ASU|{[A], staCertAuthInfo}, {[B], apCertAuthInfo, Ta}
≡≡a a
由假设8)以及裁判规则：
P|Q|X P|Q|X
P|X
≡⇒≡≡≡，
得到
-1Ka
K asu B|[A]≡a ，B|staCertAuthInfo ≡； AP 端达到证书鉴别目标。
从消息4得到 R2
Kb MAC B {nextmIDsta,{A B}}↔<
由BAN 逻辑规则K
K P|P P {X}P X
≡a <<，
和假设(12)得到 R2
MAC B {nextmIDsta A B}↔<，
由BAN 逻辑中的消息意义规则K
K P|P Q P {X}P|Q|~X
≡↔≡<，
和假设(6)得到
R2
B |A |~{nextmIDsta,A B}≡↔
B 通过检查nextmIDsta 字段值可以判断该条消息的新鲜
性，若新鲜则B |#nextmIDsta ≡，应用随机数验证规则得到
R2
B |A |{A B}≡≡↔
由裁判规则和假设(14)得到
R2
B |A B ≡↔
AP 端达到单播密钥协商目标。
从消息6得到MAC B {gkeyIdx gNonce}<， 由消息意义规则和假设(6)得到 B |A |~{gkeyIdx gNonce}≡，
B 通过检查gNonce 字段可以判断该字段值是否新鲜，
若新鲜则B |#gNonce ≡，应用随机数验证规则得到
B |A |gkeyIdx ≡≡ B 通过检查gkeyIdx 的字段值是否与组播通告分组中的gkeyIdx 相同，就可以判断出此次组播通告是否成功。 3.2.2 STA 端的验证过程
STA 在证书鉴别之前预存有接入点AP 的证书，因此有
Kb
-1asu A [B]K <a ，应用消息意义规则和假设(3)得到
Kb
A|ASU |[B]≡ a
协议的前提条件中假设AP 和STA 的证书总是新鲜有效的， 因此应用随机数验证规则、裁判规则和假设(7)得到
Kb
A|[B]≡a
从消息2得到
—13—
-1-1
-1
Ka
K asu Kb
K
asu
K
asu
A {{[A], staCertAuthInfo}, {[B], apCertAuthInfo, Ta}}<a a
使用消息意义规则和假设(3)得到
-1-1
Ka
K asu Kb
K
asu
A |ASU |~{{[A], staCertAuthInfo}, {[B], apCertAuthInfo, Ta}}
≡a a
A 通过验证Ta 判断消息的新鲜性，若新鲜则A|#
Ta ≡（），利用随机数验证规则得到
-1-1
Ka
K asu Kb
K
asu
A |ASU |{{[A], staCertAuthInfo}, {[B], apCertAuthInfo, Ta}}
≡≡a a
由裁判规则和假设(7)得到
-1-1
Ka
K asu Kb
K asu A |{{[A], staCertAuthInfo},
{[B], apCertAuthInfo, Ta}}
≡a a 因此得到
-1Kb
K asu A|[B]≡a ，A|apCertAuthInfo ≡
STA 端达到证书鉴别的目标。由于AP 在向ASU 发送的证书鉴别请求中使用私钥签名，因此可以惟一地确定AP 的身份。
从消息3得到 -1R1
Ka Kb A {mIDap,{A B}}↔< 使用消息意义规则和假设(11)得到
-1
R1
Kb A {mIDap A B}↔<，
由于前面已经证明Kb
A|[B]≡a ，使用消息意义规则得到 R1
A |
B |~{mIDap,A B}≡↔
A 通过检查mIDap 字段的值可以判断该条消息是否新鲜，若新鲜，则有A |#mIDap ≡，应用随机数验证规则得到
R1
A |
B |A B ≡≡↔
再使用裁判规则和假设(13)可以得到 R1
A |A
B ≡↔
STA 端达到单播密钥协商的目标。 从消息5得到
noticeData
Ka MAC
A {gkeyIdx,gNonce,{A B}}↔
<
由BAN 逻辑中的规则K
K P|P P {X}P X
≡a <<，和假设(11)得到
noticeData
MAC
A {gkeyIdx,gNonce,A B}↔
<
由消息意义规则和假设(5)得到
noticeData
A |
B |~{gkeyIdx,gNonce,A
B}≡↔
A 通过检查gNonce 字段值可以判断该条消息是否新鲜，若新鲜则有A |#gNonce ≡，应用随机数验证规则得到
noticeData
A |
B |{gkeyIdx,A
B}≡≡↔
使用裁判规则和假设(15)得到
noticeData
A |A
B ≡↔
因此STA 端达到组播密钥通告的目标。
以上的验证结果表明，在接入鉴别过程结束后STA 和AP 能够达到身份认证和密钥协商的目标。STA 和AP 通过使用公钥加密和私钥解密保证了信息的保密性；在密钥协商过程中STA 和AP 使用单播完整性校验密钥、组播完整性校验密钥和消息鉴别码保证了数据的完整性；证书鉴别过程中ASU 通过验证AP 的证书和签名能够惟一地确定AP 的身份，从而实现身份认证的安全目标。
另外值得一提的是，虽然在鉴别接入请求分组中STA 没有使用私钥签名，可能会引起证书的盗用问题，但是在随后的密钥协商过程中由于证书盗用者无法解密密钥协商数据，不能通过密钥协商，因此能够保证实现对STA 身份认证的安全目标。
4 结束语
WAPI 是我国自行开发的第1个WLAN 协议标准，它的实施将对我国在协议标准制定和无线通信安全等领域的发展具有重要的意义。本文在对WAPI 协议及其实施指南进行了深入细致的研究后使用BAN 形式化逻辑分析工具分析验证了WAPI 协议的安全性能。验证的结果证明WAPI 协议的鉴别接入过程能够实现信息保密性、保证数据完整性、实现身份认证、接入控制的安全目标，从而保证了无线通信的信息安全。
参考文献
1 Arbaugh W A, Shankar N, Wan Y C J, et al. Your 802.11 Wireless Network Has No Clothes[J]. IEEE Wireless Communications, 2002, 9(6): 44-51.
2 Nikita B, Lan G , David W. Intercepting Mobile Communications: the Insecurity of 802.11[C]. Proceedings of the 7th Annual International Conference on Mobile Computing and Networking, Rome, Italy, 2001.
3 中华人民共和国国家质量监督检验检疫总局. GB15629 无线局域
网媒体访问(MAC)和物理(PHY)层规范[S]. 2003-05-12.
4 中华人民共和国国家质量监督检验检疫总局.
GB15629 1102-
2003. 无线局域网媒体访问控制和物理层规范: 2.4GHz 频段较高速物理层扩展规范[S]. 2003-05-12.
5 Menezes A J, Oorschot van P C, Vanstone S A. Handbook of Applied Cryptography[M]. CRC Press, 1996.
6 Burrows M, Abadi M, Needham R. A Logic of Authentication[J]. ACM Transaction on Computer Systems, 1990, 8(1): 18-36.
7 Gritzalis S, Spinellis D, Georgiadis P. Security Protocols over Open Networks and Distributed Systems: Formal Methods for Their Analysis, Design, and Verification[J]. Computer Communications, 1999, 22(8): 695-707.
8 Aziz A, Diffie W. Privacy and Authentication for Wireless Local Area Networks[J]. IEEE Personal Communications, 1994, 1(1): 25-31. 9 刘健伟, 王育民. 个人通信系统中的移动用户登记认证协议[J].
西安电子科技大学学报, 1997, 24(3): 323-327.
