Computer-Aided Cryptographic Proofs

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

2012

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 type | Inproceedings |

Published in | 19th International Symposium on Static Analysis, SAS 2012 |

URL | http://dx.doi.org/10.1007/978-3-642-33125-1_1 |

Pages | 1-2 |

Volume | 7460 |

Series | Lecture Notes in Computer Science |

Publisher | Springer |

- Formal Certification of Code-Based Cryptographic Proofs
- Probabilistic Relational Reasoning for Differential Privacy
- Probabilistic Relational Verification for Cryptographic Implementations

> Publications > Computer-Aided Cryptographic Proofs