Computational Soundness of Indistinguishability Properties without Computable Parsing

  • Hubert Comon-Lundh
  • Masami Hagiya
  • Yusuke Kawamoto
  • Hideki Sakurada
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7232)


We provide a symbolic model for protocols using public-key encryption and hash function, and prove that this model is computationally sound: if there is an attack in the computational world, then there is an attack in the symbolic (abstract) model. Our original contribution is that we deal with the security properties, such as anonymity, which cannot be described using a single execution trace, while considering an unbounded number of sessions of the protocols in the presence of active and adaptive adversaries. Our soundness proof is different from all existing studies in that it does not require a computable parsing function from bit strings to terms. This allows us to deal with more cryptographic primitives, such as a preimage-resistant and collision-resistant hash function whose input may have different lengths.


Hash Function Function Symbol Computation Tree Security Parameter Symbolic 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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Proc. of the 28th ACM Symposium on Principles of Programming Languages (POPL 2001), pp. 104–115 (2001)Google Scholar
  2. 2.
    Abadi, M., Rogaway, P.: Reconciling two views of cryptography (the computational soundness of formal encryption). Journal of Cryptology 15(2), 103–127 (2002)MathSciNetzbMATHGoogle Scholar
  3. 3.
    Backes, M., Hofheinz, D., Unruh, D.: CoSP: A general framework for computational soundness proofs. Cryptology ePrint Archive, Report 2009/080 (2009),
  4. 4.
    Backes, M., Pfitzmann, B., Waidner, M.: A composable cryptographic library with nested operations. In: Proc. of the 10th ACM Concerence on Computer and Communications Security (CCS 2003), pp. 220–230 (2003)Google Scholar
  5. 5.
    Backes, M., Pfitzmann, B., Waidner, M.: Limits of the BRSIM/UC Soundness of Dolev-Yao Models with Hashes. In: Gollmann, D., Meier, J., Sabelfeld, A. (eds.) ESORICS 2006. LNCS, vol. 4189, pp. 404–423. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  6. 6.
    Backes, M., Pfitzmann, B., Waidner, M.: The reactive simulatability (RSIM) framework for asynchronous systems. Information and Computation 205(12), 1685–1720 (2007)MathSciNetzbMATHCrossRefGoogle Scholar
  7. 7.
    Comon-Lundh, H., Cortier, V.: Computational soundness of observational equivalence. In: Proc. of the 15th ACM Conference on Computer and Communications Security (CCS 2008), pp. 109–118 (2008)Google Scholar
  8. 8.
    Cortier, V., Kremer, S., Küsters, R., Warinschi, B.: Computationally Sound Symbolic Secrecy in the Presence of Hash Functions. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 176–187. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  9. 9.
    Cortier, V., Warinschi, B.: Computationally Sound, Automated Proofs for Security Protocols. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 157–171. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  10. 10.
    Garcia, F.D., van Rossum, P.: Sound and complete computational interpretation of symbolic hashes in the standard model. Theor. Comput. Sci. 394(1-2), 112–133 (2008)zbMATHCrossRefGoogle Scholar
  11. 11.
    Janvier, R., Lakhnech, Y., Mazaré, L.: Computational soundness of symbolic analysis for protocols using hash functions. Electr. Notes Theor. Comput. Sci. 186, 121–139 (2007)CrossRefGoogle Scholar
  12. 12.
    Kawamoto, Y., Sakurada, H., Hagiya, M.: Computationally sound symbolic anonymity of a ring signature. In: Proc. of Joint Workshop on Foundations of Computer Security, Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security (FCS-ARSPA-WITS 2008), pp. 161–175 (2008)Google Scholar
  13. 13.
    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
  14. 14.
    Rogaway, P., Shrimpton, T.: Cryptographic Hash-Function Basics: Definitions, Implications, and Separations for Preimage Resistance, Second-Preimage Resistance, and Collision Resistance. In: Roy, B., Meier, W. (eds.) FSE 2004. LNCS, vol. 3017, pp. 371–388. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  15. 15.
    Unruh, D.: Termination-insensitive computational indistinguishability (and applications to computational soundness). In: Proc. of the 24th IEEE Computer Security Foundations Symposium (CSF 2011). IEEE Computer Society (June 2011)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Hubert Comon-Lundh
    • 1
  • Masami Hagiya
    • 2
  • Yusuke Kawamoto
    • 1
  • Hideki Sakurada
    • 3
  1. 1.LSV, CNRS, ENS Cachan and INRIAFrance
  2. 2.University of TokyoJapan
  3. 3.NTT Communication Science LaboratoriesNTT CorporationJapan

Personalised recommendations