Relational reasoning via probabilistic coupling

DOI10.1007/978-3-662-48899-7_27zbMATH Open1471.68127arXiv1509.03476OpenAlexW2228964661MaRDI QIDQ3460069FDOQ3460069

Authors: Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Léo Stefanesco, Pierre-Yves Strub 

Publication date: 12 January 2016

Published in: Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Abstract: 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.

Full work available at URL: https://arxiv.org/abs/1509.03476

Recommendations

• Coupling proofs are probabilistic product programs
• Proving uniformity and independence by self-composition and coupling
• Constraint-based synthesis of coupling proofs
• Proving differential privacy via probabilistic couplings
• Relational reasoning for Markov chains in a probabilistic guarded lambda calculus

Mathematics Subject Classification ID

Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Cryptography (94A60) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cited In (7)

• Constraint-based synthesis of coupling proofs
• Title not available (Why is that?)
• Title not available (Why is that?)
• Relational reasoning for Markov chains in a probabilistic guarded lambda calculus
• Mixed nondeterministic-probabilistic automata: blending graphical probabilistic models with nondeterminism
• Relational Analysis and Precision via Probabilistic Abstract Interpretation
• Coupling proofs are probabilistic product programs

Uses Software

• EasyCrypt

This page was built for publication: Relational reasoning via probabilistic coupling

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3460069)