Description | Bulletproof [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 |