Computer-Aided Cryptographic Proofs

Gilles Barthe, Benjamin Grégoire, and Santiago Zanella-Béguelin


Provable security is at the heart of modern cryptography. It advocates a mathematical approach in which the security of new cryptographic constructions is defined rigorously, and provably reduced to one or several assumptions, such as the hardness of a computational problem, or the existence of an ideal functionality. A typical provable security statement is of the form: for any adversary A against the cryptographic construction S, there exists an adversary B against a security assumption H, such that if A has a high probability of breaking the scheme S in time t, then B has a high probability of breaking the assumption H in time t′ (defined as a function of t).


Publication typeInproceedings
Published in19th International Symposium on Static Analysis, SAS 2012
SeriesLecture Notes in Computer Science
> Publications > Computer-Aided Cryptographic Proofs