Relational Reasoning via Probabilistic Coupling

By Gilles Barthe, Thomas Espitau, Benjamin Gr'egoire, Justin Hsu, Léo Stefanesco, Pierre-Yves Strub. 2015

43 citations recorded by the source corpus.

Probabilistic coupling is a powerful tool for analyzing pairs of probabilistic processes. Roughly, coupling two processes requires finding an appropriate witness process that models both processes in the same probability space. Couplings are powerful tools proving properties about the relation between two processes, include reasoning about convergence of distributions and stochastic dominance---a probabilistic version of a monotonicity property. While the mathematical definition of coupling looks rather complex and cumbersome to manipulate, we show that the relational program logic pRHL---the logic underlying the EasyCrypt cryptographic proof assistant---already internalizes a generalization of probabilistic coupling. With this insight, constructing couplings is no harder than constructing logical proofs. We demonstrate how to express and verify classic examples of couplings in pRHL, and we mechanically verify several couplings in EasyCrypt.

Subfields: Artificial Intelligence, Computer Vision and Pattern Recognition

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

In Computer Vision and Pattern Recognition

Citations in the corpus

Advanced Probabilistic Couplings for Differential Privacy (2016, neutral): “The connection between liftings and couplings was recently noted by Barthe et al. [8] and explored for differential privacy by Barthe et al. [10].”
Proving Differential Privacy via Probabilistic Couplings (2016, neutral): “Similarly, we are not aware of couplings in differential privacy, though there seems to be an implicit coupling argument by Dwork et al. (2015b). There are seemingly few applications of coupling in formal verification, despite considerable research on probabilistic bisimulation (first introduced by ”
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].”
A Program Logic for Union Bounds (2016, unknown): “These logics rely on the powerful abstraction of probabilistic couplings to derive probabilistic facts from non-probabilistic assertions [7].”