My perspective is that we know how to design protocols which are provably secure.

Your perspective is... I'm not quite sure, actually. Maybe you just don't believe in mathematical proofs?

As you say, agree to disagree -- but I'm not going to stop pointing and laughing every time a new SSL/TLS vulnerability comes out. :-)

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!

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

Have there been any proposed contenders to TLS/SSL?

SSH and IPv6 come to mind.

For HTTP traffic?

Vulnerabilities don't arise by study, they arise because of vulnerabilities. We have plenty of well-studied crypto that is fine, ranging from SHA to Kerberos.

Colin is right that we know how to prove that cryptographic systems have certain security properties. The academic literature is filled with laments about TLS and proofs of fixed versions of it.

SHA? The Secure Hash Algorithm? The Secure Hash Algorithm with the length extension property? The Secure Hash Algorithm with the length extension property that was specifically forbidden from the SHA-3 contestants because it creates implementation vulnerabilities in the real world? That SHA?

Also, how does one compare a cryptographic hash function core to an entire cryptographic protocol to produce a statement about the fallibility of crypto design?