Formally Verified Bulletproof in Coq, Lean, or Dafny

  by   Mukesh Tiwari






Departments Computer Science
DescriptionBulletproof [1, 2] is a zero-knowledge proof that does not requires trusted set and goal of this project is to implement a bulletproof in Coq, Lean, or Dafny. Although the original idea for this paper was to prove the range in cryptocurrencies transaction but it can also be used to prove an encrypted ballot is well-formed and contains only allowed values. This project requires understanding of logic, programming, and cryptography but you don't need to an expert. If you don't feel comfortable in Coq, Lean, or Dafny, we can find some middle ground and implement it in Haskell. [1] https://crypto.stanford.edu/bulletproofs/ [2] https://eprint.iacr.org/2017/1066.pdf
Preparation
Project Categories Security, Software Engineering
Project Keywords Cryptocurrencies, Cybersecurity, Logic, Proofs


Level of Studies

Level 6 (Undergraduate Year 3) yes
Level 7 (Masters) yes
Level 8 (PhD) yes