{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,7]],"date-time":"2025-12-07T11:26:17Z","timestamp":1765106777333,"version":"3.46.0"},"publisher-location":"Singapore","reference-count":25,"publisher":"Springer Nature Singapore","isbn-type":[{"value":"9789819550951","type":"print"},{"value":"9789819550968","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,12,8]],"date-time":"2025-12-08T00:00:00Z","timestamp":1765152000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,12,8]],"date-time":"2025-12-08T00:00:00Z","timestamp":1765152000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-981-95-5096-8_5","type":"book-chapter","created":{"date-parts":[[2025,12,7]],"date-time":"2025-12-07T11:24:24Z","timestamp":1765106664000},"page":"137-167","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["How Hard can it be to\u00a0Formalize a\u00a0Proof?"],"prefix":"10.1007","author":[{"given":"Fran\u00e7ois","family":"Dupressoir","sequence":"first","affiliation":[]},{"given":"Andreas","family":"H\u00fclsing","sequence":"additional","affiliation":[]},{"given":"Cameron","family":"Low","sequence":"additional","affiliation":[]},{"given":"Matthias","family":"Meijers","sequence":"additional","affiliation":[]},{"given":"Charlotte","family":"Mylog","sequence":"additional","affiliation":[]},{"given":"Sabine","family":"Oechsner","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,12,8]]},"reference":[{"key":"5_CR1","unstructured":"CryptoVerif: cryptographic protocol verifier in the computational model. https:\/\/bblanche.gitlabpages.inria.fr\/CryptoVerif\/"},{"key":"5_CR2","unstructured":"Easycrypt. https:\/\/easycrypt.info"},{"key":"5_CR3","unstructured":"Squirrel prover. https:\/\/squirrel-prover.github.io\/"},{"key":"5_CR4","unstructured":"SSProve. https:\/\/github.com\/SSProve\/ssprove"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Abate, C., et al.: SSProve: a foundational framework for modular cryptographic proofs in COQ. In: K\u00fcsters, R., Naumann, D., eds, CSF 2021 Computer Security Foundations Symposium, pp. 1\u201315. IEEE Computer Society Press (2021)","DOI":"10.1109\/CSF51468.2021.00048"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"Baelde, D., Delaune, S., Jacomme, C., Koutsos, A., Moreau, S.: An interactive prover for protocol verification in the computational model. In: 2021 IEEE Symposium on Security and Privacy, pp. 537\u2013554. IEEE Computer Society Press (2021)","DOI":"10.1109\/SP40001.2021.00078"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"Barbosa, M., et al.: SoK: computer-aided cryptography. In: 2021 IEEE Symposium on Security and Privacy, pp. 777\u2013795. IEEE Computer Society Press (2021)","DOI":"10.1109\/SP40001.2021.00008"},{"key":"5_CR8","doi-asserted-by":"publisher","unstructured":"Barthe, G., Dupressoir, F., Gr\u00e9goire, B., Kunz, C., Schmidt, B., Strub, P.-Y.: Easycrypt: a tutorial. In: Aldini, A., L\u00f3pez, J., Martinelli, F., eds., Foundations of Security Analysis and Design VII - FOSAD 2012\/2013 Tutorial Lectures, volume 8604 of Lecture Notes in Computer Science, pp. 146\u2013166. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-319-10082-1_6","DOI":"10.1007\/978-3-319-10082-1_6"},{"key":"5_CR9","doi-asserted-by":"publisher","unstructured":"Barthe, G., Gr\u00e9goire, B., Heraud, S., B\u00e9guelin, S.Z.: Computer-aided security proofs for the working cryptographer. In: Rogaway, P. (ed.) CRYPTO 2011. LNCS, vol. 6841, pp. 71\u201390. Springer, Berlin, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22792-9_5","DOI":"10.1007\/978-3-642-22792-9_5"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Bellare, M., Ng, R., Tackmann, B.: Nonces are noticed: AEAD revisited. In: Boldyreva, A., Micciancio, D. (eds.) CRYPTO 2019. Part I, volume 11692 of LNCS, pp. 235\u2013265. Springer, Cham (2019)","DOI":"10.1007\/978-3-030-26948-7_9"},{"key":"5_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. 4004, pp. 409\u2013426. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11761679_25"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/11745853_14","volume-title":"Public Key Cryptography - PKC 2006","author":"DJ Bernstein","year":"2006","unstructured":"Bernstein, D.J.: Curve25519: new Diffie-Hellman speed records. In: Yung, M., Dodis, Y., Kiayias, A., Malkin, T. (eds.) PKC 2006. LNCS, vol. 3958, pp. 207\u2013228. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11745853_14"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"Bhargavan, K., Fournet, C., Kohlweiss, M., Pironti, A., Strub, P.-Y.: Implementing TLS with verified cryptographic security. In: 2013 IEEE Symposium on Security and Privacy, pp. 445\u2013459. IEEE Computer Society Press (2013)","DOI":"10.1109\/SP.2013.37"},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: A computationally sound mechanized prover for security protocols. In: 2006 IEEE Symposium on Security and Privacy, pp. 140\u2013154. IEEE Computer Society Press (2006)","DOI":"10.1109\/SP.2006.1"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"Brzuska, C., Cornelissen, E., Kohbrok, K.: Security analysis of the MLS key derivation. In: 2022 IEEE Symposium on Security and Privacy, pp. 2535\u20132553. IEEE Computer Society Press (2022)","DOI":"10.1109\/SP46214.2022.9833678"},{"key":"5_CR16","doi-asserted-by":"publisher","unstructured":"Brzuska, C., Delignat-Lavaud, A., Egger, C., Fournet, C., Kohbrok, K., Kohlweiss, M.: Key-schedule security for the TLS 1.3 standard. In: Agrawal, S., Lin, D. (eds.) ASIACRYPT 2022. Part I, volume 13791 of LNCS, pp. 621\u2013650. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-22963-3_21","DOI":"10.1007\/978-3-031-22963-3_21"},{"key":"5_CR17","doi-asserted-by":"publisher","unstructured":"Brzuska, C., Delignat-Lavaud, A., Fournet, C., Kohbrok, K., Kohlweiss, M.: State separation for code-based game-playing proofs. In: Peyrin, T., Galbraith, S. (eds.) ASIACRYPT 2018. Part III, volume 11274 of LNCS, pp. 222\u2013249. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03332-3_9","DOI":"10.1007\/978-3-030-03332-3_9"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"Brzuska, C., Oechsner, S.: A state-separating proof for Yao\u2019s garbling scheme. In: CSF 2023 Computer Security Foundations Symposium, pp. 137\u2013152. IEEE Computer Society Press (2023)","DOI":"10.1109\/CSF57540.2023.00009"},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"Canetti, R., Stoughton, A., Varia, M.: EasyUC: using EasyCrypt to mechanize proofs of universally composable security. In: Delaune, S., Jia, L., eds., CSF 2019 Computer Security Foundations Symposium, pp. 167\u2013183. IEEE Computer Society Press (2019)","DOI":"10.1109\/CSF.2019.00019"},{"issue":"6","key":"5_CR20","doi-asserted-by":"publisher","first-page":"644","DOI":"10.1109\/TIT.1976.1055638","volume":"22","author":"W Diffie","year":"1976","unstructured":"Diffie, W., Hellman, M.E.: New directions in cryptography. IEEE Trans. Inf. Theory 22(6), 644\u2013654 (1976)","journal-title":"IEEE Trans. Inf. Theory"},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"Dolev, D., Yao, A.C.-C.: On the security of public key protocols. IEEE Trans. Inf. Theory 29(2), 198\u2013207 (1983)","DOI":"10.1109\/TIT.1983.1056650"},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"Dupressoir, F., Kohbrok, K., Oechsner, S.: Bringing state-separating proofs to EasyCrypt a security proof for CryptoBox. In: CSF 2022 Computer Security Foundations Symposium, pp. 227\u2013242. IEEE Computer Society Press (2022)","DOI":"10.1109\/CSF54842.2022.9919671"},{"key":"5_CR23","unstructured":"Dupressoir, F., H\u00fclsing, A., Low, C., Meijers, M., Mylog, C., Oechsner, S.: How hard can it be to formalize a proof? Lessons from formalizing CryptoBox three times in EasyCrypt. Cryptology ePrint Archive, Paper 2025\/1569 (2025)"},{"key":"5_CR24","unstructured":"Freire, E.S.V., Hofheinz, D., Kiltz, E., Paterson, K.G.: Non-interactive key exchange. Cryptology ePrint Archive, Report 2012\/732 (2012)"},{"key":"5_CR25","unstructured":"Shoup, V.: Sequences of games: a tool for taming complexity in security proofs. Cryptology ePrint Archive, Report 2004\/332 (2004)"}],"container-title":["Lecture Notes in Computer Science","Advances in Cryptology \u2013 ASIACRYPT 2025"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-95-5096-8_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,7]],"date-time":"2025-12-07T11:24:27Z","timestamp":1765106667000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-95-5096-8_5"}},"subtitle":["Lessons from Formalizing CryptoBox Three Times in EasyCrypt"],"short-title":[],"issued":{"date-parts":[[2025,12,8]]},"ISBN":["9789819550951","9789819550968"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-981-95-5096-8_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,12,8]]},"assertion":[{"value":"8 December 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ASIACRYPT","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on the Theory and Application of Cryptology and Information Security","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Melbourne, VIC","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Australia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 December 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 December 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"asiacrypt2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/asiacrypt.iacr.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}