4 ms·
We did formally verify the 802.11i protocol, though: https://link.springer.com/article/10.1007%2Fs12204-009-0122-3?LI=true https://link.springer.com/article/10.
by munin 9y ago
We did formally verify the 802.11i protocol, though: https://link.springer.com/article/10.1007%2Fs12204-009-0122-3?LI=true https://link.springer.com/article/10.1007%2Fs12204-009-0122-...
- scott_karana 9y agoAnd the implementations ignored all the fundamental "nonces should never be used" part of the formal handshake protocol, and thus would have failed the aforementioned testing.
- tom_mellior 9y agoQuestion about this, because the featured article strangely doesn't actually say what the problem is: Did this verification result simply forget/not consider nonce reuse? The article seems to imply there's nothing wrong with the proof or the statement of the properties to be proved, it's about integration with another component. But if "don't reuse nonces" is a standard security property to verify, then I would think that that is a hole in the verification. Could someone shed more light on this?
- kruczek 9y agoIt is covered in Q&A at https://www.krackattacks.com/#faq https://www.krackattacks.com/#faq - basically the proof didn't cover this particular scenario: > The 4-way handshake was mathematically proven as secure. How is your attack possible? > The brief answer is that the formal proof does not assure a key is installed once. Instead, it only assures the negotiated key remains secret, and that handshake messages cannot be forged.