公共无线局域网安全体系研究及其可验安全性形式化分析
详细信息    本馆镜像全文|  推荐本文 |  |   获取CNKI官网全文
摘要
公共无线局域网(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) * 2~(-24),TKIP的攻击成功率约为O(n~3) * 2~(-48),这两个加密协议都没有达到提供预期的安全强度。
     3.提出了TKIP算法的一种改进算法。在该算法中把TKIP序列计数器(TSC)值由原来的48比特扩大到128比特,使其安全强度比RC4算法提高了约3个数量级。
     4.证明了CCMP加密协议的安全性和可靠性。分析表明,当AES算法的攻击成功率为O(n~2) * 2~(-128)时,CCMP的可靠性和机密性对应的攻击成功率分别为O(n) * 2~(-64)和O(n2) * 2~(-128),达到了预期的设计目标,可以满足公共无线局域网的安全需求。
     5.利用Bellare-Rogoway模型,对密码交换协议进行了可验安全性分析。证明了公共无线局域网采用的四步握手密钥交换机制的保密性和认证正确性;
     6.提出了一种增强的Bellare-Rogoway模型。采用该模型对802.1X认证协议进行了可验安全性分析,发现了该协议存在安全缺陷,容易遭受中间人攻击。在此基础上提出了一种攻击方法及改进措施。
     7.设计和实现了符合公共无线局域网技术规范的无线接入点和接入控制器。
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) * 2~(-128), the ad-vantage of attack successful probability to WEP algorithm is approximate O(n~2)*2~(-24)and the advantage of attack successful probability to TKIP is approximate O(n~3)*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) * 2~(-128), the advantages of attack successful probabilityon authenticity and privacy are approximate O(n)*2~(-64) and O(n~2)*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.
引文
[1] IEEE 802.11,Information technology―Telecommunications and information exchange between sys-tems―Local and metropolitan area networks―Specific requirements―Part 11: Wireless LANMedium Access Control (MAC) and Physical Layer(PHY) Specifications. Technical report, IEEE,1999.
    [2] IEEE802.11b,Supplement to IEEE Standard for Information technology―Telecommunicationsand information exchange between systems―Local and metropolitan area networks―Specific re-quirements―Part 11: Wireless LAN Medium Access control (MAC) and Physical Layer (PHY)specifications:Higher-Speed Physical Layer Extension in the 2.4GHz Band. Technical report, IEEE,1999.
    [3] IEEE802.11a,Supplement to IEEE Standard for information technology―Telecommunications andinformation exchange between systems―Local and metropolitan area networks―Specific re-quirements―Part 11: Wireless LAN Medium Access Control(MAC) and Physical Layer (PHY)specifications:High-speed Physical Layer in the 5 GHz Band. Technical report, IEEE, 1999.
    [4] IEEE802.11g,IEEE Standard for information technology-Telecommunications and information ex-change between systems-Local and metropolitan area networks-Specific requirements part 11: Wire-less LAN Medium Access control (MAC) and Physical Layer (PHY) specifications:Higher-SpeedPhysical Layer Extension in the 2.4GHz Band. Technical report, IEEE, 1999.
    [5] Wi-fi protected access (wpa). Technical Report Version: 1.2, Wi-Fi Alliance, 2003.
    [6] IEEE802.1x, IEEE Standard for Local and Metropolitan Area Networks – Port-Based Network Ac-cess Control. Technical report, IEEE, 2001.
    [7] IEEE802.11i,IEEE Standard for information technology-Telecommunications and information ex-change between systems-Local and metropolitan area networks-Specific requirements part 11: Wire-less LAN Medium Access control (MAC) and Physical Layer (PHY) specifications:Medium AccessControl (MAC) Security Enhancements. Technical report, IEEE, 2004.
    [8] Announcing the advanced encryption standard(aes). Technical Report FIPS197, NIST, November2001.
    [9] 信息技术-系统间远程通信和信息交换局域网和城域网-特定要求-第11 部分:无线局域网媒体访问控制和物理层规范. Technical Report GB 15629.11-2003, 中华人民共和国国家标准,2003.
    [10] Michael Burrows, Martin Abadi, and Roger Needham. A logic of authentication. Research Report39, Digital Systems Research Center, February 1989.
    [11] L. Gong, R. Needham, and R. Yahalom. Reasoning about belief in cryptographic protocols. InProceedings of the 1990 IEEE Computer society Symposium on Research in Security and Privacy,pages 234–248, Los Alamitos, California, 1990. IEEE, IEEE Computer Society Press.
    [12] R. Canetti and H. Krawczyk. Security analysis of ike’s signature-based key-exchange protocol. InAdvances in Cryptology - Proceedings of CRYPTO’02, Lecture Notes in Computer Science 2442,pages 143–161. Spinger Verlag, 2002.
    [13] M. Abadi and P. Rogaway. Reconciling two views of cryptography(the computational soundness offormal encryption). Journal of Cryptology, 15(2):103–127, 2002.
    [14] ETSI TS 101 475 v1.3.1 Technical Specification,Broadband Radio Access Net-works(BRAN);HIPERLAN Type 2;Physical(PHY) layer. Technical report, ETSI, 2001.
    [15] PARAMVIR BAHL, WILF RUSSELL, YI-MIN WANG, et al. Pawns: Satisfying the Need forUbiquitous Secure Connectivity and Location Services. IEEE Wireless Communications, 9:40–48,Feburary 2002.
    [16] Acharya Arup, Bisdikian Chatschik, Misra Archan, et al. airconn: A framework for tiered servicesin public wireless lan hot spots. IEEE Communications Magazine, 9:124–132, September 2004.
    [17] Acharya Arup, Bisdikian Chatschik, Misra Archan, et al. ts-pwlan: a value-add system for providingtiered wireless services in public hot-spots. In IEEE International Conference on Communications,ICC ’03, volume 1, pages 193–197, May 2003.
    [18] Anton B., Bullock B., and Short J. Best current practices for wireless internet service provider (wisp)roaming. Technical report, WiFi Alliance, February 2003.
    [19] Ala-Laurila Juha, Mikkonen Jouni, and Rinnemaa Jyri. Wireless lan access network architecture formobile operators. IEEE Communications Magazine, 39:82–89, November 2001.
    [20] Ahmavaara Kalle, Haverinen Henry, and Pichna Roman. Interworking architecture between 3gppand wlan systems. IEEE Communications Magazine, 41:74–81, November 2003.
    [21] Buddhikot M.M., Chandranmenon G., Seungjae Han, et al. Design and implementation of awlan/cdma2000 interworking architecture. IEEE Communications Magazine, 41:90–100, Novem-ber 2003.
    [22] Buddhikot M., Chandranmenon G., Han S., et al. Integration of 802.11 and third-generation wirelessdata networks. In INFOCOM 2003. Twenty-Second Annual Joint Conference of the IEEE Computerand Communications Societies, volume 1, pages 503–512, March 2003.
    [23] Thaison Dao, Chan H.A., and Rejeb J. Interworking between wireless lan and cdma2000. In The29th Annual Conference of the IEEE Industrial Electronics Society, IECON ’03, volume 2, pages1215–1220, November 2003.
    [24] Surtees A., McCann S., Hepworth E., et al. Combining w-isp and cellular interworking models forwlan. In 4th International Conference on 3G Mobile Communication Technologies, 3G 2003, pages259–263, June 2003.
    [25] Salkintzis A.K., Fors C., and Pazhyannur R. Wlan-gprs integration for next-generation mobile datanetworks. IEEE Wireless Communications, 9:112–124, October 2003.
    [26] Salkintzis A.K. Wlan/3g interworking architectures for next generation hybrid data networks. 2004IEEE International Conference on Communications, 7:3984–3988, June 2004.
    [27] 3rd generation partnership project; technical specification group services and system aspects; 3gppsystem to wireless local area network (wlan) interworking; system description(release 6). TechnicalReport TS 23.234.V.6.4.0, 3GPP, March 2005.
    [28] 3rd generation partnership project;technical specification group services and system as-pects;feasibility study on 3gpp system to wireless local area network (wlan) interworking (release6). Technical Report TR 22.934 V6.2.0, 3GPP, September 2003.
    [29] Requirements and architectures for interworking between hiperlan/3 and 3rd generation cellular sys-tems. Technical Report TR 101 957, ETSI, August 2001.
    [30] Hui Luo, Zhimei Jiang, Byoung-Jo Kim, et al. Integrating wireless lan and cellular data for theenterprise. IEEE Computer Society, 7:25–33, MARCH.APRIL 2003.
    [31] 曹秀英,耿嘉,沈平等编著. 无线局域网安全系统. 北京:电子工业出版社, 2004年3月.
    [32] Public wlan interworking study. Technical Report Document Revision 1.0, Intel, September 2004.
    [33] Koien G.M. and T. Haslestad. Security aspects of 3g-wlan interworking. IEEE CommunicationsMagazine, 41:82–88, November 2003.
    [34] D. Dolev and A.C. Yao. On the security of pubic key protocols. In Proceedings of IEEE 22nd AnnualSymposium on Foundations of Computer Science, pages 350–357, 1981.
    [35] Wenbo Mao. Modern Cryptography: Theory and Practice. Person Education, Inc., 2004.
    [36] M.R. Garey and D.S. Johnson. Computers and Intractability: A Guide to the Theory of NP-Completeness. Freeman, San Francisco, 1979.
    [37] S. GoldWasser and S. Micali. Probabilistic encryption. J. of Computer and System Sciences, 28:270–299, Apirl 1984.
    [38] S. Micali, C. Rackoff, and R. Sloan. The notion of security for probabilistic cryptosystems. SIAM J.of Computing, Apirl 1988.
    [39] A. C. YAO. Theory and applications of trapdoor functions. In Proceedings of the 23rd Symposiumon Foundations of Computer Science, IEEE, 1982.
    [40] O. Goldreich. A uniform complexity treatment of encryption and zero-knowledge. Journal of Cryp-tology, 6:21–53, 1993.
    [41] M. Luby. Pseudorandomness and Cryptiographic Applications. Princeton University Press, 1996.
    [42] M. Luby and C. Rackoff. How to construct pseudorandom permutations from pseudorandom func-tions. SIAM J. Computation, 17, April 1988.
    [43] M. Bellare and P. Rogaway. Random oracles are practical: a paradigm for designing efficient proto-cols. In First ACM Conference on Computer and Communications Security, pages 62–73, 1993.
    [44] R. Canetti, O. Goldreich, and S. Halevi. The random oracle methodology, revisited. In Proceedingsof the 30th Annual Symposium on the Theory of Computing(STOC’98), pages 209–218, 1998.
    [45] M. Bellare, J. Kilian, and P. Rogaway. The security of the cpher block chaining message authentica-tion code. Advances in Cryptology - Crypto ’94, LNCS, 839, 1994.
    [46] R L.Rivest. The rc4 encryption algorithm. USA, RSA Data Security, Inc, 17, Mar 1992.
    [47] M. Bellare and P. Rogaway. Entity authentication and key distribution. In Cryptology - Crypto 93Proceedings, Lecture Notes in Computer Science, volume 773, 1994.
    [48] M. Bellare and P. Rogaway. Provably secure session key distribution: the three party case. In Proc.27th Annual Symposium on the Theory of Computing, ACM, 1995.
    [49] M. Bellare, R. Canetti, and H. Krawczyk. A modular approach to the design and analysis of authen-tication and key exchange protocols. In Proc. 30th Annual Symposium on the Theory of Computing,ACM, 1998.
    [50] M. Bellare, D. Pointcheval, and P. Rogaway. Authenticated key exchange secure against dictionaryattacks. In Cryptology - Eurocrypt 2000 Proceedings, Lecture Notes in Computer Science, 2000.
    [51] Bruce Schneier and John Kelsey. Unbalanced feistel networks and block-cipher design. In FastSoftware Encryption, Third International Workshop Proceedings, Springer-Verlag, pages 121–144,February 1995.
    [52] Alex Biryukov and David Wagner. Slide attack. In Proceedings of FSE’99, 1999.
    [53] Mathieu Ciet, Gilles Piret, and Jean-Jacques Quisquater. Related-key and slide attack: Analysis,connections, and improvements. In 23rd Symposium on INFORMATION THEORY in the BENELUX,Louvain-la-Neuve, Belgium, pages 315–325, May 2002.
    [54] R. Lidl and H. Niederreiter. Introduction to finite fields and their applications. Cambridge UniversityPress, 1986.
    [55] D. Whiting, R. Housley, and N. Ferguson. Counter with cbc-mac(ccm). Technical report, NIST, June2002. http://csrc.nist.gov/encryption/modes/proposedmodes/.
    [56] Helger Lipmaa, Phillip Rogaway, and David Wagner. Ctr-mode encryption.http://csrc.nist.gov/encryption/modes/proposedmodes/.
    [57] NIST. Recommendation for block cipher modes of operation. Technical report, NIST, July 2001.
    [58] J. R. Walker. Unsafe at any key size; an analysis of the wep encapsulation. IEEE Document 802.11-00/362, October 2000.
    [59] D. Simon, Aboba B., and Moore T. Ieee 802.11 security and 802.1x. IEEE Document 802.11-00/034r1, March 2000.
    [60] E. Dawson and L. Nielsen. Automated cryptanalysis of xor plaintext strings. Cryptologia, pages165–181, April 1996.
    [61] Fluhrer S., Mantin I., and Shamir A. Weaknesses in the key scheduling algorithm of rc4. In EighthAnnual Workshop on Selected Areas in Cryptography, August 2001.
    [62] Stubblefield A., Ioannidis J., and Rubin A. Using the ?uhrer, mantin, and shamir attack to break wep.Technical report, AT&T Labs Technical Report TD-4ZCPZZ, 2001.
    [63] 耿嘉,曹秀英. 无线局域网中基于rc4的加密算法的分析与改进. 通信技术, 09:95–97, 2002.
    [64] Ying Wenping. Key hopping? - a security enhancement scheme for ieee 802.11 wep standards.Technical report, February 2002.
    [65] Abdalla M and Bellare M. Increasing the lifetime of a key: A comparative analysis of the securityof re-keying techniques. In Advances in Cryptology - ASIACRYPT 2000, Tatsuaki Okamoto, editorvolume 1976 of Lecture Notes in Computer Science, 2000.
    [66] Bellare M, Canetti R, and Krawczyk H. Keying hash funtions for message authentication. In Ad-vances in Cryptology - Crypto ’96, edited by Neal Koblitz, Lecture Notes in Computer Science,volume 1109, pages 1–15, 1996.
    [67] Rivest R. L. The rc4 encryption algorithm. Technical report, RSA Data Security, Inc, March 1992.
    [68] M. Bellare, A. Desai, E. Jokipii, et al. A concrete security treatment of symmetric encryption: Anal-ysis of the des modes of operation. In Proceedings of 38th Annual Symposium on Foundations ofComputer Science (FOCS 97), IEEE, 1997.
    [69] M. Bellare and C. Namprempre. Authenticated encryption: Relations among notions and analysis ofthe generic composition paradigm. In Advances in Cryptology - ASIACRYPT 2000, pages 531–545,2000.
    [70] M. Bellare and P. Rogaway. Encode-then-encipher encryption: How to exploit nonces or redundancyin plaintexts for efficient encryption. In Advances in Cryptology - ASIACRYPT 2000, pages 317–330,2000.
    [71] T. Dierks and C. Allen. Ietf rfc 2246: The tls protocol version 1.0. Technical report, IETF, January1999.
    [72] P. Rogaway, M. Bellare, J. Black, et al. Ocb: A block-cipher mode of operation for efficient au-thenticated encryption. Technical report, 8th ACM Conference on Computer and CommunicationsSecurity (CCS-8), 2001.
    [73] J. Daemen. Cipher and hash function design strategies based on linear and differential cryptanalysis.PhD thesis, K.U.Leuven, March 1995.

© 2004-2018 中国地质图书馆版权所有 京ICP备05064691号 京公网安备11010802017129号

地址:北京市海淀区学院路29号 邮编:100083

电话:办公室:(+86 10)66554848;文献借阅、咨询服务、科技查新:66554700