{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T20:55:55Z","timestamp":1763499355918,"version":"3.45.0"},"publisher-location":"New York, NY, USA","reference-count":30,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,11,13]],"date-time":"2021-11-13T00:00:00Z","timestamp":1636761600000},"content-version":"vor","delay-in-days":1,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"DARPA","award":["HR001120C0086"],"award-info":[{"award-number":["HR001120C0086"]}]},{"name":"FCT","award":["PTDC\/EEI-COM\/28550\/2017"],"award-info":[{"award-number":["PTDC\/EEI-COM\/28550\/2017"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2021,11,12]]},"DOI":"10.1145\/3460120.3484771","type":"proceedings-article","created":{"date-parts":[[2021,11,13]],"date-time":"2021-11-13T12:05:34Z","timestamp":1636805134000},"page":"2587-2600","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Machine-checked ZKP for NP relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head"],"prefix":"10.1145","author":[{"given":"Jos\u00e9 Bacelar","family":"Almeida","sequence":"first","affiliation":[{"name":"University of Minho & INESC TEC, Braga, Portugal"}]},{"given":"Manuel","family":"Barbosa","sequence":"additional","affiliation":[{"name":"University of Porto (FCUP) & INESC TEC, Porto, Portugal"}]},{"given":"Manuel L.","family":"Correia","sequence":"additional","affiliation":[{"name":"University of Porto (FCUP) & INESC TEC, Porto, Portugal"}]},{"given":"Karim","family":"Eldefrawy","sequence":"additional","affiliation":[{"name":"SRI International, Menlo Park, CA, USA"}]},{"given":"St\u00e9phane","family":"Graham-Lengrand","sequence":"additional","affiliation":[{"name":"SRI International, Menlo Park, CA, USA"}]},{"given":"Hugo","family":"Pacheco","sequence":"additional","affiliation":[{"name":"University of Porto (FCUP) & INESC TEC, Porto, Portugal"}]},{"given":"Vitor","family":"Pereira","sequence":"additional","affiliation":[{"name":"SRI International, Menlo Park, CA, USA"}]}],"member":"320","published-online":{"date-parts":[[2021,11,13]]},"reference":[{"doi-asserted-by":"publisher","key":"e_1_3_2_2_1_1","DOI":"10.1145\/3133956.3134017"},{"doi-asserted-by":"publisher","key":"e_1_3_2_2_2_1","DOI":"10.1109\/SP40000.2020.00028"},{"doi-asserted-by":"publisher","key":"e_1_3_2_2_3_1","DOI":"10.1109\/CSF.2018.00017"},{"doi-asserted-by":"publisher","key":"e_1_3_2_2_4_1","DOI":"10.1145\/3319535.3363211"},{"doi-asserted-by":"publisher","key":"e_1_3_2_2_5_1","DOI":"10.1145\/3133956.3134104"},{"doi-asserted-by":"publisher","key":"e_1_3_2_2_6_1","DOI":"10.1145\/2382196.2382249"},{"key":"e_1_3_2_2_7_1","volume-title":"SoK: Computer-Aided Cryptography","author":"Barbosa Manuel","year":"2021","unstructured":"Manuel Barbosa, Gilles Barthe, Karthikeyan Bhargavan, Bruno Blanchet, Cas Cremers, Kevin Liao, and Bryan Parno. 2021. SoK: Computer-Aided Cryptography. IEEE Security and Privacy (2021)."},{"doi-asserted-by":"publisher","key":"e_1_3_2_2_8_1","DOI":"10.1109\/CSF.2010.24"},{"doi-asserted-by":"publisher","key":"e_1_3_2_2_9_1","DOI":"10.1007\/978--3-030--75245--3_11"},{"doi-asserted-by":"publisher","key":"e_1_3_2_2_10_1","DOI":"10.1007\/978-3-030-45374-9_17"},{"doi-asserted-by":"publisher","key":"e_1_3_2_2_11_1","DOI":"10.1145\/62212.62213"},{"unstructured":"Michael Ben-Or Shafi Goldwasser and Avi Wigderson. 2019. Completeness theorems for non-cryptographic fault-tolerant distributed computation. In Providing Sound Foundations for Cryptography: On the Work of Shafi Goldwasser and Silvio Micali. 351--371.","key":"e_1_3_2_2_12_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_2_13_1","DOI":"10.1145\/3372297.3417893"},{"doi-asserted-by":"publisher","key":"e_1_3_2_2_14_1","DOI":"10.1007\/978-3-540-88313-5_13"},{"key":"e_1_3_2_2_15_1","volume-title":"Formalising Sigma-Protocols and Commitment Schemes Using CryptHOL. Journal of Automated Reasoning","author":"Butler David","year":"2020","unstructured":"David Butler, Andreas Lochbihler, David Aspinall, and Adri\u00e0 Gasc\u00f3n. 2020. Formalising Sigma-Protocols and Commitment Schemes Using CryptHOL. Journal of Automated Reasoning (2020), 1--47."},{"doi-asserted-by":"publisher","key":"e_1_3_2_2_16_1","DOI":"10.1145\/3133956.3133997"},{"doi-asserted-by":"publisher","key":"e_1_3_2_2_17_1","DOI":"10.1007\/978--3-030--38471--5_27"},{"key":"e_1_3_2_2_18_1","volume-title":"Limbo: Efficient Zero-knowledge MPCitH-based Arguments. Cryptology ePrint Archive, Report 2021\/215. https:\/\/eprint.iacr.org\/2021\/215.","author":"de Saint Guilhem Cyprien Delpech","year":"2021","unstructured":"Cyprien Delpech de Saint Guilhem, Emmanuela Orsini, and Titouan Tanguy. 2021. Limbo: Efficient Zero-knowledge MPCitH-based Arguments. Cryptology ePrint Archive, Report 2021\/215. https:\/\/eprint.iacr.org\/2021\/215."},{"doi-asserted-by":"publisher","key":"e_1_3_2_2_19_1","DOI":"10.1145\/3319535.3354205"},{"key":"e_1_3_2_2_20_1","volume-title":"ZKBoo: Faster Zero-Knowledge for Boolean Circuits. In 25th USENIX Security Symposium, USENIX Security 16","author":"Giacomelli Irene","year":"2016","unstructured":"Irene Giacomelli, Jesper Madsen, and Claudio Orlandi. 2016. ZKBoo: Faster Zero-Knowledge for Boolean Circuits. In 25th USENIX Security Symposium, USENIX Security 16, Austin, TX, USA, August 10--12, 2016, Thorsten Holz and Stefan Savage (Eds.). USENIX Association, 1069--1083. https:\/\/www.usenix.org\/conference\/usenixsecurity16\/technical-sessions\/presentation\/giacomelli"},{"doi-asserted-by":"publisher","key":"e_1_3_2_2_21_1","DOI":"10.1007\/978--3--319--63697--9_3"},{"doi-asserted-by":"publisher","key":"e_1_3_2_2_22_1","DOI":"10.1007\/978--3-030--78375--4_15"},{"volume-title":"Proceedings of the 31st Computer Security Foundations Symposium. IEEE, In print.","author":"Haagh Helene","unstructured":"Helene Haagh, Aleksandr Karbyshev, Sabine Oechsner, Bas Spitters, and Pierre-Yves Strub. [n.,d.]. Computer-aided proofs for multiparty computation with active security. In Proceedings of the 31st Computer Security Foundations Symposium. IEEE, In print.","key":"e_1_3_2_2_23_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_2_24_1","DOI":"10.1109\/CSF.2018.00016"},{"doi-asserted-by":"publisher","key":"e_1_3_2_2_25_1","DOI":"10.1145\/1250790.1250794"},{"doi-asserted-by":"publisher","key":"e_1_3_2_2_26_1","DOI":"10.1145\/3243734.3243805"},{"doi-asserted-by":"publisher","key":"e_1_3_2_2_27_1","DOI":"10.1016\/j.dam.2005.03.020"},{"key":"e_1_3_2_2_28_1","volume-title":"Pinocchio: Nearly Practical Verifiable Computation. In IEEE Symposium on Security and Privacy. 238--252","author":"Parno Bryan","year":"2013","unstructured":"Bryan Parno, Jon Howell, Craig Gentry, and Mariana Raykova. 2013. Pinocchio: Nearly Practical Verifiable Computation. In IEEE Symposium on Security and Privacy. 238--252."},{"doi-asserted-by":"publisher","key":"e_1_3_2_2_29_1","DOI":"10.1145\/3372297.3417889"},{"doi-asserted-by":"crossref","unstructured":"Nikolaj Sidorenco Sabine Oechsner and Bas Spitters. 2021. Formal security analysis of MPC-in-the-head zero-knowledge protocols. Cryptology ePrint Archive Report 2021\/437. https:\/\/eprint.iacr.org\/2021\/437.","key":"e_1_3_2_2_30_1","DOI":"10.1109\/CSF51468.2021.00050"}],"event":{"sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"],"acronym":"CCS '21","name":"CCS '21: 2021 ACM SIGSAC Conference on Computer and Communications Security","location":"Virtual Event Republic of Korea"},"container-title":["Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3460120.3484771","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3460120.3484771","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3460120.3484771","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T20:51:16Z","timestamp":1763499076000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3460120.3484771"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,11,12]]},"references-count":30,"alternative-id":["10.1145\/3460120.3484771","10.1145\/3460120"],"URL":"https:\/\/doi.org\/10.1145\/3460120.3484771","relation":{},"subject":[],"published":{"date-parts":[[2021,11,12]]},"assertion":[{"value":"2021-11-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}