Dear all, we (me and Prof. Ulrich Berger) are looking for a PhD student to formalise zero-knowledge succinct non-interactive argument of knowledge (ZkSNARK) in the Rocq/Coq theorem prover [1]. It is fully funded and the scholarship covers the full cost of tuition fees and an annual stipend at UKRI rate (currently £19,237 for 2024/25). Additional research expenses of up to £1,000 per year will also be available. You can reach out to me if you have any question.
Project description:
Recently, many councils in Wales started using single transferable vote (STV) method for counting ballots. While counting plaintext ballots using STV method is straight forward, but a rank-based ballot may leak the voter’s preferences if published publicly in plaintext, as the ranking order can reveal detailed information about the voter’s identity. Therefore encryption is necessary to hide the ranking. However, STV method becomes considerably more complex with encrypted ballots. Our goal is to develop an algorithm/protocol to count encrypted ballot using the STV method. Our first point of investigation will be zero-knowledge succint non-interactive argument of knowledge – ZkSNARK. Subsequently, we will formalise the front-end (R1CS) and back-end (Groth16) of ZkSNARK in the Coq theorem prover and use this formalisation to encode our STV algorithm on encrypted ballots. This approach aims to ensure both the correctness and privacy of the tallying process, paving the way for verifiable and secure election systems that is resistent to coercion.
Requirement: You are not required to be an expert in Coq or Cryptography; familiarity with Coq and Cryptography is fine. However, you should be comfortable with a functional programming language Haskell, OCaml, etc.