This project explores zero-knowledge proofs (ZKPs), cryptographic protocols that allow a prover to convince a verifier of the truth of a statement without revealing any additional information. We focused on an interactive Σ-protocol based on the quadratic residue problem, formalizing its three core properties: completeness, soundness, and zero-knowledge. Using the EasyCrypt proof assistant, we developed both informal “pen-and-paper” proofs and machine-checked formalizations, analyzing the extent to which our implementation upheld these security guarantees.
📄