Formal certification of code-based cryptographic proofs

By Gilles Barthe, Benjamin Gr'egoire, Santiago Zanella-B'eguelin. 2009

190 citations recorded by the source corpus.

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

Citations in the corpus

Advanced Probabilistic Couplings for Differential Privacy (2016, neutral): “We take inspiration from the treatment of adversaries in the logic pRHL, an exact version of apRHL that has been used for verifying cryptographic proofs [4].”
Proving Differential Privacy via Probabilistic Couplings (2016, neutral): “[3]).”
Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif (2016, methodology): “Several tools exist for verifying cryptographic primitives and protocols in this model, in particular, CertiCrypt (Barthe et al., 2009; Béguelin et al., 2009) and its successor EasyCrypt (Barthe et al.”
Computer-Aided Security Proofs for the Working Cryptographer (2011, methodology): “However, the tool builds on a monadic representation of distributions, as in [6].”
Probabilistic relational reasoning for differential privacy (2012, methodology): “This line of work has been generalized to a probabilistic setting by CertiCrypt [3], which formalizes an extension of RHL for probabilistic programs.”
Measure Transformer Semantics for Bayesian Machine Learning (2011, background): “This choice is a generalization of the (discrete) semantics of pWHILE [2].”
Beyond Differential Privacy: Composition Theorems and Relational Logic for f-divergences between Probabilistic Programs (2013, background): “As for its predecessor pRHL [5], the notion of valid judgment in apRHL rests on a lifting operator that turns a relation R over states into a relation Lα(R) over distributions of states: formally, the judgment above is valid iff for every pair of memories m1 and m2, m1 Ψm2 implies (Jc1K m1) Lα(Φ) (J”
Coupling proofs are probabilistic product programs (2016, methodology): “[12] noticed a close connection between couplings and probabilistic relational Hoare logic (pRHL), originally designed for reasoning about the computational security of cryptographic constructions [5].”
InnerCircle: A parallelizable decentralized privacy-preserving location proximity protocol (2015, methodology): “For the convenience of the reader a few constructs used in the paper are outlined here, but for details the reader is directed to [3].”