CISPA
Browse

A Formal Analysis of IEEE 802.11's WPA2: Countering the Kracks Caused by Cracking the Counters

Download (921.13 kB)
conference contribution
posted on 2023-11-29, 18:14 authored by Cas CremersCas Cremers, Benjamin Kiesl, Niklas MedingerNiklas Medinger
The IEEE 802.11 WPA2 protocol is widely used across the globe to protect network connections. The protocol, which is specified on more than three-thousand pages and has received various patches over the years, is extremely complex and therefore hard to analyze. In particular, it involves various mechanisms that interact with each other in subtle ways, which offers little hope for modular reasoning. Perhaps because of this, there exists no formal or cryptographic argument that shows that the patches to the core protocol indeed prevent the corresponding attacks, such as, e.g., the notorious KRACK attacks from 2017. In this work, we address this situation and present an extensive formal analysis of the WPA2 protocol design. Our model is the first that is detailed enough to detect the KRACK attacks; it includes mechanisms such as the four-way handshake, the group-key handshake, WNM sleep mode, the data-confidentiality protocol, and their complex interactions. Our analysis provides the first security argument, in any formalism, that the patched WPA2 protocol meets its claimed security guarantees in the face of complex modern attacks.

History

Preferred Citation

Cas Cremers, Benjamin Kiesl and Niklas Medinger. A Formal Analysis of IEEE 802.11's WPA2: Countering the Kracks Caused by Cracking the Counters. In: Usenix Security Symposium (USENIX-Security). 2020.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

Usenix Security Symposium (USENIX-Security)

Legacy Posted Date

2020-10-08

Open Access Type

  • Unknown

BibTeX

@inproceedings{cispa_all_3239, title = "A Formal Analysis of IEEE 802.11's WPA2: Countering the Kracks Caused by Cracking the Counters", author = "Cremers, Cas and Kiesl, Benjamin and Medinger, Niklas", booktitle="{Usenix Security Symposium (USENIX-Security)}", year="2020", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC