Relational reasoning via probabilistic coupling

DOI10.1007/978-3-662-48899-7_27MaRDI QIDQ3460069zbMATH OpenOpenAlexFDO

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)

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

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)

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.

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

Cited in

(7)

• Constraint-based synthesis of coupling proofs
• scientific article; zbMATH DE number 6026985 (Why is no real title available?)
• scientific article; zbMATH DE number 4074044 (Why is no real title available?)
• 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

Describes a project that uses

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)