{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T23:23:03Z","timestamp":1743117783877,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540887324"},{"type":"electronic","value":"9783540887331"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-88733-1_13","type":"book-chapter","created":{"date-parts":[[2008,10,17]],"date-time":"2008-10-17T02:08:02Z","timestamp":1224209282000},"page":"185-199","source":"Crossref","is-referenced-by-count":0,"title":["Computationally Sound Symbolic Analysis of Probabilistic Protocols with Ideal Setups"],"prefix":"10.1007","author":[{"given":"Zhengqin","family":"Luo","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"13_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1007\/11681878_20","volume-title":"Theory of Cryptography","author":"R. Canetti","year":"2006","unstructured":"Canetti, R., Herzog, J.: Universally composable symbolic analysis of mutual authentication and key-exchange protocols. In: Halevi, S., Rabin, T. (eds.) TCC 2006. LNCS, vol.\u00a03876, pp. 380\u2013403. Springer, Heidelberg (2006)"},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"Dolev, D., Yao, A.C.-C.: On the security of public key protocols (extended abstract). In: FOCS, pp. 350\u2013357 (1981)","DOI":"10.1109\/SFCS.1981.32"},{"key":"13_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/3-540-44929-9_1","volume-title":"Theoretical Computer Science: Exploring New Frontiers of Theoretical Informatics","author":"M. Abadi","year":"2000","unstructured":"Abadi, M., Rogaway, P.: Reconciling two views of cryptography (the computational soundness of formal encryption). In: Watanabe, O., Hagiya, M., Ito, T., van Leeuwen, J., Mosses, P.D. (eds.) TCS 2000. LNCS, vol.\u00a01872, pp. 3\u201322. Springer, Heidelberg (2000)"},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/3-540-45500-0_4","volume-title":"Theoretical Aspects of Computer Software","author":"M. Abadi","year":"2001","unstructured":"Abadi, M., J\u00fcrjens, J.: Formal eavesdropping and its computational interpretation. In: Kobayashi, N., Pierce, B.C. (eds.) TACS 2001. LNCS, vol.\u00a02215, pp. 82\u201394. Springer, Heidelberg (2001)"},{"key":"13_CR5","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 - CRYPTO 2003","author":"O. Horvitz","year":"2003","unstructured":"Horvitz, O., Gligor, V.D.: Weak key authenticity and the computational completeness of formal encryption. In: Boneh, D. (ed.) CRYPTO 2003. LNCS, vol.\u00a02729, pp. 530\u2013547. Springer, Heidelberg (2003)"},{"issue":"1","key":"13_CR6","doi-asserted-by":"publisher","first-page":"99","DOI":"10.3233\/JCS-2004-12105","volume":"12","author":"D. Micciancio","year":"2004","unstructured":"Micciancio, D., Warinschi, B.: Completeness theorems for the abadi-rogaway language of encrypted expressions. Journal of Computer Security\u00a012(1), 99\u2013130 (2004)","journal-title":"Journal of Computer Security"},{"key":"13_CR7","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":"13_CR8","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":"13_CR9","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, J., L\u00f3pez, J. (eds.) ESORICS 2007. LNCS, vol.\u00a04734, pp. 610\u2013625. Springer, Heidelberg (2007)"},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"Comon-Lundh, H., Cortier, V.: Computational soundness of observational equivalence. Technical report, INRIA (2008)","DOI":"10.1145\/1455770.1455786"},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"Canetti, R.: Universally composable security: A new paradigm for cryptographic protocols. In: FOCS, pp. 136\u2013145 (2001)","DOI":"10.1109\/SFCS.2001.959888"},{"key":"13_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-540-76637-7_12","volume-title":"Programming Languages and Systems","author":"J. Goubault-Larrecq","year":"2007","unstructured":"Goubault-Larrecq, J., Palamidessi, C., Troina, A.: A probabilistic applied pi-calculus. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol.\u00a04807, pp. 175\u2013190. Springer, Heidelberg (2007)"},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"Backes, M., Pfitzmann, B., Waidner, M.: A composable cryptographic library with nested operations. In: CCS, pp. 220\u2013230 (2003)","DOI":"10.1145\/948109.948140"},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"Backes, M., Pfitzmann, B.: Symmetric encryption in a simulatable dolev-yao style cryptographic library. In: CSFW, pp. 204\u2013218 (2004)","DOI":"10.1109\/CSFW.2004.1310742"},{"key":"13_CR15","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/s10207-004-0056-6","volume":"4","author":"M. Backes","year":"2005","unstructured":"Backes, M., Pfitzmann, B., Waidner, M.: Symmetric authentication in a simulatable dolev-yao-style cryptographic library. Int. J. Inf. Sec.\u00a04, 135\u2013154 (2005)","journal-title":"Int. J. Inf. Sec."},{"key":"13_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-24597-1_1","volume-title":"FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science","author":"M. Backes","year":"2003","unstructured":"Backes, M., Pfitzmann, B.: A cryptographically sound security proof of the needham-schroeder-lowe public-key protocol. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol.\u00a02914, pp. 1\u201312. Springer, Heidelberg (2003)"},{"key":"13_CR17","doi-asserted-by":"crossref","unstructured":"Backes, M., D\u00fcrmuth, M.: A cryptographically sound dolev-yao style security proof of an electronic payment system. In: CSFW, pp. 78\u201393 (2005)","DOI":"10.1109\/CSFW.2005.5"},{"key":"13_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/978-3-540-30108-0_6","volume-title":"Computer Security \u2013 ESORICS 2004","author":"M. Backes","year":"2004","unstructured":"Backes, M.: A cryptographically sound dolev-yao style security proof of the otway-rees protocol. In: Samarati, P., Ryan, P.Y.A., Gollmann, D., Molva, R. (eds.) ESORICS 2004. LNCS, vol.\u00a03193, pp. 89\u2013108. Springer, Heidelberg (2004)"},{"key":"13_CR19","unstructured":"Patil, A.: On symbolic analysis of cryptographic protocols. Master\u2019s thesis, Massachusetts Institute of Technology (2006)"},{"key":"13_CR20","doi-asserted-by":"crossref","unstructured":"Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: POPL, pp. 104\u2013115 (2001)","DOI":"10.1145\/360204.360213"},{"issue":"1\u20132","key":"13_CR21","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.tcs.2006.08.032","volume":"367","author":"M. Abadi","year":"2006","unstructured":"Abadi, M., Cortier, V.: Deciding knowledge in security protocols under equational theories. Theor. Comput. Sci.\u00a0367(1\u20132), 2\u201332 (2006)","journal-title":"Theor. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Provable Security"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-88733-1_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,1]],"date-time":"2025-02-01T22:53:29Z","timestamp":1738450409000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-88733-1_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540887324","9783540887331"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-88733-1_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}