Formal Verification of the Sumcheck Protocol

• URL: http://arxiv.org/abs/2402.06093v1
• Date: Thu, 8 Feb 2024 23:01:32 GMT
• Title: Formal Verification of the Sumcheck Protocol
• Authors: Azucena Garvía Bosshard, Jonathan Bootle, Christoph Sprenger,
• Abstract summary: The sumcheck protocol, introduced in 1992, is an interactive proof which is a key component of many probabilistic proof systems. We provide a formally verified security analysis of the sumcheck protocol using the interactive theorem prover Isabelle/HOL.
• Score: 2.3591022864158067
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: The sumcheck protocol, introduced in 1992, is an interactive proof which is a key component of many probabilistic proof systems in computational complexity theory and cryptography, some of which have been deployed. However, none of these proof systems based on the sumcheck protocol enjoy a formally-verified security analysis. In this paper, we make progress in this direction by providing a formally verified security analysis of the sumcheck protocol using the interactive theorem prover Isabelle/HOL. We follow a general and modular approach. First, we give a general formalization of public-coin interactive proofs. We then define a generalized sumcheck protocol for which we axiomatize the underlying mathematical structure and we establish its soundness and completeness. Finally, we prove that these axioms hold for multivariate polynomials, the original setting of the sumcheck protocol. Our modular analysis facilitates formal verification of sumcheck instances based on different mathematical structures with little effort, by simply proving that these structures satisfy the axioms. Moreover, the analysis supports the development and formal verification of future cryptographic protocols using the sumcheck protocol as a building block.

Related papers

• Strands Rocq: Why is a Security Protocol Correct, Mechanically? [3.6840775431698893]
  StrandsRocq is a mechanization of the strand spaces in Coq. It incorporates new original proof techniques and a novel notion of maximal penetrator. It provides a compositional proof of security for two simple authentication protocols.
  arXiv  Detail & Related papers  (2025-02-18T13:34:58Z)
• CryptoFormalEval: Integrating LLMs and Formal Verification for Automated Cryptographic Protocol Vulnerability Detection [41.94295877935867]
  We introduce a benchmark to assess the ability of Large Language Models to autonomously identify vulnerabilities in new cryptographic protocols. We created a dataset of novel, flawed, communication protocols and designed a method to automatically verify the vulnerabilities found by the AI agents.
  arXiv  Detail & Related papers  (2024-11-20T14:16:55Z)
• Quantum Rewinding for IOP-Based Succinct Arguments [45.5096562396529]
  We prove that an interactive variant of the BCS transformation is secure in the standard model against quantum adversaries when the vector commitment scheme is collapsing. As a consequence of our results, we obtain standard-model post-quantum secure succinct arguments with the best complexity known.
  arXiv  Detail & Related papers  (2024-11-08T06:33:08Z)
• Protocols for Quantum Weak Coin Flipping [0.1499944454332829]
  Weak coin flipping is an important cryptographic primitive. We give exact constructions of related unitary operators. We illustrate the construction of explicit weak coin flipping protocols.
  arXiv  Detail & Related papers  (2024-02-24T16:52:54Z)
• Prototype-based Aleatoric Uncertainty Quantification for Cross-modal Retrieval [139.21955930418815]
  Cross-modal Retrieval methods build similarity relations between vision and language modalities by jointly learning a common representation space. However, the predictions are often unreliable due to the Aleatoric uncertainty, which is induced by low-quality data, e.g., corrupt images, fast-paced videos, and non-detailed texts. We propose a novel Prototype-based Aleatoric Uncertainty Quantification (PAU) framework to provide trustworthy predictions by quantifying the uncertainty arisen from the inherent data ambiguity.
  arXiv  Detail & Related papers  (2023-09-29T09:41:19Z)
• Entropy Accumulation under Post-Quantum Cryptographic Assumptions [4.416484585765028]
  In device-independent (DI) quantum protocols, the security statements are oblivious to the characterization of the quantum apparatus. We present a flexible framework for proving the security of such protocols by utilizing a combination of tools from quantum information theory.
  arXiv  Detail & Related papers  (2023-07-02T12:52:54Z)
• CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model [8.838422697156195]
  We introduce the CryptoVampire cryptographic protocol verifier, which for the first time fully automates proofs of trace properties in the BC Logic. Key technical contribution is a first-order (FO) formalization of protocol properties with tailored handling of subterm relations. On the theoretical side, we restrict full FO logic with cryptographic axioms to ensure that, by losing the expressivity of the HO BC Logic, we do not lose soundness.
  arXiv  Detail & Related papers  (2023-05-20T11:26:51Z)
• Verifying Quantum Phase Estimation (QPE) using Prove-It [0.0]
  The general-purpose interactive theorem-proving assistant called Prove-It was used to verify the Quantum Phase Estimation (QPE) algorithm. Prove-It is unique in its ability to express sophisticated mathematical statements, including statements about quantum circuits.
  arXiv  Detail & Related papers  (2023-04-05T01:21:00Z)
• DeepSec: Deciding Equivalence Properties for Security Protocols -- Improved theory and practice [8.735998284944436]
  We contribute both to the theory and practice of this verification problem. We establish new complexity results for static equivalence, trace equivalence and labelled bisimilarity. Our procedure is the first to decide trace equivalence and labelled bisimilarity exactly for a large variety of cryptographic primitives.
  arXiv  Detail & Related papers  (2022-11-06T22:01:04Z)
• Relational Action Bases: Formalization, Effective Safety Verification, and Invariants (Extended Version) [67.99023219822564]
  We introduce the general framework of relational action bases (RABs) RABs generalize existing models by lifting both restrictions. We demonstrate the effectiveness of this approach on a benchmark of data-aware business processes.
  arXiv  Detail & Related papers  (2022-08-12T17:03:50Z)
• 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)
• Revisiting the Sample Complexity of Sparse Spectrum Approximation of Gaussian Processes [60.479499225746295]
  We introduce a new scalable approximation for Gaussian processes with provable guarantees which hold simultaneously over its entire parameter space. Our approximation is obtained from an improved sample complexity analysis for sparse spectrum Gaussian processes (SSGPs)
  arXiv  Detail & Related papers  (2020-11-17T05:41:50Z)
• A refinement of Reznick's Positivstellensatz with applications to quantum information theory [72.8349503901712]
  In Hilbert's 17th problem Artin showed that any positive definite in several variables can be written as the quotient of two sums of squares. Reznick showed that the denominator in Artin's result can always be chosen as an $N$-th power of the squared norm of the variables.
  arXiv  Detail & Related papers  (2019-09-04T11:46:26Z)

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.