Proving uniformity and independence by self-composition and coupling

Abstract : 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 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 EasyCrypt proof assistant.
Complete list of metadatas

Cited literature [17 references]  Display  Hide  Download

https://hal.sorbonne-universite.fr/hal-01541198
Contributor : Thomas Espitau <>
Submitted on : Sunday, June 18, 2017 - 3:43:22 PM
Last modification on : Thursday, March 21, 2019 - 1:04:51 PM
Long-term archiving on : Sunday, December 17, 2017 - 8:28:42 PM

File

1701.06477.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01541198, version 1

Citation

Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub. Proving uniformity and independence by self-composition and coupling. LPAR 2017 - International Conferences on Logic for Programming, Artificial Intelligence and Reasoning, May 2017, Maun, Botswana. pp.19. ⟨hal-01541198⟩

Share

Metrics

Record views

554

Files downloads

328