Open access
Date
2023Type
- Master Thesis
ETH Bibliography
yes
Altmetrics
Abstract
The sumcheck protocol is an interactive proof which is widely used in computational complexity and cryptography. First introduced in 1992, the proofs of its security properties, namely its completeness and soundness, are widely known and accepted. In this thesis we provide a formal proof of the soundness and completeness properties of the sumcheck protocol using the Isabelle automated theorem prover. We highlight two stages in the proof. Firstly, we establish the protocol’s security properties for an abstract version of the protocol where the required underlying mathematical structure is axiomatized. Secondly, we prove that these axioms hold for multivariate polynomials. Our mechanized proof strengthens the confidence in the security of the protocol. Moreover, our modular proof approach enables others to establish the security of protocol variants based on different mathematical structures (e.g., tensor codes) with little effort, by simply proving that these structures satisfy the axioms. Overall this thesis provides a deeper understanding of the sumcheck protocol and its security properties, which can aid in the development of future cryptographic protocols and will encourage their subsequent formal verification. Show more
Permanent link
https://doi.org/10.3929/ethz-b-000611002Publication status
publishedPublisher
ETH ZurichOrganisational unit
03634 - Basin, David / Basin, David
More
Show all metadata
ETH Bibliography
yes
Altmetrics