CoChat
Sign Up
Cited by 21Advanced Authentication Protocols SecurityWireless Networks and ProtocolsSecurity and Verification in Computing

The DOI matches its DataCite record.

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

Open access
Cremers, Cas, Kiesl, Benjamin, Medinger, Niklas·2020·CISPA
DOI 10.60882/cispa.24613353
Open this paper in CoChat — free account

Abstract

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.

Overview

Integrity signals

Registry

DataCite · 10.60882/cispa.24613353

Cites

Statistics

Recomputing p-values needs the paper’s full text.

Verification

Claims the paper makes

We couldn’t retrieve this paper’s full text, so its claims and self-check weren’t run. The registry and citation checks still apply.

Claims other papers make about this one

Each is checked against this paper’s own text: does it say what the citing paper says it does?

  • The Cremers et al. (2020) protocols identify nonce-reuse weaknesses of underlying cryptographic algorithms, thereby improving the security of handshake mechanisms in 802.11 standards, and are security patches that manage nonce and replay counter reuses in 4-way handshake, group key handshake, WNM sleep mode, etc.

    “These protocols identify the nonce-reuse weaknesses of underlying cryptographic algorithms, thereby improving the security of handshake mechanisms in 802.11 standards, and are basically security patches that manage the nonce and replay counter reuses 4-way handshake, group key handshake, WNM sleep mode, etc.”

    From Multi-Channel Man-in-the-Middle attacks against protected Wi-Fi networks: A state of the art review (2022) · cites this paper as Cremers et al., 2020

  • Cremers et al. (2020) enhanced previous stage 2 defense mechanisms by developing completely new handshake protocols for preventing different forms of key reinstallation attacks.

    “(Cremers et al., 2020) have enhanced previous stage 2 defense mechanisms by developing completely new handshake protocols for preventing different forms of key reinstallation attacks.”

    From Multi-Channel Man-in-the-Middle attacks against protected Wi-Fi networks: A state of the art review (2022) · cites this paper as Cremers et al., 2020

  • There is no evidence that the formal models by Cremers et al. (2020) and Singh et al. (2020) are tested in real-world attack scenarios.

    “However, there is no evidence that these formal models are tested in realworld attack scenarios.”

    From Multi-Channel Man-in-the-Middle attacks against protected Wi-Fi networks: A state of the art review (2022) · cites this paper as Cremers et al., 2020

Citations

Cites

Still being checked.

Cited by

Sorted by citations

Related

Metadata

Authors
Cremers, C., Kiesl, B., & Medinger, N.
Affiliations
Helmholtz Center for Information Security (DE)
ORCID
Venue
CISPA
Publisher
CISPA
Published
2020-08-01
Pages
1-17
DOI
10.60882/cispa.24613353
OpenAlex
W3047818225
Cited by
20
References
0
Citations by year
2023: 13 · 2022: 4 · 2021: 2 · 2020: 1
FWCI
4.19
Type
conference paper
Language
en
Open access
Licence
rightsstatements.org/vocab/InC/1.0/
Locations
  • Figshare (submittedVersion)
  • CISPA Helmholtz Center
  • USENIX Security Symposium
Topics
  • Physical Sciences › Computer Science › Computer Networks and Communications › Advanced Authentication Protocols Security
  • Physical Sciences › Computer Science › Computer Networks and Communications › Wireless Networks and Protocols
  • Physical Sciences › Computer Science › Hardware and Architecture › Security and Verification in Computing
Keywords
WPA2, IEEE 802.11, formal verification, wireless LAN security, four-way handshake, data confidentiality

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