Computational soundness for interactive primitives. (English) Zbl 1502.68052

Backes, Michael; Mohammadi, Esfandiar; Ruffing, Tim

Pernul, Günther (ed.) et al., Computer security – ESORICS 2015. 20th European symposium on research in computer security, Vienna, Austria, September 21–25, 2015. Proceedings. Part I. Cham: Springer. Lect. Notes Comput. Sci. 9326, 125-145 (2015).

Summary: 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.
For the entire collection see [Zbl 1492.68028].

MSC:

68M25	Computer security
94A60	Cryptography

References:

[1]	Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: POPL 2001, pp. 104-115. ACM (2001) · Zbl 1323.68398
[2]	Abadi, M.; Baudet, M.; Warinschi, B.; Aceto, L.; Ingólfsdóttir, A., Guessing attacks and the computational soundness of static equivalence, Foundations of Software Science and Computation Structures, 398-412, 2006, Heidelberg: Springer, Heidelberg · Zbl 1180.94044 · doi:10.1007/11690634_27
[3]	Backes, M., Hofheinz, D., Unruh, D.: CoSP: a general framework for computational soundness proofs. In: CCS 2009, pp. 66-78. ACM (2009)
[4]	Backes, M., Laud, P.: Computationally sound secrecy proofs by mechanized flow analysis. In: CCS, pp. 370-379. ACM (2006)
[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) · Zbl 1245.68027
[6]	Backes, M.; Mohammadi, E.; Ruffing, T.; Abadi, M.; Kremer, S., Computational soundness results for ProVerif, Principles of Security and Trust, 42-62, 2014, Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-54792-8_3
[7]	Backes, M., Pfitzmann, B., Waidner, M.: A composable cryptographic library with nested operations (extended abstract). In: CCS 2003, pp. 220-230. ACM (2003)
[8]	Backes, M.; Pfitzmann, B.; Waidner, M., The reactive simulatability (RSIM) framework for asynchronous systems, Inf. Comput., 205, 12, 1685-1720, 2007 · Zbl 1132.68025 · doi:10.1016/j.ic.2007.05.002
[9]	Bana, G., Comon-Lundh, H.: A computationally complete symbolic attacker for equivalence properties. In: CCS 2014, pp. 609-620 (2014)
[10]	Bana, G.; Comon-Lundh, H.; Degano, P.; Guttman, JD, Towards unconditional soundness: computationally complete symbolic attacker, Principles of Security and Trust, 189-208, 2012, Heidelberg: Springer, Heidelberg · Zbl 1353.68018 · doi:10.1007/978-3-642-28641-4_11
[11]	Baudet, M.; Cortier, V.; Kremer, S.; Caires, L.; Italiano, GF; Monteiro, L.; Palamidessi, C.; Yung, M., Computationally sound implementations of equational theories against passive adversaries, Automata, Languages and Programming, 652-663, 2005, Heidelberg: Springer, Heidelberg · Zbl 1084.94510 · doi:10.1007/11523468_53
[12]	Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. In: LICS, pp. 331-340 (2005)
[13]	Blanchet, B., Fournet, C.: Automated verification of selected equivalences for security protocols. In: LICS 2005, pp. 331-340. IEEE (2005)
[14]	Böhl, F., Cortier, V., Warinschi, B.: Deduction soundness: prove one, get five for free. In: CCS 2013, pp. 1261-1272. ACM (2013)
[15]	Böhl, F., Unruh, D.: Symbolic universal composability. In: CSF 2013. IEEE (2013)
[16]	Camenisch, J.; Krenn, S.; Shoup, V.; Lee, DH; Wang, X., A framework for practical universally composable zero-knowledge protocols, Advances in Cryptology - ASIACRYPT 2011, 449-467, 2011, Heidelberg: Springer, Heidelberg · Zbl 1227.94036 · doi:10.1007/978-3-642-25385-0_24
[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)
[18]	Canetti, R.; Fischlin, M.; Kilian, J., Universally composable commitments, Advances in Cryptology — CRYPTO 2001, 19-23, 2001, Heidelberg: Springer, Heidelberg · doi:10.1007/3-540-44647-8_2
[19]	Canetti, R., Gajek, S.: Universally Composable Symbolic Analysis of Diffie-Hellman based Key Exchange. IACR ePrint Archive: 2010/303 (2010)
[20]	Canetti, R.; Herzog, J., Universally composable symbolic security analysis, J. Cryptol., 24, 1, 83-147, 2011 · Zbl 1208.94039 · doi:10.1007/s00145-009-9055-0
[21]	Canetti, R.; Krawczyk, H.; Yung, M., Security analysis of IKE’s signature-based key-exchange protocol, Advances in Cryptology — CRYPTO 2002, 143-161, 2002, Heidelberg: Springer, Heidelberg · Zbl 1026.94524 · doi:10.1007/3-540-45708-9_10
[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 · Zbl 1038.94523
[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) · Zbl 1192.94112
[24]	Chandran, N.; Goyal, V.; Sahai, A.; Smart, N., New constructions for UC secure computation using tamper-proof hardware, Advances in Cryptology - EUROCRYPT 2008, 545-562, 2008, Heidelberg: Springer, Heidelberg · Zbl 1149.68376 · doi:10.1007/978-3-540-78967-3_31
[25]	Chaum, D.: Blind Signatures for Untraceable Payments. In: CRYPTO 1982, pp. 199-203. Plenum Press (1982) · Zbl 0521.94012
[26]	Cheval, V.; Ábrahám, E.; Havelund, K., APTE: an algorithm for proving trace equivalence, Tools and Algorithms for the Construction and Analysis of Systems, 587-592, 2014, Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-54862-8_50
[27]	Comon-Lundh, H., Cortier, V.: Computational Soundness of Observational Equivalence. In: CCS 2008, pp. 109-118. ACM (2008)
[28]	Comon-Lundh, H.; Cortier, V.; Scerri, G.; Degano, P.; Guttman, JD, Security proof with dishonest keys, Principles of Security and Trust, 149-168, 2012, Heidelberg: Springer, Heidelberg · Zbl 1353.68070 · doi:10.1007/978-3-642-28641-4_9
[29]	Comon-Lundh, H.; Hagiya, M.; Kawamoto, Y.; Sakurada, H.; Ryan, MD; Smyth, B.; Wang, G., Computational soundness of indistinguishability properties without computable parsing, Information Security Practice and Experience, 63-79, 2012, Heidelberg: Springer, Heidelberg · Zbl 1292.94048 · doi:10.1007/978-3-642-29101-2_5
[30]	Computational Soundness for Interactive Primitives (full version of this paper). https://www.infsec.cs.uni-saarland.de/ mohammadi/interactive.html
[31]	Cortier, V.; Kremer, S.; Küsters, R.; Warinschi, B.; Arun-Kumar, S.; Garg, N., Computationally sound symbolic secrecy in the presence of hash functions, FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science, 176-187, 2006, Heidelberg: Springer, Heidelberg · Zbl 1177.94142 · doi:10.1007/11944836_18
[32]	Cortier, V., Warinschi, B.: A Composable Computational Soundness Notion. In: CCS 2011, pp. 63-74. ACM (2011)
[33]	Dahl, M.; Damgård, I.; Nguyen, PQ; Oswald, E., Universally composable symbolic analysis for two-party protocols based on homomorphic encryption, Advances in Cryptology - EUROCRYPT 2014, 695-712, 2014, Heidelberg: Springer, Heidelberg · Zbl 1328.68025 · doi:10.1007/978-3-642-55220-5_38
[34]	Delaune, S., Kremer, S., Pereira, O.: Simulation based security in the applied Pi calculus. In: FSTTCS 2009, pp. 169-180. Schloss Dagstuhl (2009) · Zbl 1250.94035
[35]	Delaune, S.; Kremer, S.; Ryan, M., Verifying privacy-type properties of electronic voting protocols, J. Comput. Secur., 17, 4, 435-487, 2009 · doi:10.3233/JCS-2009-0340
[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)
[37]	Diffie, W.; Van Oorschot, PC; Wiener, MJ, Authentication and authenticated key exchanges, Des. Codes Crypt., 2, 2, 107-125, 1992 · doi:10.1007/BF00124891
[38]	Dolev, D.; Yao, AC, On the security of public key protocols, IEEE Trans. Inf. Theory, 29, 2, 198-208, 1983 · Zbl 0502.94005 · doi:10.1109/TIT.1983.1056650
[39]	Dougherty, DJ; Guttman, JD; Palamidessi, C.; Ryan, MD, An algebra for symbolic Diffie-Hellman protocol analysis, Trustworthy Global Computing, 164-181, 2013, Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-41157-1_11
[40]	Even, S., Goldreich, O.: On the security of multi-party ping-pong protocols. In: FOCS 1983, pp. 34-39. IEEE (1983)
[41]	Fischlin, M.; Dwork, C., Round-optimal composable blind signatures in the common reference string model, Advances in Cryptology - CRYPTO 2006, 60-77, 2006, Heidelberg: Springer, Heidelberg · Zbl 1161.94441 · doi:10.1007/11818175_4
[42]	Fournet, C., Kohlweiss, M., Strub, P.-Y.: Modular code-based cryptographic verification. In: CCS 2011, pp. 341-350. ACM (2011)
[43]	Goldwasser, S.; Micali, S.; Rackoff, C., The knowledge complexity of interactive proof systems, SIAM J. Comp., 18, 1, 186-207, 1989 · Zbl 0677.68062 · doi:10.1137/0218012
[44]	Hofheinz, D.; Shoup, V., GNUC: a new universal composability framework, J. Cryptol., 28, 3, 423-508, 2013 · Zbl 1356.94062 · doi:10.1007/s00145-013-9160-y
[45]	Kremer, S.; Mazaré, L.; Biskup, S.; López, J., Adaptive soundness of static equivalence, Computer Security - ESORICS 2007, 610-625, 2007, Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-540-74835-9_40
[46]	Küsters, R.; Scapin, E.; Truderung, T.; Graf, J.; Abadi, M.; Kremer, S., Extending and applying a framework for the cryptographic verification of java programs, Principles of Security and Trust, 220-239, 2014, Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-54792-8_12
[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)
[48]	Küsters, R., Tuengerthal, M.: The IITM Model: a Simple and Expressive Model for Universal Composability. IACR ePrint Archive: 2013/025 (2013)
[49]	Meier, S.; Schmidt, B.; Cremers, C.; Basin, D.; Sharygina, N.; Veith, H., The TAMARIN prover for the symbolic analysis of security protocols, Computer Aided Verification, 696-701, 2013, Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-39799-8_48
[50]	Micciancio, D.; Warinschi, B.; Naor, M., Soundness of formal encryption in the presence of active adversaries, Theory of Cryptography, 133-151, 2004, Heidelberg: Springer, Heidelberg · Zbl 1197.94198 · doi:10.1007/978-3-540-24638-1_8
[51]	ProVerif code of the case study. https://www.infsec.cs.uni-saarland.de/ mohammadi/paper/case_study_untraceable_payments.zip
[52]	Sprenger, C., Backes, M., Basin, D., Pfitzmann, B., Waidner, M.: Cryptographically sound theorem proving. In: CSFW 2006, pp. 153-166. IEEE (2006)
[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)
[54]	Unruh, D.: Termination-insensitive computational indistinguishability (and applications to computational soundness). In: CSF 2011, pp. 251-265. IEEE (2011)