{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T14:53:11Z","timestamp":1725893591573},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540756699"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-75670-5_10","type":"book-chapter","created":{"date-parts":[[2007,10,5]],"date-time":"2007-10-05T03:13:20Z","timestamp":1191554000000},"page":"151-168","source":"Crossref","is-referenced-by-count":11,"title":["Formal Proof of Provable Security by Game-Playing in a Proof Assistant"],"prefix":"10.1007","author":[{"given":"Reynald","family":"Affeldt","sequence":"first","affiliation":[]},{"given":"Miki","family":"Tanaka","sequence":"additional","affiliation":[]},{"given":"Nicolas","family":"Marti","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"10_CR1","unstructured":"The LogiCal Project, INRIA. The Coq proof assistant, http:\/\/coq.inria.fr"},{"key":"10_CR2","volume-title":"Type Theory and Functional Programming","author":"S. Thompson","year":"1991","unstructured":"Thompson, S.: Type Theory and Functional Programming. Addison-Wesley, Reading (1991)"},{"key":"10_CR3","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/3054.001.0001","volume-title":"The Formal Semantics of Programming Languages","author":"G. Winskel","year":"1993","unstructured":"Winskel, G.: The Formal Semantics of Programming Languages. MIT Press, Cambridge (1993)"},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"Bellare, M., Rogaway, P.: Random Oracle are Practical: A Paradigm for Designing Efficient Protocols. In: CCS 1993. 1st ACM Conference on Computer and Communications Security, pp. 62\u201373. ACM Press, New York","DOI":"10.1145\/168588.168596"},{"key":"10_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/3-540-68339-9_34","volume-title":"Advances in Cryptology - EUROCRYPT 1996","author":"M. Bellare","year":"1996","unstructured":"Bellare, M., Rogaway, P.: The Exact Security of Digital Signatures\u2014How to Sign with RSA and Rabin. In: Maurer, U.M. (ed.) EUROCRYPT 1996. LNCS, vol.\u00a01070, pp. 399\u2013416. Springer, Heidelberg (1996)"},{"key":"10_CR6","unstructured":"Shoup, V.: Sequence of Games: A Tool for Taming Complexity in Security Proofs. Manuscript (2004) (Revised 2006), available at http:\/\/www.shoup.net\/papers\/games.pdf"},{"key":"10_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.: Code-Based Game-Playing Proofs and the Security of Triple Encryption. In: Vaudenay, S. (ed.) EUROCRYPT 2006. LNCS, vol.\u00a04004, pp. 409\u2013426. Springer, Heidelberg (2006)"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Pointcheval, D.: Provable Security for Public Key Schemes. In: Contemporary Cryptology, Advanced Courses in Mathematics CRM Barcelona, pp. 133\u2013189. Birkh\u00e4user Publishers (2005)","DOI":"10.1007\/3-7643-7394-6_4"},{"key":"10_CR9","unstructured":"Halevi, S.: A plausible approach to computer-aided cryptographic proofs. Cryptology ePrint Archive: Report (2005)\/181"},{"key":"10_CR10","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)"},{"key":"10_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"400","DOI":"10.1007\/11901433_22","volume-title":"Formal Methods and Software Engineering","author":"N. Marti","year":"2006","unstructured":"Marti, N., Affeldt, R., Yonezawa, A.: Formal Verification of the Heap Manager of an Operating System using Separation Logic. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol.\u00a04260, pp. 400\u2013419. Springer, Heidelberg (2006)"},{"key":"10_CR12","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":"10_CR13","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":"10_CR14","doi-asserted-by":"crossref","unstructured":"Affeldt, R., Marti, N.: An Approach to Formal Verification of Arithmetic Functions in Assembly. In: 11th Annual Asian Computing Science Conference (ASIAN 2006), Focusing on Secure Software and Related Issues, Lecture Notes in Computer Science. Springer, Heidelberg (to appear, 2007)","DOI":"10.1007\/978-3-540-77505-8_27"},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"Nowak, D.: A Framework for Game-Based Security Proofs. Cryptology ePrint Archive: Report (2007)\/199","DOI":"10.1007\/978-3-540-77048-0_25"},{"key":"10_CR16","unstructured":"Affeldt, R., Tanaka, M., Marti, N.: Formal Proof of Provable Security by Game-playing in a Proof Assistant. Coq scripts, available at http:\/\/staff.aist.go.jp\/reynald.affeldt\/secprf\/provsec2007"}],"container-title":["Lecture Notes in Computer Science","Provable Security"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-75670-5_10.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T00:27:04Z","timestamp":1605745624000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-75670-5_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540756699"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-75670-5_10","relation":{},"subject":[]}}