{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,2]],"date-time":"2025-02-02T20:10:34Z","timestamp":1738527034176,"version":"3.35.0"},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540894384"},{"type":"electronic","value":"9783540894391"}],"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-89439-1_26","type":"book-chapter","created":{"date-parts":[[2008,11,15]],"date-time":"2008-11-15T03:03:10Z","timestamp":1226718190000},"page":"353-376","source":"Crossref","is-referenced-by-count":16,"title":["A Formal Language for Cryptographic Pseudocode"],"prefix":"10.1007","author":[{"given":"Michael","family":"Backes","sequence":"first","affiliation":[]},{"given":"Matthias","family":"Berg","sequence":"additional","affiliation":[]},{"given":"Dominique","family":"Unruh","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"26_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":"26_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":"26_CR3","doi-asserted-by":"crossref","unstructured":"Backes, M., Pfitzmann, B.: Symmetric encryption in a simulatable Dolev-Yao style cryptographic library. In: Proc. 17th IEEE Computer Security Foundations Workshop (CSFW), pp. 204\u2013218 (2004)","DOI":"10.1109\/CSFW.2004.1310742"},{"key":"#cr-split#-26_CR4.1","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???230 (2003);","DOI":"10.1145\/948109.948140"},{"key":"#cr-split#-26_CR4.2","unstructured":"Full version in IACR Cryptology ePrint Archive 2003\/015 (January 2003), http:\/\/eprint.iacr.org\/"},{"key":"26_CR5","doi-asserted-by":"crossref","unstructured":"Barthe, G., Gregoire, B., Janvier, R., Zanella Beguelin, S.: Formal certification of code-based cryptographic proofs. IACR ePrint Archive (August. 2007), http:\/\/eprint.iacr.org\/2007\/314","DOI":"10.1145\/1480881.1480894"},{"key":"26_CR6","doi-asserted-by":"crossref","unstructured":"Basin, D., M\u00f6dersheim, S., Vigan\u00f2, L.: OFMC: A symbolic model checker for security protocols. International Journal of Information Security (2004)","DOI":"10.1007\/s10207-004-0055-7"},{"key":"26_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/11761679_25","volume-title":"Advances in Cryptology - EUROCRYPT 2006","author":"M. Bellare","year":"2006","unstructured":"Bellare, M., Rogaway, P.: The security of triple encryption and a framework for code-based game-playing proofs. In: Vaudenay, S. (ed.) EUROCRYPT 2006. LNCS, vol.\u00a04004, pp. 409\u2013426. Springer, Heidelberg (2006), http:\/\/eprint.iacr.org\/2004\/331.ps"},{"key":"26_CR8","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: A computationally sound mechanized prover for security protocols. In: Proc. 27th IEEE Symposium on Security & Privacy, pp. 140\u2013154 (2006)","DOI":"10.1109\/SP.2006.1"},{"key":"26_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"537","DOI":"10.1007\/11818175_32","volume-title":"Advances in Cryptology - CRYPTO 2006","author":"B. Blanchet","year":"2006","unstructured":"Blanchet, B., Pointcheval, D.: Automated security proofs with sequences of games. In: Dwork, C. (ed.) CRYPTO 2006. LNCS, vol.\u00a04117, pp. 537\u2013554. Springer, Heidelberg (2006)"},{"key":"26_CR10","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":"26_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/11787006_22","volume-title":"Automata, Languages and Programming","author":"R. Corin","year":"2006","unstructured":"Corin, R., den Hartog, J.: A probabilistic hoare-style logic for game-based cryptographic proofs. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol.\u00a04052, pp. 252\u2013263. Springer, Heidelberg (2006)"},{"key":"26_CR12","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":"26_CR13","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"N.G. Bruijn de","year":"1972","unstructured":"de Bruijn, N.G.: Lambda Calculus notation with nameless dummies: a tool for automatic formula manipulation. Indagationes Mathematic\u00e6\u00a034, 381\u2013392 (1972)","journal-title":"Indagationes Mathematic\u00e6"},{"key":"26_CR14","series-title":"Basic Applications","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511721656","volume-title":"Foundations of Cryptography","author":"O. Goldreich","year":"2004","unstructured":"Goldreich, O.: Foundations of Cryptography, May 2004. Basic Applications, vol.\u00a02. Cambridge University Press, Cambridge (May 2004), http:\/\/www.wisdom.weizmann.ac.il\/~oded\/frag.html"},{"key":"26_CR15","unstructured":"Halevi, S.: A plausible approach to computer-aided cryptographic proofs. Cryptology ePrint Archive, Report 2005\/181 (2005), http:\/\/eprint.iacr.org\/"},{"key":"26_CR16","series-title":"Graduate Texts in Mathematics","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-9976-0","volume-title":"Measure Theory","author":"P.R. Halmos","year":"1974","unstructured":"Halmos, P.R.: Measure Theory. Graduate Texts in Mathematics, vol.\u00a018. Springer, Heidelberg (1974)"},{"issue":"4","key":"26_CR17","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":"26_CR18","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":"26_CR19","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":"26_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/3-540-45793-3_16","volume-title":"Computer Science Logic","author":"P.B. Levy","year":"2002","unstructured":"Levy, P.B.: Possible world semantics for general storage in call-by-value. In: Bradfield, J.C. (ed.) CSL 2002 and EACSL 2002. LNCS, vol.\u00a02471, pp. 232\u2013246. Springer, Heidelberg (2002)"},{"key":"26_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/3-540-61042-1_43","volume-title":"Proc. 2nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"G. Lowe","year":"1996","unstructured":"Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: TACAS 1996. LNCS, vol.\u00a01055, pp. 147\u2013166. Springer, Heidelberg (1996)"},{"issue":"3","key":"26_CR22","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1017\/S0956796800000125","volume":"1","author":"I. Mason","year":"1991","unstructured":"Mason, I., Talcott, C.: Equivalence in Functional Languages with Effects. Journal of Functional Programming\u00a01(3), 287\u2013327 (1991)","journal-title":"Journal of Functional Programming"},{"key":"26_CR23","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":"26_CR24","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":"26_CR25","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"},{"issue":"2","key":"26_CR26","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1017\/S095679689900341X","volume":"9","author":"O. M\u00fcller","year":"1999","unstructured":"M\u00fcller, O., Nipkow, T., von Oheimb, D., Slotosch, O.: HOLCF = HOL + LCF. Journal of Functional Programming\u00a09(2), 191\u2013223 (1999)","journal-title":"Journal of Functional Programming"},{"key":"26_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"26_CR28","doi-asserted-by":"crossref","unstructured":"Nowak, D.: A framework for game-based security proofs. IACR Cryptology ePrint Archive 2007\/199 (2007), http:\/\/eprint.iacr.org\/","DOI":"10.1007\/978-3-540-77048-0_25"},{"issue":"1","key":"26_CR29","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":"26_CR30","volume-title":"Types and programming languages","author":"B.C. Pierce","year":"2002","unstructured":"Pierce, B.C.: Types and programming languages. MIT Press, Cambridge (2002)"},{"key":"26_CR31","unstructured":"Schwinghammer, J.: Reasoning about Denotations of Recursive Objects. PhD thesis, Department of Informatics, University of Sussex, Brighton, UK (July 2006)"},{"key":"26_CR32","unstructured":"Shoup, V.: Sequences of games: A tool for taming complexity in security proofs. IACR ePrint Archive (November 2004), http:\/\/eprint.iacr.org\/2004\/332.ps"},{"key":"26_CR33","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":"26_CR34","unstructured":"The Coq development team. The Coq Proof Assistant Reference Manual (2006), http:\/\/coq.inria.fr"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-89439-1_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,2]],"date-time":"2025-02-02T19:50:54Z","timestamp":1738525854000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-89439-1_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540894384","9783540894391"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-89439-1_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}