{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,28]],"date-time":"2026-02-28T13:00:33Z","timestamp":1772283633513,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":39,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540374329","type":"print"},{"value":"9783540374336","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11818175_32","type":"book-chapter","created":{"date-parts":[[2006,9,23]],"date-time":"2006-09-23T06:21:52Z","timestamp":1158992512000},"page":"537-554","source":"Crossref","is-referenced-by-count":48,"title":["Automated Security Proofs with Sequences of Games"],"prefix":"10.1007","author":[{"given":"Bruno","family":"Blanchet","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Pointcheval","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"32_CR1","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1007\/s00145-001-0014-7","volume":"15","author":"M. Abadi","year":"2002","unstructured":"Abadi, M., Rogaway, P.: Reconciling two views of cryptography (the computational soundness of formal encryption). Journal of Cryptology\u00a015(2), 103\u2013127 (2002)","journal-title":"Journal of Cryptology"},{"key":"32_CR2","unstructured":"Backes, M., Laud, P.: A mechanized, cryptographically sound type inference checker. In: Workshop on Formal and Computational Cryptography (FCC 2006) (July 2006) (to appear)"},{"key":"32_CR3","volume-title":"CSFW 2004","author":"M. Backes","year":"2004","unstructured":"Backes, M., Pfitzmann, B.: Symmetric encryption in a simulatable Dolev-Yao style cryptographic library. In: CSFW 2004, June 2004. IEEE, Los Alamitos (2004)"},{"key":"32_CR4","first-page":"171","volume-title":"26th IEEE Symposium on Security and Privacy","author":"M. Backes","year":"2005","unstructured":"Backes, M., Pfitzmann, B.: Relating symbolic and cryptographic secrecy. In: 26th IEEE Symposium on Security and Privacy, May 2005, pp. 171\u2013182. IEEE, Los Alamitos (2005)"},{"key":"32_CR5","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1145\/948109.948140","volume-title":"CCS 2003","author":"M. Backes","year":"2003","unstructured":"Backes, M., Pfitzmann, B., Waidner, M.: A composable cryptographic library with nested operations. In: CCS 2003, October 2003, pp. 220\u2013230. ACM Press, New York (2003)"},{"key":"32_CR6","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":"32_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/978-3-540-25984-8_29","volume-title":"Automated Reasoning","author":"G. Barthe","year":"2004","unstructured":"Barthe, G., Cederquist, J., Tarento, S.: A machine-checked formalization of the generic model and the random oracle model. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS, vol.\u00a03097, pp. 385\u2013399. Springer, Heidelberg (2004)"},{"key":"32_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030423","volume-title":"Information Security","author":"M. Bellare","year":"1998","unstructured":"Bellare, M.: Practice-Oriented Provable Security. In: Okamoto, E. (ed.) ISW 1997. LNCS, vol.\u00a01396. Springer, Heidelberg (1998)"},{"key":"32_CR9","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1145\/168588.168596","volume-title":"CCS 1993","author":"M. Bellare","year":"1993","unstructured":"Bellare, M., Rogaway, P.: Random Oracles Are Practical: a Paradigm for Designing Efficient Protocols. In: CCS 1993, pp. 62\u201373. ACM Press, New York (1993)"},{"key":"32_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"399","DOI":"10.1007\/3-540-68339-9_34","volume-title":"Advances in Cryptology - EUROCRYPT \u201996","author":"M. Bellare","year":"1996","unstructured":"Bellare, M., Rogaway, P.: The Exact Security of Digital Signatures - How to Sign with RSA and Rabin. In: Maurer, U.M. (ed.) EUROCRYPT 1996. LNCS, vol.\u00a01070, pp. 399\u2013416. Springer, Heidelberg (1996)"},{"key":"32_CR11","unstructured":"Bellare, M., Rogaway, P.: The Game-Playing Technique and its Application to Triple Encryption. Cryptology ePrint Archive 2004\/331 (2004)"},{"key":"32_CR12","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: Automatic proof of strong secrecy for security protocols. In: IEEE Symposium on Security and Privacy, May 2004, pp. 86\u2013100 (2004)","DOI":"10.1109\/SECPRI.2004.1301317"},{"key":"32_CR13","unstructured":"Blanchet, B.: A computationally sound mechanized prover for security protocols. Cryptology ePrint Archive, Report 2005\/401 (November 2005), Available at: http:\/\/eprint.iacr.org\/2005\/401"},{"key":"32_CR14","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: A computationally sound mechanized prover for security protocols. In: IEEE Symposium on Security and Privacy, May 2006, pp. 140\u2013154 (2006)","DOI":"10.1109\/SP.2006.1"},{"key":"32_CR15","unstructured":"Blanchet, B., Pointcheval, D.: Automated security proofs with sequences of games. Cryptology ePrint Archive, Report 2006\/069 (Feburary 2006), Available at: http:\/\/eprint.iacr.org\/2006\/069"},{"key":"32_CR16","first-page":"136","volume-title":"FOCS 2001","author":"R. Canetti","year":"2001","unstructured":"Canetti, R.: Universally composable security: A new paradigm for cryptographic protocols. In: FOCS 2001, October 2001, pp. 136\u2013145. IEEE, Los Alamitos (2001); Cryptology ePrint Archive, An updated version is available at: http:\/\/eprint.iacr.org\/2000\/067"},{"key":"32_CR17","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), Available at: http:\/\/eprint.iacr.org\/2004\/334"},{"key":"32_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-540-31987-0_12","volume-title":"Programming Languages and Systems","author":"V. Cortier","year":"2005","unstructured":"Cortier, V., Warinschi, B.: Computationally sound, automated proofs for security protocols. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 157\u2013171. Springer, Heidelberg (2005)"},{"key":"32_CR19","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":"6","key":"32_CR20","doi-asserted-by":"publisher","first-page":"644","DOI":"10.1109\/TIT.1976.1055638","volume":"IT\u201322","author":"W. Diffie","year":"1976","unstructured":"Diffie, W., Hellman, M.E.: New Directions in Cryptography. IEEE Transactions on Information Theory\u00a0IT\u201322(6), 644\u2013654 (1976)","journal-title":"IEEE Transactions on Information Theory"},{"issue":"2","key":"32_CR21","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":"32_CR22","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":"32_CR23","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.: A Digital Signature Scheme Secure Against Adaptative Chosen-Message Attacks. SIAM Journal of Computing\u00a017(2), 281\u2013308 (1988)","journal-title":"SIAM Journal of Computing"},{"key":"32_CR24","unstructured":"Halevi, S.: A plausible approach to computer-aided cryptographic proofs. Cryptology ePrint Archive, Report 2005\/181 (June 2005), Available at: http:\/\/eprint.iacr.org\/2005\/181"},{"key":"32_CR25","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":"32_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/3-540-36575-3_12","volume-title":"Programming Languages and Systems","author":"P. Laud","year":"2003","unstructured":"Laud, P.: Handling encryption in an analysis for secure information flow. In: Degano, P. (ed.) ESOP 2003 and ETAPS 2003. LNCS, vol.\u00a02618, pp. 159\u2013173. Springer, Heidelberg (2003)"},{"key":"32_CR27","doi-asserted-by":"crossref","unstructured":"Laud, P.: Symmetric encryption in automatic analyses for confidentiality against active adversaries. In: IEEE Symposium on Security and Privacy, May 2004, pp. 71\u201385 (2004)","DOI":"10.1109\/SECPRI.2004.1301316"},{"key":"32_CR28","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1145\/1102120.1102126","volume-title":"CCS 2005","author":"P. Laud","year":"2005","unstructured":"Laud, P.: Secrecy types for a simulatable cryptographic library. In: CCS 2005, November 2005, pp. 26\u201335. ACM Press, New York (2005)"},{"key":"32_CR29","doi-asserted-by":"crossref","unstructured":"Lincoln, P.D., Mitchell, J.C., Mitchell, M., Scedrov, A.: A probabilistic poly-time framework for protocol analysis. In: CCS 1998, November 1998, pp. 112\u2013121 (1998)","DOI":"10.1145\/288090.288117"},{"key":"32_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"776","DOI":"10.1007\/3-540-48119-2_43","volume-title":"FM\u201999 - Formal Methods","author":"P. Lincoln","year":"1999","unstructured":"Lincoln, P., Mitchell, J., Mitchell, M., Scedrov, A.: Probabilistic polynomial-time equivalence and security analysis. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol.\u00a01708, pp. 776\u2013793. Springer, Heidelberg (1999)"},{"key":"32_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/978-3-540-45187-7_22","volume-title":"CONCUR 2003 - Concurrency Theory","author":"P. Mateus","year":"2003","unstructured":"Mateus, P., Mitchell, J., Scedrov, A.: Composition of cryptographic protocols in a probabilistic polynomial-time process calculus. In: Amadio, R., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol.\u00a02761, pp. 327\u2013349. Springer, Heidelberg (2003)"},{"key":"32_CR32","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)"},{"issue":"1\u20133","key":"32_CR33","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1016\/j.tcs.2005.10.044","volume":"353","author":"J.C. Mitchell","year":"2006","unstructured":"Mitchell, J.C., Ramanathan, A., Scedrov, A., Teague, V.: A probabilistic polynomial-time calculus for the analysis of cryptographic protocols. Theoretical Computer Science\u00a0353(1\u20133), 118\u2013164 (2006)","journal-title":"Theoretical Computer Science"},{"key":"32_CR34","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1145\/73007.73011","volume-title":"STOC 1989","author":"M. Naor","year":"1989","unstructured":"Naor, M., Yung, M.: Universal One-Way Hash Functions and Their Cryptographic Applications. In: STOC 1989, pp. 33\u201343. ACM Press, New York (1989)"},{"key":"32_CR35","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":"32_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"468","DOI":"10.1007\/978-3-540-24727-2_33","volume-title":"Foundations of Software Science and Computation Structures","author":"A. Ramanathan","year":"2004","unstructured":"Ramanathan, A., Mitchell, J., Scedrov, A., Teague, V.: Probabilistic bisimulation and equivalence for security analysis of network protocols. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol.\u00a02987, pp. 468\u2013483. Springer, Heidelberg (2004)"},{"key":"32_CR37","unstructured":"Shoup, V.: Sequences of games: a tool for taming complexity in security proofs. Cryptology ePrint Archive 2004\/332 (2004)"},{"key":"32_CR38","volume-title":"CSFW 2006","author":"C. Sprenger","year":"2006","unstructured":"Sprenger, C., Backes, M., Basin, D., Pfitzmann, B., Waidner, M.: Cryptographically sound theorem proving. In: CSFW 2006, July 2006. IEEE, Los Alamitos (2006) (to appear)"},{"key":"32_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/11555827_9","volume-title":"Computer Security \u2013 ESORICS 2005","author":"S. Tarento","year":"2005","unstructured":"Tarento, S.: Machine-checked security proofs of cryptographic signature schemes. In: di Vimercati, S.d.C., Syverson, P.F., Gollmann, D. (eds.) ESORICS 2005. LNCS, vol.\u00a03679, pp. 140\u2013158. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Advances in Cryptology - CRYPTO 2006"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11818175_32.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,10]],"date-time":"2025-01-10T23:44:49Z","timestamp":1736552689000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11818175_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540374329","9783540374336"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/11818175_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}