Computer-Aided Cryptographic Proofs

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