Lyubashevsky's identification protocol

Lyubashevsky's lattice-based identification protocol ([Lyu09], [Lyu12]), with the uniform-box rejection sampling of Dilithium ([DKL+18]), as a Sigma protocol with aborts. The statement is a pair (A, T) of matrices over ZMod q, of sizes n × m and n × k; a witness is an integer matrix S with small entries and A S = T. Challenges are bit strings c ∈ {0,1}^k, read as integer vectors ĉ (lyubashevskyChallenge).

• The prover draws y uniformly from the box [-γ, γ]^m and commits to w = A y.
• On the challenge c it computes z = y + S ĉ. It answers z when z lies in the inner box [-(γ - β), γ - β]^m, and aborts otherwise.
• The verifier accepts z when z lies in the inner box and A z = w + T ĉ.

When every entry of S is at most η in absolute value and k η ≤ β ≤ γ:

• Completeness (lyubashevsky_nonAbortComplete). Every answer the prover gives is accepted, for any S with A S = T. At every challenge the prover aborts with probability exactly 1 - ((2 (γ - β) + 1) / (2 γ + 1)) ^ m, which is at most 2 m β / (2 γ + 1).
• Special soundness (lyubashevsky_specialSoundness). Two accepting conversations (w, c, z) and (w, c', z') with c ≠ c' give (z - z', ĉ' - ĉ), a short integer solution for [A | T] with bound max (2 (γ - β)) 1. As usual for lattice protocols, the extracted witness belongs to this relaxed relation, not to the prover's.
• Zero knowledge up to aborts (lyubashevsky_nonAbortSpecialHVZK). At each challenge, the simulator draws z uniformly from [-γ, γ]^m, aborts unless z lies in the inner box, and solves for w = A z - T ĉ. It has exactly the law of the honest prover's published transcripts and aborts. The proof is the box rejection-sampling lemma (Cslib.Probability.PMF.boxReject_eq).

All statements are exact laws over PMF. The protocol's samplers are not claimed to be efficient, and no hardness assumption is used here.

Main definitions

• SigmaProtocol.lyubashevsky: the protocol.
• SigmaProtocol.lyubashevskyRelation: witnesses with small entries.
• SigmaProtocol.lyubashevskyExtract, SigmaProtocol.lyubashevskySimulate: its extractor and simulator.

Main results

• SigmaProtocol.lyubashevsky_nonAbortComplete: answers are always accepted.
• SigmaProtocol.lyubashevsky_acceptedTranscript_none, SigmaProtocol.lyubashevsky_acceptedTranscript_none_le: the exact abort probability and its bound.
• SigmaProtocol.lyubashevsky_specialSoundness: extraction of a short integer solution.
• SigmaProtocol.lyubashevsky_nonAbortSpecialHVZK: exact zero knowledge up to aborts.

References

• V. Lyubashevsky, Fiat-Shamir with Aborts: Applications to Lattice and Factoring-Based Signatures
• V. Lyubashevsky, Lattice Signatures without Trapdoors
• L. Ducas et al., CRYSTALS-Dilithium: A Lattice-Based Digital Signature Scheme

def Cslib.Crypto.Protocols.SigmaProtocol.lyubashevskyChallenge {k : ℕ} (c : BitString k) : Fin k → ℤ

A bit-string challenge as a 0-1 integer vector.

noncomputable def Cslib.Crypto.Protocols.SigmaProtocol.lyubashevsky (n m k q γ β : ℕ) : SigmaProtocol (Matrix (Fin m) (Fin k) ℤ) (Matrix (Fin n) (Fin m) (ZMod q) × Matrix (Fin n) (Fin k) (ZMod q)) (Fin n → ZMod q) (BitString k) (Option (Fin m → ℤ))

Lyubashevsky's identification protocol with box rejection sampling, for statements (A, T) and witnesses S with A S = T. The prover commits to A y for y uniform in [-γ, γ]^m, and answers the challenge c with y + S ĉ if it lies in [-(γ - β), γ - β]^m, and aborts otherwise. The verifier checks that the answer z lies in that box and that A z = w + T ĉ.

def Cslib.Crypto.Protocols.SigmaProtocol.lyubashevskyRelation {n m k q : ℕ} (η : ℕ) (S : Matrix (Fin m) (Fin k) ℤ) (y : Matrix (Fin n) (Fin m) (ZMod q) × Matrix (Fin n) (Fin k) (ZMod q)) : Prop

The witness relation: A S = T modulo q, and every entry of S lies in [-η, η].

@[instance_reducible]

instance Cslib.Crypto.Protocols.SigmaProtocol.instDecidableLyubashevskyRelation {n m k q : ℕ} (η : ℕ) (S : Matrix (Fin m) (Fin k) ℤ) (y : Matrix (Fin n) (Fin m) (ZMod q) × Matrix (Fin n) (Fin k) (ZMod q)) : Decidable (lyubashevskyRelation η S y)

def Cslib.Crypto.Protocols.SigmaProtocol.lyubashevskyExtract (n m k q : ℕ) : Matrix (Fin n) (Fin m) (ZMod q) × Matrix (Fin n) (Fin k) (ZMod q) → (Fin n → ZMod q) → (c : BitString k) → (z : Option (Fin m → ℤ)) → (c' : BitString k) → (z' : Option (Fin m → ℤ)) → Fin m ⊕ Fin k → ℤ

The extractor returns (z - z', ĉ' - ĉ), a kernel vector of [A | T].

noncomputable def Cslib.Crypto.Protocols.SigmaProtocol.lyubashevskySimulate (n m k q γ β : ℕ) (y : Matrix (Fin n) (Fin m) (ZMod q) × Matrix (Fin n) (Fin k) (ZMod q)) (c : BitString k) : PMF (Option ((Fin n → ZMod q) × (Fin m → ℤ)))

The simulator draws z by rejection sampling with no shift, uniformly from [-γ, γ]^m and kept only inside [-(γ - β), γ - β]^m, and solves the verification equation for the commitment.

@[simp]

theorem Cslib.Crypto.Protocols.SigmaProtocol.lyubashevsky_not_accepts_none {n m k q γ β : ℕ} {y : Matrix (Fin n) (Fin m) (ZMod q) × Matrix (Fin n) (Fin k) (ZMod q)} {w : Fin n → ZMod q} {c : BitString k} : ¬(lyubashevsky n m k q γ β).Accepts y w c none

The verifier rejects aborts.

@[simp]

theorem Cslib.Crypto.Protocols.SigmaProtocol.lyubashevsky_accepts_some_iff {n m k q γ β : ℕ} {y : Matrix (Fin n) (Fin m) (ZMod q) × Matrix (Fin n) (Fin k) (ZMod q)} {w : Fin n → ZMod q} {c : BitString k} {z : Fin m → ℤ} : (lyubashevsky n m k q γ β).Accepts y w c (some z) ↔ z ∈ Probability.intBox (Fin m) (γ - β) ∧ y.1.mulVec (Int.cast ∘ z) = w + y.2.mulVec (Int.cast ∘ lyubashevskyChallenge c)

The verifier accepts an answer in the inner box that satisfies the linear equation.

theorem Cslib.Crypto.Protocols.SigmaProtocol.lyubashevsky_acceptedTranscript {n m k q γ β : ℕ} (S : Matrix (Fin m) (Fin k) ℤ) (y : Matrix (Fin n) (Fin m) (ZMod q) × Matrix (Fin n) (Fin k) (ZMod q)) (c : BitString k) : (lyubashevsky n m k q γ β).acceptedTranscript S y c = PMF.map (Option.map fun (z : Fin m → ℤ) => (y.1.mulVec (Int.cast ∘ (z - S.mulVec (lyubashevskyChallenge c))), z)) (Probability.PMF.boxReject (Fin m) γ β (S.mulVec (lyubashevskyChallenge c)))

The accepted view at a challenge is box rejection sampling shifted by S ĉ, with the commitment A (z - S ĉ) of the published answer z.

theorem Cslib.Crypto.Protocols.SigmaProtocol.lyubashevsky_nonAbortComplete {n m k q γ β : ℕ} : (lyubashevsky n m k q γ β).NonAbortComplete fun (S : Matrix (Fin m) (Fin k) ℤ) (y : Matrix (Fin n) (Fin m) (ZMod q) × Matrix (Fin n) (Fin k) (ZMod q)) => y.1 * S.map Int.cast = y.2

Completeness up to aborts. Every answer of the honest prover is accepted, for any witness with A S = T, however large its entries.

theorem Cslib.Crypto.Protocols.SigmaProtocol.lyubashevsky_acceptedTranscript_none {n m k q γ β η : ℕ} (hβ : β ≤ γ) (hη : k * η ≤ β) {S : Matrix (Fin m) (Fin k) ℤ} (hS : ∀ (i : Fin m) (j : Fin k), |S i j| ≤ ↑η) (y : Matrix (Fin n) (Fin m) (ZMod q) × Matrix (Fin n) (Fin k) (ZMod q)) (c : BitString k) : ((lyubashevsky n m k q γ β).acceptedTranscript S y c) none = 1 - (↑(2 * (γ - β) + 1) / (2 * ↑γ + 1)) ^ m

Abort probability. If the entries of S are at most η and k η ≤ β ≤ γ, then at every challenge the prover aborts with probability exactly 1 - ((2 (γ - β) + 1) / (2 γ + 1)) ^ m.

theorem Cslib.Crypto.Protocols.SigmaProtocol.lyubashevsky_acceptedTranscript_none_le {n m k q γ β η : ℕ} (hβ : β ≤ γ) (hη : k * η ≤ β) {S : Matrix (Fin m) (Fin k) ℤ} (hS : ∀ (i : Fin m) (j : Fin k), |S i j| ≤ ↑η) (y : Matrix (Fin n) (Fin m) (ZMod q) × Matrix (Fin n) (Fin k) (ZMod q)) (c : BitString k) : ((lyubashevsky n m k q γ β).acceptedTranscript S y c) none ≤ 2 * ↑m * ↑β / (2 * ↑γ + 1)

Abort bound. Under the same hypotheses, the prover aborts with probability at most 2 m β / (2 γ + 1) at every challenge.

theorem Cslib.Crypto.Protocols.SigmaProtocol.lyubashevsky_specialSoundness {n m k q γ β : ℕ} : (lyubashevsky n m k q γ β).SpecialSoundness (fun (u : Fin m ⊕ Fin k → ℤ) (y : Matrix (Fin n) (Fin m) (ZMod q) × Matrix (Fin n) (Fin k) (ZMod q)) => SIS.IsSolution (y.1.fromCols y.2) (max (2 * (γ - β)) 1) u) (lyubashevskyExtract n m k q)

Special soundness. From two accepting conversations with a common commitment and distinct challenges, lyubashevskyExtract computes a short integer solution for [A | T] with bound max (2 (γ - β)) 1.

theorem Cslib.Crypto.Protocols.SigmaProtocol.lyubashevsky_nonAbortSpecialHVZK {n m k q γ β η : ℕ} (hβ : β ≤ γ) (hη : k * η ≤ β) : (lyubashevsky n m k q γ β).NonAbortSpecialHVZK (lyubashevskyRelation η) (lyubashevskySimulate n m k q γ β)

Zero knowledge up to aborts. If k η ≤ β ≤ γ, then for every witness in lyubashevskyRelation η and every challenge, lyubashevskySimulate has exactly the law of the prover's published transcripts and aborts.