That protocols without security proofs can survive in the real world, and protocols with security proofs still fall to implementation bugs, and that if you were going to bet on incidence of protocol design flaws vs. implementation flaws, the safe bet is on implementation flaws.
The level of civility in this thread is great, but I would pay money to see a DEF CON panel debate between you two where you each had to take a shot every 8 minutes. We could get Mikko Hypponen to moderate and pour shots!
If you've got a provably secure protocol, what's the problem with formally verifying the implementation of the protocol?
I work in an area where bugs are very scary, so we use formal verification, and that's on top of having many more testers than developers.
From the perspective of this naive outsider, I'd would have expected FV to be worth it for security sensitive protocols. Is it that the protocols are too complex to be verified, or is it just not considered to be worth the effort?
I'm not making an argument against formal methods. I'm saying that if you replaced TLS with a protocol with a design proof, you could easily end up less secure.
