The speaker for this week’s seminar is our own Mukesh. Please find the title and abstract below.

Title One Proof, Many Implementations of Certified Sigma-Protocols

Abstract Sigma-protocols are a core building block in a wide range of privacy-preserving applications, but one particular application where they have found a widespread adoption is electronic voting. They remain a popular choice in electronic voting to maintain privacy and verifiability of elections and are still used in prominent electronic voting systems such as Helios, Belenois, and SwissPost. However, existing implementations of Sigma-protocols have two critical shortcomings: (i) the same code must be written multiple times, once for the front-end (JavaScript/TypeScript) and once for the back-end (Python/OCaml/Java), which is error-prone because the front-end and back-end codes are often written by different developers, leading to inconsistencies and bugs, and (ii) none of these implementations provide formal security guarantees.

In this talk, I will present a certified formalisation of a comprehensive library of Sigma-protocols in the Rocq theorem prover and formally prove (special) soundness, completeness, and (special honest-verifier) zero-knowledge properties. Our generic formalisation over abstract vector spaces enables us to uniformly express and compose a wide class of discrete-logarithm-based Sigma-protocols, while remaining independent of any concrete group or cryptographic instantiation. Moreover, the constructive nature of our formalisation allow us to extract and compile to executable implementations in OCaml, Rust, and WebAssembly and thereby eliminating code duplication. I will demonstrate the practical applicability of our framework by implementing a voting server and client for the Approval voting and IACR tally-sheet verifier. Our certified cryptographic library provides a foundation for building formally verified privacy-preserving applications. The source code can be accessed https://github.com/mukeshtiwari/SigmaProtocol/tree/master