A modular correctness proof of IEEE 802.11i and TLS

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.

REFERENCES

• 1: IEEE Standard 802.11-1999. Local and metropolitan area networks - specific requirements - part 11: Wireless LAN Medium Access Control and Physical Layer specifications. 1999.
• 2: 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.
• 3: Verified By Visa. 2004. https://usa.visa.com/personal/security/vbv/.
• 4: Martín Abadi , Andrew D. Gordon, A calculus for cryptographic protocols: the spi calculus, Proceedings of the 4th ACM conference on Computer and communications security, p.36-47, April 01-04, 1997, Zurich, Switzerland [doi>10.1145/266420.266432]
• 5: 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.
• 6: Mihir Bellare , Phillip Rogaway, Entity authentication and key distribution, Proceedings of the 13th annual international cryptology conference on Advances in cryptology, p.232-249, January 1994, Santa Barbara, California, United States
• 7: Nikita Borisov , Ian Goldberg , David Wagner, Intercepting mobile communications: the insecurity of 802.11, Proceedings of the 7th annual international conference on Mobile computing and networking, p.180-189, July 2001, Rome, Italy [doi>10.1145/381677.381695]
• 8: Michael Burrows , Martin Abadi , Roger Needham, A logic of authentication, ACM Transactions on Computer Systems (TOCS), v.8 n.1, p.18-36, Feb. 1990 [doi>10.1145/77648.77649]
• 9: H. Cheung. FBI Teaches Lesson in how to break into Wi-Fi networks. Information Week Network Pipeline, 2005.
• 10: 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.
• 11: 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.
• 12: Anupam Datta , Ante Derek , John C. Mitchell , Dusko Pavlovic, Abstraction and Refinement in Protocol Derivation, Proceedings of the 17th IEEE Computer Security Foundations Workshop (CSFW'04), p.30, June 28-30, 2004 [doi>10.1109/CSFW.2004.4]
• 13: A. Datta, A. Derek, J. C. Mitchell, and D. Pavlovic. A derivation system and compositional logic for security protocols. Journal of Computer Security, 2005.
• 14: 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.
• 15: T. Dierks and C. Allen. The TLS Protocol --- Version 1.0. IETF RFC 2246, January 1999.
• 16: Whitfield Diffie , Paul C. Van Oorschot , Michael J. Wiener, Authentication and authenticated key exchanges, Designs, Codes and Cryptography, v.2 n.2, p.107-125, June 1992 [doi>10.1007/BF00124891]
• 17: Nancy Durgin , John Mitchell , Dusko Pavlovic, A Compositional Logic for Protocol Correctness, Proceedings of the 14th IEEE Workshop on Computer Security Foundations, p.241, June 11-13, 2001
• 18: Nancy Durgin , John Mitchell , Dusko Pavlovic, A compositional logic for proving security properties of protocols, Journal of Computer Security, v.11 n.4, p.677-721, 01/01/2004
• 19: Scott R. Fluhrer , Itsik Mantin , Adi Shamir, Weaknesses in the Key Scheduling Algorithm of RC4, Revised Papers from the 8th Annual International Workshop on Selected Areas in Cryptography, p.1-24, August 16-17, 2001
• 20: Changhua He , John C. Mitchell, Analysis of the 802.11i 4-way handshake, Proceedings of the 2004 ACM workshop on Wireless security, October 01-01, 2004, Philadelphia, PA, USA [doi>10.1145/1023646.1023655]
• 21: 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.
• 22: Gavin Lowe, A Hierarchy of Authentication Specifications, Proceedings of the 10th Computer Security Foundations Workshop (CSFW '97), p.31, June 10-12, 1997
• 23: 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.
• 24: Catherine Meadows, Open Issues in Formal Methods for Cryptographic Protocol Analysis, Proceedings of the International Workshop on Information Assurance in Computer Networks: Methods, Models, and Architectures for Network Security, p.21, May 21-23, 2001
• 25: C. Meadows and D. Pavlovic. Deriving, attacking and defending the GDOI protocol. In ESORICS, pages 53--72, 2004.
• 26: Jonathan Millen , Vitaly Shmatikov, Constraint solving for bounded-process cryptographic protocol analysis, Proceedings of the 8th ACM conference on Computer and Communications Security, November 05-08, 2001, Philadelphia, PA, USA [doi>10.1145/501983.502007]
• 27: John C. Mitchell, Finite-State Analysis of Security Protocols, Proceedings of the 10th International Conference on Computer Aided Verification, p.71-76, June 28-July 02, 1998
• 28: J. C. Mitchell , M. Mitchell , U. Stern, Automated analysis of cryptographic protocols using Mur/spl phi/, Proceedings of the 1997 IEEE Symposium on Security and Privacy, p.141, May 04-07, 1997
• 29: 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.
• 30: Vebjørn Moen , Håvard Raddum , Kjell J. Hole, Weaknesses in the temporal key hash of WPA, ACM SIGMOBILE Mobile Computing and Communications Review, v.8 n.2, April 2004 [doi>10.1145/997122.997132]
• 31: Lawrence C. Paulson, The inductive approach to verifying cryptographic protocols, Journal of Computer Security, v.6 n.1-2, p.85-128, Sept. 1998
• 32: Lawrence C. Paulson, Inductive analysis of the Internet protocol TLS, ACM Transactions on Information and System Security (TISSEC), v.2 n.3, p.332-351, Aug. 1999 [doi>10.1145/322510.322530]
• 33: L. C. Paulson. Verifying the SET protocol. In Proceedings of International Joint Conference on Automated Reasoning, 2001.
• 34: A. W. Roscoe, Intensional specifications of security protocols, Proceedings of the Ninth IEEE Computer Security Foundations Workshop, p.28, March 10-12, 1996
• 35: P. Ryan, S. Schneider, M. Goldsmith, G. Lowe, and A. Roscoe. Modelling and Analysis of Security Protocols. Addison-Wesley Publishing Co., 2000.
• 36: SETCo. SET Secure Electronic Transaction specification: Business description, 1997.
• 37: 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.
• 38: J. R. Walker. Unsafe at any key size; an analysis of the WEP encapsulation. In IEEE Document 802.11-00/362, 2000.

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.2 COMPUTER-COMMUNICATION NETWORKS
      C.2.2 Network Protocols

General Terms:
Security

Keywords:
IEEE 802.11i, TLS, protocol composition logic