Lean Formalization of Sigma Protocols

Warning

This is a proof of concept and a work in progress.

A formalization of sigma protocols in Lean 4 with Mathlib, with the Schnorr identification protocol as the first instance.

Contents

• Sigma/Basic.lean: the general framework. Defines Prover, Verifier, Transcript, and SigmaProtocol, honest execution, and the security notions Completeness and SpecialSoundness (via WitnessExtractor).
• Sigma/Schnorr.lean: the Schnorr identification protocol over a finite commutative group of prime order q, for the discrete-logarithm relation x = g^α. Proves:
  • SchnorrId.completeness: perfect completeness.
  • SchnorrId.special_soundness: an explicit extractor recovers the DLog witness from two accepting transcripts with the same commitment and distinct challenges.

Building

Requires elan; the toolchain (Lean 4.31.0) is pinned in lean-toolchain.

lake exe cache get   # fetch prebuilt Mathlib
lake build