3 ms·

> In the end we all know that the answer is for humans to stop doing this work. We need machine-assisted verification of protocols, preferably tied to the actua

> In the end we all know that the answer is for humans to stop doing this work. We need machine-assisted verification of protocols, preferably tied to the actual source code that implements them. This would ensure that the protocol actually does what it says, and that implementers don’t further screw it up, thus invalidating the security proof. And yet, there are still regular posts here about whether static type systems have any merit at all... never mind advanced things like linear/dependent types, theorem provers, TLA+, etc. Just use Go!

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 ago
  And 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 ago
  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.

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 ago
And 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 ago
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.