{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,17]],"date-time":"2026-06-17T15:06:33Z","timestamp":1781708793576,"version":"3.54.5"},"publisher-location":"Berlin, Heidelberg","reference-count":73,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540289555","type":"print"},{"value":"9783540319368","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11554578_1","type":"book-chapter","created":{"date-parts":[[2005,9,27]],"date-time":"2005-09-27T12:51:11Z","timestamp":1127825471000},"page":"1-41","source":"Crossref","is-referenced-by-count":1,"title":["Justifying a Dolev-Yao Model Under Active Attacks"],"prefix":"10.1007","author":[{"given":"Michael","family":"Backes","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Birgit","family":"Pfitzmann","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Michael","family":"Waidner","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"1_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":"1_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":"1_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1007\/3-540-44750-4_19","volume-title":"Advances in Cryptology - CRYPTO \u201995","author":"R. Anderson","year":"1995","unstructured":"Anderson, R., Needham, R.: Robustness principles for public key protocols. In: Coppersmith, D. (ed.) CRYPTO 1995. LNCS, vol.\u00a0963, pp. 236\u2013247. Springer, Heidelberg (1995)"},{"key":"1_CR4","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":"1_CR5","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)"},{"key":"1_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45853-0_1","volume-title":"Computer Security - ESORICS 2002","author":"M. Backes","year":"2002","unstructured":"Backes, M., Pfitzmann, B.: Computational probabilistic non-interference. In: Gollmann, D., Karjoth, G., Waidner, M. (eds.) ESORICS 2002. LNCS, vol.\u00a02502, pp. 1\u201323. Springer, Heidelberg (2002)"},{"key":"1_CR7","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":"1_CR8","doi-asserted-by":"crossref","unstructured":"Backes, M., Pfitzmann, B.: Intransitive non-interference for cryptographic purposes. In: Proc. 24th IEEE Symposium on Security & Privacy, pp. 140\u2013152 (2003)","DOI":"10.1109\/SECPRI.2003.1199333"},{"key":"1_CR9","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, Feb. 2004. Full version in IACR Cryptology ePrint Archive 2004\/059 (2004), http:\/\/eprint.iacr.org\/"},{"key":"1_CR10","unstructured":"Backes, M., Pfitzmann, B.: Relating symbolic and cryptographic key secrecy. In: Proc. 26th IEEE Symposium on Security & Privacy 2005. Extended version in IACR Cryptology ePrint Archive 2004\/300 (2005)"},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"Backes, M., Pfitzmann, B., Steiner, M., Waidner, M.: Polynomial fairness and liveness. In: Proc. 15th IEEE Computer Security Foundations Workshop (CSFW), pp. 160\u2013174 (2002)","DOI":"10.1109\/CSFW.2002.1021814"},{"key":"1_CR12","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, January 2003. Full version in IACR Cryptology ePrint Archive 2003\/015, pp. 220\u2013230 (2003), http:\/\/eprint.iacr.org\/","DOI":"10.1145\/948109.948140"},{"key":"1_CR13","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":"1_CR14","doi-asserted-by":"crossref","unstructured":"Backes, M., Pfitzmann, B., Waidner, M.: A universally composable cryptographic library. IACR Cryptology ePrint Archive 2003\/015 (January 2003), http:\/\/eprint.iacr.org\/","DOI":"10.1145\/948109.948140"},{"issue":"2","key":"1_CR15","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/BF00196771","volume":"4","author":"D. Beaver","year":"1991","unstructured":"Beaver, D.: Secure multiparty protocols and zero knowledge proof systems tolerating a faulty minority. Journal of Cryptology\u00a04(2), 75\u2013122 (1991)","journal-title":"Journal of Cryptology"},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"Bella, G., Massacci, F., Paulson, L.C.: The verification of an industrial payment protocol: The SET purchase phase. In: Proc. 9th ACM Conference on Computer and Communications Security, pp. 12\u201320 (2002)","DOI":"10.1145\/586110.586113"},{"key":"1_CR17","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":"1_CR18","doi-asserted-by":"crossref","unstructured":"Bellare, M., Kohno, T., Namprempre, C.: Authenticated encryption in ssh: Provably fixing the ssh binary packet protocol. In: Proc. 9th ACM Conference on Computer and Communications Security, pp. 1\u201311 (2002)","DOI":"10.1145\/586110.586112"},{"key":"1_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"232","DOI":"10.1007\/3-540-48329-2_21","volume-title":"Advances in Cryptology - CRYPTO \u201993","author":"M. Bellare","year":"1994","unstructured":"Bellare, M., Rogaway, P.: Entity authentication and key distribution. In: Stinson, D.R. (ed.) CRYPTO 1993. LNCS, vol.\u00a0773, pp. 232\u2013249. Springer, Heidelberg (1994)"},{"key":"1_CR20","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)"},{"issue":"1","key":"1_CR21","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/s001459910006","volume":"3","author":"R. Canetti","year":"2000","unstructured":"Canetti, R.: Security and composition of multiparty cryptographic protocols. Journal of Cryptology\u00a03(1), 143\u2013202 (2000)","journal-title":"Journal of Cryptology"},{"key":"1_CR22","unstructured":"Canetti, R.: A unified framework for analyzing security of protocols. IACR Cryptology ePrint Archive 2000\/067 (December 2000), http:\/\/eprint.iacr.org\/"},{"key":"1_CR23","doi-asserted-by":"crossref","unstructured":"Canetti, R.: Universally composable security: A new paradigm for cryptographic protocols. In: Proc. 42nd IEEE Symposium on Foundations of Computer Science (FOCS). Extended version in Cryptology ePrint Archive, Report 2000\/67, pp. 136\u2013145 (2001), http:\/\/eprint.iacr.org\/","DOI":"10.1109\/SFCS.2001.959888"},{"key":"1_CR24","doi-asserted-by":"crossref","unstructured":"Canetti, R., Goldreich, O., Halevi, S.: The random oracle methodology, revisited. In: Proc. 30th Annual ACM Symposium on Theory of Computing (STOC), pp. 209\u2013218 (1998)","DOI":"10.1145\/276698.276741"},{"key":"1_CR25","unstructured":"Canetti, R., Herzog, J.: Universally composable symbolic analysis of cryptographic protocols (the case of encryption-based mutual authentication and key exchange). Cryptology ePrint Archive, Report 2004\/334 (2004), http:\/\/eprint.iacr.org\/"},{"key":"1_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1007\/3-540-44750-4_24","volume-title":"Advances in Cryptology - CRYPTO \u201995","author":"R. Cramer","year":"1995","unstructured":"Cramer, R., Damg\u00e5rd, I.: Secure signature schemes based on interactive protocols. In: Coppersmith, D. (ed.) CRYPTO 1995. LNCS, vol.\u00a0963, pp. 297\u2013310. Springer, Heidelberg (1995)"},{"key":"1_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/3-540-68697-5_14","volume-title":"Advances in Cryptology - CRYPTO \u201996","author":"R. Cramer","year":"1996","unstructured":"Cramer, R., Damg\u00e5rd, I.: New generation of secure and practical RSA-based signatures. In: Koblitz, N. (ed.) CRYPTO 1996. LNCS, vol.\u00a01109, pp. 173\u2013185. Springer, Heidelberg (1996)"},{"key":"1_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1007\/BFb0055717","volume-title":"Advances in Cryptology - CRYPTO \u201998","author":"R. Cramer","year":"1998","unstructured":"Cramer, R., Shoup, V.: Practical public key cryptosystem provably secure against adaptive chosen ciphertext attack. In: Krawczyk, H. (ed.) CRYPTO 1998. LNCS, vol.\u00a01462, pp. 13\u201325. Springer, Heidelberg (1998)"},{"key":"1_CR29","doi-asserted-by":"crossref","unstructured":"Cramer, R., Shoup, V.: Signature schemes based on the strong RSA assumption. In: Proc. 6th ACM Conference on Computer and Communications Security, pp. 46\u201351 (1999)","DOI":"10.1145\/319709.319716"},{"key":"1_CR30","unstructured":"Dang, Z., Kemmerer, R.: Using the ASTRAL model checker for cryptographic protocol analysis. In: Proc. DIMACS Workshop on Design and Formal Verification of Security Protocols (1997), http:\/\/dimacs.rutgers.edu\/Workshops\/Security\/"},{"issue":"8","key":"1_CR31","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"},{"key":"1_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"557","DOI":"10.1007\/3-540-45539-6_39","volume-title":"Advances in Cryptology - EUROCRYPT 2000","author":"Y. Desmedt","year":"2000","unstructured":"Desmedt, Y., Kurosawa, K.: How to break a practical mix and design a new one. In: Preneel, B. (ed.) EUROCRYPT 2000. LNCS, vol.\u00a01807, pp. 557\u2013572. Springer, Heidelberg (2000)"},{"issue":"2","key":"1_CR33","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":"1_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/BFb0028390","volume-title":"Theorem Proving in Higher Order Logics","author":"B. Dutertre","year":"1997","unstructured":"Dutertre, B., Schneider, S.: Using a PVS embedding of CSP to verify authentication protocols. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol.\u00a01275, pp. 121\u2013136. Springer, Heidelberg (1997)"},{"key":"1_CR35","unstructured":"Fisher, D.: Millions of .Net Passport accounts put at risk. In: Fisher, D. (ed.) eWeek, May 2003. Flaw detected by Muhammad Faisal Rauf Danka (2003)"},{"key":"1_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/3-540-48910-X_9","volume-title":"Advances in Cryptology - EUROCRYPT \u201999","author":"R. Gennaro","year":"1999","unstructured":"Gennaro, R., Halevi, S., Rubin, T.: Secure hash-and-sign signatures without the random oracle. In: Stern, J. (ed.) EUROCRYPT 1999. LNCS, vol.\u00a01592, pp. 123\u2013139. Springer, Heidelberg (1999)"},{"key":"1_CR37","series-title":"Lecture Notes in Computer Science","first-page":"104","volume-title":"Advances in Cryptology - CRYPTO \u201986","author":"O. Goldreich","year":"1987","unstructured":"Goldreich, O.: Two remarks concerning the Goldwasser-Micali-Rivest signature scheme. In: Odlyzko, A.M. (ed.) CRYPTO 1986. LNCS, vol.\u00a0263, pp. 104\u2013110. Springer, Heidelberg (1987)"},{"key":"1_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1007\/3-540-38424-3_6","volume-title":"Advances in Cryptology - CRYPTO \u201990","author":"S. Goldwasser","year":"1991","unstructured":"Goldwasser, S., Levin, L.: Fair computation of general functions in presence of immoral majority. In: Menezes, A., Vanstone, S.A. (eds.) CRYPTO 1990. LNCS, vol.\u00a0537, pp. 77\u201393. Springer, Heidelberg (1991)"},{"key":"1_CR39","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":"2","key":"1_CR40","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1137\/0217017","volume":"17","author":"S. Goldwasser","year":"1988","unstructured":"Goldwasser, S., Micali, S., Rivest, R.L.: A digital signature scheme secure against adaptive chosen-message attacks. SIAM Journal on Computing\u00a017(2), 281\u2013308 (1988)","journal-title":"SIAM Journal on Computing"},{"key":"1_CR41","doi-asserted-by":"crossref","unstructured":"Guttman, J.D., Thayer Fabrega, F.J., Zuck, L.: The faithfulness of abstract protocol analysis: Message authentication. In: Proc. 8th ACM Conference on Computer and Communications Security, pp. 186\u2013195 (2001)","DOI":"10.1145\/501983.502009"},{"key":"1_CR42","unstructured":"Herzog, J.: Computational Soundness of Formal Adversaries. PhD thesis, MIT (2002)"},{"key":"1_CR43","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)"},{"issue":"1","key":"1_CR44","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s001459910003","volume":"13","author":"M. Hirt","year":"2000","unstructured":"Hirt, M., Maurer, U.: Player simulation and general adversary structures in perfect multiparty computation. Journal of Cryptology\u00a013(1), 31\u201360 (2000)","journal-title":"Journal of Cryptology"},{"key":"1_CR45","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 (FOCS), pp. 372\u2013381 (2003)","DOI":"10.1109\/SFCS.2003.1238211"},{"issue":"2","key":"1_CR46","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. Journal of Cryptology\u00a07(2), 79\u2013130 (1994)","journal-title":"Journal of Cryptology"},{"key":"1_CR47","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":"1_CR48","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":"1_CR49","doi-asserted-by":"crossref","unstructured":"Lincoln, P., Mitchell, J., Mitchell, M., Scedrov, A.: A probabilistic poly-time framework for protocol analysis. In: Proc. 5th ACM Conference on Computer and Communications Security, pp. 112\u2013121 (1998)","DOI":"10.1145\/288090.288117"},{"issue":"3","key":"1_CR50","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1016\/0020-0190(95)00144-2","volume":"56","author":"G. Lowe","year":"1995","unstructured":"Lowe, G.: An attack on the Needham-Schroeder public-key authentication protocol. Information Processing Letters\u00a056(3), 131\u2013135 (1995)","journal-title":"Information Processing Letters"},{"key":"1_CR51","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":"Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol.\u00a01055, pp. 147\u2013166. Springer, Heidelberg (1996)"},{"key":"1_CR52","doi-asserted-by":"crossref","unstructured":"Lowe, G.: Casper: A compiler for the analysis of security protocols. In: Proc. 10th IEEE Computer Security Foundations Workshop (CSFW), pp. 18\u201330 (1997)","DOI":"10.1109\/CSFW.1997.596779"},{"key":"1_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1007\/3-540-61770-1_46","volume-title":"Computer Security - ESORICS 96","author":"C. Meadows","year":"1996","unstructured":"Meadows, C.: Analyzing the Needham-Schroeder public key protocol: A comparison of two approaches. In: Martella, G., Kurth, H., Montolivo, E., Bertino, E. (eds.) ESORICS 1996. LNCS, vol.\u00a01146, pp. 351\u2013364. Springer, Heidelberg (1996)"},{"key":"1_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"392","DOI":"10.1007\/3-540-46766-1_32","volume-title":"Advances in Cryptology - CRYPTO \u201991","author":"S. Micali","year":"1992","unstructured":"Micali, S., Rogaway, P.: Secure computation. In: Feigenbaum, J. (ed.) CRYPTO 1991. LNCS, vol.\u00a0576, pp. 392\u2013404. Springer, Heidelberg (1992)"},{"key":"1_CR55","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":"1_CR56","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 (FOCS), pp. 725\u2013733 (1998)","DOI":"10.1109\/SFCS.1998.743523"},{"key":"1_CR57","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"},{"key":"1_CR58","doi-asserted-by":"crossref","unstructured":"Mitchell, J., Mitchell, M., Stern, U.: Automated analysis of cryptographic protocols using mur\u03c6. In: Proc. 18th IEEE Symposium on Security & Privacy, pp. 141\u2013151 (1997)","DOI":"10.1109\/SECPRI.1997.601329"},{"issue":"21","key":"1_CR59","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"},{"key":"1_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction - CADE-11","author":"S. Owre","year":"1992","unstructured":"Owre, S., Shankar, N., Rushby, J.M.: PVS: A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, pp. 748\u2013752. Springer, Heidelberg (1992)"},{"issue":"1","key":"1_CR61","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":"1_CR62","doi-asserted-by":"crossref","unstructured":"Pfitzmann, B., Schunter, M., Waidner, M.: Cryptographic security of reactive systems. In: Presented at the DERA\/RHUL Workshop on Secure Architectures and Information Flow, 1999, March 2000. Electronic Notes in Theoretical Computer Science, ENTCS (2000), http:\/\/www.elsevier.nl\/cas\/tree\/store\/tcs\/free\/noncas\/pc\/menu.htm","DOI":"10.1016\/S1571-0661(04)00095-7"},{"key":"1_CR63","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"338","DOI":"10.1007\/3-540-46766-1_28","volume-title":"Advances in Cryptology - CRYPTO \u201991","author":"B. Pfitzmann","year":"1992","unstructured":"Pfitzmann, B., Waidner, M.: How to break and repair a \u201cprovably secure\u201d untraceable payment system. In: Feigenbaum, J. (ed.) CRYPTO 1991. LNCS, vol.\u00a0576, pp. 338\u2013350. Springer, Heidelberg (1992)"},{"key":"1_CR64","doi-asserted-by":"crossref","unstructured":"Pfitzmann, B., Waidner, M.: Composition and integrity preservation of secure reactive systems. In: Proc. 7th ACM Conference on Computer and Communications Security, May 2000. Extended version (with Matthias Schunter) IBM Research Report RZ 3206, pp. 245\u2013254 (2000), http:\/\/www.semper.org\/sirene\/publ\/PfSW1_00ReactSimulIBM.ps.gz","DOI":"10.1145\/352600.352639"},{"key":"1_CR65","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. Extended version of the model (with Michael Backes) IACR Cryptology ePrint Archive 2004\/082, pp. 184\u2013200 (2001), http:\/\/eprint.iacr.org\/","DOI":"10.1109\/SECPRI.2001.924298"},{"key":"1_CR66","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"433","DOI":"10.1007\/3-540-46766-1_35","volume-title":"Advances in Cryptology - CRYPTO \u201991","author":"C. Rackoff","year":"1992","unstructured":"Rackoff, C., Simon, D.R.: Non-interactive zero-knowledge proof of knowledge and chosen ciphertext attack. In: Feigenbaum, J. (ed.) CRYPTO 1991. LNCS, vol.\u00a0576, pp. 433\u2013444. Springer, Heidelberg (1992)"},{"key":"1_CR67","doi-asserted-by":"crossref","unstructured":"Rogaway, P.: Authenticated-encryption with associated-data. In: Proc. 9th ACM Conference on Computer and Communications Security, pp. 98\u2013107 (2002)","DOI":"10.1145\/586110.586125"},{"key":"1_CR68","doi-asserted-by":"crossref","unstructured":"Schneider, S.: Verifying authentication protocols with CSP. In: Proc. 10th IEEE Computer Security Foundations Workshop (CSFW), pp. 3\u201317 (1997)","DOI":"10.1109\/CSFW.1997.596775"},{"issue":"3","key":"1_CR69","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/230908.230911","volume":"30","author":"P. Syverson","year":"1996","unstructured":"Syverson, P.: A new look at an old protocol. Operation Systems Review\u00a030(3), 1\u20134 (1996)","journal-title":"Operation Systems Review"},{"key":"1_CR70","doi-asserted-by":"crossref","unstructured":"Thayer Fabrega, F.J., Herzog, J.C., Guttman, J.D.: Strand spaces: Why is a security protocol correct? In: Proc. 19th IEEE Symposium on Security & Privacy, pp. 160\u2013171 (1998)","DOI":"10.21236\/ADA459060"},{"key":"1_CR71","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":"1_CR72","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"},{"key":"1_CR73","doi-asserted-by":"crossref","unstructured":"Yao, A.C.: Theory and applications of trapdoor functions. In: Proc. 23rd IEEE Symposium on Foundations of Computer Science (FOCS), pp. 80\u201391 (1982)","DOI":"10.1109\/SFCS.1982.45"}],"container-title":["Lecture Notes in Computer Science","Foundations of Security Analysis and Design III"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11554578_1.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,4]],"date-time":"2025-01-04T15:33:42Z","timestamp":1736004822000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11554578_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540289555","9783540319368"],"references-count":73,"URL":"https:\/\/doi.org\/10.1007\/11554578_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}