Formal modeling

The 4WHS protocol was described in detail in Section 2.2.3, and our formal modeling of it is shown in Figure 6.1. The 4WHS depends on a pseudorandom function PRF and a MAC scheme Σ = (MAC,Vrfy). We use the notation [x]_k^def= xσto denote a messagextogether with its MAC tagσ←MAC(k, x).

An IEEE 802.11 network is identified by its SSID. In the PSK setting each SSID is associated with a single 256 bit pairwise master key (PMK). However, the same SSID can be broadcasted by multiple different access points. This could happen either by chance if independent networks unknowingly configuring the same SSID, or deliberately if multiple access points are combined to form an extended service set (ESS) in order increase the coverage of the network. In the former case, the PMK will (usually) be different, while in the latter case the same PMK will be shared by all the access points of the ESS. Technically speaking, if two independent networks configure the same SSIDandPMK, then they are in fact part of the same ESS.

An access point can also broadcast multiple SSIDs at the same time, and hence belong to more than one ESS (using different PMKs). For simplicity we are going to assume that every ESS has a unique SSID. In the PSK setting all clients connecting to the same ESS will share the same PMK.

We are mostly going to ignore the details of the IEEE 802.11 frame format used in the real 4WHS protocol. For our purposes it is sufficient to model the four handshake messages as consisting of a nonce plus some value p_i = ix which uniquely determines each message m_i. If a received message does not match the expected format it is silently discarded.

Forp₁ in particular we moreover assume thatxis a constant, which means thatp₁itself is a constant. Thus, although the first handshake message lacks in-tegrity protection, an attacker can in effect only modify the nonce value because a client will always check that it matches the excepted format of “η_AP1x”.

Of course, a real IEEE 802.11 frame consists of many bit fields, but for message m₁they all have pre-determined values except for the nonce field. So modeling p₁ as a constant faithfully represents the real IEEE 802.11 frame.

For the other three handshake messages therearevariable bit fields that an attacker could potentially influence. But since these messages are protected by a MAC, the adversary will be unable to modify them (as we will show).

C AP

m1= (ηAP, p1) m2= [ηC, p2]_kμ m3= [ηAP, p3]_kμ

m4= [p4]_kμ

ηAP ← {0,1}^λ ηC← {0,1}^λ

P = MinMax(C, AP) η= MinMax(ηC, ηAP) kμkα←PRF(PMK, Pη)

P = MinMax(C, AP) η= MinMax(ηC, ηAP) kμkα←PRF(PMK, Pη) ifΣ.Vrfy(kμ, m2)= 1:

discardkμ,kα,m2

if ηAP =m1.ηAP or Σ.Vrfy(kμ, m3)= 1:

discardm3

Legend: [x]_kμ^def=xΣ.MAC(kμ, x)

Figure 6.1: Our formal model of the IEEE 802.11 4-Way Handshake protocol. The clientC and access pointAP share a symmetric key PMK.

Recall from Section 2.2.3 that prior to the 4WHS there is a negotiation phase where the client and access point agree upon the ciphersuite to use.

This includes the choice of PRFand Σ. In this section we assume that there is a single fixed ciphersuite being used. The topic of multi-ciphersuite and negotiation security will be treated in Section 6.4.

Identities in the 4WHS protocol are based on the parties’ 48 bit link-layer addresses. The functions min and max compute the minimum and maximum of two link-layer addresses when treated as 48 bit unsigned integers. In the following, let

MinMax(X, Y) = min{X, Y}||max{X, Y}. (6.1) The 4WHS protocol proceeds as follows.

1. The exchange begins with the access pointAP sending the messagem₁= η_APp₁to the clientC, whereη_AP is a 256 bit nonce andp₁is a constant.

2. On receivingm₁=η_APp₁, the client C generates its own 256 bit nonce η_C and derives apairwise transient key (PTK)as

PTK^def= k_μkk_α←PRF(PMK, Pη), (6.2) where P←MinMax(C, AP) andη←MinMax(η_C, η_AP).

The sub-keyk_αwill be the session key eventually output by the client in the 4WHS. The sub-keyk_μis the MAC key used to protect the handshake messages. The sub-key k is an encryption key used to protect a group

key GTK transmitted fromAP toC. Since we do not model any group aspect of IEEE 802.11 in this thesis, we ignore k and set it to be the empty stringε.

After deriving PTK,Ccreates and sends the next protocol messagem₂= [η_Cp₂]_kμ.

3. On receiving m₂ = [η_Cp2]_kμ, the access point AP derives the pairwise transient key PTK = k_μkα ← PRF(PMK, Pη) according to Equa-tion (6.2). With the sub-keyk_μ it verifies the MAC tag on m₂.

If the verification succeeds, then AP stores PTK ← k_μk_α as its PTK and sends out the third protocol messagem₃= [η_APp₃]_kμ. Additionally, AP, or rather the corresponding session at AP, sets the accept state to α=accepted(since the 4WHS does not consist of any sub-protocols, we simplify the accept vector α#»to a single valueα=α_F).

If the verification fails, thenAP silently discardsm₂, as well as the derived PTK, and continues running.

4. On receivingm₃= [η_APp₃]_kμ, the clientC checks thatη_AP is the same as the nonce it received in messagem₁(denoted “m₁.η_AP” in Figure 6.1) and verifies that the MAC tag on message m₃is valid.

If either of these checks fail, then C silently discards m₃ and continues running.

Otherwise,C sends out the final handshake message m₄= [p₄]_kμ. Addi-tionally, it sets its own acceptance state toα=accepted.

5. On receivingm₄, the access pointAP verifies the MAC with the keyk_μ. If the verification succeeds, then the 4WHS is over and AP is ready to receive encrypted messages under the keyk_α.

If the verification fails, thenAP silently discards the message and contin-ues running.

Note that the fourth handshake messagem₄serves no cryptographic purpose and could safely have been omitted. However, to stay true to the actual 4WHS protocol, we leave it in.

Note also that the error handling semantics of the 4WHS is different from protocols like TLS and SSH. Specifically, rather than rejecting immediately on receiving a bad message, a session will instead silently discard it. Combined with the fact that the key used to verify the handshake messages (k_μ) is derived from the handshake messages themselves, modeling the error handling seman-tics of the 4WHS protocol will make our analysis a little more complicated (specifically the proof of explicit entity authentication in Section 6.2.3).