Modelling of 802.11 4-Way Handshake Attacks and Analysis of Security Properties

Rajiv Ranjan Singh, Jose Moreira-Sanchez, Tom Chothia, Mark Ryan

Research output: Chapter in Book/Report/Conference proceedingConference contribution


The IEEE 802.11 standard defines a 4-way handshake between a supplicant and an authenticator for secure communication. Many attacks such as KRACK, cipher downgrades, and key recovery attacks have been recently discovered against it. These attacks raise the question as to whether the implementation violates one of the required security properties or whether the security properties are insufficient. To the best of our knowledge, this is the first work that shows how to answer this question using formal methods. We model and analyse a variety of these attacks using the Tamarin prover against the security properties mandated by the standard for the 4-way handshake. This lets us see which security properties are violated. We find that our Tamarin models vulnerable to the KRACK attacks do not violate any of the standard’s security properties, indicating that the properties, as specified by the standard, are insufficient. We propose an additional security property and show that it is violated by systems vulnerable to KRACK attacks, and that enforcing this property is successful in stopping them. We demonstrate how to use Tamarin to automatically test the adequacy of a set of security properties against attacks, and that the suggested mitigations make 802.11 secure against these attacks.
Original languageEnglish
Title of host publicationSTM 2020: Security and Trust Management
Number of pages21
Publication statusPublished - 16 Sept 2020


Dive into the research topics of 'Modelling of 802.11 4-Way Handshake Attacks and Analysis of Security Properties'. Together they form a unique fingerprint.

Cite this