Overview

Introduced by the ancient Greeks, the notion of theorems established through rigorous formal proofs has been a central paradigm of theoretical mathematics. The power and elegance of this paradigm is appreciated to some extent even among the general public. Anyone graduating from secondary school can be presumed not only to know the statement of the Pythagorean Theorem, but also to have seen and understood a rigorous proof. [1]

In cryptography during the last 20 years, leading researchers (such as Katz and Lindell in their well-regarded textbook) have cited the use of formal mathematical techniques to "prove" the security of a protocol as the main justification for saying that cryptography has been transformed from an art to a science.

However, in our view the theorem-proof paradigm of pure mathematics is of limited use in evaluating the real-world security of a cryptographic protocol, and the very term "provable security" is misleading. Over the years many problems have arisen with the way proofs are used in cryptography. Among the issues addressed in our series of "Another Look..." papers are the following:

1. An alarming number of security proofs — even ones by prominent researchers that have influenced cryptographic practice — have turned out to be fallacious. Part of the explanation can be found in the sociology of the profession. Researchers are under considerable pressure to publish frequently (with their merit evaluations depending more on the quantity than on the quality of their publications). In addition, papers are often rushed in order to meet conference deadlines. And papers are not always refereed carefully — again, because of time pressures.
2. A security theorem is conditional in a strong sense — it assumes the intractability of some mathematical problem. This type of conditionality is very different from what a proof means in traditional mathematics (where there is even controversy over the value of theorems that are proved under the Riemann Hypothesis).
3. Often the intractability assumption is made for a complicated and contrived problem that has never been carefully studied. In fact, in some cases the problem is trivially equivalent to the cryptanalysis problem for the protocol whose security is being "proved," and the "proof" is essentially circular.
4. It is often difficult to interpret what a reductionist security proof really means in practice. Proofs under different assumptions sometimes lead to contradictory conclusions about such important practical issues as where to hash, how much randomness to use, and which of two versions of a protocol is more secure.
5. Sometimes a proof has a large tightness gap, but parameter sizes are still recommended as if the proof had been tight. In such cases the proof usually gives a useless lower bound on the running time of a successful attack.
6. Cryptographers sometimes forget that an asymptotic result does not necessarily provide any assurance of security for parameters in the range used in practice.
7. A security theorem uses a certain definition ("model") of what security means. There has been much debate and uncertainty about what the "right" security definitions are — even for some of the basic types of cryptographic functionality.
8. Certain attacks — especially side-channel attacks — are very hard to model, and the models that have been proposed are woefully inadequate. The problem is that the adversary is always coming up with ingenious new methods to compromise the security of a cryptographic system.
9. If security proofs are used as a guide to protocol construction — and if features are dropped that are not needed for the security proof — then the protocol might become more vulnerable than before to attacks that are not included in the security model. One can end up with a protocol that, although provably secure, is very insecure.

We wish to emphasize that we are not opposed to proofs in cryptography. Mathematical proofs have their place. What we are opposed to is the misleading hype that often accompanies them. We believe that designers of protocols would be on more solid ground if they (1) deleted the terms "proof of security" and "provable security" from the cryptographic lexicon, and (2) showed some humility and realism when presenting security assurances to the public.

Above all, our work highlights the important role that old-fashioned cryptanalysis and sound engineering practices continue to play in establishing and maintaining confidence in the security of a cryptographic system.

——————