More interesting than the attack itself is their overall effort of combining formal verification with protocol implementation. Along the way, they've found all these problems in the <i>other</i> protocols because they didn't use such rigorous methods. Quite an argument in favor of using high assurance techniques for at least critical, slow-changing protocols like TLS.<p>Anyway, I found this paper...<p><a href="http://www.ieee-security.org/TC/SP2015/papers-archived/6949a535.pdf" rel="nofollow">http://www.ieee-security.org/TC/SP2015/papers-archived/6949a...</a><p>...that reminds me of older, high assurance designs. The classic way to do it is the so-called abstract or interacting state machine models. Each component is a state-machine where you know every successful or failure state that can happen plus argument security is maintained. Then, you compose these in a semi-functional way to describe overall system. Seems the miTLS people did something similar for theirs that they call "composite, state machines." The result was clean implementation and verification of what got really messy in other protocol engines. Plus, new techniques for handling that of course.<p>Really good stuff. Worth extending and improving in new projects.