公共无线局域网安全体系研究及其可验安全性形式化分析

【作者】 宋宇波；

【导师】 胡爱群；

【作者基本信息】 东南大学 ， 信号与信息处理， 2005， 博士

【摘要】 公共无线局域网（PWLAN）是目前无线网络技术发展的热点之一,旨在给用户提供随时随地高效率、高质量、低成本的移动接入,其安全性直接影响到公共无线局域网技术的推广应用。如何设计和实现公共无线局域网的安全体系,为其安全协议的设计与分析提供理论指导,从而确保公共无线局域网的安全是目前迫切需要解决的问题。本文采用形式化分析手段,对当前公共无线局域网安全协议的安全性进行证明,并比较不同协议的安全性能,从而为选择合适的安全协议提供依据。为此,本文开展了以下几个方面的研究:1.通过对公共无线局域网现有应用模式和体系结构的分析,将公共无线局域网归纳为:WISP-owned PWLAN、Operator PWLAN以及PWLAN for Enterprise三种类型。在此基础上,提出了一个可以基本满足各种类型公共无线局域网需求的基于接入控制器模式的通用公共无线局域网安全体系结构,给出了该体系设计的合理性分析。2.根据预言机模型,从协议的机密性和可靠性两方面,对WEP、TKIP以及CCMP密码协议进行了精确量化的可验安全性形式化分析;推导出WEP、TKIP和CCMP协议的安全量化函数,该函数采用攻击成功率的优势函数来衡量加密机制的安全性能。分析表明,当攻击RC4算法的成功率为O（n2） * 2^-128（密钥长度为128比特）时,WEP的攻击成功率约为O（n²） * 2^-24,TKIP的攻击成功率约为O（n³） * 2^-48,这两个加密协议都没有达到提供预期的安全强度。3.提出了TKIP算法的一种改进算法。在该算法中把TKIP序列计数器（TSC）值由原来的48比特扩大到128比特,使其安全强度比RC4算法提高了约3个数量级。4.证明了CCMP加密协议的安全性和可靠性。分析表明,当AES算法的攻击成功率为O（n²） * 2^-128时,CCMP的可靠性和机密性对应的攻击成功率分别为O（n） * 2^-64和O（n2） * 2^-128,达到了预期的设计目标,可以满足公共无线局域网的安全需求。5.利用Bellare-Rogoway模型,对密码交换协议进行了可验安全性分析。证明了公共无线局域网采用的四步握手密钥交换机制的保密性和认证正确性;6.提出了一种增强的Bellare-Rogoway模型。采用该模型对802.1X认证协议进行了可验安全性分析,发现了该协议存在安全缺陷,容易遭受中间人攻击。在此基础上提出了一种攻击方法及改进措施。7.设计和实现了符合公共无线局域网技术规范的无线接入点和接入控制器。更多还原

【Abstract】 The public wireless local area network （PWLAN）, which can provide convenient high-speed wireless access to the Internet in’hot spots’such as airport, park and business quarter,is becoming one of the most interesting techniques in wireless network area. It would helppeople to enjoy high efficiency, high quality and low business cost mobile network services atanytime and anywhere. The security of PWLAN is the mainly concerned aspect in PWLANresearch. The problems which should be solved urgently include how to design and realizethe PWLAN security system, how to provide theoretic instruction in security protocols de-sign, and how to guarantee the PWLAN security. The proofs of security protocols validitybased on formal analysis methods are discussed in this dissertation. Especially, the securityperformances of security protocols adopted in PWLAN architecture are concretely comparedwith each other based on the conclusions of these proofs. The research in this dissertationincludes following aspects:1. The research on the PWLAN architecture: With a wide survey on the existing PWLANapplication pattern and system structure, we generalize the PWLAN into ISP-ownedPWLAN, Operator PWLAN and PWLAN for Enterprise. A PWLAN security systemarchitecture based on controller mode is proposed to meet the need of all PWLANtypes. Furthermore, the rational analysis of this system design is discussed after study-ing the component of the system structure and corresponding security mechanisms.2. The research on the correctness analysis and validity analysis of WEP and TKIP proto-cols: Concrete security analyses of WEP, TKIP and CCMP protocols are provided here.There are two aspects of security in our analysis: privacy and authenticity. We quantifythe security provided by these protocols as the advantage of attack successful probabil-ity and a function of the security of the underlying cipher. It is showed that while theadvantage of attack successful probability to RC4 algorithm is O（n²） * 2^-128, the ad-vantage of attack successful probability to WEP algorithm is approximate O（n²）*2^-24and the advantage of attack successful probability to TKIP is approximate O（n³）*2^-48.The conclusion is that both WEP and TKIP protocols do not provide a level of privacythat satisfies the PWLAN environment.3. The research on the enhancement of TKIP protocol: We enhance the TKIP algorithmby increasing the space of the TKIP sequence counter （TSC） from 48bits to 128bits. Itis showed that the security strength of this enhanced algorithm is 3 magnitudes higherthan RC4 algorithm.4. The research on the security analysis on privacy and authenticity of CCMP protocol:The concrete bounds for the security of CCMP are presented in terms of the security ofthe AES algorithm. The result is that while the advantage of attack successful probabil-ity to AES algorithm is O（n²） * 2^-128, the advantages of attack successful probabilityon authenticity and privacy are approximate O（n）*2^-64 and O（n²）*2^-128. It achievesthe anticipated design goals and satisfies the security requirements of the PWLAN.5. The research on the security analysis of key exchange protocol. We make a provablesecurity analysis of key exchange protocol with the Bellare-Rogoway model. It isshowed that the 4-way handshake protocol adopted in PWLAN does indeed bringingsignificant, provable security gains in practical situations.6. The research on the security analysis of authentication protocol. We proposed an ex-pansion Bellare-Rogoway model to analyze the provable security of 802.1X authentica-tion protocol. A security problem was found and the corresponding man-in-the-middleattack is given here. Furthermore, some proposed solutions are presented to preventthe discussed attack.7. The research on the design and realization of access point and controller: The designsand realizations of wireless access point and controller are discussed at the end of thisdissertation. The designs of these devices are confirmed with the PWLAN technologycriterion.更多还原