{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T00:40:10Z","timestamp":1748652010729,"version":"3.41.0"},"publisher-location":"Cham","reference-count":54,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319241739"},{"type":"electronic","value":"9783319241746"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-24174-6_7","type":"book-chapter","created":{"date-parts":[[2015,10,9]],"date-time":"2015-10-09T11:36:32Z","timestamp":1444390592000},"page":"125-145","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Computational Soundness for Interactive Primitives"],"prefix":"10.1007","author":[{"given":"Michael","family":"Backes","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Esfandiar","family":"Mohammadi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tim","family":"Ruffing","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,1,13]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: POPL 2001, pp. 104\u2013115. ACM (2001)","DOI":"10.1145\/373243.360213"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1007\/11690634_27","volume-title":"Foundations of Software Science and Computation Structures","author":"M Abadi","year":"2006","unstructured":"Abadi, M., Baudet, M., Warinschi, B.: Guessing attacks and the computational soundness of static equivalence. In: Aceto, L., Ing\u00f3lfsd\u00f3ttir, A. (eds.) FOSSACS 2006. LNCS, vol. 3921, pp. 398\u2013412. Springer, Heidelberg (2006)"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"Backes, M., Hofheinz, D., Unruh, D.: CoSP: a general framework for computational soundness proofs. In: CCS 2009, pp. 66\u201378. ACM (2009)","DOI":"10.1145\/1653662.1653672"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"Backes, M., Laud, P.: Computationally sound secrecy proofs by mechanized flow analysis. In: CCS, pp. 370\u2013379. ACM (2006)","DOI":"10.1145\/1180405.1180450"},{"key":"7_CR5","unstructured":"Backes, M., Maffei, M., Mohammadi, E.: Computationally sound abstraction and verification of secure multi-party computations. In: FSTTCS 2010, pp. 352\u2013363. Schloss Dagstuhl (2010)"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/978-3-642-54792-8_3","volume-title":"Principles of Security and Trust","author":"M Backes","year":"2014","unstructured":"Backes, M., Mohammadi, E., Ruffing, T.: Computational soundness results for ProVerif. In: Abadi, M., Kremer, S. (eds.) POST 2014. LNCS, vol. 8414, pp. 42\u201362. Springer, Heidelberg (2014)"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Backes, M., Pfitzmann, B., Waidner, M.: A composable cryptographic library with nested operations (extended abstract). In: CCS 2003, pp. 220\u2013230. ACM (2003)","DOI":"10.1145\/948109.948140"},{"issue":"12","key":"7_CR8","doi-asserted-by":"publisher","first-page":"1685","DOI":"10.1016\/j.ic.2007.05.002","volume":"205","author":"M Backes","year":"2007","unstructured":"Backes, M., Pfitzmann, B., Waidner, M.: The reactive simulatability (RSIM) framework for asynchronous systems. Inf. Comput. 205(12), 1685\u20131720 (2007)","journal-title":"Inf. Comput."},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Bana, G., Comon-Lundh, H.: A computationally complete symbolic attacker for equivalence properties. In: CCS 2014, pp. 609\u2013620 (2014)","DOI":"10.1145\/2660267.2660276"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/978-3-642-28641-4_11","volume-title":"Principles of Security and Trust","author":"G Bana","year":"2012","unstructured":"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\u2013208. Springer, Heidelberg (2012)"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"652","DOI":"10.1007\/11523468_53","volume-title":"Automata, Languages and Programming","author":"M Baudet","year":"2005","unstructured":"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\u2013663. Springer, Heidelberg (2005)"},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. In: LICS, pp. 331\u2013340 (2005)","DOI":"10.1109\/LICS.2005.8"},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"Blanchet, B., Fournet, C.: Automated verification of selected equivalences for security protocols. In: LICS 2005, pp. 331\u2013340. IEEE (2005)","DOI":"10.1109\/LICS.2005.8"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"B\u00f6hl, F., Cortier, V., Warinschi, B.: Deduction soundness: prove one, get five for free. In: CCS 2013, pp. 1261\u20131272. ACM (2013)","DOI":"10.1145\/2508859.2516711"},{"key":"7_CR15","doi-asserted-by":"crossref","unstructured":"B\u00f6hl, F., Unruh, D.: Symbolic universal composability. In: CSF 2013. IEEE (2013)","DOI":"10.1109\/CSF.2013.24"},{"key":"7_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1007\/978-3-642-25385-0_24","volume-title":"Advances in Cryptology \u2013 ASIACRYPT 2011","author":"J Camenisch","year":"2011","unstructured":"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\u2013467. Springer, Heidelberg (2011)"},{"key":"7_CR17","unstructured":"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)"},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/3-540-44647-8_2","volume-title":"Advances in Cryptology \u2014 CRYPTO 2001","author":"R Canetti","year":"2001","unstructured":"Canetti, R., Fischlin, M.: Universally composable commitments. In: Kilian, J. (ed.) CRYPTO 2001. LNCS, vol. 2139, pp. 19\u201323. Springer, Heidelberg (2001)"},{"key":"7_CR19","unstructured":"Canetti, R., Gajek, S.: Universally Composable Symbolic Analysis of Diffie-Hellman based Key Exchange. IACR ePrint Archive: 2010\/303 (2010)"},{"issue":"1","key":"7_CR20","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/s00145-009-9055-0","volume":"24","author":"R Canetti","year":"2011","unstructured":"Canetti, R., Herzog, J.: Universally composable symbolic security analysis. J. Cryptol. 24(1), 83\u2013147 (2011)","journal-title":"J. Cryptol."},{"key":"7_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/3-540-45708-9_10","volume-title":"Advances in Cryptology \u2014 CRYPTO 2002","author":"R Canetti","year":"2002","unstructured":"Canetti, R., Krawczyk, H.: Security analysis of IKE\u2019s signature-based key-exchange protocol. In: Yung, M. (ed.) CRYPTO 2002. LNCS, vol. 2442, pp. 143\u2013161. Springer, Heidelberg (2002)"},{"issue":"2","key":"7_CR22","first-page":"68","volume":"19","author":"R Canetti","year":"2003","unstructured":"Canetti, R., Kushilevitz, E., Lindell, Y.: On the limitations of universally composable two-party computation without set-up assumptions. J. Cryptol. 19(2), 68\u201386 (2003)","journal-title":"J. Cryptol."},{"key":"7_CR23","doi-asserted-by":"crossref","unstructured":"Canetti, R., Lindell, Y., Ostrovsky, R., Sahai, A.: Universally composable two-party and multi-party secure computation. In: STOC 2002, pp. 494\u2013503. ACM (2002)","DOI":"10.1145\/509907.509980"},{"key":"7_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"545","DOI":"10.1007\/978-3-540-78967-3_31","volume-title":"Advances in Cryptology \u2013 EUROCRYPT 2008","author":"N Chandran","year":"2008","unstructured":"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\u2013562. Springer, Heidelberg (2008)"},{"key":"7_CR25","doi-asserted-by":"crossref","unstructured":"Chaum, D.: Blind Signatures for Untraceable Payments. In: CRYPTO 1982, pp. 199\u2013203. Plenum Press (1982)","DOI":"10.1007\/978-1-4757-0602-4_18"},{"key":"7_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"587","DOI":"10.1007\/978-3-642-54862-8_50","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"V Cheval","year":"2014","unstructured":"Cheval, V.: APTE: an algorithm for proving trace equivalence. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 587\u2013592. Springer, Heidelberg (2014)"},{"key":"7_CR27","doi-asserted-by":"crossref","unstructured":"Comon-Lundh, H., Cortier, V.: Computational Soundness of Observational Equivalence. In: CCS 2008, pp. 109\u2013118. ACM (2008)","DOI":"10.1145\/1455770.1455786"},{"key":"7_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-642-28641-4_9","volume-title":"Principles of Security and Trust","author":"H Comon-Lundh","year":"2012","unstructured":"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\u2013168. Springer, Heidelberg (2012)"},{"key":"7_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/978-3-642-29101-2_5","volume-title":"Information Security Practice and Experience","author":"H Comon-Lundh","year":"2012","unstructured":"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\u201379. Springer, Heidelberg (2012)"},{"key":"7_CR30","unstructured":"Computational Soundness for Interactive Primitives (full version of this paper). https:\/\/www.infsec.cs.uni-saarland.de\/~mohammadi\/interactive.html"},{"key":"7_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/11944836_18","volume-title":"FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science","author":"V Cortier","year":"2006","unstructured":"Cortier, V., Kremer, S., K\u00fcsters, 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\u2013187. Springer, Heidelberg (2006)"},{"key":"7_CR32","doi-asserted-by":"crossref","unstructured":"Cortier, V., Warinschi, B.: A Composable Computational Soundness Notion. In: CCS 2011, pp. 63\u201374. ACM (2011)","DOI":"10.1145\/2046707.2046717"},{"key":"7_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"695","DOI":"10.1007\/978-3-642-55220-5_38","volume-title":"Advances in Cryptology \u2013 EUROCRYPT 2014","author":"M Dahl","year":"2014","unstructured":"Dahl, M., Damg\u00e5rd, 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\u2013712. Springer, Heidelberg (2014)"},{"key":"7_CR34","unstructured":"Delaune, S., Kremer, S., Pereira, O.: Simulation based security in the applied Pi calculus. In: FSTTCS 2009, pp. 169\u2013180. Schloss Dagstuhl (2009)"},{"issue":"4","key":"7_CR35","doi-asserted-by":"publisher","first-page":"435","DOI":"10.3233\/JCS-2009-0340","volume":"17","author":"S Delaune","year":"2009","unstructured":"Delaune, S., Kremer, S., Ryan, M.: Verifying privacy-type properties of electronic voting protocols. J. Comput. Secur. 17(4), 435\u2013487 (2009)","journal-title":"J. Comput. Secur."},{"key":"7_CR36","doi-asserted-by":"crossref","unstructured":"Delaune, S., Kremer, S., Ryan, M.D., Steel, G.: Formal analysis of protocols based on TPM state registers. In: CSF, pp. 66\u201380. IEEE (2011)","DOI":"10.1109\/CSF.2011.12"},{"issue":"2","key":"7_CR37","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/BF00124891","volume":"2","author":"W Diffie","year":"1992","unstructured":"Diffie, W., Van Oorschot, P.C., Wiener, M.J.: Authentication and authenticated key exchanges. Des. Codes Crypt. 2(2), 107\u2013125 (1992)","journal-title":"Des. Codes Crypt."},{"issue":"2","key":"7_CR38","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"29","author":"D Dolev","year":"1983","unstructured":"Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Trans. Inf. Theory 29(2), 198\u2013208 (1983)","journal-title":"IEEE Trans. Inf. Theory"},{"key":"7_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/978-3-642-41157-1_11","volume-title":"Trustworthy Global Computing","author":"DJ Dougherty","year":"2013","unstructured":"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\u2013181. Springer, Heidelberg (2013)"},{"key":"7_CR40","doi-asserted-by":"crossref","unstructured":"Even, S., Goldreich, O.: On the security of multi-party ping-pong protocols. In: FOCS 1983, pp. 34\u201339. IEEE (1983)","DOI":"10.1109\/SFCS.1983.42"},{"key":"7_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/11818175_4","volume-title":"Advances in Cryptology - CRYPTO 2006","author":"M Fischlin","year":"2006","unstructured":"Fischlin, M.: Round-optimal composable blind signatures in the common reference string model. In: Dwork, C. (ed.) CRYPTO 2006. LNCS, vol. 4117, pp. 60\u201377. Springer, Heidelberg (2006)"},{"key":"7_CR42","doi-asserted-by":"crossref","unstructured":"Fournet, C., Kohlweiss, M., Strub, P.-Y.: Modular code-based cryptographic verification. In: CCS 2011, pp. 341\u2013350. ACM (2011)","DOI":"10.1145\/2046707.2046746"},{"issue":"1","key":"7_CR43","doi-asserted-by":"publisher","first-page":"186","DOI":"10.1137\/0218012","volume":"18","author":"S Goldwasser","year":"1989","unstructured":"Goldwasser, S., Micali, S., Rackoff, C.: The knowledge complexity of interactive proof systems. SIAM J. Comp. 18(1), 186\u2013207 (1989)","journal-title":"SIAM J. Comp."},{"issue":"3","key":"7_CR44","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/s00145-013-9160-y","volume":"28","author":"D Hofheinz","year":"2013","unstructured":"Hofheinz, D., Shoup, V.: GNUC: a new universal composability framework. J. Cryptol. 28(3), 423\u2013508 (2013)","journal-title":"J. Cryptol."},{"key":"7_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"610","DOI":"10.1007\/978-3-540-74835-9_40","volume-title":"Computer Security \u2013 ESORICS 2007","author":"S Kremer","year":"2007","unstructured":"Kremer, S., Mazar\u00e9, L.: Adaptive soundness of static equivalence. In: Biskup, S., L\u00f3pez, J. (eds.) ESORICS 2007. LNCS, vol. 4734, pp. 610\u2013625. Springer, Heidelberg (2007)"},{"key":"7_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/978-3-642-54792-8_12","volume-title":"Principles of Security and Trust","author":"R K\u00fcsters","year":"2014","unstructured":"K\u00fcsters, 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\u2013239. Springer, Heidelberg (2014)"},{"key":"7_CR47","doi-asserted-by":"crossref","unstructured":"K\u00fcsters, R., Truderung, T., Graf, J.: A framework for the cryptographic verification of java-like programs. In: CSF 2012, pp. 198\u2013212. IEEE (2012)","DOI":"10.1109\/CSF.2012.9"},{"key":"7_CR48","unstructured":"K\u00fcsters, R., Tuengerthal, M.: The IITM Model: a Simple and Expressive Model for Universal Composability. IACR ePrint Archive: 2013\/025 (2013)"},{"key":"7_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1007\/978-3-642-39799-8_48","volume-title":"Computer Aided Verification","author":"S Meier","year":"2013","unstructured":"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\u2013701. Springer, Heidelberg (2013)"},{"key":"7_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/978-3-540-24638-1_8","volume-title":"Theory of Cryptography","author":"D Micciancio","year":"2004","unstructured":"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\u2013151. Springer, Heidelberg (2004)"},{"key":"7_CR51","unstructured":"ProVerif code of the case study. https:\/\/www.infsec.cs.uni-saarland.de\/~mohammadi\/paper\/case_study_untraceable_payments.zip"},{"key":"7_CR52","doi-asserted-by":"crossref","unstructured":"Sprenger, C., Backes, M., Basin, D., Pfitzmann, B., Waidner, M.: Cryptographically sound theorem proving. In: CSFW 2006, pp. 153\u2013166. IEEE (2006)","DOI":"10.1109\/CSFW.2006.10"},{"key":"7_CR53","doi-asserted-by":"crossref","unstructured":"Swamy, N., Weinberger, J., Schlesinger, C., Chen, J., Livshits, B.: Verifying higherorder programs with the Dijkstra Monad. In: PLDI 2013, pp. 387\u2013398. ACM (2013)","DOI":"10.1145\/2499370.2491978"},{"key":"7_CR54","doi-asserted-by":"crossref","unstructured":"Unruh, D.: Termination-insensitive computational indistinguishability (and applications to computational soundness). In: CSF 2011, pp. 251\u2013265. IEEE (2011)","DOI":"10.1109\/CSF.2011.24"}],"container-title":["Lecture Notes in Computer Science","Computer Security -- ESORICS 2015"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24174-6_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T00:01:22Z","timestamp":1748649682000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-24174-6_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319241739","9783319241746"],"references-count":54,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24174-6_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"13 January 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}