{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,20]],"date-time":"2026-05-20T22:07:48Z","timestamp":1779314868071,"version":"3.51.4"},"reference-count":65,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2010,3,9]],"date-time":"2010-03-09T00:00:00Z","timestamp":1268092800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Cryptol"],"published-print":{"date-parts":[[2011,1]]},"DOI":"10.1007\/s00145-009-9055-0","type":"journal-article","created":{"date-parts":[[2010,3,8]],"date-time":"2010-03-08T16:57:46Z","timestamp":1268067466000},"page":"83-147","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":17,"title":["Universally Composable Symbolic Security Analysis"],"prefix":"10.1007","volume":"24","author":[{"given":"Ran","family":"Canetti","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jonathan","family":"Herzog","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2010,3,9]]},"reference":[{"key":"9055_CR1","doi-asserted-by":"crossref","unstructured":"M. Abadi, B. Blanchet, Analyzing security protocols with secrecy types and logic programs, in Conference Record of POPL 2002: The 2pth SIGPLAN\u2013SIGACT Symposium on Principles of Programming Languages, January 2002, pp. 33\u201344","DOI":"10.1145\/565816.503277"},{"issue":"1","key":"9055_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1998.2740","volume":"148","author":"M. Abadi","year":"1999","unstructured":"M. Abadi, A. Gordon, A calculus for cryptographic protocols: the spi calculus. Inf. Comput. 148(1), 1\u201370 (1999)","journal-title":"Inf. Comput."},{"key":"9055_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1007\/3-540-45500-0_4","volume-title":"Proceedings, 4th International Symposium on Theoretical Aspects of Computer Software TACS 2001","author":"M. Abadi","year":"2001","unstructured":"M. Abadi, J. J\u00fcrjens, Formal eavesdropping and its computational interpretation, in Proceedings, 4th International Symposium on Theoretical Aspects of Computer Software TACS 2001, ed. by N. Kobayashi, B.C. Pierce. Lecture Notes in Computer Science, vol. 2215 (Springer, Berlin, 2001), pp. 82\u201394"},{"issue":"2","key":"9055_CR4","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1007\/s00145-001-0014-7","volume":"15","author":"M. Abadi","year":"2002","unstructured":"M. Abadi, P. Rogaway, Reconciling two views of cryptography (the computational soundness of formal encryption). J. Cryptol. 15(2), 103\u2013127 (2002)","journal-title":"J. Cryptol."},{"key":"9055_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"374","DOI":"10.1007\/11555827_22","volume-title":"Proceedings, 10th European Symposium on Research in Computer Security (ESORICS)","author":"P. Ad\u00e3o","year":"2005","unstructured":"P. Ad\u00e3o, G. Bana, J. Herzog, A. Scedrov, Soundness of Abadi\u2013Rogaway logics in the presence of key-cycles, in Proceedings, 10th European Symposium on Research in Computer Security (ESORICS), ed. by S. De Capitani di Vimercati, P.F. Syverson, D. Gollmann. Lecture Notes in Computer Science, vol. 3679 (Springer, Berlin, 2005), pp. 374\u2013396"},{"key":"9055_CR6","series-title":"Lecture Notes in Computer Science","first-page":"140","volume-title":"Proceedings of the 23rd Conference on Foundations of Software Technology and Theoretical Computer Science\u2014FSTTCS","author":"M. Backes","year":"2003","unstructured":"M. Backes, B. Pfitzmann, A cryptographically sound security proof of the Needham\u2013Schroeder\u2013Lowe public-key protocol, in Proceedings of the 23rd Conference on Foundations of Software Technology and Theoretical Computer Science\u2014FSTTCS. Lecture Notes in Computer Science, vol. 2914 (Springer, Berlin, 2003), pp. 140\u2013152"},{"key":"9055_CR7","doi-asserted-by":"crossref","unstructured":"M. Backes, B. Pfitzmann, Relating symbolic and cryptographic secrecy. IEEE Trans. Dependable Secure Comput. 2(2) (2005)","DOI":"10.1109\/TDSC.2005.25"},{"key":"9055_CR8","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1145\/948109.948140","volume-title":"Proceedings, 10th ACM Conference on Computer and Communications Security (CCS)","author":"M. Backes","year":"2003","unstructured":"M. Backes, B. Pfitzmann, M. Waidner, A composable cryptographic library with nested operations (extended abstract), in Proceedings, 10th ACM Conference on Computer and Communications Security (CCS), ed. by S. Jajodia, V. Atluri, T. Jaeger (ACM, New York, 2003), pp. 220\u2013230. Full version available at http:\/\/eprint.iacr.org\/2003\/015\/"},{"issue":"2","key":"9055_CR9","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/BF00196771","volume":"4","author":"D. Beaver","year":"1991","unstructured":"D. Beaver, Secure multiparty protocols and zero-knowledge proof systems tolerating a faulty minority. J. Cryptol. 4(2), 75\u2013122 (1991)","journal-title":"J. Cryptol."},{"key":"9055_CR10","series-title":"Lecture Notes in Computer Science","first-page":"232","volume-title":"Advances in Cryptology\u2014CRYPTO 1993","author":"M. Bellare","year":"1993","unstructured":"M. Bellare, P. Rogaway, Entity authentication and key distribution, in Advances in Cryptology\u2014CRYPTO 1993, ed. by D. Stinson. Lecture Notes in Computer Science, vol. 773 (Springer, Berlin, 1993), pp. 232\u2013249. Full version of paper available at http:\/\/www-cse.ucsd.edu\/users\/mihir\/"},{"key":"9055_CR11","first-page":"82","volume-title":"Proceedings of the 14th IEEE Computer Security Foundations Workshop (CSFW 14)","author":"B. Blanchet","year":"2001","unstructured":"B. Blanchet, An efficient cryptographic protocol verifier based on Prolog rules, in Proceedings of the 14th IEEE Computer Security Foundations Workshop (CSFW 14) (IEEE Computer Society, Washington, 2001), pp. 82\u201396"},{"key":"9055_CR12","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1109\/SECPRI.2004.1301317","volume-title":"Proceedings of the 2004 IEEE Symposium on Security and Privacy (S&P)","author":"B. Blanchet","year":"2004","unstructured":"B. Blanchet, Automatic proof of strong secrecy for security protocols, in Proceedings of the 2004 IEEE Symposium on Security and Privacy (S&P) (IEEE Computer Society, Washington, 2004), pp. 86\u2013102"},{"key":"9055_CR13","unstructured":"B. Blanchet, ProVerif automatic cryptographic protocol verifier user manual. Available at http:\/\/www.di.ens.fr\/~blanchet\/crypto-eng.html , November 2004"},{"key":"9055_CR14","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1109\/CSF.2007.16","volume-title":"Proceedings of the 20th IEEE Computer Security Foundations Symposium (CSFW 20)","author":"B. Blanchet","year":"2007","unstructured":"B. Blanchet, Computationally sound mechanized proofs of correspondence assertions, in Proceedings of the 20th IEEE Computer Security Foundations Symposium (CSFW 20) (IEEE Computer Society, Washington, 2007), pp. 97\u2013111"},{"issue":"4","key":"9055_CR15","doi-asserted-by":"publisher","first-page":"850","DOI":"10.1137\/0213053","volume":"13","author":"M. Blum","year":"1984","unstructured":"M. Blum, S. Micali, How to generate cryptographically strong sequences of pseudo-random bits. SIAM J. Comput. 13(4), 850\u2013864 (1984)","journal-title":"SIAM J. Comput."},{"issue":"1","key":"9055_CR16","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1145\/77648.77649","volume":"8","author":"M. Burrows","year":"1990","unstructured":"M. Burrows, M. Abadi, R. Needham, A logic of authentication. ACM Trans. Comput. Syst. 8(1), 18\u201336 (1990)","journal-title":"ACM Trans. Comput. Syst."},{"issue":"1","key":"9055_CR17","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/s001459910006","volume":"13","author":"R. Canetti","year":"2000","unstructured":"R. Canetti, Security and composition of multiparty cryptographic protocols. J. Cryptol. 13(1), 143\u2013202 (2000)","journal-title":"J. Cryptol."},{"key":"9055_CR18","first-page":"136","volume-title":"42nd Annual Symposium on Foundations of Computer Science (FOCS 2001","author":"R. Canetti","year":"2001","unstructured":"R. Canetti, Universal composable security: A new paradigm for cryptographic protocols, in 42nd Annual Symposium on Foundations of Computer Science (FOCS 2001 (IEEE Computer Society, Washington, 2001), pp. 136\u2013145. Full version available at eprint.iacr.org\/2000\/067"},{"key":"9055_CR19","unstructured":"R. Canetti, Universally composable signatures, certification, and authentication. Cryptology ePrint Archive, http:\/\/eprint.iacr.org\/2003\/239 , 2003"},{"key":"9055_CR20","first-page":"219","volume-title":"Proceedings of the 17th IEEE Computer Security Foundations Workshop (CSFW 16)","author":"R. Canetti","year":"2004","unstructured":"R. Canetti, Universally composable signature, certification, and authentication, in Proceedings of the 17th IEEE Computer Security Foundations Workshop (CSFW 16) (IEEE Computer Society, Washington, 2004), pp. 219\u2013233"},{"key":"9055_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/3-540-44987-6_28","volume-title":"Advances in Cryptology\u2014Eurocrypt 2001","author":"R. Canetti","year":"2001","unstructured":"R. Canetti, H. Krawczyk, Analysis of key-exchange protocols and their use for building secure channels, in Advances in Cryptology\u2014Eurocrypt 2001, ed. by B. Pfitzmann. Lecture Notes in Computer Science, vol. 2045 (Springer, Berlin, 2001), pp. 453\u2013474"},{"key":"9055_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-540-45146-4_16","volume-title":"Advances in Cryptology\u2014CRYPTO 2003","author":"R. Canetti","year":"2003","unstructured":"R. Canetti, T. Rabin, Universal composition with joint state, in Advances in Cryptology\u2014CRYPTO 2003, ed. by D. Boneh. Lecture Notes in Computer Science, vol. 2729 (Springer, Berlin, 2003), pp. 265\u2013281"},{"key":"9055_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"565","DOI":"10.1007\/978-3-540-45146-4_33","volume-title":"Advances in Cryptology\u2014CRYPTO 2003","author":"R. Canetti","year":"2003","unstructured":"R. Canetti, H. Krawczyk, J.B. Nielsen, Relaxing chosen-ciphertext security, in Advances in Cryptology\u2014CRYPTO 2003, ed. by D. Boneh. Lecture Notes in Computer Science, vol. 2729 (Springer, Berlin, 2003), pp. 565\u2013582"},{"key":"9055_CR24","volume-title":"Proceedings of the 12th IEEE Computer Security Foundations Workshop (CSFW 12)","author":"I. Cervesato","year":"1999","unstructured":"I. Cervesato, N.A. Durgin, P.D. Lincoln, J.C. Mitchell, A. Scedrov, A meta-notion for protocol analysis, in Proceedings of the 12th IEEE Computer Security Foundations Workshop (CSFW 12) (IEEE Computer Society, Washington, 1999)"},{"key":"9055_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1007\/978-3-540-31987-0_12","volume-title":"Proceedings, 14th European Symposium on Programming (ESOP2005)","author":"V. Cortier","year":"2005","unstructured":"V. Cortier, B. Warinschi, Computationally sound, automated proofs for security protocols, in Proceedings, 14th European Symposium on Programming (ESOP2005), ed. by S. Sagiv. Lecture Notes in Computer Science, vol. 3444 (Springer, Berlin, 2005), pp. 157\u2013171"},{"key":"9055_CR26","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"29","author":"D. Dolev","year":"1983","unstructured":"D. Dolev, A. Yao, On the security of public-key protocols. IEEE Trans. Inf. Theory 29, 198\u2013208 (1983)","journal-title":"IEEE Trans. Inf. Theory"},{"issue":"2","key":"9055_CR27","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1137\/S0097539795291562","volume":"30","author":"D. Dolev","year":"2000","unstructured":"D. Dolev, C. Dwork, M. Naor, Non-malleable cryptography. SIAM J. Comput. 30(2), 391\u2013437 (2000)","journal-title":"SIAM J. Comput."},{"issue":"2","key":"9055_CR28","doi-asserted-by":"crossref","first-page":"247","DOI":"10.3233\/JCS-2004-12203","volume":"12","author":"N. Durgin","year":"2004","unstructured":"N. Durgin, P. Lincoln, J. Mitchell, A. Scedrov, Multiset rewriting and the complexity of bounded security protocols. J. Comput. Secur. 12(2), 247\u2013311 (2004)","journal-title":"J. Comput. Secur."},{"key":"9055_CR29","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1109\/SFCS.1983.42","volume-title":"Proceedings, 24th Annual Symposium on Foundations of Computer Science (FOCS)","author":"S. Even","year":"1983","unstructured":"S. Even, O. Goldreich, On the security of multi-party ping-pong protocols, in Proceedings, 24th Annual Symposium on Foundations of Computer Science (FOCS) (IEEE, New York, 1983), pp. 34\u201339"},{"key":"9055_CR30","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511546891","volume-title":"Foundations of Cryptography","author":"O. Goldreich","year":"2001","unstructured":"O. Goldreich, Foundations of Cryptography, vol. 1 (Cambridge University Press, Cambridge, 2001)"},{"issue":"1","key":"9055_CR31","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF00195207","volume":"7","author":"O. Goldreich","year":"1994","unstructured":"O. Goldreich, Y. Oren, Definitions and properties of zero-knowledge proof systems. J. Cryptol. 7(1), 1\u201332 (1994)","journal-title":"J. Cryptol."},{"key":"9055_CR32","doi-asserted-by":"crossref","first-page":"218","DOI":"10.1145\/28395.28420","volume-title":"Proceedings of the Nineteenth Annual ACM Symposium on Theory of Computing (STOC)","author":"O. Goldreich","year":"1987","unstructured":"O. Goldreich, S. Micali, A. Wigderson, How to play any mental game or a completeness theorem for protocols with honest majority, in Proceedings of the Nineteenth Annual ACM Symposium on Theory of Computing (STOC) (ACM, New York, 1987), pp. 218\u2013229"},{"issue":"1","key":"9055_CR33","first-page":"691","volume":"38","author":"O. Goldreich","year":"1991","unstructured":"O. Goldreich, S. Micali, A. Wigderson, Proofs that yield nothing but their validity or all languages in NP have zero-knowledge proof systems. J. ACM 38(1), 691\u2013729 (1991)","journal-title":"J. ACM"},{"key":"9055_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1007\/0-387-34799-2","volume-title":"Advances in Cryptology (CRYPTO \u201990)","author":"S. Goldwasser","year":"1990","unstructured":"S. Goldwasser, L. Levin, Fair computation of general functions in presence of immoral majority, in Advances in Cryptology (CRYPTO \u201990), ed. by A. Menezes, S.A. Vanstone. Lecture Notes in Computer Science, vol. 537 (Springer, Berlin, 1990), pp. 77\u201393"},{"issue":"2","key":"9055_CR35","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1016\/0022-0000(84)90070-9","volume":"28","author":"S. Goldwasser","year":"1984","unstructured":"S. Goldwasser, S. Micali, Probabilistic encryption. J. Comput. Syst. Sci. 28(2), 270\u2013299 (1984)","journal-title":"J. Comput. Syst. Sci."},{"issue":"2","key":"9055_CR36","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1137\/0217017","volume":"17","author":"S. Goldwasser","year":"1988","unstructured":"S. Goldwasser, S. Micali, R.L. Rivest, A digital-signature scheme secure against adaptive chosen-message attacks. SIAM J. Comput. 17(2), 281\u2013308 (1988)","journal-title":"SIAM J. Comput."},{"issue":"1","key":"9055_CR37","doi-asserted-by":"publisher","first-page":"186","DOI":"10.1137\/0218012","volume":"18","author":"S. Goldwasser","year":"1989","unstructured":"S. Goldwasser, S. Micali, C. Rackoff, The knowledge complexity of interactive proof systems. SIAM J. Comput. 18(1), 186\u2013208 (1989)","journal-title":"SIAM J. Comput."},{"key":"9055_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/11580850_8","volume-title":"Trustworthy Global Computing (TGC 2005)","author":"J.D. Guttman","year":"2005","unstructured":"J.D. Guttman, J. Herzog, J.D. Ramsdell, B.T. Sniffen, Programming cryptographic protocols, in Trustworthy Global Computing (TGC 2005), ed. by R. Nicola, D. Sangiorgi. Lecture Notes in Computer Science, vol. 3702 (Springer, Berlin, 2005), pp. 116\u2013145"},{"key":"9055_CR39","unstructured":"J. Herzog, Computational soundness for standard assumptions of formal cryptography. PhD thesis, Massachusetts Institute of Technology, May 2004"},{"key":"9055_CR40","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1016\/j.tcs.2005.03.003","volume":"340","author":"J. Herzog","year":"2005","unstructured":"J. Herzog, A computational interpretation of Dolev\u2013Yao adversaries. Theor. Comput. Sci. 340, 57\u201381 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"9055_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"548","DOI":"10.1007\/978-3-540-45146-4_32","volume-title":"Advances in Cryptology\u2014CRYPTO 2003","author":"J. Herzog","year":"2003","unstructured":"J. Herzog, M. Liskov, S. Micali, Plaintext awareness via key registration, in Advances in Cryptology\u2014CRYPTO 2003, ed. by D. Boneh. Lecture Notes in Computer Science, vol. 2729 (Springer, Berlin, 2003), pp. 548\u2013564"},{"key":"9055_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"530","DOI":"10.1007\/978-3-540-45146-4_31","volume-title":"Advances in Cryptology\u2014CRYPTO 2003","author":"O. Horvitz","year":"2003","unstructured":"O. Horvitz, V. Gligor, Weak key authenticity and the computational completeness of formal encryption, in Advances in Cryptology\u2014CRYPTO 2003, ed. by D. Boneh. Lecture Notes in Computer Science, vol. 2729 (Springer, Berlin, 2003), pp. 530\u2013547"},{"key":"9055_CR43","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1109\/SECPRI.2004.1301316","volume-title":"Proceedings of the 2004 IEEE Symposium on Security and Privacy (S&P)","author":"P. Laud","year":"2004","unstructured":"P. Laud, Symmetric encryption in automatic analyses for confidentiality against active adversaries, in Proceedings of the 2004 IEEE Symposium on Security and Privacy (S&P) (IEEE Computer Society, Washington, 2004), pp. 71\u201385"},{"key":"9055_CR44","doi-asserted-by":"crossref","unstructured":"P.D. Lincoln, J.C. Mitchell, M. Mitchell, A. Scedrov, A probabilistic poly-time framework for protocol analysis, in Proceedings of the 5th ACM Conference on Computer and Communication Security (CCS \u201998), November 1998, pp. 112\u2013121","DOI":"10.1145\/288090.288117"},{"key":"9055_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"776","DOI":"10.1007\/3-540-48119-2_43","volume-title":"World Congress on Formal Methods","author":"P.D. Lincoln","year":"1999","unstructured":"P.D. Lincoln, J.C. Mitchell, M. Mitchell, A. Scedrov, Probabilistic polynomial-time equivalence and security protocols, in World Congress on Formal Methods, ed. by J.M. Wing, J. Woodcock, J. Davies. Lecture Notes in Computer Science, vol. 1708 (Springer, Berlin, 1999), pp. 776\u2013793"},{"key":"9055_CR46","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1016\/0020-0190(95)00144-2","volume":"56","author":"G. Lowe","year":"1995","unstructured":"G. Lowe, An attack on the Needham\u2013Schroeder public-key authentication protocol. Inf. Process. Lett. 56, 131\u2013133 (1995)","journal-title":"Inf. Process. Lett."},{"key":"9055_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/3-540-61042-1_43","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Lowe","year":"1996","unstructured":"G. Lowe, Breaking and fixing the Needham\u2013Schroeder public-key protocol using FDR, in Tools and Algorithms for the Construction and Analysis of Systems, ed. by Margaria, Steffen. Lecture Notes in Computer Science, vol. 1055 (Springer, Berlin, 1996), pp. 147\u2013166"},{"key":"9055_CR48","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1109\/CSFW.1999.779759","volume-title":"Proceedings of the 12th IEEE Computer Security Foundations Workshop (CSFW 12)","author":"N. Lynch","year":"1999","unstructured":"N. Lynch, I\/O automaton models and proofs for shared-key communication systems, in Proceedings of the 12th IEEE Computer Security Foundations Workshop (CSFW 12) (IEEE Computer Society, Washington, 1999), pp. 14\u201329"},{"issue":"1","key":"9055_CR49","doi-asserted-by":"crossref","first-page":"5","DOI":"10.3233\/JCS-1992-1102","volume":"1","author":"C. Meadows","year":"1992","unstructured":"C. Meadows, Applying formal methods to the analysis of a key management protocol. J. Comput. Secur. 1(1), 5\u201336 (1992)","journal-title":"J. Comput. Secur."},{"key":"9055_CR50","series-title":"Lecture Notes in Computer Science","first-page":"392","volume-title":"Advances in Cryptology (CRYPTO \u201991)","author":"S. Micali","year":"1991","unstructured":"S. Micali, P. Rogaway, Secure computation (abstract), in Advances in Cryptology (CRYPTO \u201991), ed. by J. Feigenbaum. Lecture Notes in Computer Science, vol. 576 (Springer, Berlin, 1991), pp. 392\u2013404"},{"issue":"2","key":"9055_CR51","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1137\/0217025","volume":"17","author":"S. Micali","year":"1988","unstructured":"S. Micali, C. Rackoff, B. Sloan, The notion of security for probabilistic cryptosystems. SIAM J. Comput. 17(2), 412\u2013426 (1988)","journal-title":"SIAM J. Comput."},{"key":"9055_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1007\/978-3-540-30576-7_10","volume-title":"Proceedings, Second Theory of Cryptography Conference (TCC 2005)","author":"D. Micciancio","year":"2005","unstructured":"D. Micciancio, S. Panjwani, Adaptive security of symbolic encryption, in Proceedings, Second Theory of Cryptography Conference (TCC 2005), ed. by J. Kilian. Lecture Notes in Computer Science, vol. 3378 (Springer, Berlin, 2005), pp. 169\u2013187"},{"issue":"1","key":"9055_CR53","doi-asserted-by":"crossref","first-page":"99","DOI":"10.3233\/JCS-2004-12105","volume":"12","author":"D. Micciancio","year":"2004","unstructured":"D. Micciancio, B. Warinschi, Completeness theorems for the Abadi\u2013Rogaway logic of encrypted expressions. J. Comput. Secur. 12(1), 99\u2013129 (2004)","journal-title":"J. Comput. Secur."},{"key":"9055_CR54","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":"Proceedings, Theory of Cryptography Conference","author":"D. Micciancio","year":"2004","unstructured":"D. Micciancio, B. Warinschi, Soundness of formal encryption in the presence of active adversaries, in Proceedings, Theory of Cryptography Conference. Lecture Notes in Computer Science, vol. 2951 (Springer, Berlin, 2004), pp. 133\u2013151"},{"key":"9055_CR55","first-page":"141","volume-title":"Proceedings, 1997 IEEE Symposium on Security and Privacy","author":"J.C. Mitchell","year":"1997","unstructured":"J.C. Mitchell, M. Mitchell, U. Stern, Automated analysis of cryptographic protocols using Mur\u03c6, in Proceedings, 1997 IEEE Symposium on Security and Privacy (IEEE Computer Society, Washington, 1997), pp. 141\u2013153"},{"issue":"12","key":"9055_CR56","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1145\/359657.359659","volume":"21","author":"R. Needham","year":"1978","unstructured":"R. Needham, M. Schroeder, Using encryption for authentication in large networks of computers. Commun. ACM 21(12), 993\u2013999 (1978)","journal-title":"Commun. ACM"},{"key":"9055_CR57","unstructured":"A. Patil, On symbolic analysis of cryptographic protocols. Master\u2019s thesis, Massachusetts Institute of Technology, May 2005"},{"key":"9055_CR58","doi-asserted-by":"crossref","first-page":"85","DOI":"10.3233\/JCS-1998-61-205","volume":"6","author":"L.C. Paulson","year":"1998","unstructured":"L.C. Paulson, The inductive approach to verifying cryptographic protocols. J. Comput. Secur. 6, 85\u2013128 (1998)","journal-title":"J. Comput. Secur."},{"key":"9055_CR59","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/352600.352639","volume-title":"Proceedings of the 7th ACM Conference on Computer and Communication Security (CCS 2000)","author":"B. Pfitzmann","year":"2000","unstructured":"B. Pfitzmann, M. Waidner, Composition and integrity preservation of secure reactive systems, in Proceedings of the 7th ACM Conference on Computer and Communication Security (CCS 2000) (ACM Press, New York, 2000), pp. 245\u2013254"},{"key":"9055_CR60","series-title":"Lecture Notes in Computer Science","first-page":"433","volume-title":"Advances in Cryptology\u2014CRYPTO 91","author":"C. Rackoff","year":"1991","unstructured":"C. Rackoff, D. Simon, Noninteractive zero-knowledge proof of knowledge and the chosen-ciphertext attack, in Advances in Cryptology\u2014CRYPTO 91. Lecture Notes in Computer Science, vol. 576 (Springer, Berlin, 1991), pp. 433\u2013444"},{"key":"9055_CR61","doi-asserted-by":"crossref","first-page":"192","DOI":"10.1109\/CSFW.1999.779773","volume-title":"Proceedings of the 12th IEEE Computer Security Foundations Workshop (CSFW 12)","author":"D. Song","year":"1999","unstructured":"D. Song, Athena, an automatic checker for security protocol analysis, in Proceedings of the 12th IEEE Computer Security Foundations Workshop (CSFW 12) (IEEE Computer Society, Washington, 1999), pp. 192\u2013202"},{"key":"9055_CR62","first-page":"153","volume-title":"CSFW","author":"C. Sprenger","year":"2006","unstructured":"C. Sprenger, M. Backes, D.A. Basin, B. Pfitzmann, M. Waidner, Cryptographically sound theorem proving, in CSFW (IEEE Computer Society, Washington, 2006), pp. 153\u2013166"},{"issue":"23","key":"9055_CR63","doi-asserted-by":"crossref","first-page":"191","DOI":"10.3233\/JCS-1999-72-304","volume":"7","author":"F.J. Thayer F\u00e1brega","year":"1999","unstructured":"F.J. Thayer F\u00e1brega, J.C. Herzog, J.D. Guttman, Strand spaces: Proving security protocols correct. J.\u00a0Comput. Secur. 7(23), 191\u2013230 (1999)","journal-title":"J.\u00a0Comput. Secur."},{"key":"9055_CR64","doi-asserted-by":"crossref","unstructured":"A. Yao, Theory and applications of trapdoor functions (extended abstract), in Proceedings, 22th Annual Symposium on Foundations of Computer Science (FOCS 1982), 1982, pp. 80\u201391","DOI":"10.1109\/SFCS.1982.45"},{"key":"9055_CR65","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1109\/SFCS.1986.25","volume-title":"Proceedings, 27th Annual Symposium on Foundations of Computer Science (FOCS)","author":"A.C.-C. Yao","year":"1986","unstructured":"A.C.-C. Yao, How to generate and exchange secrets (extended abstract), in Proceedings, 27th Annual Symposium on Foundations of Computer Science (FOCS) (IEEE, New York, 1986), pp. 162\u2013167"}],"container-title":["Journal of Cryptology"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00145-009-9055-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00145-009-9055-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00145-009-9055-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00145-009-9055-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,30]],"date-time":"2023-05-30T20:09:53Z","timestamp":1685477393000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00145-009-9055-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,3,9]]},"references-count":65,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2011,1]]}},"alternative-id":["9055"],"URL":"https:\/\/doi.org\/10.1007\/s00145-009-9055-0","relation":{},"ISSN":["0933-2790","1432-1378"],"issn-type":[{"value":"0933-2790","type":"print"},{"value":"1432-1378","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,3,9]]},"assertion":[{"value":"17 April 2009","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"2 October 2009","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"9 March 2010","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}