{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,27]],"date-time":"2026-05-27T03:02:28Z","timestamp":1779850948481,"version":"3.53.1"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032078902","type":"print"},{"value":"9783032078919","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,10,17]],"date-time":"2025-10-17T00:00:00Z","timestamp":1760659200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,10,17]],"date-time":"2025-10-17T00:00:00Z","timestamp":1760659200000},"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-3-032-07891-9_16","type":"book-chapter","created":{"date-parts":[[2025,10,17]],"date-time":"2025-10-17T09:28:03Z","timestamp":1760693283000},"page":"303-320","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Formalisation of\u00a0the\u00a0KZG Polynomial Commitment Schemes in\u00a0EasyCrypt"],"prefix":"10.1007","author":[{"family":"Palak","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thomas","family":"Haines","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,10,17]]},"reference":[{"key":"16_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-319-10082-1_6","volume-title":"Foundations of Security Analysis and Design VII","author":"G Barthe","year":"2014","unstructured":"Barthe, G., Dupressoir, F., Gr\u00e9goire, B., Kunz, C., Schmidt, B., Strub, P.-Y.: EasyCrypt: a tutorial. In: Aldini, A., Lopez, J., Martinelli, F. (eds.) FOSAD 2012-2013. LNCS, vol. 8604, pp. 146\u2013166. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10082-1_6"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"Haines, T., Gor\u00e9, R., Sharma, B.: Did you mix me? Formally verifying verifiable mix nets in electronic voting. In: SP, pp. 1748\u20131765. IEEE (2021)","DOI":"10.1109\/SP40001.2021.00033"},{"issue":"3","key":"16_CR3","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1109\/MSEC.2022.3154689","volume":"20","author":"DA Basin","year":"2022","unstructured":"Basin, D.A., Cremers, C., Dreier, J., Sasse, R.: Tamarin: verification of large-scale, real-world, cryptographic protocols. IEEE Secur. Priv. 20(3), 24\u201332 (2022)","journal-title":"IEEE Secur. Priv."},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Sprenger, C., Backes, M., Basin, D.A., Pfitzmann, B., Waidner, M.: Cryptographically sound theorem proving. In: CSFW, pp. 153\u2013166. IEEE Computer Society (2006)","DOI":"10.1109\/CSFW.2006.10"},{"key":"16_CR5","unstructured":"Baritel-Ruet, C.: Formal security proofs of cryptographic: a necessity achieved using easycrypt, Ph.D. dissertation, Universit\u00e9 c\u00f4te d\u2019azur (2020)"},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"Almeida, J.B., et al.: Machine-checked proofs for cryptographic standards: in differentiability of sponge and secure high-assurance implementations of SHA-3. In: CCS, pp. 1607\u20131622. ACM (2019)","DOI":"10.1145\/3319535.3363211"},{"key":"16_CR7","unstructured":"Bosshard, A.G., Bootle, J., Sprenger, C.: Formal verification of the sum check protocol. CoRR, vol. abs\/2402.06093 (2024)"},{"key":"16_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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., 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, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22792-9_5"},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"Nowak, D.: On formal verification of arithmetic-based cryptographic primitives. CoRR, vol. abs\/0904.1110 (2009)","DOI":"10.1007\/978-3-642-00730-9_23"},{"key":"16_CR10","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. 4117, pp. 537\u2013554. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11818175_32"},{"key":"16_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/978-3-642-17373-8_11","volume-title":"Advances in Cryptology - ASIACRYPT 2010","author":"A Kate","year":"2010","unstructured":"Kate, A., Zaverucha, G.M., Goldberg, I.: Constant-size commitments to polynomials and their applications. In: Abe, M. (ed.) ASIACRYPT 2010. LNCS, vol. 6477, pp. 177\u2013194. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17373-8_11"},{"key":"16_CR12","unstructured":"Rothmann, T., Kreuzer, K.: Formal verification of the kate-zaverucha-goldberg polynomial commitment scheme (2024)"},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"Maller, M., Bowe, S., Kohlweiss, M., Meiklejohn, S.: Sonic: zero-knowledge snarks from linear-size universal and updatable structured reference strings. In: CCS, pp. 2111\u20132128. ACM (2019)","DOI":"10.1145\/3319535.3339817"},{"key":"16_CR14","unstructured":"Gabizon, A.: Improved prover efficiency and SRS size in a sonic-like system. IACR Cryptol. ePrint Arch., 601 (2019)"},{"key":"16_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"738","DOI":"10.1007\/978-3-030-45721-1_26","volume-title":"Advances in Cryptology \u2013 EUROCRYPT 2020","author":"A Chiesa","year":"2020","unstructured":"Chiesa, A., Hu, Y., Maller, M., Mishra, P., Vesely, N., Ward, N.: Marlin: preprocessing zkSNARKs with universal and updatable SRS. In: Canteaut, A., Ishai, Y. (eds.) EUROCRYPT 2020. LNCS, vol. 12105, pp. 738\u2013768. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45721-1_26"},{"key":"16_CR16","unstructured":"Gabizon, A., Williamson, Z.J., Ciobotaru, O.: PLONK: permutations over lagrange-bases for oecumenical noninteractive arguments of knowledge. IACR Cryptol. ePrint Arch., 953 (2019)"},{"key":"16_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/978-3-319-65127-9_22","volume-title":"Computer Network Security","author":"R Metere","year":"2017","unstructured":"Metere, R., Dong, C.: Automated cryptographic analysis of the Pedersen commitment scheme. In: Rak, J., Bay, J., Kotenko, I., Popyack, L., Skormin, V., Szczypiorski, K. (eds.) MMM-ACNS 2017. LNCS, vol. 10446, pp. 275\u2013287. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-65127-9_22"},{"issue":"4","key":"16_CR18","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1007\/s10817-020-09581-w","volume":"65","author":"D Butler","year":"2021","unstructured":"Butler, D., Lochbihler, A., Aspinall, D., Gasc\u00f3n, A.: Formalising $$\\varsigma $$-protocols and commitment schemes using crypthol. J. Autom. Reason. 65(4), 521\u2013567 (2021)","journal-title":"J. Autom. Reason."},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"Barthe, G., Hedin, D., B\u00e9guelin, S.Z., Gr\u00e9goire, B., Heraud, S.: A machine-checked formalization of sigma-protocols. In: CSF, pp. 246\u2013260. IEEE Computer Society (2010)","DOI":"10.1109\/CSF.2010.24"},{"key":"16_CR20","doi-asserted-by":"crossref","unstructured":"Avigad, J., Goldberg, L., Levit, D., Seginer, Y., Titelman, A.: A verified algebraic representation of Cairo program execution. In: CPP, pp. 153\u2013165. ACM (2022)","DOI":"10.1145\/3497775.3503675"},{"key":"16_CR21","unstructured":"Bailey, B., Miller, A.: Formalizing soundness proofs of linear PCP snarks. In: USENIX Security Symposium. USENIX Association (2024)"},{"key":"16_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/978-3-662-49896-5_11","volume-title":"Advances in Cryptology \u2013 EUROCRYPT 2016","author":"J Groth","year":"2016","unstructured":"Groth, J.: On the size of pairing-based non-interactive arguments. In: Fischlin, M., Coron, J.-S. (eds.) EUROCRYPT 2016. LNCS, vol. 9666, pp. 305\u2013326. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49896-5_11"},{"issue":"2","key":"16_CR23","doi-asserted-by":"publisher","first-page":"494","DOI":"10.1007\/s00145-019-09341-z","volume":"33","author":"DA Basin","year":"2020","unstructured":"Basin, D.A., Lochbihler, A., Sefidgar, S.R.: CryptHOL: game-based proofs in higher-order logic. J. Cryptol. 33(2), 494\u2013566 (2020)","journal-title":"J. Cryptol."},{"key":"16_CR24","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL - A Proof Assistant for Higher-Order Logic, ser. Lecture Notes in Computer Science, vol. 2283. Springer (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"16_CR25","doi-asserted-by":"crossref","unstructured":"Barthe, G., et al.: Fully automated analysis of padding-based encryption in the computational model. In: CCS, pp. 1247\u20131260. ACM (2013)","DOI":"10.1145\/2508859.2516663"},{"key":"16_CR26","doi-asserted-by":"crossref","unstructured":"Pedersen, T.P.: Non-interactive and information-theoretic secure verifiable secret sharing. In: CRYPTO, series Lecture Notes in Computer Science, vol. 576, pp. 129\u2013140. Springer (1991)","DOI":"10.1007\/3-540-46766-1_9"},{"key":"16_CR27","doi-asserted-by":"crossref","unstructured":"Faonio, A., Fiore, D., Kohlweiss, M., Russo, L., Zajac, M.: From polynomial IOP and commitments to non-malleable zksnarks. In: TCC (3), series Lecture Notes in Computer Science, vol. 14371, pp. 455\u2013485. Springer (2023)","DOI":"10.1007\/978-3-031-48621-0_16"}],"container-title":["Lecture Notes in Computer Science","Computer Security \u2013 ESORICS 2025"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-07891-9_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,27]],"date-time":"2026-05-27T02:19:17Z","timestamp":1779848357000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-07891-9_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,17]]},"ISBN":["9783032078902","9783032078919"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-07891-9_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,17]]},"assertion":[{"value":"17 October 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESORICS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Research in Computer Security","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Toulouse","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","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":"22 September 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 September 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esorics2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.esorics2025.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}