{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,27]],"date-time":"2025-07-27T07:15:21Z","timestamp":1753600521433},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642323461"},{"type":"electronic","value":"9783642323478"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-32347-8_2","type":"book-chapter","created":{"date-parts":[[2012,8,10]],"date-time":"2012-08-10T07:33:54Z","timestamp":1344584034000},"page":"11-27","source":"Crossref","is-referenced-by-count":6,"title":["Computer-Aided Cryptographic Proofs"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[]},{"given":"Juan Manuel","family":"Crespo","sequence":"additional","affiliation":[]},{"given":"Benjamin","family":"Gr\u00e9goire","sequence":"additional","affiliation":[]},{"given":"C\u00e9sar","family":"Kunz","sequence":"additional","affiliation":[]},{"given":"Santiago","family":"Zanella B\u00e9guelin","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"8","key":"2_CR1","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. Sci. Comput. Program.\u00a074(8), 568\u2013589 (2009)","journal-title":"Sci. Comput. Program."},{"doi-asserted-by":"crossref","unstructured":"Backes, M., Barthe, G., Berg, M., Gr\u00e9goire, B., Kunz, C., Skoruppa, M., Zanella B\u00e9guelin, S.: Verified security of Merkle-Damg\u00e5rd. In: 25rd IEEE Computer Security Foundations Symposium, CSF 2012. IEEE Computer Society (2012)","key":"2_CR2","DOI":"10.1109\/CSF.2012.14"},{"key":"2_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-642-28641-4_12","volume-title":"Principles of Security and Trust","author":"G. Barthe","year":"2012","unstructured":"Barthe, G., Gr\u00e9goire, B., Heraud, S., Olmedo, F., Zanella B\u00e9guelin, S.: Verified Indifferentiable Hashing into Elliptic Curves. In: Degano, P., Guttman, J.D. (eds.) POST 2012. LNCS, vol.\u00a07215, pp. 209\u2013228. Springer, Heidelberg (2012)"},{"key":"2_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1007\/978-3-642-22792-9_5","volume-title":"Advances in Cryptology \u2013 CRYPTO 2011","author":"G. Barthe","year":"2011","unstructured":"Barthe, G., Gr\u00e9goire, B., Heraud, S., Zanella B\u00e9guelin, S.: Computer-Aided Security Proofs for the Working Cryptographer. In: Rogaway, P. (ed.) CRYPTO 2011. LNCS, vol.\u00a06841, pp. 71\u201390. Springer, Heidelberg (2011)"},{"key":"2_CR5","first-page":"90","volume-title":"36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009","author":"G. Barthe","year":"2009","unstructured":"Barthe, G., Gr\u00e9goire, B., Zanella B\u00e9guelin, S.: Formal certification of code-based cryptographic proofs. In: 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, pp. 90\u2013101. ACM, New York (2009)"},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","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, pp. 221\u2013231. Springer, Heidelberg (1998)"},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"Advances in Cryptology - CRYPTO \u201996","author":"M. Bellare","year":"1996","unstructured":"Bellare, M., Canetti, R., Krawczyk, H.: Keying Hash Functions for Message Authentication. In: Koblitz, N. (ed.) CRYPTO 1996. LNCS, vol.\u00a01109, pp. 1\u201315. Springer, Heidelberg (1996)"},{"key":"2_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1007\/3-540-48658-5_32","volume-title":"Advances in Cryptology - CRYPTO \u201994","author":"M. Bellare","year":"1994","unstructured":"Bellare, M., Kilian, J., Rogaway, P.: The Security of Cipher Block Chaining. In: Desmedt, Y.G. (ed.) CRYPTO 1994. LNCS, vol.\u00a0839, pp. 341\u2013358. Springer, Heidelberg (1994)"},{"key":"2_CR9","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1145\/168588.168596","volume-title":"1st ACM Conference on Computer and Communications Security, CCS 1993","author":"M. Bellare","year":"1993","unstructured":"Bellare, M., Rogaway, P.: Random oracles are practical: a paradigm for designing efficient protocols. In: 1st ACM Conference on Computer and Communications Security, CCS 1993, pp. 62\u201373. ACM, New York (1993)"},{"key":"2_CR10","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":"2_CR11","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\u00a0for\u00a0Code-Based\u00a0Game-Playing\u00a0Proofs. In: Vaudenay, S. (ed.) EUROCRYPT 2006. LNCS, vol.\u00a04004, pp. 409\u2013426. Springer, Heidelberg (2006)"},{"key":"2_CR12","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 #1. In: Krawczyk, H. (ed.) CRYPTO 1998. LNCS, vol.\u00a01462, pp. 1\u201312. Springer, Heidelberg (1998)"},{"issue":"3","key":"2_CR13","doi-asserted-by":"publisher","first-page":"586","DOI":"10.1137\/S0097539701398521","volume":"32","author":"D. Boneh","year":"2003","unstructured":"Boneh, D., Franklin, M.: Identity-based encryption from the Weil pairing. SIAM J. Comput.\u00a032(3), 586\u2013615 (2003)","journal-title":"SIAM J. Comput."},{"issue":"4","key":"2_CR14","doi-asserted-by":"publisher","first-page":"557","DOI":"10.1145\/1008731.1008734","volume":"51","author":"R. Canetti","year":"2004","unstructured":"Canetti, R., Goldreich, O., Halevi, S.: The random oracle methodology, revisited. J. ACM\u00a051(4), 557\u2013594 (2004)","journal-title":"J. ACM"},{"issue":"2","key":"2_CR15","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/j.entcs.2008.04.080","volume":"198","author":"S. Conchon","year":"2008","unstructured":"Conchon, S., Contejean, E., Kanig, J., Lescuyer, S.: CC(X): Semantic combination of congruence closure with solvable theories. Electronic Notes in Theoretical Computer Science\u00a0198(2), 51\u201369 (2008)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-540-73420-8_2","volume-title":"Automata, Languages and Programming","author":"I. Damg\u00e5rd","year":"2007","unstructured":"Damg\u00e5rd, I.: A \u201cproof-reading\u201d of Some Issues in Cryptography. In: Arge, L., Cachin, C., Jurdzi\u0144ski, T., Tarlecki, A. (eds.) ICALP 2007. LNCS, vol.\u00a04596, pp. 2\u201311. Springer, Heidelberg (2007)"},{"unstructured":"Deng, Y., Du, W.: Logical, metric, and algorithmic characterisations of probabilistic bisimulation. Technical Report CMU-CS-11-110, Carnegie Mellon University (March 2011)","key":"2_CR17"},{"issue":"1849","key":"2_CR18","doi-asserted-by":"publisher","first-page":"3215","DOI":"10.1098\/rsta.2006.1895","volume":"364","author":"A.W. Dent","year":"2006","unstructured":"Dent, A.W.: Fundamental problems in provable security and cryptography. Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences\u00a0364(1849), 3215\u20133230 (2006)","journal-title":"Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences"},{"key":"2_CR19","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1109\/FOCS.2008.56","volume-title":"49th Annual IEEE Symposium on Foundations of Computer Science, FOCS 2008","author":"S. Dziembowski","year":"2008","unstructured":"Dziembowski, S., Pietrzak, K.: Leakage-resilient cryptography. In: 49th Annual IEEE Symposium on Foundations of Computer Science, FOCS 2008, pp. 293\u2013302. IEEE Computer Society, Washington (2008)"},{"issue":"2","key":"2_CR20","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."},{"unstructured":"Halevi, S.: A plausible approach to computer-aided cryptographic proofs. Cryptology ePrint Archive, Report 2005\/181 (2005)","key":"2_CR21"},{"issue":"11","key":"2_CR22","first-page":"1395","volume":"55","author":"J. Harrison","year":"2008","unstructured":"Harrison, J.: Formal proof \u2013 theory and practice. Notices of the American Mathematical Society\u00a055(11), 1395\u20131406 (2008)","journal-title":"Notices of the American Mathematical Society"},{"key":"2_CR23","doi-asserted-by":"crossref","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., Yi, W., Larsen, K.G.: Probabilistic extensions of process algebras. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, pp. 685\u2013710. Elsevier, Amsterdam (2001)"},{"key":"2_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"104","DOI":"10.1007\/3-540-68697-5_9","volume-title":"Advances in Cryptology - CRYPTO \u201996","author":"P.C. Kocher","year":"1996","unstructured":"Kocher, P.C.: Timing Attacks on Implementations of Diffie-Hellman, RSA, DSS, and Other Systems. In: Koblitz, N. (ed.) CRYPTO 1996. LNCS, vol.\u00a01109, pp. 104\u2013113. Springer, Heidelberg (1996)"},{"key":"2_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"388","DOI":"10.1007\/3-540-48405-1_25","volume-title":"Advances in Cryptology - CRYPTO \u201999","author":"P.C. Kocher","year":"1999","unstructured":"Kocher, P.C., Jaffe, J., Jun, B.: Differential Power Analysis. In: Wiener, M. (ed.) CRYPTO 1999. LNCS, vol.\u00a01666, pp. 388\u2013397. Springer, Heidelberg (1999)"},{"key":"2_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/3-540-44647-8_14","volume-title":"Advances in Cryptology - CRYPTO 2001","author":"J. Manger","year":"2001","unstructured":"Manger, J.: A Chosen Ciphertext Attack on RSA Optimal Asymmetric Encryption Padding (OAEP) as Standardized in PKCS #1 v2.0. In: Kilian, J. (ed.) CRYPTO 2001. LNCS, vol.\u00a02139, pp. 230\u2013238. Springer, Heidelberg (2001)"},{"key":"2_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-540-24638-1_2","volume-title":"Theory of Cryptography","author":"U. Maurer","year":"2004","unstructured":"Maurer, U., Renner, R., Holenstein, C.: Indifferentiability, Impossibility Results on Reductions, and Applications to the Random Oracle Methodology. In: Naor, M. (ed.) TCC 2004. LNCS, vol.\u00a02951, pp. 21\u201339. Springer, Heidelberg (2004)"},{"doi-asserted-by":"crossref","unstructured":"Pollack, R.: How to believe a machine-checked proof. In: Twenty-Five Years of Constructive Type Theory: Proceedings of a Congress Held in Venice, October 1995. Oxford Logic Guides, vol.\u00a036. Oxford University Press (1998)","key":"2_CR28","DOI":"10.1093\/oso\/9780198501275.003.0013"},{"key":"2_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"487","DOI":"10.1007\/978-3-642-20465-4_27","volume-title":"Advances in Cryptology \u2013 EUROCRYPT 2011","author":"T. Ristenpart","year":"2011","unstructured":"Ristenpart, T., Shacham, H., Shrimpton, T.: Careful with Composition: Limitations of the Indifferentiability Framework. In: Paterson, K.G. (ed.) EUROCRYPT 2011. LNCS, vol.\u00a06632, pp. 487\u2013506. Springer, Heidelberg (2011)"},{"unstructured":"Rogaway, P.: Practice-oriented provable security and the social construction of cryptography (2009) (unpublished essay)","key":"2_CR30"},{"key":"2_CR31","doi-asserted-by":"crossref","first-page":"656","DOI":"10.1002\/j.1538-7305.1949.tb00928.x","volume":"28","author":"C. Shannon","year":"1949","unstructured":"Shannon, C.: Communication theory of secrecy systems. Bell System Technical Journal\u00a028, 656\u2013715 (1949)","journal-title":"Bell System Technical Journal"},{"unstructured":"Shoup, V.: Sequences of games: a tool for taming complexity in security proofs. Cryptology ePrint Archive, Report 2004\/332 (2004)","key":"2_CR32"},{"key":"2_CR33","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1109\/SP.2009.17","volume-title":"30th IEEE Symposium on Security and Privacy, S&P 2009","author":"S. Zanella B\u00e9guelin","year":"2009","unstructured":"Zanella B\u00e9guelin, S., Gr\u00e9goire, B., Barthe, G., Olmedo, F.: Formally certifying the security of digital signature schemes. In: 30th IEEE Symposium on Security and Privacy, S&P 2009, pp. 237\u2013250. IEEE Computer Society, Los Alamitos (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-32347-8_2.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,25]],"date-time":"2022-01-25T23:37:22Z","timestamp":1643153842000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-32347-8_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642323461","9783642323478"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-32347-8_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}