Changhua He
John C. Mitchell
ABSTRACT
The IEEE 802.11i wireless networking protocol provides mutual authentication between a network access point and user devices prior to user connectivity. The protocol consists of several parts, including an 802.1X authentication phase using TLS over EAP, the 4-Way Handshake to establish a fresh session key, and an optional Group Key Handshake for group communications. Motivated by previous vulnerabilities in related wireless protocols and changes in 802.11i to provide better security, we carry out a formal proof of correctness using a Protocol Composition Logic previously used for other protocols. The proof is modular, comprising a separate proof for each protocol section and providing insight into the networking environment in which each section can be reliably used. Further, the proof holds for a variety of failure recovery strategies and other implementation and configuration options. Since SSL/TLS is widely used apart from 802.11i, the security proof for SSL/TLS has independent interest.
- IEEE Standard 802.11-1999. Local and metropolitan area networks - specific requirements - part 11: Wireless LAN Medium Access Control and Physical Layer specifications. 1999.]]Google Scholar
- IEEE P802.11i/D10.0. Medium Access Control (MAC) security enhancements, amendment 6 to IEEE Standard for local and metropolitan area networks part 11: Wireless Medium Access Control (MAC) and Physical Layer (PHY) specifications. April 2004.]]Google Scholar
- Verified By Visa. 2004. https://usa.visa.com/personal/security/vbv/.]]Google Scholar
- M. Abadi and A. D. Gordon. A calculus for cryptographic protocols The Spi Calculus. In Proceedings of Fourth ACM Conference on Computer and Communications Security, 1997.]] Google ScholarDigital Library
- W. A. Arbaugh, N. Shankar, and J. Wang. Your 802.11 network has no clothes. In Proceedings of the First IEEE International Conference on Wireless LANs and Home Networks, pages 131--144, 2001.]]Google ScholarCross Ref
- M. Bellare and P. Rogaway. Entity authentication and key distribution. In Advances in Cryprtology - Crypto'93 Proceedings. Springer-Verlag, 1994.]] Google ScholarDigital Library
- N. Borisov, I. Goldberg, and D. Wagner. Intercepting mobile communications: the insecurity of 802.11. In Proceedings of the 7th Annual International Conference on Mobile Computing and Networking, 2001.]] Google ScholarDigital Library
- M. Burrows, M. Abadi, and R. Needham. A logic of authentication. ACM Transactions on Computer Systems, 8(1):18--36, 1990.]] Google ScholarDigital Library
- H. Cheung. FBI Teaches Lesson in how to break into Wi-Fi networks. Information Week Network Pipeline, 2005.]]Google Scholar
- A. Datta, A. Derek, J. Mitchell, V. Shmatikov, and M. Turuani. Probabilistic polynomial-time semantics for a protocol security logic. In Int'l Colloquium on Automata, Languages, and Programming (ICALP), 2005.]] Google ScholarDigital Library
- A. Datta, A. Derek, J. C. Mitchell, and D. Pavlovic. A derivation system for security protocols and its logical formalization. In Proceedings of 16th IEEE Computer Security Foundations Workshop, pages 109--125. IEEE, 2003.]]Google ScholarCross Ref
- A. Datta, A. Derek, J. C. Mitchell, and D. Pavlovic. Abstraction and refinement in protocol derivation. In Proceedings of 17th IEEE Computer Security Foundations Workshop, pages 30--45. IEEE, 2004.]] Google ScholarDigital Library
- A. Datta, A. Derek, J. C. Mitchell, and D. Pavlovic. A derivation system and compositional logic for security protocols. Journal of Computer Security, 2005.]] Google ScholarDigital Library
- A. Datta, A. Derek, J. C. Mitchell, and D. Pavlovic. Secure protocol composition. In Proceedings of 19th Annual Conference on Mathematical Foundations of Programming Semantics, volume 83 of Electronic Notes in Theoretical Computer Science, 2004.]]Google Scholar
- T. Dierks and C. Allen. The TLS Protocol --- Version 1.0. IETF RFC 2246, January 1999.]] Google ScholarDigital Library
- W. Diffie, P. C. V. Oorschot, and M. J. Wiener. Authentication and authenticated key exchanges. Des. Codes Cryptography, 2(2):107--125, 1992.]] Google ScholarDigital Library
- N. Durgin, J. C. Mitchell, and D. Pavlovic. A compositional logic for protocol correctness. In Proceedings of 14th IEEE Computer Security Foundations Workshop, pages 241--255. IEEE, 2001.]] Google ScholarDigital Library
- N. Durgin, J. C. Mitchell, and D. Pavlovic. A compositional logic for proving security properties of protocols. Journal of Computer Security, 11:677--721, 2003.]] Google ScholarDigital Library
- S. Fluhrer, I. Mantin, and A. Shamir. Weaknesses in the key scheduling algorithm of RC4. In Proceedings of the 8th Annual International Workshop on Selected Areas in Cryptography, pages 1--24, 2001.]] Google ScholarDigital Library
- C. He and J. C. Mitchell. Analysis of 802.11i 4-way handshake. In Proceedings of the Third ACM International Workshop on Wireless Security (WiSe'04), 2004.]] Google ScholarDigital Library
- C. He and J. C. Mitchell. Security analysis and improvements for IEEE 802.11i. In Proceedings of the 12th Annual Network and Distributed System Security Symposium (NDSS'05), 2005.]]Google Scholar
- G. Lowe. A hierarchy of authentication specifications. In Proceedings of the 10th Computer Security Foundations Workshop (CSFW'97), page 31, Washington, DC, USA, 1997. IEEE Computer Society.]] Google ScholarDigital Library
- C. Meadows. A model of computation for the NRL protocol analyzer. In Proceedings of 7th IEEE Computer Security Foundations Workshop, pages 84--89. IEEE, 1994.]]Google ScholarCross Ref
- C. Meadows. Open issues in formal methods for cryptographic protocol analysis. Lecture Notes in Computer Science, 2052:21--36, 2001.]] Google ScholarDigital Library
- C. Meadows and D. Pavlovic. Deriving, attacking and defending the GDOI protocol. In ESORICS, pages 53--72, 2004.]]Google ScholarCross Ref
- J. K. Millen and V. Shmatikov. Constraint solving for bounded-process cryptographic protocol analysis. In Proceedings of ACM Conference on Computer and Communications Security, pages 166--175, 2001.]] Google ScholarDigital Library
- J. C. Mitchell. Finite-state analysis of security protocols. In Computer Aided Verification, pages 71--76, 1998.]] Google ScholarDigital Library
- J. C. Mitchell, M. Mitchell, and U.Stern. Automated analysis of cryptographic protocols using murphi. In IEEE Symp. Security and Privacy, pages 141--153, 1997.]] Google ScholarDigital Library
- J. C. Mitchell, V. Shmatikov, and U. Stern. Finite-state analysis of SSL 3.0. In Proceedings of Seventh USENIX Security Symposium, pages 201--216, 1998.]] Google ScholarDigital Library
- V. Moen, H. Raddum, and K. J. Hole. Weakness in the temporal key hash of WPA. ACM SIGMOBILE Mobile Computing and Communications Review, 8:76--83, 2004.]] Google ScholarDigital Library
- L. C. Paulson. The inductive approach to verifying cryptographic protocols. Journal of Computer Security, 6:85--128, 1998.]] Google ScholarDigital Library
- L. C. Paulson. Inductive analysis of the Internet protocol TLS. ACM Transactions on Computer and System Security, 2(3):332--351, 1999.]] Google ScholarDigital Library
- L. C. Paulson. Verifying the SET protocol. In Proceedings of International Joint Conference on Automated Reasoning, 2001.]]Google Scholar
- A. W. Roscoe. Intensional specifications of security protocols. In Proceedings of the Ninth IEEE Computer Security Foundations Workshop (CSFW'96), page 28, Washington, DC, USA, 1996. IEEE Computer Society.]] Google ScholarDigital Library
- P. Ryan, S. Schneider, M. Goldsmith, G. Lowe, and A. Roscoe. Modelling and Analysis of Security Protocols. Addison-Wesley Publishing Co., 2000.]]Google Scholar
- SETCo. SET Secure Electronic Transaction specification: Business description, 1997.]]Google Scholar
- F. J. Thayer-Fábrega, J. C. Herzog, and J. D. Guttman. Strand spaces: Why is a security protocol correct? In Proceedings of the 1998 IEEE Symposium on Security and Privacy, pages 160--171, Oakland, CA, May 1998. IEEE Computer Society Press.]]Google Scholar
- J. R. Walker. Unsafe at any key size; an analysis of the WEP encapsulation. In IEEE Document 802.11-00/362, 2000.]]Google Scholar
Index Terms
- A modular correctness proof of IEEE 802.11i and TLS
Recommendations
Authenticated Confidential Channel Establishment and the Security of TLS-DHE
Transport Layer Security (TLS) is the most important cryptographic protocol in use today. However, finding a cryptographic security proof for the complete, unaltered protocol has proven to be a challenging task. We give the first such proof in the ...
On the Security of TLS-DHE in the Standard Model
Proceedings of the 32nd Annual Cryptology Conference on Advances in Cryptology --- CRYPTO 2012 - Volume 7417TLS is the most important cryptographic protocol in use today. However, up to now there is no complete cryptographic security proof in the standard model, nor in any other model. We give the first such proof for the core cryptographic protocol of TLS ...
The TLS Handshake Protocol: A Modular Analysis
We study the security of the widely deployed Secure Session Layer/Transport Layer Security (TLS) key agreement protocol. Our analysis identifies, justifies, and exploits the modularity present in the design of the protocol: the application keys offered ...
Comments