On the Equality of Probabilistic Terms

  • Gilles Barthe
  • Marion Daubignard
  • Bruce Kapron
  • Yassine Lakhnech
  • Vincent Laporte
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6355)


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.


Decision Procedure Function Symbol Equational Theory Proof System Universal Algebra 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)CrossRefzbMATHGoogle Scholar
  2. 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
  3. 3.
    Baudet, M., Cortier, V., Kremer, S.: Computationally sound implementations of equational theories against passive adversaries. Inf. Comput. 207(4), 496–520 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Bellare, M., Rogaway, P.: The security of triple encryption and a framework for code-based game-playing proofs. In: Vaudenay, S. (ed.) EUROCRYPT 2006. LNCS, vol. 4004, pp. 409–426. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  5. 5.
    Bellare, M., Rogaway, P.: Optimal asymmetric encryption – How to encrypt with RSA. In: De Santis, A. (ed.) EUROCRYPT 1994. LNCS, vol. 950, pp. 92–111. Springer, Heidelberg (1995)CrossRefGoogle Scholar
  6. 6.
    Bresson, E., Lakhnech, Y., Mazaré, L., Warinschi, B.: A generalization of ddh with applications to protocol analysis and computational soundness. In: Menezes, A. (ed.) CRYPTO 2007. LNCS, vol. 4622, pp. 482–499. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  7. 7.
    Cortier, V., Delaune, S., Lafourcade, P.: A survey of algebraic properties used in cryptographic protocols. Journal of Computer Security 14(1), 1–43 (2006)CrossRefGoogle Scholar
  8. 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
  9. 9.
    Fujisaki, E., Okamoto, T., Pointcheval, D., Stern, J.: RSA-OAEP is secure under the RSA assumption. Journal of Cryptology 17(2), 81–104 (2004)MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    Goguen, J.A., Meseguer, J.: Completeness of many-sorted equational logic. SIGPLAN Not. 16(7), 24–32 (1981)CrossRefzbMATHGoogle Scholar
  11. 11.
    Impagliazzo, R., Kapron, B.M.: Logics for reasoning about cryptographic constructions. Journal of Computer and Systems Sciences 72(2), 286–320 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    Kumar, N., Sen, K., Meseguer, J., Agha, G.: A rewriting based model for probabilistic distributed object systems. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol. 2884, pp. 32–46. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  13. 13.
    Nipkow, T.: Unification in primal algebras, their powers and their varieties. J. ACM 37(4), 742–776 (1990)MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    Shoup, V.: A Computational Introduction to Number Theory and Algebra. Cambridge University Press, Cambridge (2008)CrossRefzbMATHGoogle Scholar
  15. 15.
    Stern, J.: Why provable security matters? In: Biham, E. (ed.) EUROCRYPT 2003. LNCS, vol. 2656, pp. 449–461. Springer, Heidelberg (2003)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2010

Authors and Affiliations

  • Gilles Barthe
    • 1
  • Marion Daubignard
    • 2
  • Bruce Kapron
    • 3
  • Yassine Lakhnech
    • 2
  • Vincent Laporte
    • 4
  1. 1.IMDEA SoftwareMadridSpain
  2. 2.VERIMAGGrenobleFrance
  3. 3.University of VictoriaCanada
  4. 4.ENS CachanFrance

Personalised recommendations