×

Proving uniformity and independence by self-composition and coupling. (English) Zbl 1403.68140

Eiter, Thomas (ed.) et al., LPAR-21. 21st international conference on logic for programming, artificial intelligence and reasoning, Maun, Botswana, May 8–12, 2017. Selected papers. Manchester: EasyChair. EPiC Series in Computing 46, 385-403 (2017).
Summary: Proof by coupling is a classical proof technique for establishing probabilistic properties of two probabilistic processes, like stochastic dominance and rapid mixing of Markov chains. More recently, couplings have been investigated as a useful abstraction for formal reasoning about relational properties of probabilistic programs, in particular for modeling reduction-based cryptographic proofs and for verifying differential privacy. In this paper, we demonstrate that probabilistic couplings can be used for verifying non-relational probabilistic properties. Specifically, we show that the program logic \(\mathsf{pRHL}\) – whose proofs are formal versions of proofs by coupling – can be used for formalizing uniformity and probabilistic independence. We formally verify our main examples using the \(\mathsf{EasyCrypt}\) proof assistant.
For the entire collection see [Zbl 1398.68026].

MSC:

68Q87 Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)
03B70 Logic in computer science
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Software:

EasyCrypt
PDFBibTeX XMLCite
Full Text: DOI arXiv