Computational Soundness of Coinductive Symbolic Security under Active Attacks

  • Mohammad Hajiabadi
  • Bruce M. Kapron
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7785)


In Eurocrypt 2010, Miccinacio initiated an investigation of cryptographically sound, symbolic security analysis with respect to coinductive adversarial knowledge, and showed that under an adversarially passive model, certain security criteria may be given a computationally sound symbolic characterization, without the assumption of key acyclicity. Left open in his work was the fundamental question of “the viability of extending the coinductive approach to prove computational soundness results in the presence of active adversaries.” In this paper we make some initial steps toward this goal with respect to an extension of a trace-based security model (Micciancio and Warinschi, TCC 2004) including asymmetric and symmetric encryption; in particular we prove that a random computational trace can be soundly abstracted by a coinductive symbolic trace with overwhelming probability, provided that both the underlying encryption schemes provide IND-CCA2 security (plus ciphertext integrity for the symmetric scheme), and that the diameter of the underlying coinductively-hidden subgraph is constant in every symbolic trace. This result holds even if the protocol allows arbitrarily nested applications of symmetric/asymmetric encryption, unrestricted transmission of symmetric keys, and adversaries who adaptively corrupt users, along with other forms of active attack.

As part of our proof, we formulate a game-based definition of encryption security allowing adaptive corruptions of keys and certain forms of adaptive key-dependent plaintext attack, along with other common forms of CCA2 attack. We prove that (with assumptions similar to above) security under this game is implied by IND-CCA2 security. This also characterizes a provably benign form of cyclic encryption implied by standard security definitions, which may be of independent interest.


Computational soundness adaptive corruptions coinduction circular security trace-based protocol security active adversaries 


  1. 1.
    Abadi, M., Rogaway, P.: Reconciling Two Views of Cryptography (the computational soundness of formal encryption). In: Watanabe, O., Hagiya, M., Ito, T., van Leeuwen, J., Mosses, P.D. (eds.) TCS 2000. LNCS, vol. 1872, pp. 3–22. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  2. 2.
    Acar, T., Belenkiy, M., Bellare, M., Cash, D.: Cryptographic Agility and Its Relation to Circular Encryption. In: Gilbert, H. (ed.) EUROCRYPT 2010. LNCS, vol. 6110, pp. 403–422. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  3. 3.
    Backes, M., Dürmuth, M., Unruh, D.: OAEP Is Secure under Key-Dependent Messages. In: Pieprzyk, J. (ed.) ASIACRYPT 2008. LNCS, vol. 5350, pp. 506–523. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  4. 4.
    Backes, M., Pfitzmann, B.: Symmetric encryption in a simulatable dolev-yao style cryptographic library. In: CSFW, pp. 204–218. IEEE Computer Society (2004)Google Scholar
  5. 5.
    Backes, M., Pfitzmann, B., Scedrov, A.: Key-dependent message security under active attacks - brsim/uc-soundness of symbolic encryption with key cycles. In: CSF, pp. 112–124. IEEE Computer Society (2007)Google Scholar
  6. 6.
    Backes, M., Pfitzmann, B., Waidner, M.: A composable cryptographic library with nested operations. In: Jajodia, S., Atluri, V., Jaeger, T. (eds.) ACM Conference on Computer and Communications Security, pp. 220–230. ACM (2003)Google Scholar
  7. 7.
    Bana, G., Comon-Lundh, H.: Towards Unconditional Soundness: Computationally Complete Symbolic Attacker. In: Degano, P., Guttman, J.D. (eds.) POST 2012. LNCS, vol. 7215, pp. 189–208. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  8. 8.
    Barthe, G., Daubignard, M., Kapron, B.M., Lakhnech, Y.: Computational indistinguishability logic. In: Al-Shaer, E., Keromytis, A.D., Shmatikov, V. (eds.) ACM Conference on Computer and Communications Security, pp. 375–386. ACM (2010)Google Scholar
  9. 9.
    Bellare, M., Boldyreva, A., Micali, S.: Public-Key Encryption in a Multi-user Setting: Security Proofs and Improvements. In: Preneel, B. (ed.) EUROCRYPT 2000. LNCS, vol. 1807, pp. 259–274. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  10. 10.
    Bellare, M., Desai, A., Pointcheval, D., Rogaway, P.: Relations among Notions of Security for Public-Key Encryption Schemes. In: Krawczyk, H. (ed.) CRYPTO 1998. LNCS, vol. 1462, pp. 26–45. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  11. 11.
    Bellare, M., Namprempre, C.: Authenticated encryption: Relations among notions and analysis of the generic composition paradigm. J. Cryptology 21(4), 469–491 (2008)MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    Bellare, M., Rogaway, P.: Entity Authentication and Key Distribution. In: Stinson, D.R. (ed.) CRYPTO 1993. LNCS, vol. 773, pp. 232–249. Springer, Heidelberg (1994)CrossRefGoogle Scholar
  13. 13.
    Bellare, M., Rogaway, P.: Provably secure session key distribution: the three party case. In: Leighton, F.T., Borodin, A. (eds.) STOC, pp. 57–66. ACM (1995)Google Scholar
  14. 14.
    Boneh, D., Halevi, S., Hamburg, M., Ostrovsky, R.: Circular-Secure Encryption from Decision Diffie-Hellman. In: Wagner, D. (ed.) CRYPTO 2008. LNCS, vol. 5157, pp. 108–125. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  15. 15.
    Burrows, M., Abadi, M., Needham, R.: A logic of authentication. ACM Trans. Comput. Syst. 8, 18–36 (1990)CrossRefzbMATHGoogle Scholar
  16. 16.
    Camenisch, J., Chandran, N., Shoup, V.: A Public Key Encryption Scheme Secure against Key Dependent Chosen Plaintext and Adaptive Chosen Ciphertext Attacks. In: Joux, A. (ed.) EUROCRYPT 2009. LNCS, vol. 5479, pp. 351–368. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  17. 17.
    Canetti, R.: Universally composable security: A new paradigm for cryptographic protocols. In: FOCS, pp. 136–145. IEEE Computer Society (2001)Google Scholar
  18. 18.
    Canetti, R., Feige, U., Goldreich, O., Naor, M.: Adaptively secure multi-party computation. In: Miller, G.L. (ed.) STOC, pp. 639–648. ACM (1996)Google Scholar
  19. 19.
    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
  20. 20.
    Cash, D., Green, M., Hohenberger, S.: New Definitions and Separations for Circular Security. In: Fischlin, M., Buchmann, J., Manulis, M. (eds.) PKC 2012. LNCS, vol. 7293, pp. 540–557. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  21. 21.
    Clark, J., Jacob, J.: A survey of authentication protocol literature. Technical report (1997)Google Scholar
  22. 22.
    Comon-Lundh, H., Cortier, V.: Computational soundness of observational equivalence. In: Ning, P., Syverson, P.F., Jha, S. (eds.) ACM Conference on Computer and Communications Security, pp. 109–118. ACM (2008)Google Scholar
  23. 23.
    Datta, A., Derek, A., Mitchell, J.C., Warinschi, B.: Computationally sound compositional logic for key exchange protocols. In: CSFW, pp. 321–334. IEEE Computer Society (2006)Google Scholar
  24. 24.
    Dolev, D., Yao, A.C.: On the security of public key protocols. In: Annual IEEE Symposium on Foundations of Computer Science, pp. 350–357 (1981)Google Scholar
  25. 25.
    Gilbert, H. (ed.): EUROCRYPT 2010. LNCS, vol. 6110. Springer, Heidelberg (2010)zbMATHGoogle Scholar
  26. 26.
    Goldwasser, S., Micali, S.: Probabilistic encryption. J. Comput. Syst. Sci. 28(2), 270–299 (1984)MathSciNetCrossRefzbMATHGoogle Scholar
  27. 27.
    Hajiabadi, M., Kapron, B.M.: Computational soundness of coinductive symbolic security under active attacks. IACR Cryptology ePrint Archive, 2012:560 (2012)Google Scholar
  28. 28.
    Herzog, J.: A computational interpretation of dolev-yao adversaries. Theor. Comput. Sci. 340(1), 57–81 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  29. 29.
    Impagliazzo, R., Kapron, B.M.: Logics for reasoning about cryptographic constructions. J. Comput. Syst. Sci. 72(2), 286–320 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  30. 30.
    Küsters, R., Tuengerthal, M.: Computational soundness for key exchange protocols with symmetric encryption. In: Al-Shaer, E., Jha, S., Keromytis, A.D. (eds.) ACM Conference on Computer and Communications Security, pp. 91–100. ACM (2009)Google Scholar
  31. 31.
    Lincoln, P., Mitchell, J.C., Mitchell, M., Scedrov, A.: A probabilistic poly-time framework for protocol analysis. In: Gong, L., Reiter, M.K. (eds.) ACM Conference on Computer and Communications Security, pp. 112–121. ACM (1998)Google Scholar
  32. 32.
    Micciancio, D.: Computational Soundness, Co-induction, and Encryption Cycles. In: Gilbert, H. (ed.) EUROCRYPT 2010. LNCS, vol. 6110, pp. 362–380. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  33. 33.
    Micciancio, D., Panjwani, S.: Adaptive Security of Symbolic Encryption. In: Kilian, J. (ed.) TCC 2005. LNCS, vol. 3378, pp. 169–187. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  34. 34.
    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
  35. 35.
    Mitchell, J.C., Ramanathan, A., Scedrov, A., Teague, V.: A probabilistic polynomial-time process calculus for the analysis of cryptographic protocols. Theor. Comput. Sci. 353(1-3), 118–164 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  36. 36.
    Panjwani, S.: Tackling Adaptive Corruptions in Multicast Encryption Protocols. In: Vadhan, S.P. (ed.) TCC 2007. LNCS, vol. 4392, pp. 21–40. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  37. 37.
    Pfitzmann, B., Waidner, M.: A model for asynchronous reactive systems and its application to secure message transmission. In: IEEE Symposium on Security and Privacy, pp. 184–200 (2001)Google Scholar
  38. 38.
    Rackoff, C., Simon, D.R.: Non-interactive Zero-Knowledge Proof of Knowledge and Chosen Ciphertext Attack. In: Feigenbaum, J. (ed.) CRYPTO 1991. LNCS, vol. 576, pp. 433–444. Springer, Heidelberg (1992)Google Scholar

Copyright information

© International Association for Cryptologic Research 2013

Authors and Affiliations

  • Mohammad Hajiabadi
    • 1
  • Bruce M. Kapron
    • 1
  1. 1.Dept. of Computer ScienceUniversity of VictoriaVictoriaCanada

Personalised recommendations