Key reinstallation attacks: Forcing nonce reuse in WPA2

Wi-Fi networks are secured using a communications protocol called Wi-Fi Protected Access (WPA/2). The protocol defines how to exchange messages in order to create and maintain a secret (encrypted) communications service by what is known as a 4-way handshake. Vanhoef and Piessens identified design flaws in the 4-way handshake. All Wi-Fi clients that they tested were vulnerable to an attack against the handshake. This vulnerability (VU#228519) exploitation is known as a Key Reinstallation AttaCK (KRACK) and security patches to resolve the issue are available for many systems.

Under WPA/2, the decryption key is changed constantly to make it harder to guess. The first 2 messages of the handshake exchange counts (nonces and replay counters) so that the wifi access point and client know where in the sequence they are up to. The third message sends a new key based on those numbers. Under real-world conditions messages may be lost so the access point will resend the third message if it did not receive an appropriate response. This makes it possible for the client to receive the third message multiple times. To cope the client will use the key with this message and will reset its exchange count to match. An attacker may collect and resend the third message to a client forcing it to use the same key repetitively and undermine the security of communications. This could allow for the replay, decryption and forgery of messages.

Key reinstallation attacks can be mitigated by implementing a check as to whether an already-in-use key is being used and not reset associated counters in this case or assure that a particular key is only installed once during the handshake.

An interesting characteristic of this attack is that it does not violate the security properties of the handshake method as proven by formal analysis. This provides a lesson from this research that goes beyond the particular attack. It provides a clear example of how a formal proof of protocol security does not guarantee that its implementations are also secure. In this regard, formal proofs of security measures or counter-measures can be counterproductive as the community may lose interest in auditing implementations of a formally verified protocol. It also indicates the importance of precision and explicitness in the specification of protocols, as interpretation may differ from intent.

This research showed the limitations of the WPA/2 security protocol with regards to the implementation of the 4-way handshake. It also highlights an important lesson for the community by showing that a secure protocol does not make for a secure implementation.

Vous pourriez également aimer

Mots-clés