A Modular Correctness Proof of IEEE 802.11i and TLS

Full textClick to download.
CitationIn Proceedings of the 12th ACM Conference on Computer and Communications Security, November 2005
AuthorsChanghua 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.

Back to publications
Back to previous page