On the Equality of Probabilistic Terms
- 616 Downloads
We consider a mild extension of universal algebra in which terms are built both from deterministic and probabilistic variables, and are interpreted as distributions. We formulate an equational proof system to establish equality between probabilistic terms, show its soundness, and provide heuristics for proving the validity of equations. Moreover, we provide decision procedures for deciding the validity of a system of equations under specific theories that are commonly used in cryptographic proofs, and use concatenation, truncation, and xor. We illustrate the applicability of our formalism in cryptographic proofs, showing how it can be used to prove standard equalities such as optimistic sampling and one-time padding as well as non-trivial equalities for standard schemes such as OAEP.
KeywordsDecision Procedure Function Symbol Equational Theory Proof System Universal Algebra
Unable to display preview. Download preview PDF.
- 2.Barthe, G., Grégoire, B., Béguelin, S.Z.: Formal certification of code-based cryptographic proofs. In: Proceedings of POPL 2009, pp. 90–101. ACM Press, New York (2009)Google Scholar
- 8.Courant, J., Daubignard, M., Ene, C., Lafourcade, P., Lakhnech, Y.: Towards automated proofs for asymmetric encryption schemes in the random oracle model. In: Proceedings of CCS 2008, pp. 371–380. ACM Press, New York (2008)Google Scholar