Formalisation of Schnorr Protocol and other proofs (https://www.win.tue.nl/~berry/2WC13/LectureNotes.pdf)
Here is my plan to proceed:
- I am going to write a concrete implementation of Group and Field and their respective functions (addition, multiplication, division, etc), assuming the Schnorr group. (Finished)
- Then I write a power function that interacts between Group and Field and show that it respects the vector-space axioms. (Finished)
- Now that we have all the concrete implementation, we can demonstrate that they are efficient. (Finished)
- Formalise others, e.g., Parallel, EQ, AND, OR sigma protocol (Finished)
- Formalise some vote counting method where we can use our sigma protocol library to demonstrate usability.
The end goal is verify all the crypto primitives of SwissPost in Coq.