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

To some extent this is just efficient hubris -- I can't do it so it can't be any good. Call it chutzpah, if you like, but there's slightly more relevance to that than egotism, as, if I can't do it, it generally signals that businesses will have a lot of trouble dealing with it. Not because there aren't enough people better than me, but because, if those that can do it cannot explain it to me, then they haven't got much of a chance in explaining it to the average business.

Added to that, there have been a steady stream of "proofs" that have been broken, and "proven systems" that have been bypassed. If you look at it from a scientific investigative point of view, generally, the proof only works because the assumptions are so constrained that they eventually leave the realm of reality, and that's particularly dangerous to do in security work.

Added to all that: The ACM is awarding its Godel prize for a proof that there is no proof:

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. These conventions involve well-defined instructions for accomplishing a task that rely on generating a sequence of numbers (known as pseudo-random number generators). The authors' findings apply to computational problems used in cryptography, authentication, and access control. They show that other proof techniques need to be applied to address this basic, unresolved challenge.The findings of Razborov and Rudich, published in a journal paper entitled "Natural Proofs" in the Journal of Computer and System Sciences in 1997, address a problem that is widely considered the most important question in computing theory. It has been designated as one of seven Prize Problems by the Clay Mathematics Institute of Cambridge, Mass., which has allocated $1 million for solving each problem. 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 problem is posed to determine whether questions exist whose answer can be quickly checked, but which require an impossibly long time to solve.

The paper proves that there is no so-called "Natural Proof" that certain computational problems often used in cryptography are hard to solve. Such cryptographic methods are critical to electronic commerce, and though these methods are widely thought to be unbreakable, the findings imply that there are no Natural Proofs for their security.

If so, this can count as a plus point for risk management, and a minus point for the school of no-risk security. However hard you try, any system you put in place will have some chances of falling flat on its face. Deal with it; the savvy financial cryptographer puts in place a strong system, then moves on to addressing what happens when it breaks.

The "Natural Proofs" result certainly matches my skepticism, but I guess we'll have to wait for the serious mathematicians to prove that it isn't so ... perhaps by proving that it is not possible to prove that there is no proof?

Posted by iang at May 22, 2007 08:21 AM | TrackBackComments

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.

Posted by: Dean at May 22, 2007 09:11 PMIan,

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

Posted by: Ray at May 25, 2007 05:13 AMProofs 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.

Posted by: nick at December 21, 2007 08:45 PMPost a comment