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

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

Standard

Modelling of 802.11 4-Way Handshake Attacks and Analysis of Security Properties. / Singh, Rajiv Ranjan; Moreira-Sanchez, Jose; Chothia, Tom; Ryan, Mark.

STM 2020: Security and Trust Management . Springer, 2020. p. 3.

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

Harvard

APA

Vancouver

Author

Singh, Rajiv Ranjan ; Moreira-Sanchez, Jose ; Chothia, Tom ; Ryan, Mark. / Modelling of 802.11 4-Way Handshake Attacks and Analysis of Security Properties. STM 2020: Security and Trust Management . Springer, 2020. pp. 3

Bibtex

@inproceedings{07d449127cb040498122147863a66013,
title = "Modelling of 802.11 4-Way Handshake Attacks and Analysis of Security Properties",
abstract = "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{\textquoteright}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.",
author = "Singh, {Rajiv Ranjan} and Jose Moreira-Sanchez and Tom Chothia and Mark Ryan",
year = "2020",
month = sep,
day = "16",
doi = "10.1007/978-3-030-59817-4_1",
language = "English",
pages = "3",
booktitle = "STM 2020: Security and Trust Management",
publisher = "Springer",

}

RIS

TY - GEN

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

AU - Singh, Rajiv Ranjan

AU - Moreira-Sanchez, Jose

AU - Chothia, Tom

AU - Ryan, Mark

PY - 2020/9/16

Y1 - 2020/9/16

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-030-59817-4_1

DO - 10.1007/978-3-030-59817-4_1

M3 - Conference contribution

SP - 3

BT - STM 2020: Security and Trust Management

PB - Springer

ER -