{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T08:47:54Z","timestamp":1770281274491,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642140518","type":"print"},{"value":"9783642140525","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14052-5_10","type":"book-chapter","created":{"date-parts":[[2010,7,12]],"date-time":"2010-07-12T14:23:14Z","timestamp":1278944594000},"page":"115-130","source":"Crossref","is-referenced-by-count":6,"title":["Programming Language Techniques for Cryptographic Proofs"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[]},{"given":"Benjamin","family":"Gr\u00e9goire","sequence":"additional","affiliation":[]},{"given":"Santiago","family":"Zanella B\u00e9guelin","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"10_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-540-75670-5_10","volume-title":"Provable Security","author":"R. Affeldt","year":"2007","unstructured":"Affeldt, R., Tanaka, M., Marti, N.: Formal proof of provable security by game-playing in a proof assistant. In: Susilo, W., Liu, J.K., Mu, Y. (eds.) ProvSec 2007. LNCS, vol.\u00a04784, pp. 151\u2013168. Springer, Heidelberg (2007)"},{"issue":"8","key":"10_CR2","doi-asserted-by":"publisher","first-page":"568","DOI":"10.1016\/j.scico.2007.09.002","volume":"74","author":"P. Audebaud","year":"2009","unstructured":"Audebaud, P., Paulin-Mohring, C.: Proofs of randomized algorithms in Coq. Science of Computer Programming\u00a074(8), 568\u2013589 (2009)","journal-title":"Science of Computer Programming"},{"key":"10_CR3","first-page":"90","volume-title":"Proceedings of the 36th ACM Symposium on Principles of Programming Languages","author":"G. Barthe","year":"2009","unstructured":"Barthe, G., Gr\u00e9goire, B., Zanella B\u00e9guelin, S.: Formal certification of code-based cryptographic proofs. In: Proceedings of the 36th ACM Symposium on Principles of Programming Languages, pp. 90\u2013101. ACM Press, New York (2009)"},{"key":"10_CR4","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1145\/168588.168596","volume-title":"Proceedings of the 1st ACM Conference on Computer and Communications Security","author":"M. Bellare","year":"1993","unstructured":"Bellare, M., Rogaway, P.: Random oracles are practical: A paradigm for designing efficient protocols. In: Proceedings of the 1st ACM Conference on Computer and Communications Security, pp. 62\u201373. ACM Press, New York (1993)"},{"key":"10_CR5","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)"},{"key":"10_CR6","first-page":"311","volume-title":"Proceedings of the ACM SIGPLAN\u201992 Conference on Programming Language Design and Implementation","author":"P. Briggs","year":"1992","unstructured":"Briggs, P., Cooper, K.D., Torczon, L.: Rematerialization. In: Proceedings of the ACM SIGPLAN\u201992 Conference on Programming Language Design and Implementation, pp. 311\u2013321. ACM Press, New York (1992)"},{"key":"10_CR7","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)"},{"issue":"2","key":"10_CR8","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/s00145-002-0204-y","volume":"17","author":"E. Fujisaki","year":"2004","unstructured":"Fujisaki, E., Okamoto, T., Pointcheval, D., Stern, J.: RSA-OAEP is secure under the RSA assumption. Journal of Cryptology\u00a017(2), 81\u2013104 (2004)","journal-title":"Journal of Cryptology"},{"issue":"1","key":"10_CR9","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1016\/j.tcs.2005.08.005","volume":"346","author":"J. Hurd","year":"2005","unstructured":"Hurd, J., McIver, A., Morgan, C.: Probabilistic guarded commands mechanized in HOL. Theor. Comput. Sci.\u00a0346(1), 96\u2013112 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"10_CR10","first-page":"44","volume-title":"Proceedings of the 21st Annual ACM Symposium on Theory of Computing","author":"R. Impagliazzo","year":"1989","unstructured":"Impagliazzo, R., Rudich, S.: Limits on the provable consequences of one-way permutations. In: Proceedings of the 21st Annual ACM Symposium on Theory of Computing, pp. 44\u201361. ACM Press, New York (1989)"},{"key":"10_CR11","first-page":"42","volume-title":"Proceedings of the 33rd ACM Symposium Principles of Programming Languages","author":"X. Leroy","year":"2006","unstructured":"Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: Proceedings of the 33rd ACM Symposium Principles of Programming Languages, pp. 42\u201354. ACM Press, New York (2006)"},{"key":"10_CR12","volume-title":"Abstraction, Refinement, and Proof for Probabilistic Systems","author":"A. McIver","year":"2005","unstructured":"McIver, A., Morgan, C.: Abstraction, Refinement, and Proof for Probabilistic Systems. Springer, Heidelberg (2005)"},{"key":"10_CR13","unstructured":"Shoup, V.: Sequences of games: a tool for taming complexity in security proofs. Cryptology ePrint Archive, Report 2004\/332 (2004), \n                    \n                      http:\/\/eprint.iacr.org\/2004\/332"},{"key":"10_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1007\/3-540-39200-9_28","volume-title":"Advances in Cryptology \u2013 EUROCRPYT 2003","author":"J. Stern","year":"2003","unstructured":"Stern, J.: Why provable security matters? In: Biham, E. (ed.) EUROCRYPT 2003. LNCS, vol.\u00a02656, pp. 449\u2013461. Springer, Heidelberg (2003)"},{"key":"10_CR15","unstructured":"The Coq development team: The Coq Proof Assistant Reference Manual Version 8.2 (2009), \n                    \n                      http:\/\/coq.inria.fr"},{"key":"10_CR16","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1145\/1542476.1542512","volume-title":"Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation","author":"J.B. Tristan","year":"2009","unstructured":"Tristan, J.B., Leroy, X.: Verified validation of lazy code motion. In: Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 316\u2013326. ACM Press, New York (2009)"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14052-5_10.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T12:17:18Z","timestamp":1619785038000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14052-5_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642140518","9783642140525"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14052-5_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}