Proving uniformity and independence by self-composition and coupling

Gilles Barthe 1 Thomas Espitau 2 Benjamin Grégoire 3 Justin Hsu 4 Pierre-Yves Strub 1
1 Institute IMDEA Software [Madrid]
2 ALMASTY - ALgorithms for coMmunicAtion SecuriTY
LIP6 - Laboratoire d'Informatique de Paris 6
3 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
4 University of Pennsylvania [Philadelphia]
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.
Type de document :
Communication dans un congrès
LPAR 2017 - International Conferences on Logic for Programming, Artificial Intelligence and Reasoning, May 2017, Maun, Botswana. pp.19, LPAR 2017 - International Conferences on Logic for Programming, Artificial Intelligence and Reasoning
Liste complète des métadonnées

Littérature citée [24 références]  Voir  Masquer  Télécharger
https://hal.sorbonne-universite.fr/hal-01541198
Contributeur : Thomas Espitau <>
Soumis le : dimanche 18 juin 2017 - 15:43:22
Dernière modification le : mercredi 21 mars 2018 - 18:58:20
Document(s) archivé(s) le : dimanche 17 décembre 2017 - 20:28:42

Fichier

1701.06477.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01541198, version 1

Collections

UPMC | INRIA | LIP6 | INRIA2017 | UNIV-COTEDAZUR

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, LPAR 2017 - International Conferences on Logic for Programming, Artificial Intelligence and Reasoning. 〈hal-01541198〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

223

Téléchargements de fichiers

86

Contact

support.ccsd.cnrs.fr
hal.support@ccsd.cnrs.fr
Logo CCSD