leanprover · ChristianoBraga · Apr 6, 2026 · Apr 6, 2026 · Apr 6, 2026
@@ -112,6 +112,9 @@ public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiSubst
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StrongNorm
 public import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic
+public import Cslib.Systems.Distributed.Protocols.Cryptographic.Sigma.Basic
+public import Cslib.Systems.Distributed.Protocols.Cryptographic.Sigma.SchnorrId
+public import Cslib.Systems.Distributed.Protocols.Cryptographic.Sigma.Properties
 public import Cslib.Logics.HML.Basic
 public import Cslib.Logics.HML.LogicalEquivalence
 public import Cslib.Logics.LinearLogic.CLL.Basic

@@ -0,0 +1,72 @@
+/-
+Copyright (c) 2026 Christiano Braga. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christiano Braga
+-/
+
+module
+
+public import Mathlib.Tactic
+
+@[expose] public section
+
+/-!
+A Sigma Protocol for R is a pair (P, V).
+
+- P is an interactive protocol algorithm called the prover, which takes as input a witness-statement
+  pair (x, y) ∈ R.
+- V is an interactive protocol algorithm called the verifier, which takes as input a statement
+  y ∈ Y, and which outputs accept or reject.
+- P and V are structured so that an interaction between them always works as follows:
+
+1. To start the protocol, P computes a message t, called the commitment, and sends t to V.
+2. Upon receiving P's commitment t, V chooses a challenge c at random from a finite challenge space
+   C, and sends c to P.
+3. Upon receiving V's challenge c, P computes a response z, and sends z to V.
+4. Upon receiving P's response z, V outputs either accept or reject, which must be computed strictly
+   as a function of the statement y and the conversation (t, c, z). In particular, V does not make
+   any random choices other than the selection of the challenge — all other computations are
+   completely deterministic.
+
+Reference:
+
+* [D. Boneh and V. Shoup, *A Graduate Course in Applied Cryptography*][BonehShoup],
+  Section 19.4.
+
+Note: The notion of an _effective relation_ is implicit in the definition of a Sigma protocol.
+      The relation R must be decidable, and the prover must be able to efficiently compute the
+      commitment and response functions, while the verifier must be able to efficiently compute
+      the verification function. In practice, these efficiency requirements are crucial for
+      the security and usability of the protocol, but they are not explicitly formalized in this
+      definition.
+-/
+
+universe u v w x y
+
+class SigmaProtocol
+    (Statement : Type u) (Witness : Type v)
+    (Commitment : Type w) (Challenge : Type x)
+    (Response : Type y) where
+  rel : Statement → Witness → Prop
+  commit : Statement → Witness → Commitment
+  respond : Statement → Witness → Commitment → Challenge → Response
+  verify : Statement → Commitment → Challenge → Response → Prop
+  extract : Statement → Commitment →
+            Challenge → Response →
+            Challenge → Response → Witness
+  simulate : Statement → Challenge → Commitment × Response
+  -- Non-degeneracy: the relation is inhabited for some statement-witness pair,
+  -- ensuring that completeness is not vacuously true.
+  nonDegenerate : ∃ (s : Statement) (w : Witness), rel s w
+  -- Properties that every instance must satisfy
+  complete : ∀ (s : Statement) (w : Witness) (e : Challenge),
+               rel s w →
+               verify s (commit s w) e (respond s w (commit s w) e)
+  sound    : ∀ (s : Statement) (a : Commitment) (e e' : Challenge) (z z' : Response),
+               e ≠ e' →
+               verify s a e z →
+               verify s a e' z' →
+               rel s (extract s a e z e' z')
+  shvzk    : ∀ (s : Statement) (e : Challenge),
+               let (a, z) := simulate s e
+               verify s a e z
@@ -0,0 +1,186 @@
+/-
+Copyright (c) 2026 Christiano Braga. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christiano Braga
+-/
+
+module
+
+public import Mathlib.Tactic
+public import Cslib.Systems.Distributed.Protocols.Cryptographic.Sigma.Basic
+
+@[expose] public section
+
+/-!
+# Algebraic Properties of Sigma Protocols
+
+This file establishes compositional properties of sigma protocols:
+
+- **AND-composition**: Given sigma protocols for relations R₁ and R₂ over the same challenge
+  space, we construct a sigma protocol for R₁ ∧ R₂. Both sub-protocols run in parallel with
+  the same challenge.
+
+- **OR-composition**: Given sigma protocols for relations R₁ and R₂ over an additive group
+  challenge space, we construct a sigma protocol for R₁ ∨ R₂. The prover simulates the
+  protocol for the unknown statement and splits the challenge as e = e₁ + e₂.
+
+- **Witness indistinguishability**: The simulator output is independent of any particular
+  witness, so the verifier cannot determine which witness was used.
+
+Reference:
+
+* [D. Boneh and V. Shoup, *A Graduate Course in Applied Cryptography*][BonehShoup],
+  Sections 19.5, 19.6.
+-/
+
+private theorem shvzk_elim {S : Type*} {W : Type*} {C : Type*} {Ch : Type*} {R : Type*}
+    [P : SigmaProtocol S W C Ch R] (s : S) (e : Ch) :
+    P.verify s (P.simulate s e).1 e (P.simulate s e).2 := by
+  have h := P.shvzk s e
+  revert h; generalize P.simulate s e = p; obtain ⟨a, z⟩ := p; grind
+
+section ANDComposition
+
+/-!
+## AND-Composition
+
+Given two sigma protocols P₁ and P₂ sharing the same challenge type Ch, we build a
+sigma protocol for the conjunction of their relations. Both sub-protocols run in parallel
+with the same challenge.
+-/
+
+instance SigmaAND
+    {S₁ : Type*} {W₁ : Type*} {C₁ : Type*} {Ch : Type*} {R₁ : Type*}
+    {S₂ : Type*} {W₂ : Type*} {C₂ : Type*} {R₂ : Type*}
+    [P₁ : SigmaProtocol S₁ W₁ C₁ Ch R₁]
+    [P₂ : SigmaProtocol S₂ W₂ C₂ Ch R₂] :
+    SigmaProtocol (S₁ × S₂) (W₁ × W₂) (C₁ × C₂) Ch (R₁ × R₂) where
+  rel := fun s w => P₁.rel s.1 w.1 ∧ P₂.rel s.2 w.2
+  commit := fun s w => (P₁.commit s.1 w.1, P₂.commit s.2 w.2)
+  respond := fun s w a e => (P₁.respond s.1 w.1 a.1 e, P₂.respond s.2 w.2 a.2 e)
+  verify := fun s a e z => P₁.verify s.1 a.1 e z.1 ∧ P₂.verify s.2 a.2 e z.2
+  extract := fun s a e z e' z' =>
+    (P₁.extract s.1 a.1 e z.1 e' z'.1, P₂.extract s.2 a.2 e z.2 e' z'.2)
+  simulate := fun s e =>
+    let p₁ := P₁.simulate s.1 e
+    let p₂ := P₂.simulate s.2 e
+    ((p₁.1, p₂.1), (p₁.2, p₂.2))
+  nonDegenerate := by
+    obtain ⟨s₁, w₁, h₁⟩ := P₁.nonDegenerate
+    obtain ⟨s₂, w₂, h₂⟩ := P₂.nonDegenerate
+    exact ⟨(s₁, s₂), (w₁, w₂), h₁, h₂⟩
+  complete := by
+    intro ⟨s₁, s₂⟩ ⟨w₁, w₂⟩ e ⟨h₁, h₂⟩
+    grind [P₁.complete, P₂.complete]
+  sound := by
+    intro ⟨s₁, s₂⟩ ⟨a₁, a₂⟩ e e' ⟨z₁, z₂⟩ ⟨z₁', z₂'⟩ hne ⟨hv₁, hv₂⟩ ⟨hv₁', hv₂'⟩
+    grind [P₁.sound, P₂.sound]
+  shvzk := by
+    intro ⟨s₁, s₂⟩ e
+    exact ⟨shvzk_elim s₁ e, shvzk_elim s₂ e⟩
+
+end ANDComposition
+
+section ORComposition
+
+/-!
+## OR-Composition
+
+Given two sigma protocols P₁ and P₂ whose challenge type Ch forms an additive commutative
+group with decidable equality, we build a sigma protocol for the disjunction of their
+relations.
+
+The prover, who knows a witness for one of the two statements, simulates the transcript for
+the other statement and splits the verifier's challenge as e = e₁ + e₂.
+
+The witness type is `(W₁ × Ch) ⊕ (Ch × W₂)`:
+- `Sum.inl (w₁, e₂)`: prover knows w₁ for s₁, picks e₂ to simulate P₂
+- `Sum.inr (e₁, w₂)`: prover knows w₂ for s₂, picks e₁ to simulate P₁
+-/
+
+instance SigmaOR
+    {S₁ : Type*} {W₁ : Type*} {C₁ : Type*} {Ch : Type*} {R₁ : Type*}
+    {S₂ : Type*} {W₂ : Type*} {C₂ : Type*} {R₂ : Type*}
+    [P₁ : SigmaProtocol S₁ W₁ C₁ Ch R₁]
+    [P₂ : SigmaProtocol S₂ W₂ C₂ Ch R₂]
+    [AddCommGroup Ch] [DecidableEq Ch] :
+    SigmaProtocol (S₁ × S₂) ((W₁ × Ch) ⊕ (Ch × W₂)) (C₁ × C₂) Ch (R₁ × R₂ × Ch) where
+  rel := fun s w => match w with
+    | .inl (w₁, _) => P₁.rel s.1 w₁
+    | .inr (_, w₂) => P₂.rel s.2 w₂
+  commit := fun s w => match w with
+    | .inl (w₁, e₂) =>
+      (P₁.commit s.1 w₁, (P₂.simulate s.2 e₂).1)
+    | .inr (e₁, w₂) =>
+      ((P₁.simulate s.1 e₁).1, P₂.commit s.2 w₂)
+  respond := fun s w a e => match w with
+    | .inl (w₁, e₂) =>
+      (P₁.respond s.1 w₁ a.1 (e - e₂), (P₂.simulate s.2 e₂).2, e - e₂)
+    | .inr (e₁, w₂) =>
+      ((P₁.simulate s.1 e₁).2, P₂.respond s.2 w₂ a.2 (e - e₁), e₁)
+  verify := fun s a e z =>
+    let (z₁, z₂, e₁) := z
+    P₁.verify s.1 a.1 e₁ z₁ ∧ P₂.verify s.2 a.2 (e - e₁) z₂
+  extract := fun s a e z e' z' =>
+    let e₁ := z.2.2
+    let e₁' := z'.2.2
+    if e₁ ≠ e₁' then
+      .inl (P₁.extract s.1 a.1 e₁ z.1 e₁' z'.1, 0)
+    else
+      .inr (0, P₂.extract s.2 a.2 (e - e₁) z.2.1 (e' - e₁') z'.2.1)
+  simulate := fun s e =>
+    let p₁ := P₁.simulate s.1 0
+    let p₂ := P₂.simulate s.2 e
+    ((p₁.1, p₂.1), (p₁.2, p₂.2, 0))
+  nonDegenerate := by
+    obtain ⟨s₁, w₁, h₁⟩ := P₁.nonDegenerate
+    obtain ⟨s₂, _, _⟩ := P₂.nonDegenerate
+    exact ⟨(s₁, s₂), .inl (w₁, 0), h₁⟩
+  complete := by
+    intro ⟨s₁, s₂⟩ w e hw
+    match w, hw with
+    | .inl (w₁, e₂), hw =>
+      refine ⟨P₁.complete s₁ w₁ (e - e₂) hw, ?_⟩
+      have : e - (e - e₂) = e₂ := by abel
+      rw [this]
+      exact shvzk_elim s₂ e₂
+    | .inr (e₁, w₂), hw =>
+      refine ⟨shvzk_elim s₁ e₁, ?_⟩
+      exact P₂.complete s₂ w₂ (e - e₁) hw
+  sound := by
+    intro ⟨s₁, s₂⟩ ⟨a₁, a₂⟩ e e' ⟨z₁, z₂, e₁⟩ ⟨z₁', z₂', e₁'⟩ hne ⟨hv₁, hv₂⟩ ⟨hv₁', hv₂'⟩
+    simp only [ne_eq]
+    by_cases h : e₁ = e₁'
+    · subst h
+      simp only [not_true_eq_false, ↓reduceIte]
+      have hne₂ : e - e₁ ≠ e' - e₁ := fun heq => hne (by
+        have : e - e₁ + e₁ = e' - e₁ + e₁ := by rw [heq]
+        rwa [sub_add_cancel, sub_add_cancel] at this)
+      exact P₂.sound s₂ a₂ (e - e₁) (e' - e₁) z₂ z₂' hne₂ hv₂ hv₂'
+    · simp only [h, not_false_eq_true, ↓reduceIte]
+      exact P₁.sound s₁ a₁ e₁ e₁' z₁ z₁' h hv₁ hv₁'
+  shvzk := by
+    intro ⟨s₁, s₂⟩ e
+    exact ⟨shvzk_elim s₁ (0 : Ch), by simp only [sub_zero]; exact shvzk_elim s₂ e⟩
+
+end ORComposition
+
+section WitnessIndistinguishability
+
+/-!
+## Witness Indistinguishability
+
+A sigma protocol with SHVZK is witness-indistinguishable for honest verifiers: the simulator
+produces valid transcripts without access to any witness. This means the simulated transcript
+is consistent with *every* valid witness — the verifier learns nothing about *which* witness
+the prover holds.
+-/
+
+theorem simulator_independent_of_witness
+    {S : Type*} {W : Type*} {C : Type*} {Ch : Type*} {R : Type*}
+    [P : SigmaProtocol S W C Ch R]
+    (s : S) (e : Ch) :
+    P.verify s (P.simulate s e).1 e (P.simulate s e).2 :=
+  shvzk_elim s e
+
+end WitnessIndistinguishability
@@ -0,0 +1,111 @@
+/-
+Copyright (c) 2026 Christiano Braga. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christiano Braga
+-/
+
+module
+
+public import Mathlib.Tactic
+public import Cslib.Systems.Distributed.Protocols.Cryptographic.Sigma.Basic
+
+@[expose] public section
+
+/-!
+# Schnorr Identification Protocol
+
+Schnorr's Identification Protocol can be understood as an instance of a sigma protocol.
+
+Let 𝔾 be a cyclic group of prime order q, and let g be a generator of 𝔾.
+The prover's secret key is α ←ᴿ ℤ_q, and the corresponding public key is u := gᵅ ∈ 𝔾.
+
+The protocol proceeds as in a sigma protocol, as follows:
+
+1. Commitment: The prover picks αₜ ←ᴿ ℤ_q, computes uₜ := gᵅᵗ, and sends uₜ to the verifier.
+2. Challenge: The verifier picks c ←ᴿ ℤ_q and sends c to the prover.
+3. Response: The prover computes α_z := αₜ + α · c (mod q) and sends α_z to the verifier.
+4. Verification: The verifier accepts if and only if gᵅᶻ = uₜ · uᶜ.
+
+Reference:
+
+* [D. Boneh and V. Shoup,V., *A Graduate Course in Applied Cryptography*,
+  Schnorr Identification Protocol][BonehShoup], Section 19.1.
+-/
+
+-- TODO: The helpers `pow_mod_q`, `pow_val_mul`, and `pow_val_sub` are general lemmas
+-- about exponentiation in groups of finite order over `ZMod q`. They should eventually
+-- be moved to a module near `ZMod` (e.g., `Mathlib.Data.ZMod.Basic` or a dedicated file).
+section SchnorrHelpers
+
+variable {G : Type u} [CommGroup G] {q : ℕ} [Fact q.Prime]
+variable (hG : ∀ x : G, x ^ q = 1)
+include hG
+
+/-
+pow_mod_q — Exponents can be reduced mod q.
+Uses the division algorithm: n = q · (n / q) + (n mod q), then hG to collapse (x^q)^(n/q) to 1.
+-/
+omit [Fact q.Prime] in
+private lemma pow_mod_q (y : G) (n : ℕ) : y ^ (n % q) = y ^ n := by
+  conv_rhs => rw [← Nat.div_add_mod n q]
+  rw [pow_add, pow_mul, hG y, one_pow, one_mul]
+
+/-
+pow_val_mul — Multiplication in ℤ/qℤ corresponds to iterated exponentiation.
+Combines ZMod.val_mul with pow_mod_q and pow_mul.
+-/
+omit [Fact q.Prime] in
+private lemma pow_val_mul (y : G) (a b : ZMod q) :
+    y ^ (a * b).val = (y ^ a.val) ^ b.val := by
+  rw [ZMod.val_mul, pow_mod_q hG, pow_mul]
+
+/-
+pow_val_sub — Subtraction in ℤ/qℤ corresponds to division in G.
+Shows y^(a-b) · y^b = y^a via ZMod.val_add and sub_add_cancel,
+then concludes by dividing both sides by y^b.
+-/
+private lemma pow_val_sub (y : G) (a b : ZMod q) :
+    y ^ (a - b).val = y ^ a.val * (y ^ b.val)⁻¹ := by
+  have h : y ^ (a - b).val * y ^ b.val = y ^ a.val := by
+    rw [← pow_add, ← pow_mod_q hG y ((a - b).val + b.val)]
+    congr 1; rw [← ZMod.val_add, sub_add_cancel]
+  exact eq_mul_inv_of_mul_eq h
+
+end SchnorrHelpers
+
+instance SchnorrProtocol {G : Type u} [CommGroup G] (g : G) (q : ℕ) [Fact q.Prime]
+    (hG : ∀ x : G, x ^ q = 1) :
+    SigmaProtocol G (ZMod q × ZMod q) G (ZMod q) (ZMod q) where
+  rel      := fun x rw => x = g ^ rw.2.val
+  commit   := fun _ rw => g ^ rw.1.val
+  respond  := fun _ rw _ e => rw.1 + e * rw.2
+  verify   := fun x a e z => g ^ z.val = a * x ^ e.val
+  extract  := fun _ _ e z e' z' => (0, (z - z') * (e - e')⁻¹)
+  simulate := fun x e => (g ^ (0 : ZMod q).val * (x ^ e.val)⁻¹, 0)
+  nonDegenerate := ⟨g ^ (0 : ZMod q).val, (0, 0), by simp⟩
+  complete := by
+    intro s w e hrel
+    subst hrel
+    have hval : (w.1 + e * w.2).val = (w.1.val + e.val * w.2.val) % q := by
+      simp [ZMod.val_add, ZMod.val_mul, Nat.add_mod,
+          Nat.mod_eq_of_lt (Nat.mod_lt _ (Nat.Prime.pos (Fact.out)))]
+    rw [hval, pow_mod_q hG, pow_add, mul_comm e.val w.2.val, pow_mul]
+  sound := by
+    intro x a e e' z z' hne hv hv'
+    simp only
+    have h1 : g ^ z.val * (g ^ z'.val)⁻¹ = x ^ e.val * (x ^ e'.val)⁻¹ := by
+      rw [hv, hv']; group
+      simp only [ZMod.natCast_val, Int.reduceNeg, zpow_neg, zpow_one, mul_inv_cancel_comm]
+    have hdiff : g ^ (z - z').val = x ^ (e - e').val := by
+      rw [pow_val_sub hG g z z', pow_val_sub hG x e e', h1]
+    calc x
+        = x ^ (1 : ZMod q).val := by rw [ZMod.val_one q, pow_one]
+      _ = x ^ ((e - e') * (e - e')⁻¹).val := by
+            congr 1; congr 1; exact (mul_inv_cancel₀ (sub_ne_zero.mpr hne)).symm
+      _ = (x ^ (e - e').val) ^ (e - e')⁻¹.val := pow_val_mul hG x _ _
+      _ = (g ^ (z - z').val) ^ (e - e')⁻¹.val := by rw [hdiff]
+      _ = g ^ ((z - z') * (e - e')⁻¹).val := (pow_val_mul hG g _ _).symm
+  shvzk := by
+    intro x e; simp only; group
+
+end
@@ -1,3 +1,11 @@
+@book{BonehShoup,
+  author    = {Boneh, Dan and Shoup, Victor},
+  title     = {A Graduate Course in Applied Cryptography},
+  year      = {2023},
+  publisher = {Self-published},
+  note      = {Version 0.6. Available at \url{https://toc.cryptobook.us/}}
+}
+
 @inproceedings{Aceto1999,
   author       = {Luca Aceto and
                   Anna Ing{\'{o}}lfsd{\'{o}}ttir},