Sigma protocols for linear relations

Fix a prime q. Boneh and Shoup's Schnorr, Okamoto, Chaum–Pedersen and generic linear protocols ([BS23], Sections 19.1 and 19.5.1–19.5.4) are one protocol, for the preimage of a ZMod q-linear map. Groups are written additively: a group of prime order q is a ZMod q-module, and the book's g ^ α is α • g. A multiplicative group of exponent q can be used through Additive with AddCommGroup.zmodModule.

In linear ψ u ι, a statement y determines a linear map ψ y : M →ₗ[ZMod q] N and a target u y : N; a witness is a preimage x with ψ y x = u y. The prover commits to ψ y r for a uniform r : M and answers the challenge c with r + c • x. Challenges come from any type C with an injection ι : C ↪ ZMod q, which covers a subset of ZMod q as well as bit strings read as numbers below q.

Completeness and special honest-verifier zero knowledge hold for every modulus. Special soundness, which divides by a difference of distinct challenges, uses that q is prime. The instances need no hypothesis that the group is cyclic or that the given elements generate it.

Main definitions

• SigmaProtocol.linear: the protocol for preimages of statement-dependent linear maps.
• SigmaProtocol.linearExtract, SigmaProtocol.linearSimulate: its extractor and simulator.
• SigmaProtocol.schnorr: knowledge of α with α • g = u (Example 19.1).
• SigmaProtocol.okamoto: knowledge of (α, β) with α • g + β • h = u (Section 19.5.1).
• SigmaProtocol.chaumPedersen: (u, v, w) is a Diffie–Hellman triple (Section 19.5.2).
• SigmaProtocol.linearSystem: a solution of ∑ j, α j • g i j = u i for all i (Section 19.5.3).

Main results

• SigmaProtocol.linear_complete, SigmaProtocol.linear_specialSoundness, SigmaProtocol.linear_specialHVZK: Theorem 19.12 for groups of prime order q.
• The same three properties for each instance, with the instance's own relation (Theorems 19.9–19.11 and Examples 19.2–19.3).

References

• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Version 0.6, Sections 19.1, 19.4 and 19.5.
• C.-P. Schnorr, Efficient Signature Generation by Smart Cards

noncomputable def Cslib.Crypto.Protocols.SigmaProtocol.linear {q : ℕ} {M N Y C : Type u} [AddCommGroup M] [Module (ZMod q) M] [Fintype M] [AddCommGroup N] [Module (ZMod q) N] [DecidableEq N] (ψ : Y → M →ₗ[ZMod q] N) (u : Y → N) (ι : C ↪ ZMod q) : SigmaProtocol M Y N C M

The Sigma protocol for a preimage of the linear map ψ y at u y ([BS23], Figures 19.8 and 19.9). The prover commits to ψ y r for a uniform r and answers the challenge c with r + ι c • x; the verifier checks ψ y z = t + ι c • u y.

def Cslib.Crypto.Protocols.SigmaProtocol.linearExtract {q : ℕ} {M N Y C : Type u} [AddCommGroup M] [Module (ZMod q) M] (ι : C ↪ ZMod q) : Y → N → (c : C) → (z : M) → (c' : C) → (z' : M) → M

The extractor divides the difference of the responses by the difference of the challenges.

noncomputable def Cslib.Crypto.Protocols.SigmaProtocol.linearSimulate {q : ℕ} {M N Y C : Type u} [AddCommGroup M] [Module (ZMod q) M] [Fintype M] [AddCommGroup N] [Module (ZMod q) N] (ψ : Y → M →ₗ[ZMod q] N) (u : Y → N) (ι : C ↪ ZMod q) (y : Y) (c : C) : PMF (N × M)

The simulator samples a uniform response and solves the verification equation for the commitment.

@[simp]

theorem Cslib.Crypto.Protocols.SigmaProtocol.linear_accepts_iff {q : ℕ} {M N Y C : Type u} [AddCommGroup M] [Module (ZMod q) M] [Fintype M] [AddCommGroup N] [Module (ZMod q) N] [DecidableEq N] (ψ : Y → M →ₗ[ZMod q] N) (u : Y → N) (ι : C ↪ ZMod q) {y : Y} {t : N} {c : C} {z : M} : (linear ψ u ι).Accepts y t c z ↔ (ψ y) z = t + ι c • u y

A conversation is accepting exactly when it satisfies the verification equation ψ y z = t + ι c • u y.

theorem Cslib.Crypto.Protocols.SigmaProtocol.linear_transcript {q : ℕ} {M N Y C : Type u} [AddCommGroup M] [Module (ZMod q) M] [Fintype M] [AddCommGroup N] [Module (ZMod q) N] [DecidableEq N] (ψ : Y → M →ₗ[ZMod q] N) (u : Y → N) (ι : C ↪ ZMod q) (x : M) (y : Y) (c : C) : (linear ψ u ι).transcript x y c = PMF.map (fun (r : M) => ((ψ y) r, r + ι c • x)) (Probability.PMF.uniformOfFintype M)

An honest transcript is (ψ y r, r + ι c • x) for a uniform r.

theorem Cslib.Crypto.Protocols.SigmaProtocol.linear_complete {q : ℕ} {M N Y C : Type u} [AddCommGroup M] [Module (ZMod q) M] [Fintype M] [AddCommGroup N] [Module (ZMod q) N] [DecidableEq N] (ψ : Y → M →ₗ[ZMod q] N) (u : Y → N) (ι : C ↪ ZMod q) : (linear ψ u ι).Complete fun (x : M) (y : Y) => (ψ y) x = u y

Honest conversations are accepting ([BS23], Theorem 19.12).

theorem Cslib.Crypto.Protocols.SigmaProtocol.linear_specialSoundness {q : ℕ} {M N Y C : Type u} [AddCommGroup M] [Module (ZMod q) M] [Fintype M] [AddCommGroup N] [Module (ZMod q) N] [DecidableEq N] (ψ : Y → M →ₗ[ZMod q] N) (u : Y → N) (ι : C ↪ ZMod q) [Fact (Nat.Prime q)] : (linear ψ u ι).SpecialSoundness (fun (x : M) (y : Y) => (ψ y) x = u y) (linearExtract ι)

linearExtract is a witness extractor when q is prime ([BS23], Theorem 19.12).

theorem Cslib.Crypto.Protocols.SigmaProtocol.linear_specialHVZK {q : ℕ} {M N Y C : Type u} [AddCommGroup M] [Module (ZMod q) M] [Fintype M] [AddCommGroup N] [Module (ZMod q) N] [DecidableEq N] (ψ : Y → M →ₗ[ZMod q] N) (u : Y → N) (ι : C ↪ ZMod q) : (linear ψ u ι).SpecialHVZK (fun (x : M) (y : Y) => (ψ y) x = u y) (linearSimulate ψ u ι)

linearSimulate is a perfect simulator at every challenge ([BS23], Theorem 19.12).

Schnorr

noncomputable def Cslib.Crypto.Protocols.SigmaProtocol.schnorr {q : ℕ} [NeZero q] {G C : Type} [AddCommGroup G] [Module (ZMod q) G] [DecidableEq G] (ι : C ↪ ZMod q) (g : G) : SigmaProtocol (ZMod q) G G C (ZMod q)

Schnorr's Sigma protocol for knowledge of α with α • g = u ([BS23], Example 19.1).

@[simp]

theorem Cslib.Crypto.Protocols.SigmaProtocol.schnorr_accepts_iff {q : ℕ} [NeZero q] {G C : Type} [AddCommGroup G] [Module (ZMod q) G] [DecidableEq G] {ι : C ↪ ZMod q} {g u t : G} {c : C} {z : ZMod q} : (schnorr ι g).Accepts u t c z ↔ z • g = t + ι c • u

Schnorr's verification equation z • g = t + c • u ([BS23], Example 19.1).

theorem Cslib.Crypto.Protocols.SigmaProtocol.schnorr_complete {q : ℕ} [NeZero q] {G C : Type} [AddCommGroup G] [Module (ZMod q) G] [DecidableEq G] {ι : C ↪ ZMod q} {g : G} : (schnorr ι g).Complete fun (α : ZMod q) (u : G) => α • g = u

theorem Cslib.Crypto.Protocols.SigmaProtocol.schnorr_specialSoundness {q : ℕ} [NeZero q] {G C : Type} [AddCommGroup G] [Module (ZMod q) G] [DecidableEq G] {ι : C ↪ ZMod q} {g : G} [Fact (Nat.Prime q)] : (schnorr ι g).SpecialSoundness (fun (α : ZMod q) (u : G) => α • g = u) (linearExtract ι)

Example 19.2 of [BS23].

theorem Cslib.Crypto.Protocols.SigmaProtocol.schnorr_specialHVZK {q : ℕ} [NeZero q] {G C : Type} [AddCommGroup G] [Module (ZMod q) G] [DecidableEq G] {ι : C ↪ ZMod q} {g : G} : (schnorr ι g).SpecialHVZK (fun (α : ZMod q) (u : G) => α • g = u) (linearSimulate (fun (x : G) => LinearMap.toSpanSingleton (ZMod q) G g) id ι)

Example 19.3 of [BS23].

Okamoto

noncomputable def Cslib.Crypto.Protocols.SigmaProtocol.okamoto {q : ℕ} [NeZero q] {G C : Type} [AddCommGroup G] [Module (ZMod q) G] [DecidableEq G] (ι : C ↪ ZMod q) (g h : G) : SigmaProtocol (ZMod q × ZMod q) G G C (ZMod q × ZMod q)

Okamoto's Sigma protocol for knowledge of a representation (α, β) of u, meaning α • g + β • h = u ([BS23], Section 19.5.1).

@[simp]

theorem Cslib.Crypto.Protocols.SigmaProtocol.okamoto_accepts_iff {q : ℕ} [NeZero q] {G C : Type} [AddCommGroup G] [Module (ZMod q) G] [DecidableEq G] {ι : C ↪ ZMod q} {g h u t : G} {c : C} {z : ZMod q × ZMod q} : (okamoto ι g h).Accepts u t c z ↔ z.1 • g + z.2 • h = t + ι c • u

Okamoto's verification equation z₁ • g + z₂ • h = t + c • u ([BS23], Section 19.5.1).

theorem Cslib.Crypto.Protocols.SigmaProtocol.okamoto_complete {q : ℕ} [NeZero q] {G C : Type} [AddCommGroup G] [Module (ZMod q) G] [DecidableEq G] {ι : C ↪ ZMod q} {g h : G} : (okamoto ι g h).Complete fun (w : ZMod q × ZMod q) (u : G) => w.1 • g + w.2 • h = u

Theorem 19.9 of [BS23]: completeness.

theorem Cslib.Crypto.Protocols.SigmaProtocol.okamoto_specialSoundness {q : ℕ} [NeZero q] {G C : Type} [AddCommGroup G] [Module (ZMod q) G] [DecidableEq G] {ι : C ↪ ZMod q} {g h : G} [Fact (Nat.Prime q)] : (okamoto ι g h).SpecialSoundness (fun (w : ZMod q × ZMod q) (u : G) => w.1 • g + w.2 • h = u) (linearExtract ι)

Theorem 19.9 of [BS23]: special soundness.

theorem Cslib.Crypto.Protocols.SigmaProtocol.okamoto_specialHVZK {q : ℕ} [NeZero q] {G C : Type} [AddCommGroup G] [Module (ZMod q) G] [DecidableEq G] {ι : C ↪ ZMod q} {g h : G} : (okamoto ι g h).SpecialHVZK (fun (w : ZMod q × ZMod q) (u : G) => w.1 • g + w.2 • h = u) (linearSimulate (fun (x : G) => (LinearMap.toSpanSingleton (ZMod q) G g).coprod (LinearMap.toSpanSingleton (ZMod q) G h)) id ι)

Theorem 19.9 of [BS23]: special honest-verifier zero knowledge.

Chaum–Pedersen

noncomputable def Cslib.Crypto.Protocols.SigmaProtocol.chaumPedersen {q : ℕ} [NeZero q] {G C : Type} [AddCommGroup G] [Module (ZMod q) G] [DecidableEq G] (ι : C ↪ ZMod q) (g : G) : SigmaProtocol (ZMod q) (G × G × G) (G × G) C (ZMod q)

The Chaum–Pedersen protocol for Diffie–Hellman triples: a witness for (u, v, w) is β with β • g = v and β • u = w ([BS23], Section 19.5.2).

@[simp]

theorem Cslib.Crypto.Protocols.SigmaProtocol.chaumPedersen_accepts_iff {q : ℕ} [NeZero q] {G C : Type} [AddCommGroup G] [Module (ZMod q) G] [DecidableEq G] {ι : C ↪ ZMod q} {g : G} {s : G × G × G} {t : G × G} {c : C} {z : ZMod q} : (chaumPedersen ι g).Accepts s t c z ↔ z • g = t.1 + ι c • s.2.1 ∧ z • s.1 = t.2 + ι c • s.2.2

The Chaum–Pedersen verification equations z • g = t₁ + c • v and z • u = t₂ + c • w ([BS23], Section 19.5.2).

theorem Cslib.Crypto.Protocols.SigmaProtocol.chaumPedersen_complete {q : ℕ} [NeZero q] {G C : Type} [AddCommGroup G] [Module (ZMod q) G] [DecidableEq G] {ι : C ↪ ZMod q} {g : G} : (chaumPedersen ι g).Complete fun (β : ZMod q) (s : G × G × G) => β • g = s.2.1 ∧ β • s.1 = s.2.2

Theorem 19.10 of [BS23]: completeness.

theorem Cslib.Crypto.Protocols.SigmaProtocol.chaumPedersen_specialSoundness {q : ℕ} [NeZero q] {G C : Type} [AddCommGroup G] [Module (ZMod q) G] [DecidableEq G] {ι : C ↪ ZMod q} {g : G} [Fact (Nat.Prime q)] : (chaumPedersen ι g).SpecialSoundness (fun (β : ZMod q) (s : G × G × G) => β • g = s.2.1 ∧ β • s.1 = s.2.2) (linearExtract ι)

Theorem 19.10 of [BS23]: special soundness.

theorem Cslib.Crypto.Protocols.SigmaProtocol.chaumPedersen_specialHVZK {q : ℕ} [NeZero q] {G C : Type} [AddCommGroup G] [Module (ZMod q) G] [DecidableEq G] {ι : C ↪ ZMod q} {g : G} : (chaumPedersen ι g).SpecialHVZK (fun (β : ZMod q) (s : G × G × G) => β • g = s.2.1 ∧ β • s.1 = s.2.2) (linearSimulate (fun (s : G × G × G) => (LinearMap.toSpanSingleton (ZMod q) G g).prod (LinearMap.toSpanSingleton (ZMod q) G s.1)) Prod.snd ι)

Theorem 19.10 of [BS23]: special honest-verifier zero knowledge.

Systems of linear equations

noncomputable def Cslib.Crypto.Protocols.SigmaProtocol.linearSystem {q : ℕ} [NeZero q] {G C : Type} [AddCommGroup G] [Module (ZMod q) G] [DecidableEq G] (ι : C ↪ ZMod q) (m n : ℕ) : SigmaProtocol (Fin n → ZMod q) ((Fin m → Fin n → G) × (Fin m → G)) (Fin m → G) C (Fin n → ZMod q)

The generic linear protocol for m equations ∑ j, α j • g i j = u i in n unknowns, with the statement (g, u) ([BS23], Section 19.5.3 and Figure 19.8).

@[simp]

theorem Cslib.Crypto.Protocols.SigmaProtocol.linearSystem_accepts_iff {q : ℕ} [NeZero q] {G C : Type} [AddCommGroup G] [Module (ZMod q) G] [DecidableEq G] {ι : C ↪ ZMod q} {m n : ℕ} {s : (Fin m → Fin n → G) × (Fin m → G)} {t : Fin m → G} {c : C} {z : Fin n → ZMod q} : (linearSystem ι m n).Accepts s t c z ↔ ∀ (i : Fin m), ∑ j : Fin n, z j • s.1 i j = t i + ι c • s.2 i

The generic linear protocol checks each equation ∑ j, z j • g i j = t i + c • u i ([BS23], Figure 19.8).

theorem Cslib.Crypto.Protocols.SigmaProtocol.linearSystem_complete {q : ℕ} [NeZero q] {G C : Type} [AddCommGroup G] [Module (ZMod q) G] [DecidableEq G] {ι : C ↪ ZMod q} {m n : ℕ} : (linearSystem ι m n).Complete fun (α : Fin n → ZMod q) (s : (Fin m → Fin n → G) × (Fin m → G)) => ∀ (i : Fin m), ∑ j : Fin n, α j • s.1 i j = s.2 i

Theorem 19.11 of [BS23]: completeness.

theorem Cslib.Crypto.Protocols.SigmaProtocol.linearSystem_specialSoundness {q : ℕ} [NeZero q] {G C : Type} [AddCommGroup G] [Module (ZMod q) G] [DecidableEq G] {ι : C ↪ ZMod q} {m n : ℕ} [Fact (Nat.Prime q)] : (linearSystem ι m n).SpecialSoundness (fun (α : Fin n → ZMod q) (s : (Fin m → Fin n → G) × (Fin m → G)) => ∀ (i : Fin m), ∑ j : Fin n, α j • s.1 i j = s.2 i) (linearExtract ι)

Theorem 19.11 of [BS23]: special soundness.

theorem Cslib.Crypto.Protocols.SigmaProtocol.linearSystem_specialHVZK {q : ℕ} [NeZero q] {G C : Type} [AddCommGroup G] [Module (ZMod q) G] [DecidableEq G] {ι : C ↪ ZMod q} {m n : ℕ} : (linearSystem ι m n).SpecialHVZK (fun (α : Fin n → ZMod q) (s : (Fin m → Fin n → G) × (Fin m → G)) => ∀ (i : Fin m), ∑ j : Fin n, α j • s.1 i j = s.2 i) (linearSimulate (fun (s : (Fin m → Fin n → G) × (Fin m → G)) => LinearMap.pi fun (i : Fin m) => Fintype.linearCombination (ZMod q) (s.1 i)) Prod.snd ι)

Theorem 19.11 of [BS23]: special honest-verifier zero knowledge.