A modular correctness proof of IEEE 802.11i and TLS

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 in...

• Type: Conference
• Year: 2005
• Where: CCS
• Authors: Changhua He, Mukund Sundararajan, Anupam Datta, Ante Derek, John C. Mitchell
• Keywords: 802.11i, CCS 2005, IEEE 802.11i, Security Privacy, Wireless Networking Protocol