Abstract

Cryptographic primitives such as encryption and digital signature schemes form the building blocks of secure computer systems. Their security is usually established by reduction, showing that a feasible attack would lead to an efficient way to solve some computationally hard problem. Yet this kind of arguments are notoriously difficult to verify and the history of modern cryptography is fraught with examples of flawed security proofs that stood unchallenged for years.

A well established methodology for structuring security proofs of cryptographic primitives is to give a precise mathematical description of the interaction between an adversary and a challenger—-such descriptions are referred to as games—-and to organise proofs as sequences of games, starting from a game that represents a security goal and proceeding by successive transformations to games that represent security assumptions.

In this talk I will show how game-based proofs can be given formal foundations by representing games as probabilistic programs where adversaries are modelled as probabilistic polynomial-time procedures, and relying on programming language techniques to justify proof steps. The techniques I will present have been implemented in the CertiCrypt framework, itself built on top of the Coq proof assistant, and include a probabilistic relational Hoare logic, a theory of observational equivalence, and certified program transformations. CertiCrypt has been notably applied to obtain for the first time machine-checked proofs of the security of the Optimal Asymmetric Encryption Scheme and of an optimal bound on the security of Full-Domain Hash signatures.

The programming language principles and techniques I developed to formalize game-based proofs transcend their initial application domain and allow to reason about probabilistic programs in general. I will outline possible extensions (e.g. approximate equivalence), applications (e.g. quantitative information flow, differential privacy) and opportunities for increasing automation.