８０２．１６ｅ中双重ＥＡＰ认证的Ｒｕｂｉｎ逻辑分析

刘丽明　潘　进　王　松

摘 要：802.16是IEEE制定的无线城域网技术标准。作为当今最具发展前景的无线宽带接入技术之一，由于传输信号的开放性，其安全问题备受关注。802.16e标准的安全体制在802.16d安全体制的基础上作了进一步的改进，不但实现了RSA的双向认证，而且引入了应用层认证协议EAP;实现了基于EAP的双重认证。根据协议分析需求,首先对所选形式化分析方法Rubin逻辑进行了扩展，并用扩展后的Rubin逻辑对双重认证模式进行分析，验证了802.16e中的双重认证模式的安全性。

关键词：802.16；TLS协议；形式化分析；Rubin逻辑

中图分类号：TN915文献标识码：A

文章编号：1004-373X(2009)05-067-05

Rubin Logic Analysis of Double EAP Authentication in 802.16e

LIU Liming1,PAN Jin1,WANG Song2

(1.Xi′an Communications Institute，Xi′an,710106,China;2.Academy of Equipment Command & Technology,Beijing,101416,China)

Abstract：802.16 is the technical standard of wirless metropolitan network made by IEEE.Its security is paid much attention because of open features of wireless channel.The security mechanism of 802.16e makes more improvement than 802.16d.It not only achieves the mutual authentication based on RSA,but also introduces EAP protocol and dual EAP protocol.According to the requirement of protocol analyzing,Rubin logic is improved,and the dual authentication mode with Rubin logic is analysed,security of the dual authentication mode is validated.

Keywords：802.16;TLS protocol;formal analysis;Rubin logic

0 引 言

IEEE802.16无线城域网技术是一种新兴的无线宽带接入技术,与其他接入技术相比,具有一系列显著优点,但由于无线信号的开放性,其面临的安全威胁比有线网络严重的多。随着人们对安全问题重视程度的日益提高,并鉴于IEEE802.11无线局域网的设计和推广经验,802.16在设计之初就充分考虑了安全问题,专门在MAC层中定义了一个安全保密子层来提供通信的安全保障。802.16d［1］发布后,文献［2,3］都对其安全体制进行了讨论,发现存在很多漏洞,其中最大的安全问题就是PKM密钥管理协议的单向认证性,即只能实现基站对客户端的身份认证。之后推出的802.16e［4］版本在802.16d安全体制的基础上进行了改进和完善,其密钥管理协议PKMv2不但实现了 RSA的双向认证,而且引入了应用层可扩展认证框架——EAP,并实现了基于EAP的双重认证模式。双重认证的思想符合当前安全协议的发展方向,但关于双重认证协议形式化分析方面的相关工作尚未收集到。为此使用形式化分析方法——Rubin逻辑验证了双重EAP认证的安全性,并根据协议分析需要首先对该方法进行了扩展。

1 双重EAP-TLS认证协议简介

可扩展认证框架EAP可以支持多种认证机制,例如EAP-MD5,EAP-OTP和EAP-TLS等。这里选择对其中应用范围最广，安全强度最高的EAP-TLS协议进行分析。TLS协议的前身是SSL协议,两者的差别非常微小。文献［5,6］对SSL协议的安全性进行了分析,认为该协议的安全性较高,但仍存在一些安全漏洞,例如,协议交互过程当中存在以明文形式传送的信息,无法标定消息来源；预主密钥(PMS)的来源和新鲜性得不到确认；此外,协议使用明文消息发送EAP-Success /EAP-Failure消息,没有任何保护措施。 PKMv2中支持双重EAP-TLS认证模式,其交互过程如图1所示。

(1) 第一轮的EAP-TLS握手过程与一次EAP-TLS相同,基站和终端用PKMv2 EAP Transfer消息来装载EAP消息,并且用刚刚产生的EIK签名的PKMv2 EAP Complete消息来装载EAP-Success/EAP-Failure。

(2) 第一轮认证成功后,基站和终端都拥有密钥PMK1和EIK。终端发送用EIK签名的PKMv2 EAP Start 消息发起第二轮认证，然后通过发送PKMv2 EAP Transfer消息进行第二轮EAP-TLS握手过程,并对每条消息用EIK进行完整性校验。

(3) 如果第二轮的EAP-TLS认证成功,终端和基站都拥有了PKM1和PKM2,并可由此生成密钥AK,至此双重接入认证结束。

由于双重EAP-TLS认证中第一轮的TLS握手交互过程与一次SSL握手过程基本相同,因此不再重复文献［6］的工作,直接在其基础上用Rubin逻辑对第二轮EAP-TLS认证展开分析,并根据协议分析需要,对Rubin逻辑进行扩展。

图1 交互过程

2 Rubin逻辑扩展

Rubin逻辑［7］是A.D.Rubin在其博士论文中提出的一种分析安全协议的新方法。关于Rubin逻辑的详细介绍参考文献［7］,由于篇幅问题不再赘述。与之前的模态逻辑分析方法相比,该逻辑具有一系列显著优点。在此沿用文献［6］中分析SSL协议时所使用的Rubin逻辑,并根据协议分析需求,对该逻辑扩展如下：

随着密码学的发展,安全协议中出现的一些新的密码操作和数据类型,Rubin逻辑都无法描述和分析,例如,Rubin逻辑中没有关于MAC校验的相关表示和推理规则,人们使用Rubin逻辑分析协议时,大都对MAC校验做了等同加密的简单处理,但两者并非同一个概念,原理和功能也大不相同。为了更好地使用Rubin逻辑对后文中安全协议进行分析,对Rubin逻辑扩展如下：

首先,定义完整性校验值的表示方法：

MIC(X,k)：表示用完整性校验密钥k对消息X进行完整性校验的值。

其次,定义以下关于完整性校验的推理规则：

·扩展的子消息来源规则

(X,MIC(X,k))∈POSS(P)

Xcontainsx1,(k∈POSS(Q))∈BEL(P)x1fromQ∈POSS(P)

说明：P拥有消息X和X的完整性校验值,X包含子消息x1,且P相信Q拥有消息X的完整性校验密钥,则P相信x1 from Q。

·签名规则

#(k)∈BEL(P),k∈POSS(P)

LINK(N璦)∈BEL(P),Xcontainsf(N璦)

X containsx1,(X,MIC(X,k))from Q∈POSS(P)BEL(P):=(BEL(P)－LINK(N璦))∪{#(x1)}

说明：在一定条件下,消息X的子消息是新鲜的。第一个条件是P拥有未使用过的临时值N璦；第二个条件是消息X必须包含f(N璦)；第三个条件是P拥有包含N璦消息X的完整性校验值,且计算该值的完整性校验密钥是新鲜的,并被P拥有。

3 协议分析

3.1 协议规范

规范协议时所用“动作”和“推理规则”取自于文献［7］以及上文中对Rubin逻辑的扩展。此外,根据协议定义以下函数,其中前6个引用文献［6］中的定义：

(1) Generate-keys(X1,X2,X3)

通过master-secret、客户的随机数和服务器的随机数生成会话密钥。

(2) Choose-ciphersuite(X)

从客户提供的CipherSuite列表中选择一个ciphersuite。

(3) Match(X1,X2)

检查CipherSuite是否包含在Cipher- Suite列表中。

(4) Finished(P,X1,X2)

对master-secret和已发送的所有消息进行散列运算,生成Finished消息。

(5) Ske(X1,X2,X3)

对客户的随机数、服务器的随机数和服务器的公开密钥进行散列运算,生成ServerKeyExchange消息。

(6) Cv(X1,X2)

对master-secret和已发送的所有消息进行散列运算,生成ClientCertificate-Verify消息。

(7) Check-same(X)

验证对方发送消息中的MAC完整性校验值是否与自己生成的一致。

规范结果如下：

PrincipalC

POSS(C)={k+瑿A∞CA,{k+璫}璳－瑿A,k+璫∞C,k－璫,ciph-ersuites璫,Finished(),Generate-keys(),Match(),Cv(),EIK,PAK}

BEL(C)={#(k+瑿A),#(k－璫),#(k+璫),#((k+璫)璳－瑿A),#(EIK),#(PAK)}

Binding(C)={k+璫∞C,k+瑿A∞CA}

BL(C)=

Generate-Nonce(N璫)

Concet(N璫,ciphersuites璫)

Send(S,{N璫,ciphersuites璫,MIC((N璫,cipher-suites璫),EIK)})

Update({N璫,ciphersuites璫,MIC((N璫,cipher-suites璫),EIK)})

Receive(S,{N璼,…,HelloDone璼,MIC((N璼,…,HelloDone璼),EIK)})

Split({N璼,…,HelloDone璼,MIC((N璼,…,Hello Done璼),EIK)})

Apply(Check-same(),{MIC})

Apply(Match,{ciphersuites璫,cipher璼})

Apply-asymkey({Ske(N璫,N璼,k+璗S)}璳－璼,k+璼)

Generate-Secret(PMS)

Apply-asymkey(PMS,k+璗S)

Generate-Secret(MS)

Forget-Secret(PMS)

Apply(Generate-keys,{MS,N璫,N璼})

Apply(Cv,{MS,SentM})

Apply-asymkey(Cv({MS,SentM}),k－璫)

Apply(Finished,{Client,MS,SentMessages})

Encrypt(Finished璫,k璫s)

Send(S,Concat({k+璫}璳－瑿A,{PMS}璳+璗S,{Cv(MS,SentM)}璳－璫,ChangeCipherSpec,{Finished璫}璳璫s,MIC(({k+璫}璳－瑿A,…,{Fini-shed璫}璳璫s),EIK))

Update({{k+璫}璳－瑿A,…,{Finished璫}璳璫s,MIC(({k+璼}璳－瑿A,…,{Finished璫}璳璫s),EIK)})

Receive(S,{ChangeCipherSpec,{Finished璼}璳璼c,MIC((ChangeCipherSpec,{Finished璼}璳璼c),EIK)})

Split({ChangeCipherSpec,{Finished璼}璳璼c,MIC((ChangeCipherSpec,{Finished璼}璳璼c),EIK)})

Apply(Check-same(),{MIC})Decrypt({Finished璼}璳璼c,k璼c)

PrinsipalS

POSS(S)={k+瑿A∞CA,{k+璼}璳－瑿A,k+璼∞S,k－璼,Fi-nished(),Generate-keys(),Choosecipher-suite(),Ske(),EIK,PAK}

BEL(S)={#(k+瑿A),#(k－璼),#(k+璼),#((k+璼)璳－瑿A),#(EIK),#(PAK)}Binding(S)={k+璼∞S,k+瑿A∞CA}

BL(S)=

Receive(C,{N璫,ciphersuites璫,MIC((N璫,ciph-ersuites璫),EIK)})

Split({N璫,ciphersuites璫,MIC(N璫,ciphersuites璫),EIK)})

Apply(Check-same(),{MIC})

Apply(Choose-ciphersuites(),{ciphersuites璫})Generate-Nonce(N璼)

Generate-key-pair(k+璗S,k－璗S)

Apply(Ske,Concat(N璫,N璼,k+璗S))

Apply-asymkey(Ske(N璫,N璼,k+璗S),k－璼)

Concat(N璼,cipher璼,{k+璼}璳－瑿A,{k+璗S,{Ske(N璫,N璼,k+璗S)}璳－璼},CertificateRequest,HelloDone璼,MIC((N璼,…,HelloDone璼),EIK))

Send(C,{N璼,…,HelloDone璼,MIC璼)(N璼,…,HelloDone璼),EIK)})

Update({N璼,…,HelloDone璼,MIC((N璼,…,He-lloDone璼),EIK)})

Receive(C,{{k+璫}璳－瑿A,…,{Finished璫}璳璫s,

MIC(({k+璫}璳－瑿A,…,{Finished璫}璳璫s),EIK)})

Split({{k+璫}璳－瑿A,…,{Finished璫}璳璫s,

MIC(({k+璫}璳－瑿A,…,{Finished璫}璳璫s),EIK)})

Apply(Check-same(),{MIC})

Apply-asymkey({k+璫}璳－瑿A,k+瑿A)

Apply-asymkey({PMS}璳+璗S,k－璗S)

Generate-Secret(MS)

Forget-Secret(PMS)

Apply(Generate-keys,{MS,N璫,N璼})

Apply-asymkey(Cv(MS,SentM)璳－璫,k+璫)

Decrypt({Finished璫}璳璫s,k璫s)

Apply(Finished,{Server,MS,SentMessages})

Encrypt(Finished璼,k璼c)

Send(C,{ChangeCipherSpec,{Finished璼}璳璼c,MIC((ChangeCipherSpec,{Finished璼}璳璼c),EIK)})

Update({ChangeCipherSpec,{Finished璼}璳璼c,MIC((ChangeCipherSpec,{Fi-nished璼}璳璼c),EIK)})

3.2 协议分析

从“行为列表”BL(C)的第一个动作开始分析协议,前5个动作执行完后,POSS(C)中增加新的元素N璫；BLE(C)中增加新的元素LINK(N璫)。Update操作使得Observer(N璫=W)(W表示所有的主体)。至此,没有使用推理规则。下一个要执行的动作是“行为列表”BL(S)中的Receive。即：

Receive(C,{N璫,ciphersuites璫,MIC((N璫,ciphersuites璫),EIK)})

BL(S)中的前3个动作执行后,加入到POSS(S)中的新元素有N璫,ciphersuites璫,MIC((N璫,ciphersuites璫),EIK)；下一个要执行的动作是：

Apply(Check-same,{MIC})

若通过MIC值校验,此时可应用扩展的子消息来源规则推得N璫 from C,ciphersuites璫 from C,即A相信该消息来自于C,将此结论加入POSS(S)中。然后继续执行之后的9个动作,执行后,加入到POSS(S)中的新元素有N璼,k+璗S∞S,k－璗S和Ske(N璫,N璼,k+璗S)；加入到BEL(S)中的新元素有LINK(N璼),#(k－璗S),#(k+璗S),#(Ske(N璫,N璼,k+璗S))。下一个要执行的动作是BL(C)中的第6个动作,即：

Receive(S,{N璼,…,HelloDone璼,MIC((N璼,…,HelloDone璼),EIK)})

Receive之后的2个动作被执行后,加入到POSS(C)中的新元素有N璼,cipher璼,{k+璼}璳－瑿A,k+璗S,Ske(N璫,N璼,k+璗S),k+璼以及MIC((N璼,…,HelloDone璼),EIK)；下面要执行的动作是：

Apply(Check-same,{MIC})

若通过MIC值校验,此时,可应用扩展的子消息来源规则推得N璼 from S,且消息中的其他元素均来自于S,即C相信该消息来自于S,将此结论加入POSS(C)中,此外扩展的签名规则也被满足,可推该消息中的所有子消息都是新鲜的,将此结论加入BEL(C)中；将k+璼∞S加入到Binding(C)中,因此C相信S,TRUST［1,2］=1。下一个要执行的动作是：

Apply-asymkey({Ske(N璫,N璼,k+璗S)}璳－璼,k+璼)

此时,用于非对称加密的子消息来源规则的条件被满足,可推得Ske(N璫,N璼,k+璗S) from S,进一步对消息来源进行了确认。并且,签名规则的条件也被满足,可进一步确认#(Ske(N璫,N璼,k+璗S)),并将LINK(N璫)从BEL(C)中删除。然后C继续执行之后的三个动作。执行后,将PMS,MS和{PMS}璳+璗S加入到POSS(C)中,PMS和MS加入到秘密集合S中,#(PMS)和#(MS)加入到BEL(C)中。然后继续执行下一个动作：

Forget-Secret(PMS)

执行这个操作后,将PMS从POSS(C)中删除,#(PMS)从集合BEL(C)中删除。随后C继续执行之后的8个动作,执行后将k璫s,k璼c,Cv(MS,SentM),{Cv(MS, SentM)}璳－璫,Finished璫,{Finished璫}璳璫s和MIC(({k+璫}璳－瑿A,…,{Finished璫}璳璫s),EIK)加入到POSS(C)中,k璫s和k璼c加入到秘密集合S中,#(k璫s)和#(k璼c)加入到BEL(C)中。Update操作将S加入到Observers (PMS)中。下一个要执行的动作是BL(S)中的Re-ceive操作,即:

Receive(C,{{k+璫}璳－瑿A,…,{Finished璫}璳璫s,MIC(({k+璫}璳－瑿A,…,{Finished璫}璳璫s),EIK)})

Receive之后的两个动作被执行后,将{k+璫}璳－瑿A,{PMS}璳+璗S,{Cv(MS,SentM)}璳－璫,{Finished璫}璳璫s,k+璫,以及 MIC(({k+璫}璳－瑿A,…,{Finished璫}璳璫s),EIK)加入到POSS(S)中,下面要执行的动作是：

Apply(Check-same,{MIC})

若通过MIC值校验,此时,可应用扩展子消息来源规则推得{PMS}璳+璗Sfrom C,且消息中的其他元素均来自于C,即S相信该消息来自于C,将此结论加入POSS(S)中。此外,扩展的签名规则也被满足,可推得#({PMS}璳+璗S),且该消息的其他子消息都是新鲜的,将此结论加入BEL(S)中；将k+璫∞C加入到集合Binding(S)中,因此S相信C,TRUST［2,1］=1。然后S继续执行下一个动作：

Apply-asymkey({PMS}璳+璗S,k－璗S)

执行此操作后,将PMS from C加入到POSS(S)中,#(PMS)加入到BEL(S)中。S继续执行以后的两个动作后,将MS加入到POSS(S)中,#(MS)加入到BEL(S)中,并将PMS from C从POSS(S)中删除,#(PMS)从集合BEL(S)中删除。随后继续执行以后的8个动作,执行后将k璫s,k璼c,Cv(MS,SentM),{Cv(MS,SentM)}璳－璫,Finished璫,和{Finished璫}璳璫s加入到POSS(S)中,k璫s和k璼c加入到秘密集合S中,#(k璫s)和#(k璼c)加入到BEL(S)中。下一个要执行的动作是BL(C)中的Receive操作,即：

Receive(S,{ChangeCipherSpec,{Finished璼}璳璼c,MIC((ChangeCipherSpec,{Finished璼}璳璼c),EIK)})

Receive之后的两个动作被执行后,加入到POSS(C)中的元素有ChangeCipher- Spec,{Finished璼}璳璼c以及MIC((ChangeC璱- pherSpec,{Finished璼}璳璼c),EIK)。下一个要执行的动作是：

Apply(Check-same,{MIC})

若通过MIC值校验,此时,可应用扩展的子消息来源规则推得ChangeCipher- Spec from S,{Finished璼}璳璼c from S,即C相信该消息来自于S,将此结论加入POSS(C)中,此外扩展的签名规则也被满足,可推得#({Finished璼}璳璼c),将此结论加入BEL(S)中；然后继续执行下一个动作：

Decrypt({Finished璼}璳璼c,k璼c)

执行后将Finished璼加入到POSS(C)中,#(Finished璼)加入到BEL(C)中,至此,协议分析完毕。

4 结果分析

通过以上分析可知,双重EAP-TLS认证的安全性比单重EAP-TLS认证有了很大的提高。通过第二轮的认证,文献［5，6］中提出的安全漏洞都得到了弥补。首先,原来发送的明文消息有了EIK的完整性校验,从而可以判断消息的来源,避免了假冒攻击；且有了完整性保护,避免了攻击者任意篡改明文消息导致的“版本滚回”等攻击。其次,通过扩展的关于完整性校验的推理规则可推知,PMS的新鲜性和来源都可以由EIK的完整性保护而得到确认,从而避免了攻击者对PMS的重放攻击和假冒攻击。再次,从分析过程可看出,秘密信息的传送有了加密和完整性校验的双重保护,其来源和新鲜性得到了双重确认,安全强度有了很大提高。此外,如前文介绍,双重认证中用PKMv2 EAP Complete消息来装载EAP-Success或EAP-Failure,并对该消息进行完整性校验,从而避免了攻击者伪造该消息造成的协议中断。

参考文献

［1］IEEE P802.16-2004.IEEE Standard for Local and Metropolitan Area Networks Part 16.Interface for Fixed Broadband Wireless Access Systems,2004.

［2］Sen Xu,Manton Matthews,ChinTser Huang.Security Issues in Privacy and Key Management Protocols of IEEE 802.16.In: ACM SE'06,Melbourne,Florida,USA,2006.

［3］David Johnston,Jesse Walker.Overview of IEEE 802.16 Security.IEEE Security & Privacy,2004,2(3).

［4］IEEE P802.16e-2005.IEEE Standard for Local and Metropolitan Area Networks Part 16.Air Interface for Fixed and Mobile Broadband Wireless Access Systems,2005.

［5］Analysis of the SSL 3.0 Protocol.Proceedings of the Second USENIX Workshop on Electronic Commerce,USENIX Press,1996.

［6］李秋山,胡游君.SSL协议的扩展Rubin逻辑形式化分析［J］.计算机工程与应用,2007,8(16):3 852-3 859.

［7］Rubin D.An Interface Specification Language for Automatically Analyzing Cryptographic Protocols.Internet Society Symposium on Network and Distributed System Security.San Diego,CA,1997.

［8］徐一兵,田绪安,樊中山.无线宽带接入技术WiMAX802．16e［J］.现代电子技术,2008,31(13):35-37.

作者简介 刘丽明 女,1983年出生，硕士研究生。主要研究方向为网络安全。

潘 进 男,1959年出生，教授。