Formal Indistinguishability Extended to the Random Oracle Model

  • Cristian Ene
  • Yassine Lakhnech
  • Van Chan Ngo
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5789)


Several generic constructions for transforming one-way functions to asymmetric encryption schemes have been proposed. One-way functions only guarantee the weak secrecy of their arguments. That is, given the image by a one-way function of a random value, an adversary has only negligible probability to compute this random value. Encryption schemes must guarantee a stronger secrecy notion. They must be at least resistant against indistinguishability-attacks under chosen plaintext text (IND-CPA). Most practical constructions have been proved in the random oracle model (ROM for short). Such computational proofs turn out to be complex and error prone. Bana et al. have introduced Formal Indistinguishability Relations (FIR), as an abstraction of computational indistinguishability. In this paper, we extend the notion of FIR to cope with the ROM on one hand and adaptive adversaries on the other hand. Indeed, when dealing with hash functions in the ROM and one-way functions, it is important to correctly abstract the notion of weak secrecy. Moreover, one needs to extend frames to include adversaries in order to capture security notions as IND-CPA. To fix these problems, we consider pairs of formal indistinguishability relations and formal non-derivability relations. We provide a general framework along with general theorems, that ensure soundness of our approach and then we use our new framework to verify several examples of encryption schemes among which the construction of Bellare Rogaway and Hashed ElGamal.


Hash Function Encryption Scheme Equational Theory Symbolic Model Random Oracle Model 
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.


  1. 1.
    Abadi, M., Rogaway, P.: Reconciling two views of cryptography. In: Watanabe, O., Hagiya, M., Ito, T., van Leeuwen, J., Mosses, P.D. (eds.) TCS 2000. LNCS, vol. 1872, p. 3. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  2. 2.
    Abadi, M., Baudet, M., Warinschi, B.: Guessing attacks and the computational soundness of static equivalence. In: Aceto, L., Ingólfsdóttir, A. (eds.) FOSSACS 2006. LNCS, vol. 3921, pp. 398–412. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  3. 3.
    Abadi, M., Gordon, A.D.: A bisimulation method for cryptographic protocols. In: Hankin, C. (ed.) ESOP 1998. LNCS, vol. 1381, pp. 12–26. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  4. 4.
    Backes, M., Pfitzmann, B.: Symmetric encryption in a simulatable dolev-yao style cryptographic library. In: CSFW, pp. 204–218. IEEE, Los Alamitos (2004)Google Scholar
  5. 5.
    Backes, M., Pfitzmann, B., Waidner, M.: Symmetric authentication within a simulatable cryptographic library. In: Snekkenes, E., Gollmann, D. (eds.) ESORICS 2003. LNCS, vol. 2808, pp. 271–290. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  6. 6.
    Baek, J., Lee, B., Kim, K.: Secure length-saving elgamal encryption under the computational diffie-hellman assumption. In: Clark, A., Boyd, C., Dawson, E.P. (eds.) ACISP 2000. LNCS, vol. 1841, pp. 49–58. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  7. 7.
    Bana, G., Mohassel, P., Stegers, T.: Computational soundness of formal indistinguishability and static equivalence. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol. 4435, pp. 182–196. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  8. 8.
    Baudet, M., Cortier, V., Kremer, S.: Computationally sound implementations of equational theories against passive adversaries. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 652–663. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  9. 9.
    Bellare, M., Rogaway, P.: Optimal asymmetric encryption. In: De Santis, A. (ed.) EUROCRYPT 1994. LNCS, vol. 950, pp. 92–111. Springer, Heidelberg (1995)CrossRefGoogle Scholar
  10. 10.
    Bellare, M., Rogaway, P.: Random oracles are practical: a paradigm for designing efficient protocols. In: CCS 1993, pp. 62–73 (1993)Google Scholar
  11. 11.
    Blanchet, B., Pointcheval, D.: Automated security proofs with sequences of games. In: Dwork, C. (ed.) CRYPTO 2006. LNCS, vol. 4117, pp. 537–554. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  12. 12.
    Canetti, R.: Universally composable security: A new paradigm for cryptographic protocols. In: FOCS, pp. 136–145 (2001)Google Scholar
  13. 13.
    Canetti, R., Herzog, J.: Universally composable symbolic analysis of mutual authentication and key-exchange protocols. In: Halevi, S., Rabin, T. (eds.) TCC 2006. LNCS, vol. 3876, pp. 380–403. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  14. 14.
    Cortier, V., Warinschi, B.: Computationally sound, automated proofs for security protocols. In: Sagiv [25], pp. 157–171Google Scholar
  15. 15.
    Courant, J., Daubignard, M., Ene, C., Lafourcade, P., Lakhnech, Y.: Towards automated proofs for asymmetric encryption schemes in the random oracle model. In: CCS 2008, pp. 371–380. ACM Press, New York (2008)Google Scholar
  16. 16.
    Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Transactions on Information Theory 29(2), 198–208 (1983)MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Feige, U., Fiat, A., Shamir, A.: Zero-knowledge proofs of identity. J. Cryptol. 1(2), 77–94 (1988)MathSciNetCrossRefzbMATHGoogle Scholar
  18. 18.
    Goldwasser, S., Micali, S.: Probabilistic encryption. Journal of Computer and System Sciences 28(2), 270–299 (1984)MathSciNetCrossRefzbMATHGoogle Scholar
  19. 19.
    Janvier, R., Lakhnech, Y., Mazaré, L.: Completing the picture: Soundness of formal encryption in the presence of active adversaries. In: Sagiv [25], pp. 172–185 (2005)Google Scholar
  20. 20.
    Laud, P.: Symmetric encryption in automatic analyses for confidentiality against adaptive adversaries. In: Symposium on Security and Privacy, pp. 71–85 (2004)Google Scholar
  21. 21.
    Micciancio, D., Warinschi, B.: Soundness of formal encryption in the presence of active adversaries. In: Naor, M. (ed.) TCC 2004. LNCS, vol. 2951, pp. 133–151. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  22. 22.
    Okamoto, T., Pointcheval, D.: React: Rapid enhanced-security asymmetric cryptosystem transform. In: Naccache, D. (ed.) CT-RSA 2001. LNCS, vol. 2020, pp. 159–175. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  23. 23.
    Phan, D.H., Pointcheval, D.: About the security of ciphers (semantic security and pseudo-random permutations). In: Handschuh, H., Hasan, M.A. (eds.) SAC 2004. LNCS, vol. 3357, pp. 182–197. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  24. 24.
    Pointcheval, D.: Chosen-ciphertext security for any one-way cryptosystem. In: Imai, H., Zheng, Y. (eds.) PKC 2000. LNCS, vol. 1751, pp. 129–146. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  25. 25.
    Sagiv, M. (ed.): ESOP 2005. LNCS, vol. 3444, pp. 1–4. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  26. 26.
    Shoup, V.: Oaep reconsidered. J. Cryptology 15(4), 223–249 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  27. 27.
    Shoup, V.: Sequences of games: a tool for taming complexity in security proofs. cryptology eprint archive, report 2004/332 (2004)Google Scholar
  28. 28.
    Zheng, Y., Seberry, J.: Immunizing public key cryptosystems against chosen ciphertext attacks. J. on Selected Areas in Communications 11(5), 715–724 (1993)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Cristian Ene
    • 1
  • Yassine Lakhnech
    • 1
  • Van Chan Ngo
    • 1
  1. 1.Université Grenoble 1, CNRS,VerimagFrance

Personalised recommendations