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.
Integrity signals
Registry
Cites
Statistics
Claims the paper makes
The citation lists haven’t been fetched yet
References 36 · Cited by 121
- Authors
- He, C., Sundararajan, M., Datta, A., Derek, A., & Mitchell, J. C.
- Affiliations
- Stanford University (US)
- Stanford University, Stanford, CA
- Venue
- Proceedings of the 12th ACM conference on Computer and communications security
- Publisher
- ACM
- Published
- 2005-11-07
- Pages
- 2-15
- ISSN
- 1543-7221 (ISSN-L)
- OpenAlex
- W2165477067
- Cited by
- 121
- References
- 36
- Citations by year
- 2025: 1 · 2024: 1 · 2023: 2 · 2022: 1 · 2020: 4 · 2019: 6 · 2018: 5 · 2017: 5 · 2016: 7 · 2015: 10 · 2014: 5 · 2013: 9 · 2012: 7
- FWCI
- 6.92
- Type
- conference paper
- Language
- en
- Open access
- closed
- Locations
- ACM SIGSAC Conference on Computer and Communications Security (CCS) (publishedVersion)
- Topics
- Physical Sciences › Computer Science › Computer Networks and Communications › Advanced Authentication Protocols Security
- Physical Sciences › Computer Science › Artificial Intelligence › Security and Verification in Computing
- Physical Sciences › Computer Science › Computational Theory and Mathematics › Formal Methods in Verification
- Keywords
- IEEE 802.11i, TLS, formal verification, protocol correctness proofs, modular proofs, 802.1X authentication, EAP, 4-way handshake, wireless network security, mutual authentication, fault recovery
About these checks
Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.
Statistics and arithmetic are recomputed, not judged.
Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.
What counts as a claim ›How we measure confidence ›How we check this ›
Are you an author, or do you see a problem with this page? Request a review
