{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,25]],"date-time":"2025-10-25T11:58:08Z","timestamp":1761393488105,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540446019"},{"type":"electronic","value":"9783540446057"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11863908_25","type":"book-chapter","created":{"date-parts":[[2006,9,16]],"date-time":"2006-09-16T03:28:46Z","timestamp":1158377326000},"page":"404-423","source":"Crossref","is-referenced-by-count":8,"title":["Limits of the BRSIM\/UC Soundness of Dolev-Yao Models with Hashes"],"prefix":"10.1007","author":[{"given":"Michael","family":"Backes","sequence":"first","affiliation":[]},{"given":"Birgit","family":"Pfitzmann","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Waidner","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"25_CR1","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":"25_CR2","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":"25_CR3","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":"25_CR4","doi-asserted-by":"crossref","unstructured":"Backes, M., D\u00fcrmuth, M.: A cryptographically sound Dolev-Yao style security proof of an electronic payment system. In: Proc. 18th IEEE CSFW, pp. 78\u201393 (2005)","DOI":"10.1109\/CSFW.2005.5"},{"issue":"10","key":"25_CR5","doi-asserted-by":"publisher","first-page":"2075","DOI":"10.1109\/JSAC.2004.836016","volume":"22","author":"M. Backes","year":"2004","unstructured":"Backes, M., Pfitzmann, B.: A cryptographically sound security proof of the Needham-Schroeder-Lowe public-key protocol. Journal on Selected Areas in Communications\u00a022(10), 2075\u20132086 (2004)","journal-title":"Journal on Selected Areas in Communications"},{"key":"25_CR6","doi-asserted-by":"crossref","unstructured":"Backes, M., Pfitzmann, B.: Symmetric encryption in a simulatable Dolev-Yao style cryptographic library. In: Proc. 17th IEEE CSFW, pp. 204\u2013218 (2004)","DOI":"10.1109\/CSFW.2004.1310742"},{"key":"25_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/11555827_11","volume-title":"Computer Security \u2013 ESORICS 2005","author":"M. Backes","year":"2005","unstructured":"Backes, M., Pfitzmann, B.: Limits of the cryptographic realization of dolev-yao-style XOR. In: di Vimercati, S.d.C., Syverson, P.F., Gollmann, D. (eds.) ESORICS 2005. LNCS, vol.\u00a03679, pp. 178\u2013196. Springer, Heidelberg (2005)"},{"key":"25_CR8","doi-asserted-by":"crossref","unstructured":"Backes, M., Pfitzmann, B., Waidner, M.: A composable cryptographic library with nested operations. In: Proc. 10th ACM CCS, pp. 220\u2013230 (2003)","DOI":"10.1145\/948109.948140"},{"key":"25_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/978-3-540-39650-5_16","volume-title":"Computer Security \u2013 ESORICS 2003","author":"M. Backes","year":"2003","unstructured":"Backes, M., Pfitzmann, B., Waidner, M.: Symmetric authentication within a simulatable cryptographic library. In: Snekkenes, E., Gollmann, D. (eds.) ESORICS 2003. LNCS, vol.\u00a02808, pp. 271\u2013290. Springer, Heidelberg (2003)"},{"key":"25_CR10","unstructured":"Backes, M., Pfitzmann, B., Waidner, M.: Limits of the Reactive Simulatability\/UC of Dolev-Yao models with hashes. IACR Cryptology ePrint Archive 2006\/068 (February 2006)"},{"key":"25_CR11","doi-asserted-by":"crossref","unstructured":"Basin, D., M\u00f6dersheim, S., Vigan\u00f2, L.: OFMC: A symbolic model checker for security protocols. Intern. Journal of Information Security (2004)","DOI":"10.1007\/s10207-004-0055-7"},{"key":"25_CR12","doi-asserted-by":"crossref","unstructured":"Bellare, M., Rogaway, P.: Random oracles are practical: A paradigm for designing efficient protocols. In: Proc. 1st ACM CCS, pp. 62\u201373 (1993)","DOI":"10.1145\/168588.168596"},{"key":"25_CR13","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: Proc. 14th IEEE CSFW, pp. 82\u201396 (2001)","DOI":"10.1109\/CSFW.2001.930138"},{"key":"25_CR14","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: A computationally sound mechanized prover for security protocols. In: Proc. 27th IEEE Symp. on Security & Privacy, pp. 140\u2013154 (2006)","DOI":"10.1109\/SP.2006.1"},{"key":"25_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"455","DOI":"10.1007\/BFb0052255","volume-title":"Advances in Cryptology - CRYPTO \u201997","author":"R. Canetti","year":"1997","unstructured":"Canetti, R.: Towards realizing random oracles: Hash functions that hide all partial information. In: Kaliski Jr., B.S. (ed.) CRYPTO 1997. LNCS, vol.\u00a01294, pp. 455\u2013469. Springer, Heidelberg (1997)"},{"key":"25_CR16","doi-asserted-by":"crossref","unstructured":"Canetti, R.: Universally composable security: A new paradigm for cryptographic protocols. In: Proc. 42nd IEEE FOCS, pp. 136\u2013145 (2001)","DOI":"10.1109\/SFCS.2001.959888"},{"key":"25_CR17","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 - CRYPTO 2001","author":"R. Canetti","year":"2001","unstructured":"Canetti, R., Fischlin, M.: Universally composable commitments. In: Kilian, J. (ed.) CRYPTO 2001. LNCS, vol.\u00a02139, pp. 19\u201340. Springer, Heidelberg (2001)"},{"key":"25_CR18","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.C.: 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":"25_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/3-540-46035-7_22","volume-title":"Advances in Cryptology - EUROCRYPT 2002","author":"R. Canetti","year":"2002","unstructured":"Canetti, R., Krawczyk, H.: Universally composable notions of key exchange and secure channels. In: Knudsen, L.R. (ed.) EUROCRYPT 2002. LNCS, vol.\u00a02332, pp. 337\u2013351. Springer, Heidelberg (2002)"},{"key":"25_CR20","doi-asserted-by":"crossref","unstructured":"Canetti, R., Micciancio, D., Reingold, O.: Perfectly one-way probabilistic hash functions. In: Proc. 30th ACM STOC, pp. 131\u2013140 (1998)","DOI":"10.1145\/276698.276721"},{"key":"25_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"360","DOI":"10.1007\/11681878_19","volume-title":"Theory of Cryptography","author":"A. Datta","year":"2006","unstructured":"Datta, A., Derek, A., Mitchell, J.C., Ramanathan, A., Scedrov, A.: Games and the impossibility of realizable ideal functionality. In: Halevi, S., Rabin, T. (eds.) TCC 2006. LNCS, vol.\u00a03876, pp. 360\u2013379. Springer, Heidelberg (2006)"},{"key":"25_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/11523468_2","volume-title":"Automata, Languages and Programming","author":"A. Datta","year":"2005","unstructured":"Datta, A., Derek, A., Mitchell, J.C., Shmatikov, V., Turuani, M.: Probabilistic polynomial-time semantics for a protocol security logic. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol.\u00a03580, pp. 16\u201329. Springer, Heidelberg (2005)"},{"issue":"2","key":"25_CR23","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":"25_CR24","doi-asserted-by":"crossref","unstructured":"Garcia, F.D., van Rossum, P.: Sound computational interpretation of formal hashes. IACR Cryptology ePrint Archive 2006\/014 (January 2006)","DOI":"10.1007\/11908739_3"},{"key":"25_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/978-3-540-24638-1_4","volume-title":"Theory of Cryptography","author":"D. Hofheinz","year":"2004","unstructured":"Hofheinz, D., M\u00fcller-Quade, J.: Universally composable commitments using random oracles. In: Naor, M. (ed.) TCC 2004. LNCS, vol.\u00a02951, pp. 58\u201376. Springer, Heidelberg (2004)"},{"key":"25_CR26","doi-asserted-by":"crossref","unstructured":"Impagliazzo, R., Kapron, B.M.: Logics for reasoning about cryptographic constructions. In: Proc. 44th IEEE FOCS, pp. 372\u2013381 (2003)","DOI":"10.1109\/SFCS.2003.1238211"},{"key":"25_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/3-540-45309-1_6","volume-title":"Programming Languages and Systems","author":"P. Laud","year":"2001","unstructured":"Laud, P.: Semantics and program analysis of computationally secure information flow. In: Sands, D. (ed.) ESOP 2001. LNCS, vol.\u00a02028, pp. 77\u201391. Springer, Heidelberg (2001)"},{"key":"25_CR28","doi-asserted-by":"crossref","unstructured":"Laud, P.: Symmetric encryption in automatic analyses for confidentiality against active adversaries. In: Proc. 25th IEEE Symp. on Security & Privacy, pp. 71\u201385 (2004)","DOI":"10.1109\/SECPRI.2004.1301316"},{"key":"25_CR29","doi-asserted-by":"crossref","unstructured":"Laud, P.: Secrecy types for a simulatable cryptographic library. In: Proc. 12th ACM CCS, pp. 26\u201335 (2005)","DOI":"10.1145\/1102120.1102126"},{"key":"25_CR30","unstructured":"Merritt, M.: Cryptographic Protocols. PhD thesis, Georgia Institute of Technology (1983)"},{"key":"25_CR31","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":"25_CR32","doi-asserted-by":"crossref","unstructured":"Mitchell, J., Mitchell, M., Scedrov, A.: A linguistic characterization of bounded oracle computation and probabilistic polynomial time. In: Proc. 39th FOCS, pp. 725\u2013733 (1998)","DOI":"10.1109\/SFCS.1998.743523"},{"key":"25_CR33","first-page":"1","volume":"47","author":"J. Mitchell","year":"2001","unstructured":"Mitchell, J., Mitchell, M., Scedrov, A., Teague, V.: A probabilistic polynominal-time process calculus for analysis of cryptographic protocols. ENTCS\u00a047, 1\u201331 (2001)","journal-title":"ENTCS"},{"issue":"1","key":"25_CR34","first-page":"85","volume":"6","author":"L. Paulson","year":"1998","unstructured":"Paulson, L.: The inductive approach to verifying cryptographic protocols. Journal of Cryptology\u00a06(1), 85\u2013128 (1998)","journal-title":"Journal of Cryptology"},{"key":"25_CR35","doi-asserted-by":"crossref","unstructured":"Pfitzmann, B., Waidner, M.: Composition and integrity preservation of secure reactive systems. In: Proc. 7th ACM CCS, pp. 245\u2013254 (2000)","DOI":"10.1145\/352600.352639"},{"key":"25_CR36","doi-asserted-by":"crossref","unstructured":"Pfitzmann, B., Waidner, M.: A model for asynchronous reactive systems and its application to secure message transmission. In: Proc. 22nd IEEE Symp. on S & P, pp. 184\u2013200 (2001)","DOI":"10.1109\/SECPRI.2001.924298"},{"key":"25_CR37","unstructured":"Sprenger, C., Backes, M., Basin, D., Pfitzmann, B., Waidner, M.: Cryptographically sound theorem proving. In: Proc. 19th IEEE CSFW (to appear, 2006)"},{"key":"25_CR38","doi-asserted-by":"crossref","unstructured":"Yao, A.C.: Theory and applications of trapdoor functions. In: Proc. 23rd FOCS, pp. 80\u201391 (1982)","DOI":"10.1109\/SFCS.1982.45"}],"container-title":["Lecture Notes in Computer Science","Computer Security \u2013 ESORICS 2006"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11863908_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,10]],"date-time":"2025-01-10T21:47:08Z","timestamp":1736545628000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11863908_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540446019","9783540446057"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/11863908_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}