> 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!
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.
> 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.
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.
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!