Computational Soundness for Interactive Primitives

  • Michael Backes
  • Esfandiar Mohammadi
  • Tim RuffingEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9326)


We present a generic computational soundness result for interactive cryptographic primitives. Our abstraction of interactive primitives leverages the Universal Composability (UC) framework, and thereby offers strong composability properties for our computational soundness result: given a computationally sound Dolev-Yao model for non-interactive primitives, and given UC-secure interactive primitives, we obtain computational soundness for the combined model that encompasses both the non-interactive and the interactive primitives. Our generic result is formulated in the CoSP framework for computational soundness proofs and supports any equivalence property expressible in CoSP such as strong secrecy and anonymity.

In a case study, we extend an existing computational soundness result by UC-secure blind signatures. We obtain computational soundness for blind signatures in uniform bi-processes in the applied \(\pi \)-calculus. This enables us to verify the untraceability of Chaum’s payment protocol in ProVerif in a computationally sound manner.



We thank the reviewers for their helpful and valuable comments. This work was supported by the German Ministry for Education and Research (BMBF) through funding for the Center for IT-Security, Privacy and Accountability (CISPA) and the German Universities Excellence Initiative.


  1. 1.
    Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: POPL 2001, pp. 104–115. ACM (2001)Google 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.
    Backes, M., Hofheinz, D., Unruh, D.: CoSP: a general framework for computational soundness proofs. In: CCS 2009, pp. 66–78. ACM (2009)Google Scholar
  4. 4.
    Backes, M., Laud, P.: Computationally sound secrecy proofs by mechanized flow analysis. In: CCS, pp. 370–379. ACM (2006)Google Scholar
  5. 5.
    Backes, M., Maffei, M., Mohammadi, E.: Computationally sound abstraction and verification of secure multi-party computations. In: FSTTCS 2010, pp. 352–363. Schloss Dagstuhl (2010)Google Scholar
  6. 6.
    Backes, M., Mohammadi, E., Ruffing, T.: Computational soundness results for ProVerif. In: Abadi, M., Kremer, S. (eds.) POST 2014. LNCS, vol. 8414, pp. 42–62. Springer, Heidelberg (2014)CrossRefGoogle Scholar
  7. 7.
    Backes, M., Pfitzmann, B., Waidner, M.: A composable cryptographic library with nested operations (extended abstract). In: CCS 2003, pp. 220–230. ACM (2003)Google Scholar
  8. 8.
    Backes, M., Pfitzmann, B., Waidner, M.: The reactive simulatability (RSIM) framework for asynchronous systems. Inf. Comput. 205(12), 1685–1720 (2007)MathSciNetCrossRefGoogle Scholar
  9. 9.
    Bana, G., Comon-Lundh, H.: A computationally complete symbolic attacker for equivalence properties. In: CCS 2014, pp. 609–620 (2014)Google Scholar
  10. 10.
    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
  11. 11.
    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
  12. 12.
    Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. In: LICS, pp. 331–340 (2005)Google Scholar
  13. 13.
    Blanchet, B., Fournet, C.: Automated verification of selected equivalences for security protocols. In: LICS 2005, pp. 331–340. IEEE (2005)Google Scholar
  14. 14.
    Böhl, F., Cortier, V., Warinschi, B.: Deduction soundness: prove one, get five for free. In: CCS 2013, pp. 1261–1272. ACM (2013)Google Scholar
  15. 15.
    Böhl, F., Unruh, D.: Symbolic universal composability. In: CSF 2013. IEEE (2013)Google Scholar
  16. 16.
    Camenisch, J., Krenn, S., Shoup, V.: A framework for practical universally composable zero-knowledge protocols. In: Lee, D.H., Wang, X. (eds.) ASIACRYPT 2011. LNCS, vol. 7073, pp. 449–467. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  17. 17.
    Canetti, R.: Universally Composable Security: A New Paradigm for Cryptographic Protocols. Full and revised version of FOCS 2001 paper. IACR ePrint Archive: 2000/067/20130717:020004 (2013)Google Scholar
  18. 18.
    Canetti, R., Fischlin, M.: Universally composable commitments. In: Kilian, J. (ed.) CRYPTO 2001. LNCS, vol. 2139, pp. 19–23. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  19. 19.
    Canetti, R., Gajek, S.: Universally Composable Symbolic Analysis of Diffie-Hellman based Key Exchange. IACR ePrint Archive: 2010/303 (2010)Google Scholar
  20. 20.
    Canetti, R., Herzog, J.: Universally composable symbolic security analysis. J. Cryptol. 24(1), 83–147 (2011)MathSciNetCrossRefGoogle Scholar
  21. 21.
    Canetti, R., Krawczyk, H.: Security analysis of IKE’s signature-based key-exchange protocol. In: Yung, M. (ed.) CRYPTO 2002. LNCS, vol. 2442, pp. 143–161. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  22. 22.
    Canetti, R., Kushilevitz, E., Lindell, Y.: On the limitations of universally composable two-party computation without set-up assumptions. J. Cryptol. 19(2), 68–86 (2003)MathSciNetzbMATHGoogle Scholar
  23. 23.
    Canetti, R., Lindell, Y., Ostrovsky, R., Sahai, A.: Universally composable two-party and multi-party secure computation. In: STOC 2002, pp. 494–503. ACM (2002)Google Scholar
  24. 24.
    Chandran, N., Goyal, V., Sahai, A.: New constructions for UC secure computation using tamper-proof hardware. In: Smart, N. (ed.) EUROCRYPT 2008. LNCS, vol. 4965, pp. 545–562. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  25. 25.
    Chaum, D.: Blind Signatures for Untraceable Payments. In: CRYPTO 1982, pp. 199–203. Plenum Press (1982)Google Scholar
  26. 26.
    Cheval, V.: APTE: an algorithm for proving trace equivalence. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 587–592. Springer, Heidelberg (2014)CrossRefGoogle Scholar
  27. 27.
    Comon-Lundh, H., Cortier, V.: Computational Soundness of Observational Equivalence. In: CCS 2008, pp. 109–118. ACM (2008)Google Scholar
  28. 28.
    Comon-Lundh, H., Cortier, V., Scerri, G.: Security proof with dishonest keys. In: Degano, P., Guttman, J.D. (eds.) POST 2012. LNCS, vol. 7215, pp. 149–168. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  29. 29.
    Comon-Lundh, H., Hagiya, M., Kawamoto, Y., Sakurada, H.: Computational soundness of indistinguishability properties without computable parsing. In: Ryan, M.D., Smyth, B., Wang, G. (eds.) ISPEC 2012. LNCS, vol. 7232, pp. 63–79. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  30. 30.
    Computational Soundness for Interactive Primitives (full version of this paper).
  31. 31.
    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
  32. 32.
    Cortier, V., Warinschi, B.: A Composable Computational Soundness Notion. In: CCS 2011, pp. 63–74. ACM (2011)Google Scholar
  33. 33.
    Dahl, M., Damgård, I.: Universally composable symbolic analysis for two-party protocols based on homomorphic encryption. In: Nguyen, P.Q., Oswald, E. (eds.) EUROCRYPT 2014. LNCS, vol. 8441, pp. 695–712. Springer, Heidelberg (2014)CrossRefGoogle Scholar
  34. 34.
    Delaune, S., Kremer, S., Pereira, O.: Simulation based security in the applied Pi calculus. In: FSTTCS 2009, pp. 169–180. Schloss Dagstuhl (2009)Google Scholar
  35. 35.
    Delaune, S., Kremer, S., Ryan, M.: Verifying privacy-type properties of electronic voting protocols. J. Comput. Secur. 17(4), 435–487 (2009)CrossRefGoogle Scholar
  36. 36.
    Delaune, S., Kremer, S., Ryan, M.D., Steel, G.: Formal analysis of protocols based on TPM state registers. In: CSF, pp. 66–80. IEEE (2011)Google Scholar
  37. 37.
    Diffie, W., Van Oorschot, P.C., Wiener, M.J.: Authentication and authenticated key exchanges. Des. Codes Crypt. 2(2), 107–125 (1992)MathSciNetCrossRefGoogle Scholar
  38. 38.
    Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Trans. Inf. Theory 29(2), 198–208 (1983)MathSciNetCrossRefGoogle Scholar
  39. 39.
    Dougherty, D.J., Guttman, J.D.: An algebra for symbolic Diffie-Hellman protocol analysis. In: Palamidessi, C., Ryan, M.D. (eds.) TGC 2012. LNCS, vol. 8191, pp. 164–181. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  40. 40.
    Even, S., Goldreich, O.: On the security of multi-party ping-pong protocols. In: FOCS 1983, pp. 34–39. IEEE (1983)Google Scholar
  41. 41.
    Fischlin, M.: Round-optimal composable blind signatures in the common reference string model. In: Dwork, C. (ed.) CRYPTO 2006. LNCS, vol. 4117, pp. 60–77. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  42. 42.
    Fournet, C., Kohlweiss, M., Strub, P.-Y.: Modular code-based cryptographic verification. In: CCS 2011, pp. 341–350. ACM (2011)Google Scholar
  43. 43.
    Goldwasser, S., Micali, S., Rackoff, C.: The knowledge complexity of interactive proof systems. SIAM J. Comp. 18(1), 186–207 (1989)MathSciNetCrossRefGoogle Scholar
  44. 44.
    Hofheinz, D., Shoup, V.: GNUC: a new universal composability framework. J. Cryptol. 28(3), 423–508 (2013)MathSciNetCrossRefGoogle Scholar
  45. 45.
    Kremer, S., Mazaré, L.: Adaptive soundness of static equivalence. In: Biskup, S., López, J. (eds.) ESORICS 2007. LNCS, vol. 4734, pp. 610–625. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  46. 46.
    Küsters, R., Scapin, E., Truderung, T., Graf, J.: Extending and applying a framework for the cryptographic verification of java programs. In: Abadi, M., Kremer, S. (eds.) POST 2014. LNCS, vol. 8414, pp. 220–239. Springer, Heidelberg (2014)CrossRefGoogle Scholar
  47. 47.
    Küsters, R., Truderung, T., Graf, J.: A framework for the cryptographic verification of java-like programs. In: CSF 2012, pp. 198–212. IEEE (2012)Google Scholar
  48. 48.
    Küsters, R., Tuengerthal, M.: The IITM Model: a Simple and Expressive Model for Universal Composability. IACR ePrint Archive: 2013/025 (2013)Google Scholar
  49. 49.
    Meier, S., Schmidt, B., Cremers, C., Basin, D.: The TAMARIN prover for the symbolic analysis of security protocols. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 696–701. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  50. 50.
    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
  51. 51.
  52. 52.
    Sprenger, C., Backes, M., Basin, D., Pfitzmann, B., Waidner, M.: Cryptographically sound theorem proving. In: CSFW 2006, pp. 153–166. IEEE (2006)Google Scholar
  53. 53.
    Swamy, N., Weinberger, J., Schlesinger, C., Chen, J., Livshits, B.: Verifying higherorder programs with the Dijkstra Monad. In: PLDI 2013, pp. 387–398. ACM (2013)Google Scholar
  54. 54.
    Unruh, D.: Termination-insensitive computational indistinguishability (and applications to computational soundness). In: CSF 2011, pp. 251–265. IEEE (2011)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2015

Open Access This chapter is licensed under the terms of the Creative Commons Attribution-NonCommercial 2.5 International License (, which permits any noncommercial use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

Authors and Affiliations

  • Michael Backes
    • 1
  • Esfandiar Mohammadi
    • 1
  • Tim Ruffing
    • 1
    Email author
  1. 1.CISPASaarland UniversitySaarbrückenGermany

Personalised recommendations