{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T08:40:53Z","timestamp":1774946453412,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642547911","type":"print"},{"value":"9783642547928","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-642-54792-8_3","type":"book-chapter","created":{"date-parts":[[2014,3,21]],"date-time":"2014-03-21T13:35:12Z","timestamp":1395408912000},"page":"42-62","source":"Crossref","is-referenced-by-count":6,"title":["Computational Soundness Results for ProVerif"],"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","reference":[{"issue":"2","key":"3_CR1","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 Transactions on Information Theory\u00a029(2), 198\u2013208 (1983)","journal-title":"IEEE Transactions on Information Theory"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"Even, S., Goldreich, O.: On the security of multi-party ping-pong protocols. In: FOCS, pp. 34\u201339. IEEE (1983)","DOI":"10.1007\/978-1-4757-0602-4_31"},{"issue":"2","key":"3_CR3","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/BF00197942","volume":"7","author":"R. Kemmerer","year":"1994","unstructured":"Kemmerer, R., Meadows, C., Millen, J.: Three systems for cryptographic protocol analysis. J. of Crypt.\u00a07(2), 79\u2013130 (1994)","journal-title":"J. of Crypt."},{"key":"3_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/3-540-45614-7_18","volume-title":"FME 2002: Formal Methods - Getting IT Right","author":"M. Backes","year":"2002","unstructured":"Backes, M., Jacobi, C., Pfitzmann, B.: Deriving cryptographically sound implementations using composition and formally verified bisimulation. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol.\u00a02391, pp. 310\u2013329. Springer, Heidelberg (2002)"},{"issue":"4","key":"3_CR5","doi-asserted-by":"crossref","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.\u00a017(4), 435\u2013487 (2009)","journal-title":"J. Comput. Secur."},{"key":"3_CR6","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"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Blanchet, B., Abadi, M., Fournet, C.: Automated Verification of Selected Equivalences for Security Protocols. In: LICS, pp. 331\u2013340. IEEE (2005)","DOI":"10.1109\/LICS.2005.8"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Backes, M., Maffei, M., Unruh, D.: Zero-knowledge in the applied pi-calculus and automated verification of the direct anonymous attestation protocol. In: S&P, pp. 202\u2013215. IEEE (2008)","DOI":"10.1109\/SP.2008.23"},{"key":"3_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/978-3-642-28641-4_7","volume-title":"Principles of Security and Trust","author":"V. Cortier","year":"2012","unstructured":"Cortier, V., Wiedling, C.: A formal analysis of the norwegian E-voting protocol. In: Degano, P., Guttman, J.D. (eds.) POST 2012. LNCS, vol.\u00a07215, pp. 109\u2013128. Springer, Heidelberg (2012)"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Backes, M., Hritcu, C., Maffei, M.: Automated verification of remote electronic voting protocols in the applied pi-calculus. In: CSF, pp. 195\u2013209. IEEE (2008)","DOI":"10.1109\/CSF.2008.26"},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-540-31987-0_13","volume-title":"Programming Languages and Systems","author":"R. Janvier","year":"2005","unstructured":"Janvier, R., Lakhnech, Y., Mazar\u00e9, L.: Completing the picture: Soundness of formal encryption in the presence of active adversaries. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 172\u2013185. Springer, Heidelberg (2005)"},{"key":"3_CR12","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.\u00a02951, pp. 133\u2013151. Springer, Heidelberg (2004)"},{"key":"3_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-540-31987-0_12","volume-title":"Programming Languages and Systems","author":"V. Cortier","year":"2005","unstructured":"Cortier, V., Warinschi, B.: Computationally sound, automated proofs for security protocols. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 157\u2013171. Springer, Heidelberg (2005)"},{"key":"3_CR14","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.\u00a04337, pp. 176\u2013187. Springer, Heidelberg (2006)"},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"Backes, M., Hofheinz, D., Unruh, D.: CoSP: a general framework for computational soundness proofs. In: CCS, pp. 66\u201378. ACM (2009)","DOI":"10.1145\/1653662.1653672"},{"issue":"6","key":"3_CR16","first-page":"1077","volume":"18","author":"M. Backes","year":"2010","unstructured":"Backes, M., Unruh, D.: Computational soundness of symbolic zero-knowledge proofs. J. of Comp. Sec.\u00a018(6), 1077\u20131155 (2010)","journal-title":"J. of Comp. Sec."},{"key":"3_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/978-3-540-79104-1_26","volume-title":"Information Security Practice and Experience","author":"D. Galindo","year":"2008","unstructured":"Galindo, D., Garcia, F.D., van Rossum, P.: Computational soundness of non-malleable commitments. In: Chen, L., Mu, Y., Susilo, W. (eds.) ISPEC 2008. LNCS, vol.\u00a04991, pp. 361\u2013376. Springer, Heidelberg (2008)"},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"Cortier, V., Warinschi, B.: A composable computational soundness notion. In: CCS, pp. 63\u201374. ACM (2011)","DOI":"10.1145\/2046707.2046717"},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"B\u00f6hl, F., Cortier, V., Warinschi, B.: Deduction soundness: Prove one, get five for free. In: CCS, pp. 1261\u20131272. ACM (2013)","DOI":"10.1145\/2508859.2516711"},{"key":"3_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/978-3-642-36830-1_11","volume-title":"Principles of Security and Trust","author":"M. Backes","year":"2013","unstructured":"Backes, M., Bendun, F., Unruh, D.: Computational soundness of symbolic zero-knowledge proofs: weaker assumptions and mechanized verification. In: Basin, D., Mitchell, J.C. (eds.) POST 2013. LNCS, vol.\u00a07796, pp. 206\u2013225. Springer, Heidelberg (2013)"},{"key":"3_CR21","unstructured":"Backes, M., Maffei, M., Mohammadi, E.: Computationally sound abstraction and verification of secure multi-party computations. In: FSTTCS, Schloss Dagstuhl, pp. 352\u2013363 (2010)"},{"key":"3_CR22","doi-asserted-by":"crossref","unstructured":"Comon-Lundh, H., Cortier, V.: Computational soundness of observational equivalence. In: CCS, pp. 109\u2013118. ACM (2008)","DOI":"10.1145\/1455770.1455786"},{"key":"3_CR23","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.\u00a07215, pp. 149\u2013168. Springer, Heidelberg (2012)"},{"issue":"1","key":"3_CR24","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. of Crypt.\u00a024(1), 83\u2013147 (2011)","journal-title":"J. of Crypt."},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Backes, M., Pfitzmann, B., Waidner, M.: A composable cryptographic library with nested operations (extended abstract). In: CCS, pp. 220\u2013230 (2003)","DOI":"10.1145\/948109.948140"},{"key":"3_CR26","doi-asserted-by":"crossref","unstructured":"Backes, M., Pfitzmann, B.: Symmetric encryption in a simulatable Dolev-Yao style cryptographic library. In: CSFW, pp. 204\u2013218. IEEE (2004)","DOI":"10.1109\/CSFW.2004.1310742"},{"key":"3_CR27","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":"3_CR28","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.\u00a07232, pp. 63\u201379. Springer, Heidelberg (2012)"},{"key":"3_CR29","doi-asserted-by":"crossref","unstructured":"Sprenger, C., Backes, M., Basin, D., Pfitzmann, B., Waidner, M.: Cryptographically sound theorem proving. In: CSFW, pp. 153\u2013166. IEEE (2006)","DOI":"10.1109\/CSFW.2006.10"},{"key":"3_CR30","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":"3_CR31","doi-asserted-by":"crossref","unstructured":"Backes, M., Malik, A., Unruh, D.: Computational soundness without protocol restrictions. In: CCS, pp. 699\u2013711. ACM (2012)","DOI":"10.1145\/2382196.2382270"},{"key":"3_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"708","DOI":"10.1007\/978-3-642-39799-8_50","volume-title":"Computer Aided Verification","author":"V. Cheval","year":"2013","unstructured":"Cheval, V., Cortier, V., Plet, A.: Lengths may break privacy \u2013 or how to check for equivalences with length. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 708\u2013723. Springer, Heidelberg (2013)"},{"key":"3_CR33","doi-asserted-by":"crossref","unstructured":"Backes, M., Maffei, M., Unruh, D.: Computationally sound verification of source code. In: CCS, pp. 387\u2013398. ACM (2010)","DOI":"10.1145\/1866307.1866351"},{"key":"3_CR34","unstructured":"Backes, M., Mohammadi, E., Ruffing, T.: Bridging the gap from trace properties to uniformity (2014), http:\/\/www.infsec.cs.uni-saarland.de\/~mohammadi\/bridge.html"},{"key":"3_CR35","unstructured":"Unruh, D.: Programmable encryption and key-dependent messages. Technical report, IACR ePrint Report 2012\/423 (2012)"}],"container-title":["Lecture Notes in Computer Science","Principles of Security and Trust"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-54792-8_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T03:47:05Z","timestamp":1746157625000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54792-8_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642547911","9783642547928"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54792-8_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}