A Framework for Language-Based Cryptographic Proofs
Gilles Barthe, Benjamin Gr · 2007
Motivation In cryptography, provable security advocates a mathematical approach where the goals and requirements of cryptographic systems are specified precisely, and where the security proof is carried out rigorously and makes explicit the assumptions it relies upon. Typically, security objectives are expressed in complexity-theoretical terms and refer to the probability of an efficient adversary to thwart a security objective (e.g. secrecy), whereas security proofs are “reductionist”, i.e. prove that the existence of an efficient adversary contradicts a computational assumption (e.g. that the Decisional Diffie-Hellman problem is hard). The game-playing technique is a general method to structure and unify cryptographic proofs that has been widely applied in the literature. In essence, the game-playing technique suggests to view the interaction between an unknown efficient adversary and a cryptosystem as a probabilistic game depending on security a parameter η where the winning probability of the adversary corresponds to the probability of breaking a given security property. The initial game is stepwise transformed in a security-preserving fashion into a final game where it is easy to analyze and bound the winning probability. Since the transformations are security-preserving, one can argue that the same bound holds for the initial game and, if this bound is a negligible function of η, then the probability of breaking the security property of the system is also negligible. Although the adoption of provable security and the gameplaying technique has significantly enhanced confidence in cryptographic systems, the community is increasingly wary about security proofs: several published proofs have been found incorrect, and in general proofs are becoming too complex to be verified. This is partly due to the fact that proofs are rather involved and rely on different kinds of mathematical reasoning including complexity theory, probability theory and group theory. However, the main reason is to be found in the difficulty in pinpointing the underlying hypotheses in the proof and in isolating the creative and original parts from the uninteresting steps recurring – with variations – in every other proof. Bellare and Rogaway [1], and Halevi [3] propose the gameplaying technique as a natural solution for taming the complexity of proofs and recognize that a fully-specified programming language is required to code games. We believe cryptographers could greatly benefit from a framework for formalizing and verifying the transformations in game-based cryptographic proofs and propose a language-based framework built on top of the Coq proof assistant.