Formal Certification of Code-Based Cryptographic Proofs.

By Gilles Barthe, Benjamin Gr'egoire, Romain Janvier, Santiago Zanella Béguelin. 2007

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

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): “Applications include formalizing reduction-based cryptographic proofs [3] and modeling stochastic dominance and convergence of probabilistic processes [6].”
Proving Differential Privacy in Hoare Logic (2014, background): “CertiCrypt [9], and EasyCrypt [8], [6], are computer-aided tools that support relational reasoning about probabilistic programs and have been used to prove security of cryptographic constructions and computational differential privacy of protocols.”
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]. a ← b means assigning a value b to a variable a , while a $ ← [0 ..n ] means assigning a random value between 0 and n to a .”
Relational Reasoning via Probabilistic Coupling (2015, methodology): “In its original form [2], implemented in the EasyCrypt proof assistant [4], pRHL reasons about programs written in a imperative language extended with random assignments with the following syntax of commands: Assertions in the language are ﬁrst-order formulae over generalized expressions.”
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 rests on a lifting operator that turns a relation R over states into a relation ∼ α,δR over distributions of states: formally, the judgment above is valid iff for every pair of memories m 1 and m 2 , The deﬁnition of the lifting operator…”
Coupling proofs are probabilistic product programs (2016, background): “Recently, Barthe et al. [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].”
Probabilistic programming (2014, unknown): “Our prototypical language P ROB is imperative, as is the C#-based modeling language underlying Infer.NET [41], and also P W HILE , the cryptographic modeling language used by the CertiCrypt [3] and EasyCrypt [4] veriﬁcation tools for reasoning about cryptographic algorithms and protocols.”
A Program Logic for Union Bounds (2016, unknown): “Examples include probabilistic relational Hoare logic [3] for proving the reductionist security of cryptographic constructions, and the related approximate probabilistic relational Hoare logic [4] for reasoning about diﬀerential privacy.”
Measure Transformer Semantics for Bayesian Machine Learning (2011, background): “This cho ice is a generalization of the (discrete) semantics of pWHILE [4].”
Computer-Aided Security Proofs for the Working Cryptographer (2011, background): “Under specific conditions on f , see [24], the validity of Ψ ⇒f Φ entails the validity of the corresponding pRHL judgment.”