| Full text | Click to download. |
| Citation | In Proceedings of the 12th ACM Conference on
Computer and Communications Security, November 2005
|
| Authors | Changhua He
Mukund Sundararajan Anupam Datta Ante Derek John C. Mitchell |
The IEEE 802.11i wireless networking protocol 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 realted 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 protocols 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/TSL is widely used apart from 802.11i, the security proof for SSL/TLS has independent interest.