3 ms·

Question about this, because the featured article strangely doesn't actually say what the problem is: Did this verification result simply forget/not consider no

Question 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 ago
It 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.