I agree, I find it highly unlikely that there are real proofs for a lot of techniques used in computer security. I do suspect that there are proofs against some of them however.

The fact that many "provable" systems have been broken is (as you assert) due to the parameters those systems operate under in realiry. Usually the proof of a system is done using parameters that don't actually exist in the real world, or if they do exist in the real world, are able to be altered to make an attack effective.

I spend a lot of time thinking about strong authentication and see this pattern a lot. Strong authentication to websites is especially vulnerable to this evolution of attack. There is not a strong authentication solution available today that can withstand a live MITM. Worse than that, I suspect that there is a proof that shows traditional forms of strong authentication cannot ever be completely secure on the web.

Does this leave us at the mercy of attackers? No, I don't think so. Putting my engineer hat on tells me that a good security system can be partly defined by what it does when it fails. I ensure that the systems I design fail gracefully, so if they are circumvented, the attackers are easy to track down and deal with in various ways. This is done in our strong authentication system by 'tagging' authentication attempts.

So, whilst we should be building the strongest security we can, we shouldn't have the hubris to think that what we have built can't be broken.

Ian,

> > I have a lot of skepticism about the notion of provable security.

Depends on what you expect of it. In cryptography it usually doesn't mean proving something secure but rather proving it at least as secure as something else believed (but not proved) to be secure. For example proving that breaking a particular cryptosystem is as hard as factoring. There are protocols in widespread use that have not even been proved secure in this sense, for example there is no known proof that breaking RSA is as hard as factoring.

> > In a paper titled "Natural Proofs" originally presented at the 1994
> > ACM STOC, the authors found that a wide class of proof techniques
> > cannot be used to resolve this challenge unless widely held conventions
> > are violated.

I haven't actually read Razborov and Rudich's Natural Proofs paper but it seems like an interesting result.

> > It asks
> > - if it is easy to check that a solution to a problem is correct, is it
> > also easy to solve the problem?

This is just a restatement of P=?NP. If the answer is yes, then there are no one-way functions and all of modern cryptography falls down. (For f to be one-way, then given y it has to be easy to check that f(x)=y but not easy to find x.)

> > ... perhaps by proving that it is not possible to prove
> > that there is no proof?

Your formulation reminds me of a category of unsolved problems that may be unprovable but if so you can never prove it, but funnily you can prove that.

For example, consider Goldbach's conjecture (that every even number is the sum of two primes). If it is false, then there exists a counterexample, i.e., an even number that is not the sum of two primes, and exhaustive verification of this counterexample would constitute a simple proof that the conjecture is false. Thus the only way it can be unprovable is if it's true, and a proof that it is unprovable would therefore be proof that it is true, a contradiction. Thus it cannot be proved unprovable. QED

The important characteristic is that one way would have an easy proof. Fermat's Last Theorem and the Four Color Map Problem were also in this category but have since been proved.

Ray

Proofs can be extremely valuable if they clearly state their assumptions and limitations. Alas, they usually don't. When their security is "broken" it is almost always because somebody discovers that the assumptions didn't match the threat model the proof user (e.g. crypto software designer) was trying to protect against. But the assumptions were hidden and nobody realized there was a mismatch.