> there is no formal description of the 802.11i handshake state machine.
Here is what the paper actually says:
The 802.11i amendment does not contain a formal state machine describing how the supplicant must implement the 4-way handshake. ... Fortunately, 802.11r ... does provide a detailed state machine of the supplicant.
The problem, as I understand it, was that when the protocol was formally verified, the properties checked were only the escape of the private key and identity related issues. The property of the nonce never being reset was simply not considered.
The missing piece, then, wasn't a precise description of how the system works, but rather a precise list of what it's supposed to guarantee. Without a clear and concise description of the requirements, it's hard to verify that the system satisfies them. Alternatively, it's possible that the list of guarantees was complete, in which case reviewers should have noticed that no nonce reset isn't one of them, yet it's required for the security of certain communication protocols used over the channel.
Here is what the paper actually says:
The 802.11i amendment does not contain a formal state machine describing how the supplicant must implement the 4-way handshake. ... Fortunately, 802.11r ... does provide a detailed state machine of the supplicant.
The problem, as I understand it, was that when the protocol was formally verified, the properties checked were only the escape of the private key and identity related issues. The property of the nonce never being reset was simply not considered.
The missing piece, then, wasn't a precise description of how the system works, but rather a precise list of what it's supposed to guarantee. Without a clear and concise description of the requirements, it's hard to verify that the system satisfies them. Alternatively, it's possible that the list of guarantees was complete, in which case reviewers should have noticed that no nonce reset isn't one of them, yet it's required for the security of certain communication protocols used over the channel.