What seems the most interesting is how Masashi Kikuchi has discovered this flaw: he seems to have used Coq and modelised a part of the states and transitions of

What seems the most interesting is how Masashi Kikuchi has discovered this flaw: he seems to have used Coq and modelised a part of the states and transitions of the TLS handshake and then observed OpenSSL wasn't following this model. Very nice.