{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T15:37:06Z","timestamp":1759333026611,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":41,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540229872"},{"type":"electronic","value":"9783540301080"}],"license":[{"start":{"date-parts":[[2004,1,1]],"date-time":"2004-01-01T00:00:00Z","timestamp":1072915200000},"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":[[2004]]},"DOI":"10.1007\/978-3-540-30108-0_6","type":"book-chapter","created":{"date-parts":[[2010,9,16]],"date-time":"2010-09-16T18:15:03Z","timestamp":1284660903000},"page":"89-108","source":"Crossref","is-referenced-by-count":22,"title":["A Cryptographically Sound Dolev-Yao Style Security Proof of the Otway-Rees Protocol"],"prefix":"10.1007","author":[{"given":"Michael","family":"Backes","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"6_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1998.2740","volume":"148","author":"M. Abadi","year":"1999","unstructured":"Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: The spi calculus. Information and Computation\u00a0148(1), 1\u201370 (1999)","journal-title":"Information and Computation"},{"key":"6_CR2","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":"6_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":"6_CR4","doi-asserted-by":"crossref","unstructured":"Backes, M.: A cryptographically sound Dolev-Yao style security proof of the Otway-Rees protocol. Research Report RZ 3539, IBM Research (2004)","DOI":"10.1007\/978-3-540-30108-0_6"},{"key":"6_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1007\/3-540-36494-3_59","volume-title":"STACS 2003","author":"M. Backes","year":"2003","unstructured":"Backes, M., Jacobi, C.: Cryptographically sound and machine-assisted verification of security protocols. In: Alt, H., Habib, M. (eds.) STACS 2003. LNCS, vol.\u00a02607, pp. 675\u2013686. Springer, Heidelberg (2003)"},{"key":"6_CR6","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":"6_CR7","unstructured":"Backes, M., Pfitzmann, B.: Symmetric encryption in a simulatable Dolev-Yao style cryptographic library. In: Proc. 17th IEEE Computer Security Foundations Workshop, CSFW (2004)"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"Backes, M., Pfitzmann, B., Waidner, M.: A composable cryptographic library with nested operations (extended abstract). In: Proc. 10th ACM Conference on Computer and Communications Security, pp. 220\u2013230 (2003); Full version in IACR Cryptology ePrint Archive 2003\/015 (January 2003), http:\/\/eprint.iacr.org\/","DOI":"10.1145\/948109.948140"},{"key":"6_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":"6_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1007\/BFb0055718","volume-title":"Advances in Cryptology - CRYPTO \u201998","author":"M. Bellare","year":"1998","unstructured":"Bellare, M., Desai, A., Pointcheval, D., Rogaway, P.: Relations among notions of security for public-key encryption schemes. In: Krawczyk, H. (ed.) CRYPTO 1998. LNCS, vol.\u00a01462, pp. 26\u201345. Springer, Heidelberg (1998)"},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"531","DOI":"10.1007\/3-540-44448-3_41","volume-title":"Advances in Cryptology - ASIACRYPT 2000","author":"M. Bellare","year":"2000","unstructured":"Bellare, M., Namprempre, C.: Authenticated encryption: Relations among notions and analysis of the generic composition paradigm. In: Okamoto, T. (ed.) ASIACRYPT 2000. LNCS, vol.\u00a01976, pp. 531\u2013545. Springer, Heidelberg (2000)"},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/3-540-44448-3_24","volume-title":"Advances in Cryptology - ASIACRYPT 2000","author":"M. Bellare","year":"2000","unstructured":"Bellare, M., Rogaway, P.: Encode-then-encipher encryption: How to exploit nonces or redundancy in plaintexts for efficient constructions. In: Okamoto, T. (ed.) ASIACRYPT 2000. LNCS, vol.\u00a01976, pp. 317\u2013330. Springer, Heidelberg (2000)"},{"key":"6_CR13","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"Advances in Cryptology - CRYPTO \u201998","author":"D. Bleichenbacher","year":"1998","unstructured":"Bleichenbacher, D.: Chosen ciphertext attacks against protocols based on the RSA encryption standard PKCS. In: Krawczyk, H. (ed.) CRYPTO 1998. LNCS, vol.\u00a01462, pp. 1\u201312. Springer, Heidelberg (1998)"},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"Burrows, M., Abadi, M., Needham, R.: A logic for authentication. Technical Report 39, SRC DIGITAL (1990)","DOI":"10.1145\/74850.74852"},{"issue":"8","key":"6_CR15","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1145\/358722.358740","volume":"24","author":"D.E. Denning","year":"1981","unstructured":"Denning, D.E., Sacco, G.M.: Timestamps in key distribution protocols. Communications of the ACM\u00a024(8), 533\u2013536 (1981)","journal-title":"Communications of the ACM"},{"issue":"2","key":"6_CR16","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":"6_CR17","unstructured":"Fisher, D.: Millions of .Net Passport accounts put at risk. eWeek (May 2003) (Flaw detected by Muhammad Faisal Rauf Danka)"},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"Goldreich, O., Micali, S., Wigderson, A.: How to play any mental game \u2013 or \u2013 a completeness theorem for protocols with honest majority. In: Proc. 19th Annual ACM Symposium on Theory of Computing (STOC), pp. 218\u2013229 (1987)","DOI":"10.1145\/28395.28420"},{"key":"6_CR19","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1016\/0022-0000(84)90070-9","volume":"28","author":"S. Goldwasser","year":"1984","unstructured":"Goldwasser, S., Micali, S.: Probabilistic encryption. Journal of Computer and System Sciences\u00a028, 270\u2013299 (1984)","journal-title":"Journal of Computer and System Sciences"},{"issue":"1","key":"6_CR20","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 Journal on Computing\u00a018(1), 186\u2013207 (1989)","journal-title":"SIAM Journal on Computing"},{"key":"6_CR21","unstructured":"Herzog, J.: Computational Soundness of Formal Adversaries. PhD thesis, MIT (2002)"},{"key":"6_CR22","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 - CRYPTO 2003","author":"J. Herzog","year":"2003","unstructured":"Herzog, J., Liskov, M., Micali, S.: Plaintext awareness via key registration. In: Boneh, D. (ed.) CRYPTO 2003. LNCS, vol.\u00a02729, pp. 548\u2013564. Springer, Heidelberg (2003)"},{"key":"6_CR23","doi-asserted-by":"crossref","unstructured":"Impagliazzo, R., Kapron, B.M.: Logics for reasoning about cryptographic constructions. In: Proc. 44th IEEE Symposium on Foundations of Computer Science, pp. 372\u2013381 (2003)","DOI":"10.1109\/SFCS.2003.1238211"},{"key":"6_CR24","unstructured":"Javier Thayer, F., Herzog, J.C., Guttman, J.D.: Honest ideals on strand spaces. In: Proc. 11th IEEE Computer Security Foundations Workshop (CSFW), pp. 66\u201377 (1998)"},{"issue":"4","key":"6_CR25","doi-asserted-by":"publisher","first-page":"448","DOI":"10.1109\/49.17707","volume":"7","author":"R. Kemmerer","year":"1989","unstructured":"Kemmerer, R.: Analyzing encryption protocols using formal verification techniques. IEEE Journal on Selected Areas in Communications\u00a07(4), 448\u2013457 (1989)","journal-title":"IEEE Journal on Selected Areas in Communications"},{"key":"6_CR26","doi-asserted-by":"crossref","unstructured":"Laud, P.: Semantics and program analysis of computationally secure information flow. In: Proc. 10th European Symposium on Programming (ESOP), pp. 77\u201391 (2001)","DOI":"10.1007\/3-540-45309-1_6"},{"key":"6_CR27","doi-asserted-by":"crossref","unstructured":"Laud, P.: Symmetric encryption in automatic analyses for confidentiality against active adversaries. In: Proc. 25th IEEE Symposium on Security & Privacy, pp. 71\u201385 (2004)","DOI":"10.1109\/SECPRI.2004.1301316"},{"key":"6_CR28","doi-asserted-by":"crossref","unstructured":"Lincoln, P., Mitchell, J., Mitchell, M., Scedrov, A.: A probabilistic poly-time framework for protocol analysis. In: Proc. 5th ACMConference on Computer and Communications Security, pp. 112\u2013121 (1998)","DOI":"10.1145\/288090.288117"},{"key":"6_CR29","doi-asserted-by":"crossref","unstructured":"Meadows, C.: Using narrowing in the analysis of key management protocols. In: Proc. 10th IEEE Symposium on Security & Privacy, pp. 138\u2013147 (1989)","DOI":"10.1109\/SECPRI.1989.36288"},{"key":"6_CR30","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":"6_CR31","doi-asserted-by":"crossref","unstructured":"Millen, J.K.: The interrogator: A tool for cryptographic protocol security. In: Proc. 5th IEEE Symposium on Security & Privacy, pp. 134\u2013141 (1984)","DOI":"10.1109\/SP.1984.10003"},{"key":"6_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 IEEE Symposium on Foundations of Computer Science, pp. 725\u2013733 (1998)","DOI":"10.1109\/SFCS.1998.743523"},{"key":"6_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 (preliminary report). Electronic Notes in Theoretical Computer Science\u00a047, 1\u201331 (2001)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"issue":"21","key":"6_CR34","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1145\/359657.359659","volume":"12","author":"R. Needham","year":"1978","unstructured":"Needham, R., Schroeder, M.: Using encryption for authentication in large networks of computers. Communications of the ACM\u00a012(21), 993\u2013999 (1978)","journal-title":"Communications of the ACM"},{"issue":"1","key":"6_CR35","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1145\/24592.24594","volume":"21","author":"D. Otway","year":"1987","unstructured":"Otway, D., Rees, O.: Efficient and timely mutual authentication. Operation Systems Review\u00a021(1), 8\u201310 (1987)","journal-title":"Operation Systems Review"},{"key":"6_CR36","doi-asserted-by":"crossref","unstructured":"Paulson, L.: Mechanized proofs for a recursive authentication protocol. In: Proc. 10th IEEE Computer Security Foundations Workshop (CSFW), pp. 84\u201395 (1997)","DOI":"10.1109\/CSFW.1997.596790"},{"issue":"1","key":"6_CR37","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":"6_CR38","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 Symposium on Security & Privacy, pp. 184\u2013200 (2001)","DOI":"10.1109\/SECPRI.2001.924298"},{"key":"6_CR39","doi-asserted-by":"crossref","unstructured":"Rogaway, P., Bellare, M., Black, J., Krovetz, T.: OCB: A block-cipher mode of operation for efficient authenticated encryption. In: Proc. 8th ACM Conference on Computer and Communications Security, pp. 196\u2013205 (2001)","DOI":"10.1145\/502010.502011"},{"key":"6_CR40","unstructured":"Wagner, D., Schneier, B.: Analysis of the SSL 3.0 protocol. In: Proc. 2nd USENIX Workshop on Electronic Commerce, pp. 29\u201340 (1996)"},{"key":"6_CR41","doi-asserted-by":"crossref","unstructured":"Warinschi, B.: A computational analysis of the Needham-Schroeder-(Lowe) protocol. In: Proc. 16th IEEE Computer Security Foundations Workshop (CSFW), pp. 248\u2013262 (2003)","DOI":"10.1109\/CSFW.2003.1212717"}],"container-title":["Lecture Notes in Computer Science","Computer Security \u2013 ESORICS 2004"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30108-0_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,25]],"date-time":"2025-02-25T21:52:22Z","timestamp":1740520342000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30108-0_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540229872","9783540301080"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30108-0_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}