Proving Circuit Functional Equivalence in Zero Knowledge

• URL: http://arxiv.org/abs/2601.11173v1
• Date: Fri, 16 Jan 2026 10:43:30 GMT
• Title: Proving Circuit Functional Equivalence in Zero Knowledge
• Authors: Sirui Shen, Zunchen Huang, Chenglu Jin,
• Abstract summary: We propose ZK- CEC, the first privacy-preserving framework for hardware formal verification.<n>By combining formal verification and zero-knowledge proof (ZKP), ZK- CEC establishes a foundation for formally verifying IP correctness and security.<n>ZK- CEC successfully verifies practical designs, such as the AES S-Box, within practical time limits.
• Score: 4.301822791698451
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• Securing Generative AI in Healthcare: A Zero-Trust Architecture Powered by Confidential Computing on Google Cloud [0.0]
  Confidential Zero-Trust Framework (CZF) is a security paradigm that combines Zero-Trust Architecture for granular access control with the hardware-enforced data isolation of Confidential Computing.<n>CZF provides a defense-in-depth architecture where data remains encrypted while in-use within a hardware-based Trusted Execution Environment.
  arXiv  Detail & Related papers  (2025-11-14T19:56:52Z)
• CSI-IBBS: Identity-Based Blind Signature using CSIDH [0.0]
  We propose an Identity-Based Blind Signature Scheme with an Honest Zero-Knowledge Verifier utilizing the CSIDH framework.<n>We analyze the security of the introduced protocol in the standard cryptographic model and demonstrate its effectiveness in safeguarding privacy and verifier honesty.<n>This work advances the creation of secure, and scalable cryptographic systems for the post-quantum era.
  arXiv  Detail & Related papers  (2025-09-07T16:31:16Z)
• Formal Verification of Physical Layer Security Protocols for Next-Generation Communication Networks (extended version) [1.5997757408973357]
  We re-model the Needham-Schroeder protocol using an Isabelle formalism that generates sound animation.<n>Our findings reveal an uncommon but expected outcome: authenticity is preserved across all examined scenarios.<n>We have proposed a PLS-based Diffie-Hellman protocol that integrates watermarking and jamming.
  arXiv  Detail & Related papers  (2025-08-26T20:59:16Z)
• ZKPROV: A Zero-Knowledge Approach to Dataset Provenance for Large Language Models [46.71493672772134]
  We introduce ZKPROV, a novel cryptographic framework that enables zero-knowledge proofs of LLM provenance.<n>It allows users to verify that a model is trained on a reliable dataset without revealing sensitive information about it or its parameters.<n>Our method cryptographically binds a trained model to its authorized training dataset(s) through zero-knowledge proofs while avoiding proof of every training step.
  arXiv  Detail & Related papers  (2025-06-26T00:49:02Z)
• Structural Vulnerability in Y00 Protocols [0.0]
  This paper critically analyzes the Y00 protocol, a quantum noise-based stream cipher proposed to enhance classical cryptographic methods.<n>We reveal a structural vulnerability that enables the leakage of secret information from measurement outcomes.
  arXiv  Detail & Related papers  (2024-12-10T08:29:44Z)
• Balancing Confidentiality and Transparency for Blockchain-based Process-Aware Information Systems [43.253676241213626]
  We propose an architecture for blockchain-based PAISs to preserve confidentiality and transparency.<n>Smart contracts enact, enforce and store public interactions, while attribute-based encryption techniques are adopted to specify access grants to confidential information.<n>We assess the security of our solution through a systematic threat model analysis and evaluate its practical feasibility.
  arXiv  Detail & Related papers  (2024-12-07T20:18:36Z)
• ACRIC: Securing Legacy Communication Networks via Authenticated Cyclic Redundancy Integrity Check [98.34702864029796]
  Recent security incidents in safety-critical industries exposed how the lack of proper message authentication enables attackers to inject malicious commands or alter system behavior.<n>These shortcomings have prompted new regulations that emphasize the pressing need to strengthen cybersecurity.<n>We introduce ACRIC, a message authentication solution to secure legacy industrial communications.
  arXiv  Detail & Related papers  (2024-11-21T18:26:05Z)
• Coding-Based Hybrid Post-Quantum Cryptosystem for Non-Uniform Information [53.85237314348328]
  We introduce for non-uniform messages a novel hybrid universal network coding cryptosystem (NU-HUNCC) We show that NU-HUNCC is information-theoretic individually secured against an eavesdropper with access to any subset of the links.
  arXiv  Detail & Related papers  (2024-02-13T12:12:39Z)
• A Survey and Comparative Analysis of Security Properties of CAN Authentication Protocols [92.81385447582882]
  The Controller Area Network (CAN) bus leaves in-vehicle communications inherently non-secure. This paper reviews and compares the 15 most prominent authentication protocols for the CAN bus. We evaluate protocols based on essential operational criteria that contribute to ease of implementation.
  arXiv  Detail & Related papers  (2024-01-19T14:52:04Z)
• Tamper-Evident Pairing [55.2480439325792]
  Tamper-Evident Pairing (TEP) is an improvement of the Push-Button configuration (PBC) standard. TEP relies on the Tamper-Evident Announcement (TEA), which guarantees that an adversary can neither tamper a transmitted message without being detected, nor hide the fact that the message has been sent. This paper provides a comprehensive overview of the TEP protocol, including all information needed to understand how it works.
  arXiv  Detail & Related papers  (2023-11-24T18:54:00Z)
• Rely-guarantee Reasoning about Concurrent Memory Management: Correctness, Safety and Security [0.0]
  An incorrect specification and implementation of the memory management may lead to system crashes or exploitable attacks. This article presents the first formal specification and mechanized proof of a concurrent memory management for a real-world OS.
  arXiv  Detail & Related papers  (2023-09-17T03:41:10Z)
• Quantum Proofs of Deletion for Learning with Errors [91.3755431537592]
  We construct the first fully homomorphic encryption scheme with certified deletion. Our main technical ingredient is an interactive protocol by which a quantum prover can convince a classical verifier that a sample from the Learning with Errors distribution in the form of a quantum state was deleted.
  arXiv  Detail & Related papers  (2022-03-03T10:07:32Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.