Hacker News Reader

Comment by tptacek | Hacker News Reader

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.

View on HN

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!

(a) I would lose the debate, (b) it would be boring, (c) I can drink Colin under the table.

(d) I would probably end up in the hospital.

There's a reason why I don't drink -- type 1 diabetes and large quantities of alcohol don't interoperate well.

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.

Reply on news.ycombinator.com