{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,7]],"date-time":"2025-11-07T09:50:07Z","timestamp":1762509007728,"version":"3.28.0"},"reference-count":104,"publisher":"IEEE","license":[{"start":{"date-parts":[[2023,5,1]],"date-time":"2023-05-01T00:00:00Z","timestamp":1682899200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-009"},{"start":{"date-parts":[[2023,5,1]],"date-time":"2023-05-01T00:00:00Z","timestamp":1682899200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-001"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023,5]]},"DOI":"10.1109\/sp46215.2023.10179393","type":"proceedings-article","created":{"date-parts":[[2023,7,21]],"date-time":"2023-07-21T17:18:15Z","timestamp":1689959895000},"page":"1112-1129","source":"Crossref","is-referenced-by-count":3,"title":["Less is more: refinement proofs for probabilistic proofs"],"prefix":"10.1109","author":[{"given":"Kunming","family":"Jiang","sequence":"first","affiliation":[{"name":"Courant Institute,NYU Department of Computer Science"}]},{"given":"Devora","family":"Chait-Roth","sequence":"additional","affiliation":[{"name":"Courant Institute,NYU Department of Computer Science"}]},{"given":"Zachary","family":"DeStefano","sequence":"additional","affiliation":[{"name":"Courant Institute,NYU Department of Computer Science"}]},{"given":"Michael","family":"Walfish","sequence":"additional","affiliation":[{"name":"Courant Institute,NYU Department of Computer Science"}]},{"given":"Thomas","family":"Wies","sequence":"additional","affiliation":[{"name":"Courant Institute,NYU Department of Computer Science"}]}],"member":"263","reference":[{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"ref2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-book - assigning programs to meanings","author":"Abrial","year":"1996"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-010-0145-y"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1145\/3208071"},{"key":"ref5","article-title":"Efficient representation of numerical optimization problems for SNARKs","author":"Angel","year":"2022","journal-title":"USENIX Security"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107256552"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1145\/273865.273901"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1145\/278298.278306"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1145\/103418.103428"},{"key":"ref10","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-1674-2","volume-title":"Refinement Calculus - A Systematic Introduction","author":"Back","year":"1998"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1145\/3551497"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480894"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35722-0_3"},{"key":"ref14","first-page":"146","article-title":"Easycrypt: A tutorial","volume-title":"FOSAD","volume":"8604","author":"Barthe","year":"2013"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44381-1_16"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1145\/2422436.2422481"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40084-1_6"},{"key":"ref18","article-title":"Succinct non-interactive zero knowledge for a von Neumann architecture","author":"Ben-Sasson","year":"2014","journal-title":"USENIX Security"},{"article-title":"Scalable, transparent, and post-quantum secure computational integrity","year":"2019","author":"Ben-Sasson","key":"ref19"},{"volume-title":"Mathematical Theory of Connecting Networks and Telephone Traffic","year":"1965","author":"Ben\u011bs","key":"ref20"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1145\/982962.964003"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1145\/3372297.3417893"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1991.185352"},{"article-title":"Certifying algorithm for strongly connected components","volume-title":"International Electrotechnical and Computer Science Conference","author":"Borov\u0161ak","key":"ref24"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00050"},{"key":"ref26","article-title":"Compiling computations to constraints for verified computation","author":"Braun","year":"2012","journal-title":"UT Austin Honors thesis HR-12-10"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1145\/2517349.2522733"},{"key":"ref28","article-title":"Proof-carrying data from accumulation schemes","volume-title":"IACR TCC","author":"B\u00fcnz","year":"2020"},{"key":"ref29","article-title":"Marlin: Preprocessing zk-SNARKs with universal and updatable SRS","author":"Chiesa","year":"2020","journal-title":"IACR Eurocrypt"},{"key":"ref30","article-title":"Leo: A programming language for formally verified, zero-knowledge applications","volume-title":"Cryptology ePrint Archive, Report 2021\/651","author":"Chin","year":"2021"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2015.23"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1007\/BF01933419"},{"volume-title":"A Discipline of Programming","year":"1976","author":"Dijkstra","key":"ref33"},{"key":"ref34","first-page":"126","article-title":"SMTCoq: A plugin for integrating SMT solvers into Coq","volume-title":"CAV (2)","volume":"10427","author":"Ekici","year":"2017"},{"key":"ref35","first-page":"2022\/1002","article-title":"Zswap: zk-SNARK based non-interactive multi-asset swaps","volume-title":"Cryptology ePrint Archive","author":"Engelmann","year":"2022"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1145\/3460120.3484795"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_19"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2016.26"},{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209174"},{"key":"ref40","article-title":"Plonk: Permutations over Lagrange-bases for oecumenical non-interactive arguments of knowledge","volume-title":"Cryptology ePrint Archive, Report 2019\/953","author":"Gabizon","year":"2019"},{"key":"ref41","article-title":"SnarkPack: Practical SNARK aggregation. Cryptology ePrint Archive","volume-title":"Report 2021\/529","author":"Gailly","year":"2021"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38348-9_37"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1561\/0400000023"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1137\/0218012"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1145\/2699436"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(72)90045-2"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49896-5_11"},{"key":"ref48","article-title":"Less is more: refinement proofs for probabilistic proofs (extended version)","volume-title":"Cryptology ePrint Archive","author":"Jiang","year":"2022"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1145\/543552.512566"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1109\/32.588534"},{"key":"ref51","article-title":"xJs-nark: a framework for efficient verifiable computation","author":"Kosba","year":"2018","journal-title":"IEEE S&P"},{"key":"ref52","article-title":"Poppins: A direct construction for asymptotically optimal zk-SNARKs","volume-title":"Cryptology ePrint Archive","author":"Kothapalli","year":"2020"},{"key":"ref53","article-title":"Nova: Recursive zero-knowledge arguments from folding schemes","volume-title":"Cryptology ePrint Archive","author":"Kothapalli","year":"2021"},{"key":"ref54","doi-asserted-by":"publisher","DOI":"10.1090\/s0002-9939-1956-0078686-7"},{"volume-title":"Snarky","key":"ref55"},{"key":"ref56","first-page":"454","article-title":"Refinement and projection of relational specifications","volume-title":"REX Workshop","volume":"430","author":"Lam","year":"1989"},{"key":"ref57","doi-asserted-by":"publisher","DOI":"10.1145\/318593.318616"},{"key":"ref58","doi-asserted-by":"publisher","DOI":"10.1145\/1133373.1133382"},{"key":"ref59","article-title":"Linear-time and post-quantum zero-knowledge SNARKs for R1CS","volume-title":"Cryptology ePrint Archive","author":"Lee","year":"2021"},{"key":"ref60","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"ref61","article-title":"Phantom: An efficient privacy protocol using zk-SNARKs based on smart contracts","volume-title":"Cryptology ePrint Archive","author":"Li","year":"2020"},{"volume-title":"libsnark","key":"ref62"},{"key":"ref63","doi-asserted-by":"publisher","DOI":"10.1145\/41840.41852"},{"key":"ref64","doi-asserted-by":"publisher","DOI":"10.1145\/3319535.3339817"},{"key":"ref65","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0014319"},{"key":"ref66","first-page":"481","article-title":"An algebraic definition of simulation between programs","volume-title":"IJCAI","author":"Milner","year":"1971"},{"key":"ref67","doi-asserted-by":"publisher","DOI":"10.1145\/44501.44503"},{"key":"ref68","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90011-6"},{"key":"ref69","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"ref70","article-title":"Scaling verifiable computation using efficient set accumulators","author":"Ozdemir","year":"2020","journal-title":"USENIX Security"},{"key":"ref71","doi-asserted-by":"publisher","DOI":"10.1109\/SP46214.2022.9833782"},{"key":"ref72","first-page":"167","article-title":"Concurrency and automata on infinite sequences","volume":"104","author":"Michael Ritchie Park","year":"1981","journal-title":"Theoretical Computer Science"},{"key":"ref73","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.47"},{"key":"ref74","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_33"},{"key":"ref75","article-title":"Pequin: A system for verifying outsourced computations, and applying SNARKs"},{"key":"ref76","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4939-2864-4_239"},{"key":"ref77","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90177-4"},{"key":"ref78","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2014.36"},{"key":"ref79","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-56877-1_25"},{"key":"ref80","article-title":"Taking proof-based verified computation a few steps closer to practicality","author":"Setty","year":"2012","journal-title":"USENIX Security"},{"key":"ref81","doi-asserted-by":"publisher","DOI":"10.1145\/2465351.2465359"},{"key":"ref82","article-title":"Proving the correct execution of concurrent services in zero-knowledge","author":"Setty","year":"2018","journal-title":"OSDI"},{"key":"ref83","doi-asserted-by":"publisher","DOI":"10.1145\/2858965.2814278"},{"key":"ref84","doi-asserted-by":"publisher","DOI":"10.1145\/2980983.2908092"},{"key":"ref85","doi-asserted-by":"publisher","DOI":"10.1137\/0201010"},{"key":"ref86","doi-asserted-by":"publisher","DOI":"10.1145\/62.2160"},{"key":"ref87","doi-asserted-by":"crossref","DOI":"10.1561\/9781638281252","article-title":"Proofs, arguments, and zero-knowledge","author":"Thaler","year":"2022"},{"key":"ref88","article-title":"Orbis specification language: a type theory for zk-SNARK programming","volume-title":"Cryptology ePrint Archive","author":"Thomas","year":"2022"},{"key":"ref89","first-page":"3","article-title":"The linear time - branching time spectrum I","author":"van Glabbeek","year":"2001","journal-title":"Handbook of Process Algebra"},{"article-title":"Practical proof systems: implementations, applications, and next steps","year":"2019","author":"Wahby","key":"ref90"},{"key":"ref91","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2015.23097"},{"key":"ref92","doi-asserted-by":"publisher","DOI":"10.1145\/321439.321449"},{"key":"ref93","doi-asserted-by":"publisher","DOI":"10.1145\/2641562"},{"key":"ref94","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00056"},{"key":"ref95","article-title":"Mystique: Efficient conversions for zero-knowledge proofs with applications to machine learning","author":"Weng","year":"2021","journal-title":"USENIX Security"},{"key":"ref96","doi-asserted-by":"crossref","DOI":"10.1109\/EuroSPW51379.2020.00058","article-title":"zkRelay: Facilitating sidechains using zkSNARK-based chain-relays","volume-title":"Cryptology ePrint Archive","author":"Westerkamp","year":"2020"},{"key":"ref97","doi-asserted-by":"publisher","DOI":"10.1145\/362575.362577"},{"key":"ref98","article-title":"DIZK: A distributed zero knowledge proof system","author":"Wu","year":"2018","journal-title":"USENIX Security"},{"key":"ref99","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.036"},{"key":"ref100","article-title":"Quick-Silver: Efficient and affordable zero-knowledge proofs for circuits and polynomials over any field","volume-title":"ACM CCS","author":"Yang","year":"2021"},{"key":"ref101","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00052"},{"key":"ref102","doi-asserted-by":"publisher","DOI":"10.1109\/ISCA52012.2021.00040"},{"key":"ref103","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2018.00013"},{"volume-title":"ZoKrates: A toolbox for zkSNARKs on Ethereum","key":"ref104"}],"event":{"name":"2023 IEEE Symposium on Security and Privacy (SP)","start":{"date-parts":[[2023,5,21]]},"location":"San Francisco, CA, USA","end":{"date-parts":[[2023,5,25]]}},"container-title":["2023 IEEE Symposium on Security and Privacy (SP)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/10179215\/10179280\/10179393.pdf?arnumber=10179393","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,20]],"date-time":"2024-07-20T05:15:25Z","timestamp":1721452525000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/10179393\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,5]]},"references-count":104,"URL":"https:\/\/doi.org\/10.1109\/sp46215.2023.10179393","relation":{},"subject":[],"published":{"date-parts":[[2023,5]]}}}