{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T17:03:32Z","timestamp":1742922212349,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642014642"},{"type":"electronic","value":"9783642014659"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-01465-9_1","type":"book-chapter","created":{"date-parts":[[2009,4,4]],"date-time":"2009-04-04T00:56:06Z","timestamp":1238806566000},"page":"1-19","source":"Crossref","is-referenced-by-count":5,"title":["Formal Certification of ElGamal Encryption"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[]},{"given":"Benjamin","family":"Gr\u00e9goire","sequence":"additional","affiliation":[]},{"given":"Sylvain","family":"Heraud","sequence":"additional","affiliation":[]},{"given":"Santiago","family":"Zanella B\u00e9guelin","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"1_CR1","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. ACM Press, New York (2009)"},{"issue":"2","key":"1_CR2","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. J. Comput. Syst. Sci.\u00a028(2), 270\u2013299 (1984)","journal-title":"J. Comput. Syst. Sci."},{"key":"1_CR3","series-title":"Lecture Notes in Computer Science","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. Springer, Heidelberg (2003)"},{"key":"1_CR4","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":"1_CR5","unstructured":"Halevi, S.: A plausible approach to computer-aided cryptographic proofs. Cryptology ePrint Archive, Report 2005\/181 (2005)"},{"key":"1_CR6","unstructured":"Shoup, V.: Sequences of games: a tool for taming complexity in security proofs. Cryptology ePrint Archive, Report 2004\/332 (2004)"},{"key":"1_CR7","unstructured":"The Coq development team: The Coq Proof Assistant Reference Manual v8.2 (2008), \n                  \n                    http:\/\/coq.inria.fr"},{"issue":"1","key":"1_CR8","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1023\/A:1011553200337","volume":"14","author":"A. Sabelfeld","year":"2001","unstructured":"Sabelfeld, A., Sands, D.: A per model of secure information flow in sequential programs. Higher-Order and Symbolic Computation\u00a014(1), 59\u201391 (2001)","journal-title":"Higher-Order and Symbolic Computation"},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"Audebaud, P., Paulin-Mohring, C.: Proofs of randomized algorithms in Coq. Science of Computer Programming (2008)","DOI":"10.1016\/j.scico.2007.09.002"},{"key":"1_CR10","first-page":"14","volume-title":"Proceedings of the 31th ACM Symposium on Principles of Programming Languages","author":"N. Benton","year":"2004","unstructured":"Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: Proceedings of the 31th ACM Symposium on Principles of Programming Languages, pp. 14\u201325. ACM Press, New York (2004)"},{"key":"1_CR11","doi-asserted-by":"publisher","first-page":"685","DOI":"10.1016\/B978-044482830-9\/50029-1","volume-title":"Handbook of Process Algebra","author":"B. Jonsson","year":"2001","unstructured":"Jonsson, B., Larsen, K.G., Yi, W.: Probabilistic extensions of process algebras. In: Handbook of Process Algebra, pp. 685\u2013711. Elsevier, Amsterdam (2001)"},{"key":"1_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/978-3-540-77048-0_25","volume-title":"Information and Communications Security","author":"D. Nowak","year":"2007","unstructured":"Nowak, D.: A framework for game-based security proofs. In: Qing, S., Imai, H., Wang, G. (eds.) ICICS 2007. LNCS, vol.\u00a04861, pp. 319\u2013333. Springer, Heidelberg (2007)"},{"key":"1_CR13","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":"1_CR14","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)"}],"container-title":["Lecture Notes in Computer Science","Formal Aspects in Security and Trust"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-01465-9_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,9]],"date-time":"2020-01-09T00:34:48Z","timestamp":1578530088000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-01465-9_1"}},"subtitle":["A Gentle Introduction to CertiCrypt"],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642014642","9783642014659"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-01465-9_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}