ANALYSIS OF SECURITY PROTOCOLS FOR WIRELESS NETWORKS A DISSERTATION SUBMITTED TO THE DEPARTMENT OF ELECTRICAL ENGINEERING AND THE COMMITTEE ON GRADUATE STUDIES OF STANFORD UNIVERSITY IN PARTIAL FULFILLMENT OF THE REQUIREMENTS FOR THE DEGREE OF DOCTOR OF PHILOSOPHY Changhua He December 2005 UMI Number: 3197441 INFORMATION TO USERS The quality of this reproduction is dependent upon the quality of the copy submitted. Broken or indistinct print, colored or poor quality illustrations and photographs, print bleed-through, substandard margins, and improper alignment can adversely affect reproduction. In the unlikely event that the author did not send a complete manuscript and there are missing pages, these will be noted. Also, if unauthorized copyright material had to be removed, a note will indicate the deletion.
® UMI UMI Microform 3197441 Copyright 2006 by ProQuest Information and Learning Company. All rights reserved. This microform edition is protected against unauthorized copying under Title 17, United States Code. ProQuest Information and Learning Company 300 North Zeeb Road P.
Box 1346 Ann Arbor, MI 48106-1346 © Copyright by Changhua He 2006 All Rights Reserved il I certify that I have read this dissertation and that, in my opinion, it is fully adequate in scope and quality as a dissertation for the degree of Doctor of Philosophy. Mitchell (Principal Advisor) I certify that I have read this dissertation and that, in my opinion, it is fully adequate in scope and quality as a dissertation for the degree of Doctor of Philosophy. Sibley Fouad Tobagi (C4 Advisor) I certify that I have read this dissertation and that, in my opinion, it is fully adequate in scope and quality as a dissertation for the degree of Doctor of Philosophy. Dan Boneh Approved for the University Committee on Graduate Studies.
1H Abstract Security is a serious concern in wireless networks. In order to eliminate the vulner- abilities in previous Standards, the IEEE 802.11i Standard is designed to provide security enhancements in MAC layer. The authentication process consists of several components, including an 802.1X authentication phase using TLS over EAP, a 4-Way Handshake to establish a fresh session key, and an optional Group Key Handshake for group communications. The objective of this work is to analyze IEEE 802.111 with respect to data confidentiality, integrity, mutual authentication, and availability.
Under our threat model, 802.11i appears to provide effective data confidentiality and integrity when CCMP is used.11i may also provide satisfactory mutual au- thentication and key management, although there are some potential implementation oversights that may cause severe problems. On the other hand, we identified several Denial of Service attacks. Different solutions are proposed for these vulnerabilities, which result in an improved variant of 802.111 with a more effecient failure recovery mechanism. Some of the resulting improvements have been adopted by the IEEE 802.11 TGi in their final deliberation.
We used a finite-state verification tool, called Murd, to analyze the 4-Way Hand- shake component. Our result shows that finite-state verification is quite effective for analyzing security protocols. Furthermore, we adopted Protocol Composition Logic to conduct a correctness proof of 802.11i, including SSL/TLS as a component. The proof is modular, comprising a separate proof for each protocol component and providing insight into the networking environment in which each component can be reliably used.
Finally, we showed that 802.111 can significantly reduce the complexity of designing a secure routing protocol when it is deployed in wireless ad hoc networks. iv Acknowledgements I am very fortunate to have an advisor, Professor John C. Mitchell, who is extremely insightful and open-minded. I have learned a lot from his knowledge and research methodology.
I am grateful to his support and guidance during my hard time in graduate study. I would like to thank Professor Fouad Tobagi, who is my associate advisor. He gave me great advice and assistance on graduate studies at Stanford. My sincere thanks also go to Professor Dan Boneh, not only for serving on my oral and reading committee, but also for teaching excellent classes in cryptography and security, which helped my research in a significant way.
It was a wonderful experience for me to be a part of the security laboratory at Stanford. I would like to thank Anupam Datta, Ante Derek, and Mukund Sundarara- jan for their collaborations on the research. Thanks also go to my cheery office mates for the interesting discussions, previously Ajith Ramanathan, now Arnab Roy and Adam Barth. All my friends at Stanford help make my life in graduate school memorable.
In particular, | want to express my gratitude towards Xirong Jiang, Meng Gu, Shuguang Cui, Hai Lan, Minhui Han, Rui Zhang, Qihua Ran, Ruixuan Zhao, Sixin Ma, Zhonghua Zhang, and Junbo Wu. They bring me lots of happiness. My deepest thanks go to my family, most of whom are far away from me most of time though. I can never achieve any of this without their dedication.
Finally, I am grateful to Mr. Chambers, for their generous donation to the Stanford Graduate Fellowship (SGF), which financially enabled my graduate study at Stanford. Contents Abstract Acknowledgements vi 1 Introduction eNCmowYO2 1.2 Link Layer vs. Upper Layer Authentication .2 Wireless Security Evolution .21 Data Confidentiality, Integrity, Authentication.2 Availability and DoS Attacks.
Qua và gà va 11 2 IEEE 802.2 Data Confidentiality and Integrity.3 Authentication and Key Management.1 RSNA Establishment Procedure.2 RSNA Security Analysis .3 Security Level Rollback Attack .1 Known DoS Attacks and Defenses.2 Michael Algorithm Countermeasure.4 4-Way Handshake Blocking. vn gà kg và g v.v va 44 Finite-State Verification 46 3.1 Finite-State Verification ©. pee eee A7 311 The Mur@ Model Checker .2 The Verification Procedure. gà gà va 50 3.2 Verification of the 4-Way Handshake .1 The 4-Way Handshake .2 The Protocol Model .3 The Protocol Clariicatons.1 The DoS attack.1 Random-Drop Queue.
0Q Lạ và va 65 3. g vn và vn và va 66 A Modular Correctness Proof 68 Al Overview.2 The Proof Method. Quà và vàn 74 4. LH Là và va 76 4.4 Improved 4-Way Handshake .4 Group Key Handshake .1 Modelling Group Key Handshake.
ii I IIắẳắẳăặa á. nu g g va v và Ta 94 Using 802.111 in Ad Hoc Routing 96 5.2 Dynamic Source Routing with 80211i.1 The Original DSR .2 The Improved DSR.32 One Malicious Node .3 Multiple Compromised Nodes. c Q c cv ng gà gà xà và và vàn a 109 Conclusions 111 6.2 Finite-State Verification. A Modular Correctness Proof .1liin Ad Hoc Routing.
A Protocol Composition Logic 119 A.1 Axioms for Protocol Actions .2 Axioms for PTK derivation. 00080 ee eee eee 123 A.4 Encryption and Signature .8 Axioms and Rules for Temporal Ordering.9 Honesty Rule 125 B Proof of the 4-Way Handshake Guarantee 126 Bibliography 132 ix List of Tables 4.1 4-Way Handshake Program .2 4-Way Handshake Precondition and Invariants .3 TLS: Client and Server Programs. Q ng và và kg va 85 4.5 Group Key Handshake Programs .6 Group-Key Protocol Precondition and Invariants. 89 List of Figures 2.1 RSNA Establishment Procedure.2 Security Level Rollback Attack .3 Reflection Attack on the 4-Way Handshake.4 TKIP MPDU Format.
eee ee ee 32 2.5 RSN Information Element Format.6 RSN IE Poisoning.7 4-Way Handshake Blocking .8 A Flow Chart of the Improved 802111.1 The Idealized 4-Way Handshake Protocol.2 The Simplified 4-Way Handshake Protocol.3 The one-message attack on the 4-Way Handshake protocol .4 Effectiveness of random-drop queue .2 Arrows-and-messages vs cords .1 DSR route discovery. Q Q Q Q Q L Q Q Q ng và xa va 100 9.2 DSR Shortest Path Property.3 The set of routes DSR can return .4 The set of returned routes with one malicious node .5 The set of returned routes with multiple malicious nodes .6 The rate limit problem .000000 eee 109 xi List of Acronyms AAA Authentication, Authorization, and Accounting ACL Access Control List AES Advanced Encryption Standard AP Access Point ARP Address Resolution Protocol BSS Basic Service Set CBC-MAC Cipher Block Chaining Message Authentication Code CCA Clear Channel Assessment CCM Counter with CBC-MAC CCMP Counter-mode/CBC-MAC Protocol CRC Cyclic Redundancy Checksum DoS Denial of Service DSR Dynamic Source Routing DSSS Direct Sequence Spread Spectrum EAP Extensible Authentication Protocol EAPOL Extensible Authentication Protocol Over Local Area Network EAP-TLS Extensible Authentication Protocol - Transport Layer Security FCS Frame Check Sequence FHSS Frequency Hopping Spread Spectrum FSM Finite-State Machine GTK Group Transient Key ICMP Internet Control Message Protocol ICV Integrity Check Value Xil IEEE Institute of Electrical and Electronics Engineers IPsec Internet Protocol Security IV Initialization Vector KCK Key Confirmation Key KEK Key Encryption Key LAN Local Area Network MAC Media Access Control MIC Message Integrity Code MitM Man-in-the-Middle MPDU MAC Protocol Data Unit MSDU MAC Service Data Unit NIC Network Interface Card MSK Master Session Key OFDM Orthogonal Frequency Division Multiplexing PCL Protocol Composition Logic PHY PHYsical Layer PMK Pairwise Master Key PMKID Pairwise Master Key Identifier PRF Pseudo Random Function PSK Pre-Shared Key PTK Pairwise Transient Key RADIUS Remote Authentication Dial In User Service RC4 Rivest Cipher 4 (Ron’s Code) RF Radio Frequency RSNA Robust Security Network Association RSN IE Robust Security Network Information Element SET Secure Electronic Transaction SIFS Short Inter-Frame Space SSH Secure SHell SSID Service Set [Dentifier SSL Secure Sockets Layer X11 TK Temporal Key TKIP Temporal Key Integrity Protocol TLS Transport Layer Security TPTK Temporary Pairwise Transient Key TSC TKIP Sequence Counter TSN Transient Security Network VPN Virtual Private Network WEP Wired Equivalent Protocol WiFi Wireless Fidelity WiMAX Worldwide Interoperability for Microwave Access WLAN Wireless Local Area Network WPA WiFi Protected Access XIV Chapter 1 Introduction Wireless networks represent a rapidly emerging area of growth and importance for providing ubiquitous networking connections. The common technologies can be clas- sified into different categories according to the range of the service area. On a world- wide scale, telecommunication companies have been making significant progress in carrying voice and data traffic over their cellular networks; furthermore, the next generation infrastructure, under developpment all over the world, aims to provide higher bandwidth and better quality for multimedia traffic.
In a metropolitan area, WiMAX (IEEE 802.16) can provide users with high-speed broadband access to the Internet. In a local area, WiFi (IEEE 802.11) enables users to establish wireless con- nections within a corporate or campus building. Moreover, in a personal area (often less than 10 meters), bluetooth (IEEE 802.15) can provide low-cost and short-range connectivity for portable devices. The focus of this dissertation is Wireless Local Area Networks (WLAN) based on IEEE 802.
Compared with the current cellular networks, a WLAN system has much higher transmission rates and shorter transmission range; hence, it is suitable for home networking, small business, and large corporations and has been widely deployed since IEEE 802.11b first appeared in 1999. However, along with the popularity of WLAN, security is a serious concern because the wireless medium is open for public access within a certain range. In 2001, Shipley [95] invented the first “War-driving” in the Bay Area to find CHAPTER 1. INTRODUCTION 2 existing wireless networks.
By driving a car along certain route through a district, people can discover the operating Access Points (APs), the corresponding Service Set Identifier (SSID), and even the physical locations of the APs, with only mod- erate equipment [33]. Obviously these capabilities release sensitive information and unauthorized services to an outsider. Furthermore, if the discovered APs are not well-configured, the outsider is able to exploit bandwidth for free Internet access, steal confidential data for malicious usage, or install advanced attacks from this open base. Even worse, the legitimate user may be unaware of these activities because the outsider can physically stay inside his car along the road or in the parking lot.
These dangers impose necessary requirements on the security of WLAN implementations.1 Security Requirements In a general network system, security has different contexts depending on different applications, among which the essential requirements are data confidentiality and integrity, authentication, and availability. Data Confidentiality and Integrity The network MUST provide strong data confidentiality, integrity, and replay protection for every transmitted message.