pith. sign in

arxiv: 2601.11173 · v2 · submitted 2026-01-16 · 💻 cs.CR · cs.LO

Proving Circuit Functional Equivalence in Zero Knowledge

Sirui Shen , Zunchen Huang , Chenglu Jin This is my paper

Pith reviewed 2026-05-16 13:51 UTC · model grok-4.3

classification 💻 cs.CR cs.LO
keywords zero-knowledge proofcircuit verificationfunctional equivalencehardware IPformal verificationprivacy-preservingunsatisfiability
0
0 comments X

The pith

ZK-CEC lets a prover show that a secret circuit matches a public specification in zero knowledge.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper constructs ZK-CEC to let a prover show that a hidden circuit design performs exactly as a public specification requires, using zero-knowledge techniques. This addresses the trust problem in using third-party hardware IP by providing formal verification guarantees without exposing the proprietary design. Previous privacy methods relied on simulation and lacked formal assurances, while standard ZKP worked only for public formulas. The new approach prevents a malicious prover from forging the secret formula. If correct, it allows secure integration of circuits like arithmetic units and AES components with practical performance.

Core claim

ZK-CEC is built on a blueprint that proves the unsatisfiability of a secret design against a public constraint. This enables the prover to convince the verifier of perfect functional alignment between the secret IP and the specification, disclosing nothing but the length and width of the resulting proof. The framework was implemented and tested on various circuits, confirming it handles practical designs within reasonable time.

What carries the argument

The blueprint for proving unsatisfiability of a secret design against a public constraint, which extends zero-knowledge protocols to secret formulas while maintaining soundness.

If this is right

  • Verifiers can confirm that a secret circuit matches the public spec without learning its internal structure.
  • Hardware integrators can trust third-party IP blocks against Trojans while keeping designs confidential.
  • The same blueprint supports property proofs for software and cyber-physical systems.
  • Practical designs such as the AES S-Box can be verified within usable time bounds.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The method could adapt to privacy-preserving software equivalence checks.
  • It might reduce supply-chain trust requirements in electronics manufacturing.
  • Automated tools could generate the public constraints directly from high-level specifications.

Load-bearing premise

Existing zero-knowledge protocols for public formulas can be safely extended to secret formulas without allowing a malicious prover to forge the formula or break soundness.

What would settle it

A successful forgery where a prover convinces the verifier of equivalence for a circuit that does not actually match the specification, or a proof that leaks more information than its length and width.

Figures

Figures reproduced from arXiv: 2601.11173 by Chenglu Jin, Sirui Shen, Zunchen Huang.

Figure 2
Figure 2. Figure 2: An AND gate and its corresponding CNF formula. [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Functionality for ZKPs of elements in F. make the outputs differ. In this case, a resolution proof of unsat￾isfiability in Sec. 3.1 serves as the formal certificate that 𝐶spec and 𝐶impl are equivalent. 3.3 VOLE-based Zero-knowledge Protocols Recent advancements [2, 9, 43–45] in zero-knowledge protocols rely on vector oblivious linear evaluation (VOLE) [29] over a finite field F. A VOLE is a two-party primi… view at source ↗
Figure 5
Figure 5. Figure 5: Functionality for clause operations in ZK. [PITH_FULL_IMAGE:figures/full_fig_p004_5.png] view at source ↗
Figure 7
Figure 7. Figure 7: An AND-gate example of secret formula property [PITH_FULL_IMAGE:figures/full_fig_p005_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Protocol for proving P1. To prevent the leakage of clause width information in the proof, we ensure that all polynomials have the same length. We identify the maximum degree𝑤 among polynomials and pad the high-order coefficients of shorter polynomials with zeros, which ensures that all polynomial commitments do not leak individual clause widths. 5.3 Proving P1 In [PITH_FULL_IMAGE:figures/full_fig_p007_8.png] view at source ↗
Figure 10
Figure 10. Figure 10: Protocol for proving P3. variables in Vio and Vsec correspond to the input/output wires and the internal wires of 𝐶impl, respectively. Since 𝐶impl shares inputs with 𝐶spec and connects its outputs to 𝐶IO, VIO is known by both parties, implying LIO ∈ Lpub. The internal wires of 𝐶impl, represented by Vsec, corresponds to Lsec. Let 𝜔sec : Vsec → {0, 1} 𝑛 be a Boolean assignment. The SAT problem of Φsec is de… view at source ↗
Figure 11
Figure 11. Figure 11: Protocol for proving P4. 𝑙 is not in clause 𝑐 if and only if Poly[𝑐] (𝜙 (𝑙)) ≠ 0. Hence the protocol verifies that for every literal 𝑙 ∈ Lpub \ LIO and every clause 𝑐 ∈ Φsec, the polynomial evaluation Poly[𝑐] (𝜙 (𝑙)) yields a non-zero value. We give the detailed protocol to prove P4 in Fig.11. To prove that Poly[𝑐] (𝜙 (𝑙)) ≠ 0 without compromising zero￾knowledge, we use a standard non-zero proof technique… view at source ↗
Figure 13
Figure 13. Figure 13: Proving time vs. input size: (a) Proving time or P1+P2 (b) Proving time for P3 (c) Proving time for P4 (d) Total proving [PITH_FULL_IMAGE:figures/full_fig_p012_13.png] view at source ↗
Figure 14
Figure 14. Figure 14: A refutation proof tree example. cheat in sub-protocols ΠP1 and ΠP4 will make the protocol abort with overwhelming probability. The soundness of the refutation in ΠP2 depends on the validity of the commitment [Φsec]. According to Lemma 4.1, ΠP3 and ΠP4 guarantee that the statement [Φsec] in ΠP2 is valid and non-contradictory. This ensures that any derived contradiction originates from the interface VIO ra… view at source ↗
read the original abstract

The modern integrated circuit ecosystem is increasingly reliant on third-party intellectual property integration, which introduces security risks, including hardware Trojans and security vulnerabilities. Addressing the resulting trust deadlock between IP vendors and system integrators without exposing proprietary designs requires novel privacy-preserving verification techniques. However, existing privacy-preserving hardware verification methods are all simulation-based and fail to offer formal guarantees. In this paper, we propose ZK-CEC, the first privacy-preserving framework for hardware formal verification. By combining formal verification and zero-knowledge proof (ZKP), ZK-CEC establishes a foundation for formally verifying IP correctness and security without compromising the confidentiality of the designs. We observe that existing zero-knowledge protocols for formal verification are designed to prove statements of public formulas. However, in a privacy-preserving verification context where the formula is secret, these protocols cannot prevent a malicious prover from forging the formula, thereby compromising the soundness of the verification. To address these gaps, we first propose a blueprint for proving the unsatisfiability of a secret design against a public constraint, which is widely applicable to proving properties in software, hardware, and cyber-physical systems. Based on the proposed blueprint, we construct ZK-CEC, which enables a prover to convince the verifier that a secret IP's functionality aligns perfectly with the public specification in zero knowledge, revealing only the length and width of the proof. We implement ZK-CEC and evaluate its performance across various circuits, including arithmetic units and cryptographic components. Experimental results show that ZK-CEC successfully verifies practical designs, such as the AES S-Box, within practical time limits.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

3 major / 2 minor

Summary. The manuscript proposes ZK-CEC, the first privacy-preserving framework combining formal verification and zero-knowledge proofs to verify that a secret hardware IP circuit is functionally equivalent to a public specification. It introduces a blueprint for proving unsatisfiability of secret designs against public constraints (applicable to hardware, software, and cyber-physical systems), constructs ZK-CEC on this blueprint, and reports experimental verification of practical circuits including arithmetic units and the AES S-Box, revealing only proof length and width.

Significance. If the soundness claims hold, ZK-CEC would enable formal verification of third-party IP without exposing proprietary designs, directly addressing trust and security risks (e.g., hardware Trojans) in the IC supply chain. The experimental results on realistic designs such as AES S-Box demonstrate practicality within reasonable time bounds, and the blueprint's generality across domains adds potential impact; however, the absence of security proofs or reductions means the significance remains conditional on the unexamined extension from public-formula ZK protocols.

major comments (3)
  1. [Blueprint section] Blueprint section: The proposed blueprint for proving unsatisfiability of a secret design against a public constraint does not specify or prove any binding mechanism (such as a circuit commitment or encoding that fixes the secret formula) to prevent a malicious prover from substituting an arbitrary satisfying circuit; this leaves the soundness reduction from standard ZKP primitives incomplete, directly undermining the central claim that formula forgery is prevented.
  2. [ZK-CEC construction] ZK-CEC construction: No theorem, security proof, or formal reduction is provided establishing that the protocol preserves soundness when the formula is secret (as opposed to public formulas in prior ZK work); the abstract explicitly notes this gap in existing protocols, yet the construction relies on an unstated assumption that the extension maintains binding without additional mechanisms.
  3. [Evaluation] Evaluation: The reported successful verification of the AES S-Box and other circuits lacks any error analysis, soundness parameter settings, or comparison to baseline ZKP schemes, making it impossible to assess whether the implementation actually achieves the claimed formal guarantees or merely demonstrates syntactic feasibility.
minor comments (2)
  1. [Abstract] The abstract and introduction use 'formal guarantees' without clarifying that these are prospective pending proofs; a brief qualification would improve precision.
  2. [Implementation] Implementation details on how the secret circuit is arithmetized and encoded into the ZK statement are high-level; adding pseudocode or a small worked example would aid reproducibility.

Simulated Author's Rebuttal

3 responses · 0 unresolved

We thank the referee for their insightful comments on our manuscript proposing ZK-CEC. We provide point-by-point responses to the major comments and indicate the revisions we will make to address the concerns regarding soundness and evaluation.

read point-by-point responses

  1. Referee: [Blueprint section] Blueprint section: The proposed blueprint for proving unsatisfiability of a secret design against a public constraint does not specify or prove any binding mechanism (such as a circuit commitment or encoding that fixes the secret formula) to prevent a malicious prover from substituting an arbitrary satisfying circuit; this leaves the soundness reduction from standard ZKP primitives incomplete, directly undermining the central claim that formula forgery is prevented.

    Authors: We agree with the referee that the blueprint would be strengthened by an explicit binding mechanism. The manuscript's blueprint uses the public constraint to define the unsatisfiability condition, and the ZKP ensures the prover cannot cheat on the proof. To complete the argument, we will revise the blueprint section to specify a commitment scheme (e.g., committing to the circuit's encoding) that binds the secret formula, and include a high-level soundness reduction showing that forgery is prevented under standard ZKP assumptions. revision: yes

  2. Referee: [ZK-CEC construction] ZK-CEC construction: No theorem, security proof, or formal reduction is provided establishing that the protocol preserves soundness when the formula is secret (as opposed to public formulas in prior ZK work); the abstract explicitly notes this gap in existing protocols, yet the construction relies on an unstated assumption that the extension maintains binding without additional mechanisms.

    Authors: The ZK-CEC construction extends the blueprint to secret formulas by using the same unsatisfiability proof structure. We acknowledge that a formal theorem and reduction are missing in the current draft. In the revised version, we will add a theorem stating the soundness of ZK-CEC for secret formulas, with a proof reduction to the underlying ZKP primitive's soundness, incorporating the binding from the blueprint. revision: yes

  3. Referee: [Evaluation] The reported successful verification of the AES S-Box and other circuits lacks any error analysis, soundness parameter settings, or comparison to baseline ZKP schemes, making it impossible to assess whether the implementation actually achieves the claimed formal guarantees or merely demonstrates syntactic feasibility.

    Authors: We will update the evaluation section to include a detailed error analysis, specify the soundness parameters (e.g., security level and proof size), and add comparisons to baseline ZKP schemes for public formulas to better demonstrate the practical achievement of the formal guarantees. revision: yes

Circularity Check

0 steps flagged

No significant circularity; construction rests on standard ZKP primitives and an independent blueprint

full rationale

The paper defines ZK-CEC by combining existing zero-knowledge protocols with a newly proposed blueprint for proving unsatisfiability of secret designs against public constraints. No equations or claims reduce by construction to fitted parameters, self-referential definitions, or load-bearing self-citations. The soundness argument for the secret-formula case is presented as an extension of public-formula ZK techniques, with the blueprint serving as the explicit additional mechanism rather than an implicit assumption. The derivation chain is therefore self-contained against external benchmarks and does not collapse to its inputs.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on standard cryptographic soundness assumptions for zero-knowledge proofs and the feasibility of adapting them to secret formulas; no new free parameters, invented entities, or ad-hoc axioms are introduced in the abstract.

axioms (1)
  • domain assumption Soundness and completeness of existing zero-knowledge protocols when applied to unsatisfiability of secret formulas
    The blueprint and ZK-CEC construction assume these protocols remain sound when the formula itself is hidden.

pith-pipeline@v0.9.0 · 5585 in / 1222 out tokens · 54329 ms · 2026-05-16T13:51:39.083573+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

49 extracted references · 49 canonical work pages

  1. [1]

    Nadarajah Asokan, Victor Shoup, and Michael Waidner. 1998. Optimistic fair exchange of digital signatures. InInternational Conference on the Theory and Applications of Cryptographic Techniques. Springer, 591–606

    work page 1998

  2. [2]

    Carsten Baum, Alex J Malozemoff, Marc B Rosen, and Peter Scholl. 2021. Mac n Cheese: zero-knowledge proofs for boolean and arithmetic circuits with nested disjunctions. InAnnual International Cryptology Conference. Springer, 92–122

    work page 2021

  3. [3]

    Alex Baumgarten, Michael Steffen, Matthew Clausman, and Joseph Zambreno

    work page

  4. [4]

    A case study in hardware Trojan design and implementation.International Journal of Information Security10, 1 (2011), 1–14

    work page 2011

  5. [5]

    Armin Biere. 2008. PicoSAT essentials.Journal on Satisfiability, Boolean Modelling and Computation4, 2-4 (2008), 75–97

    work page 2008

  6. [6]

    Brice Colombier and Lilian Bossuet. 2014. Survey of hardware protection of design data for integrated circuits and intellectual properties.IET Computers & Digital Techniques8, 6 (2014), 274–287

    work page 2014

  7. [7]

    Santiago Cuéllar, Bill Harris, James Parker, Stuart Pernsteiner, and Eran Tromer

    work page

  8. [8]

    In 32nd USENIX Security Symposium (USENIX Security 23)

    Cheesecloth: {Zero-Knowledge} proofs of real world vulnerabilities. In 32nd USENIX Security Symposium (USENIX Security 23). 6525–6540

    work page

  9. [9]

    Martin Davis and Hilary Putnam. 1960. A computing procedure for quantification theory.Journal of the ACM (JACM)7, 3 (1960), 201–215

    work page 1960

  10. [10]

    Frank Denis. [n. d.].libsodium. https://github.com/jedisct1/libsodium

    work page

  11. [11]

    Samuel Dittmer, Yuval Ishai, and Rafail Ostrovsky. 2020. Line-point zero knowl- edge and its applications.Cryptology ePrint Archive(2020)

    work page 2020

  12. [12]

    Lisa Eckey, Sebastian Faust, and Benjamin Schlosser. 2020. Optiswap: Fast optimistic fair exchange. InProceedings of the 15th ACM Asia Conference on Computer and Communications Security. 543–557

    work page 2020

  13. [13]

    Nicholas Franzese, Jonathan Katz, Steve Lu, Rafail Ostrovsky, Xiao Wang, and Chenkai Weng. 2021. Constant-overhead zero-knowledge for RAM programs. In Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security. 178–191

    work page 2021

  14. [14]

    Evguenii I Goldberg, Mukul R Prasad, and Robert K Brayton. 2001. Using SAT for combinational equivalence checking. InProceedings Design, Automation and Test in Europe. Conference and Exhibition 2001. IEEE, 114–121

    work page 2001

  15. [15]

    Charles Gouert and Nektarios Georgios Tsoutsos. 2020. Romeo: Conversion and evaluation of HDL designs in the encrypted domain. In2020 57th ACM/IEEE Design Automation Conference (DAC). IEEE, 1–6

    work page 2020

  16. [16]

    Syed Kamran Haider, Chenglu Jin, Masab Ahmad, Devu Manikantan Shila, Omer Khan, and Marten van Dijk. 2019. Advancing the state-of-the-art in hardware trojans detection.IEEE Transactions on Dependable and Secure Computing16, 1 (2019), 18–32

    work page 2019

  17. [17]

    Syed Kamran Haider, Chenglu Jin, and Marten van Dijk. 2017. Advancing the state-of-the-art in hardware trojans design. In2017 IEEE 60th International Midwest Symposium on Circuits and Systems (MWSCAS). IEEE, 823–826

    work page 2017

  18. [18]

    Yier Jin and Yiorgos Makris. 2008. Hardware Trojan detection using path delay fingerprint. In2008 IEEE International workshop on hardware-oriented security and trust. IEEE, 51–57

    work page 2008

  19. [19]

    Yier Jin and Yiorgos Makris. 2012. Proof carrying-based information flow tracking for data secrecy protection and hardware trust. In2012 IEEE 30th VLSI Test Symposium (VTS). IEEE, 252–257

    work page 2012

  20. [20]

    John C Kolesar, Shan Ali, Timos Antonopoulos, and Ruzica Piskac. 2025. Coinduc- tive Proofs of Regular Expression Equivalence in Zero Knowledge.Proceedings of the ACM on Programming Languages9, OOPSLA2 (2025), 357–385

    work page 2025

  21. [21]

    Charalambos Konstantinou, Anastasis Keliris, and Michail Maniatakos. 2015. Privacy-preserving functional IP verification utilizing fully homomorphic en- cryption. In2015 Design, Automation & Test in Europe Conference & Exhibition (DATE). IEEE, 333–338

    work page 2015

  22. [22]

    2018.Network-on-chip: the next generation of system-on-chip integration

    Santanu Kundu and Santanu Chattopadhyay. 2018.Network-on-chip: the next generation of system-on-chip integration. Taylor & Francis

    work page 2018

  23. [23]

    Evan Laufer, Alex Ozdemir, and Dan Boneh. 2024. zkpi: Proving lean theorems in zero-knowledge. InProceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security. 4301–4315

    work page 2024

  24. [24]

    Eric Love, Yier Jin, and Yiorgos Makris. 2011. Proof-carrying hardware intellec- tual property: A pathway to trusted module acquisition.IEEE Transactions on Information Forensics and Security7, 1 (2011), 25–40

    work page 2011

  25. [25]

    Daniel Luick, John C Kolesar, Timos Antonopoulos, William R Harris, James Parker, Ruzica Piskac, Eran Tromer, Xiao Wang, and Ning Luo. 2024. {ZKSMT}: A {VM} for Proving {SMT} Theorems in Zero Knowledge. In33rd USENIX Security Symposium (USENIX Security 24). 3837–3845

    work page 2024

  26. [26]

    Ning Luo, Timos Antonopoulos, William R Harris, Ruzica Piskac, Eran Tromer, and Xiao Wang. 2022. Proving UNSAT in zero knowledge. InProceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security. 2203–2217

    work page 2022

  27. [27]

    Joao P Marques-Silva and Karem A Sakallah. 2002. GRASP: A search algorithm for propositional satisfiability.IEEE Trans. Comput.48, 5 (2002), 506–521

    work page 2002

  28. [28]

    Dimitris Mouris, Charles Gouert, and Nektarios Georgios Tsoutsos. 2022. Zk- sherlock: Exposing hardware trojans in zero-knowledge. In2022 IEEE Computer Society Annual Symposium on VLSI (ISVLSI). IEEE, 170–175

    work page 2022

  29. [29]

    Dimitris Mouris, Charles Gouert, and Nektarios Georgios Tsoutsos. 2023. MPoC: Privacy-Preserving IP Verification Using Logic Locking and Secure Multiparty Computation. In2023 IEEE 29th International Symposium on On-Line Testing and Robust System Design (IOLTS). IEEE, 1–8

    work page 2023

  30. [30]

    Dimitris Mouris and Nektarios Georgios Tsoutsos. 2020. Pythia: Intellectual prop- erty verification in zero-knowledge. In2020 57th ACM/IEEE Design Automation Conference (DAC). IEEE, 1–6

    work page 2020

  31. [31]

    Jesper Buus Nielsen, Peter Sebastian Nordholt, Claudio Orlandi, and Sai Sheshank Burra. 2012. A new approach to practical active-secure two-party computation. InAnnual Cryptology Conference. Springer, 681–700

    work page 2012

  32. [32]

    Daniel Perrucci and Juan Sabia. 2007. Real roots of univariate polynomials and straight line programs.Journal of Discrete Algorithms5, 3 (2007), 471–478

    work page 2007

  33. [33]

    Reza M Rad, Xiaoxiao Wang, Mohammad Tehranipoor, and Jim Plusquellic. 2008. Power supply signal calibration techniques for improving detection resolution to hardware Trojans. In2008 IEEE/ACM International Conference on Computer-Aided Design. IEEE, 632–639

    work page 2008

  34. [34]

    Jeyavijayan JV Rajendran. 2017. An overview of hardware intellectual property protection. In2017 IEEE International Symposium on Circuits and Systems (ISCAS). IEEE, 1–4

    work page 2017

  35. [35]

    Sandip Ray, Wen Chen, and Rosario Cammarota. 2018. Protecting the supply chain for automotives and IoTs. InProceedings of the 55th Annual Design Automa- tion Conference. 1–4

    work page 2018

  36. [36]

    John Alan Robinson. 1965. A machine-oriented logic based on the resolution principle.Journal of the ACM (JACM)12, 1 (1965), 23–41

    work page 1965

  37. [37]

    Masoud Rostami, Farinaz Koushanfar, and Ramesh Karri. 2014. A primer on hardware security: Models, methods, and metrics.Proc. IEEE102, 8 (2014), 1283– 1295

    work page 2014

  38. [38]

    Saarinen and Jean-Philippe Aumasson

    Markku-Juhani O. Saarinen and Jean-Philippe Aumasson. 2015. The BLAKE2 Cryptographic Hash and Message Authentication Code (MAC). RFC 7693. doi:10. 17487/RFC7693

    work page 2015

  39. [39]

    Resve Saleh, Steve Wilton, Shahriar Mirabbasi, Alan Hu, Mark Greenstreet, Guy Lemieux, Partha Pratim Pande, Cristian Grecu, and Andre Ivanov. 2006. System-on-chip: Reuse and integration.Proc. IEEE94, 6 (2006), 1050–1069

    work page 2006

  40. [40]

    Victor Shoup et al. 2001. NTL: A library for doing number theory

    work page 2001

  41. [41]

    Yunqing Sun, Hanlin Liu, Kang Yang, Yu Yu, Xiao Wang, and Chenkai Weng

    work page

  42. [42]

    In Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security

    Committed Vector Oblivious Linear Evaluation and Its Applications. In Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security. 3635–3648

    work page 2025

  43. [43]

    Grigori S Tseitin. 1983. On the complexity of derivation in propositional calculus. InAutomation of reasoning: 2: Classical papers on computational logic 1967–1970. Springer, 466–483

    work page 1983

  44. [44]

    Adam Waksman and Simha Sethumadhavan. 2011. Silencing hardware backdoors. In2011 IEEE Symposium on Security and Privacy. IEEE, 49–63

    work page 2011

  45. [45]

    Malozemoff, and Jonathan Katz

    Xiao Wang, Alex J. Malozemoff, and Jonathan Katz. 2016. EMP-toolkit: Efficient MultiParty computation toolkit. https://github.com/emp-toolkit

    work page 2016

  46. [46]

    Chenkai Weng, Kang Yang, Jonathan Katz, and Xiao Wang. 2021. Wolverine: Fast, scalable, and communication-efficient zero-knowledge proofs for boolean and arithmetic circuits. In2021 IEEE Symposium on Security and Privacy (SP). IEEE, 1074–1091

    work page 2021

  47. [47]

    Chenkai Weng, Kang Yang, Xiang Xie, Jonathan Katz, and Xiao Wang. 2021. Mystique: Efficient conversions for {Zero-Knowledge} proofs with applications to machine learning. In30th USENIX Security Symposium (USENIX Security 21). 501–518

    work page 2021

  48. [48]

    Kang Yang, Pratik Sarkar, Chenkai Weng, and Xiao Wang. 2021. Quicksilver: Efficient and affordable zero-knowledge proofs for circuits and polynomials over any field. InProceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security. 2986–3001

    work page 2021

  49. [49]

    Zibin Zheng, Shaoan Xie, Hong-Ning Dai, Weili Chen, Xiangping Chen, Jian Weng, and Muhammad Imran. 2020. An overview on smart contracts: Challenges, advances and platforms.Future Generation Computer Systems105 (2020), 475– 491. Sirui Shen, Zunchen Huang, and Chenglu Jin A Proofs A.1 Proof of Lemma 4.1 We prove Lemma 4.1 by contradiction. GivenΦ𝑎 ∧Φ𝑏 is un...

    work page 2020