AND and OR composition of Sigma protocols

Two Sigma protocols with a common challenge type combine into protocols proving knowledge of witnesses for both statements, or for at least one of them, without revealing which ([BS23], Section 19.7).

The AND-proof runs both protocols in parallel and sends the same challenge to both. The OR-proof needs the challenges to form a finite additive group; Boneh and Shoup use {0, 1}ⁿ with exclusive or, which is the bit-string group with +. A prover with a witness for one statement simulates the other side with a challenge of its own choice, and answers the verifier's challenge c by splitting it as c₀ + c₁. A witness for the OR relation is Sum.inl x₀ or Sum.inr x₁. The honest OR prover is determined by the two simulators, which are therefore parameters of orProof.

Main definitions

• SigmaProtocol.andProof, SigmaProtocol.andExtract, SigmaProtocol.andSimulate.
• SigmaProtocol.orRelation, SigmaProtocol.orProof, SigmaProtocol.orExtract, SigmaProtocol.orSimulate.

Main results

• SigmaProtocol.andProof_complete, SigmaProtocol.andProof_specialSoundness, SigmaProtocol.andProof_specialHVZK: Theorem 19.18.
• SigmaProtocol.orProof_complete, SigmaProtocol.orProof_specialSoundness, SigmaProtocol.orProof_specialHVZK: Theorem 19.19.

References

• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Version 0.6, Section 19.7.
• R. Cramer, I. Damgård, B. Schoenmakers, Proofs of Partial Knowledge and Simplified Design of Witness Hiding Protocols

AND

noncomputable def Cslib.Crypto.Protocols.SigmaProtocol.andProof {X₀ Y₀ T₀ Z₀ X₁ Y₁ T₁ Z₁ C : Type u} (P₀ : SigmaProtocol X₀ Y₀ T₀ C Z₀) (P₁ : SigmaProtocol X₁ Y₁ T₁ C Z₁) : SigmaProtocol (X₀ × X₁) (Y₀ × Y₁) (T₀ × T₁) C (Z₀ × Z₁)

The AND-proof ([BS23], Section 19.7.1): commit with both provers and answer the shared challenge with both.

def Cslib.Crypto.Protocols.SigmaProtocol.andExtract {X₀ Y₀ T₀ Z₀ X₁ Y₁ T₁ Z₁ C : Type u} (extract₀ : Y₀ → T₀ → C → Z₀ → C → Z₀ → X₀) (extract₁ : Y₁ → T₁ → C → Z₁ → C → Z₁ → X₁) (y : Y₀ × Y₁) (t : T₀ × T₁) (c : C) (z : Z₀ × Z₁) (c' : C) (z' : Z₀ × Z₁) : X₀ × X₁

The AND extractor applies each extractor to its half of the conversations.

noncomputable def Cslib.Crypto.Protocols.SigmaProtocol.andSimulate {Y₀ T₀ Z₀ Y₁ T₁ Z₁ C : Type u} (simulate₀ : Y₀ → C → PMF (T₀ × Z₀)) (simulate₁ : Y₁ → C → PMF (T₁ × Z₁)) (y : Y₀ × Y₁) (c : C) : PMF ((T₀ × T₁) × Z₀ × Z₁)

The AND simulator runs both simulators independently at the shared challenge.

@[simp]

theorem Cslib.Crypto.Protocols.SigmaProtocol.andProof_accepts_iff {X₀ Y₀ T₀ Z₀ X₁ Y₁ T₁ Z₁ C : Type u} {P₀ : SigmaProtocol X₀ Y₀ T₀ C Z₀} {P₁ : SigmaProtocol X₁ Y₁ T₁ C Z₁} {y : Y₀ × Y₁} {t : T₀ × T₁} {c : C} {z : Z₀ × Z₁} : (P₀.andProof P₁).Accepts y t c z ↔ P₀.Accepts y.1 t.1 c z.1 ∧ P₁.Accepts y.2 t.2 c z.2

An AND conversation is accepting exactly when both halves are accepting at the shared challenge.

theorem Cslib.Crypto.Protocols.SigmaProtocol.andProof_transcript {X₀ Y₀ T₀ Z₀ X₁ Y₁ T₁ Z₁ C : Type u} {P₀ : SigmaProtocol X₀ Y₀ T₀ C Z₀} {P₁ : SigmaProtocol X₁ Y₁ T₁ C Z₁} (x : X₀ × X₁) (y : Y₀ × Y₁) (c : C) : (P₀.andProof P₁).transcript x y c = do let a ← P₀.transcript x.1 y.1 c let b ← P₁.transcript x.2 y.2 c pure ((a.1, b.1), a.2, b.2)

The AND-proof's honest transcript pairs independent honest transcripts at the shared challenge.

theorem Cslib.Crypto.Protocols.SigmaProtocol.andProof_complete {X₀ Y₀ T₀ Z₀ X₁ Y₁ T₁ Z₁ C : Type u} {P₀ : SigmaProtocol X₀ Y₀ T₀ C Z₀} {P₁ : SigmaProtocol X₁ Y₁ T₁ C Z₁} {R₀ : X₀ → Y₀ → Prop} {R₁ : X₁ → Y₁ → Prop} (h₀ : P₀.Complete R₀) (h₁ : P₁.Complete R₁) : (P₀.andProof P₁).Complete fun (x : X₀ × X₁) (y : Y₀ × Y₁) => R₀ x.1 y.1 ∧ R₁ x.2 y.2

Theorem 19.18 of [BS23]: completeness.

theorem Cslib.Crypto.Protocols.SigmaProtocol.andProof_specialSoundness {X₀ Y₀ T₀ Z₀ X₁ Y₁ T₁ Z₁ C : Type u} {P₀ : SigmaProtocol X₀ Y₀ T₀ C Z₀} {P₁ : SigmaProtocol X₁ Y₁ T₁ C Z₁} {R₀ : X₀ → Y₀ → Prop} {R₁ : X₁ → Y₁ → Prop} {extract₀ : Y₀ → T₀ → C → Z₀ → C → Z₀ → X₀} {extract₁ : Y₁ → T₁ → C → Z₁ → C → Z₁ → X₁} (h₀ : P₀.SpecialSoundness R₀ extract₀) (h₁ : P₁.SpecialSoundness R₁ extract₁) : (P₀.andProof P₁).SpecialSoundness (fun (x : X₀ × X₁) (y : Y₀ × Y₁) => R₀ x.1 y.1 ∧ R₁ x.2 y.2) (andExtract extract₀ extract₁)

Theorem 19.18 of [BS23]: special soundness.

theorem Cslib.Crypto.Protocols.SigmaProtocol.andProof_specialHVZK {X₀ Y₀ T₀ Z₀ X₁ Y₁ T₁ Z₁ C : Type u} {P₀ : SigmaProtocol X₀ Y₀ T₀ C Z₀} {P₁ : SigmaProtocol X₁ Y₁ T₁ C Z₁} {R₀ : X₀ → Y₀ → Prop} {R₁ : X₁ → Y₁ → Prop} {simulate₀ : Y₀ → C → PMF (T₀ × Z₀)} {simulate₁ : Y₁ → C → PMF (T₁ × Z₁)} (h₀ : P₀.SpecialHVZK R₀ simulate₀) (h₁ : P₁.SpecialHVZK R₁ simulate₁) : (P₀.andProof P₁).SpecialHVZK (fun (x : X₀ × X₁) (y : Y₀ × Y₁) => R₀ x.1 y.1 ∧ R₁ x.2 y.2) (andSimulate simulate₀ simulate₁)

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

OR

def Cslib.Crypto.Protocols.SigmaProtocol.orRelation {X₀ Y₀ X₁ Y₁ : Type u} (R₀ : X₀ → Y₀ → Prop) (R₁ : X₁ → Y₁ → Prop) : X₀ ⊕ X₁ → Y₀ × Y₁ → Prop

The OR relation: a witness for the first statement or a witness for the second ([BS23], Equation 19.23).

noncomputable def Cslib.Crypto.Protocols.SigmaProtocol.orProof {X₀ Y₀ T₀ Z₀ X₁ Y₁ T₁ Z₁ C : Type u} [AddCommGroup C] [Fintype C] (P₀ : SigmaProtocol X₀ Y₀ T₀ C Z₀) (P₁ : SigmaProtocol X₁ Y₁ T₁ C Z₁) (simulate₀ : Y₀ → C → PMF (T₀ × Z₀)) (simulate₁ : Y₁ → C → PMF (T₁ × Z₁)) : SigmaProtocol (X₀ ⊕ X₁) (Y₀ × Y₁) (T₀ × T₁) C (C × Z₀ × Z₁)

The OR-proof ([BS23], Section 19.7.2). With a witness for one side, the prover simulates the other side at a uniform challenge c', commits honestly on its own side, and answers the verifier's challenge c on its own side at c - c'. The response (c₀, z₀, z₁) names the first side's challenge; the second side's is c - c₀.

def Cslib.Crypto.Protocols.SigmaProtocol.orExtract {X₀ Y₀ T₀ Z₀ X₁ Y₁ T₁ Z₁ C : Type u} [AddCommGroup C] [DecidableEq C] (extract₀ : Y₀ → T₀ → C → Z₀ → C → Z₀ → X₀) (extract₁ : Y₁ → T₁ → C → Z₁ → C → Z₁ → X₁) (y : Y₀ × Y₁) (t : T₀ × T₁) (c : C) (z : C × Z₀ × Z₁) (c' : C) (z' : C × Z₀ × Z₁) : X₀ ⊕ X₁

The OR extractor uses the first side when the first side's challenges differ, and the second side otherwise.

noncomputable def Cslib.Crypto.Protocols.SigmaProtocol.orSimulate {Y₀ T₀ Z₀ Y₁ T₁ Z₁ C : Type u} [AddCommGroup C] [Fintype C] (simulate₀ : Y₀ → C → PMF (T₀ × Z₀)) (simulate₁ : Y₁ → C → PMF (T₁ × Z₁)) (y : Y₀ × Y₁) (c : C) : PMF ((T₀ × T₁) × C × Z₀ × Z₁)

The OR simulator splits the challenge uniformly and simulates both sides.

@[simp]

theorem Cslib.Crypto.Protocols.SigmaProtocol.orProof_accepts_iff {X₀ Y₀ T₀ Z₀ X₁ Y₁ T₁ Z₁ C : Type u} [AddCommGroup C] [Fintype C] {P₀ : SigmaProtocol X₀ Y₀ T₀ C Z₀} {P₁ : SigmaProtocol X₁ Y₁ T₁ C Z₁} {simulate₀ : Y₀ → C → PMF (T₀ × Z₀)} {simulate₁ : Y₁ → C → PMF (T₁ × Z₁)} {y : Y₀ × Y₁} {t : T₀ × T₁} {c : C} {z : C × Z₀ × Z₁} : (P₀.orProof P₁ simulate₀ simulate₁).Accepts y t c z ↔ P₀.Accepts y.1 t.1 z.1 z.2.1 ∧ P₁.Accepts y.2 t.2 (c - z.1) z.2.2

An OR conversation (c₀, z₀, z₁) for the challenge c is accepting exactly when the first side accepts at c₀ and the second at c - c₀.

theorem Cslib.Crypto.Protocols.SigmaProtocol.orProof_transcript_inl {X₀ Y₀ T₀ Z₀ X₁ Y₁ T₁ Z₁ C : Type u} [AddCommGroup C] [Fintype C] {P₀ : SigmaProtocol X₀ Y₀ T₀ C Z₀} {P₁ : SigmaProtocol X₁ Y₁ T₁ C Z₁} {simulate₀ : Y₀ → C → PMF (T₀ × Z₀)} {simulate₁ : Y₁ → C → PMF (T₁ × Z₁)} (x : X₀) (y : Y₀ × Y₁) (c : C) : (P₀.orProof P₁ simulate₀ simulate₁).transcript (Sum.inl x) y c = do let c₁ ← Probability.PMF.uniformOfFintype C let b ← simulate₁ y.2 c₁ let a ← P₀.transcript x y.1 (c - c₁) pure ((a.1, b.1), c - c₁, a.2, b.2)

With a witness for the first statement, the OR prover simulates the second side at a uniform challenge and answers honestly on the first side.

theorem Cslib.Crypto.Protocols.SigmaProtocol.orProof_transcript_inr {X₀ Y₀ T₀ Z₀ X₁ Y₁ T₁ Z₁ C : Type u} [AddCommGroup C] [Fintype C] {P₀ : SigmaProtocol X₀ Y₀ T₀ C Z₀} {P₁ : SigmaProtocol X₁ Y₁ T₁ C Z₁} {simulate₀ : Y₀ → C → PMF (T₀ × Z₀)} {simulate₁ : Y₁ → C → PMF (T₁ × Z₁)} (x : X₁) (y : Y₀ × Y₁) (c : C) : (P₀.orProof P₁ simulate₀ simulate₁).transcript (Sum.inr x) y c = do let c₀ ← Probability.PMF.uniformOfFintype C let a ← simulate₀ y.1 c₀ let b ← P₁.transcript x y.2 (c - c₀) pure ((a.1, b.1), c₀, a.2, b.2)

With a witness for the second statement, the OR prover simulates the first side at a uniform challenge and answers honestly on the second side.

theorem Cslib.Crypto.Protocols.SigmaProtocol.orProof_complete {X₀ Y₀ T₀ Z₀ X₁ Y₁ T₁ Z₁ C : Type u} [AddCommGroup C] [Fintype C] {P₀ : SigmaProtocol X₀ Y₀ T₀ C Z₀} {P₁ : SigmaProtocol X₁ Y₁ T₁ C Z₁} {R₀ : X₀ → Y₀ → Prop} {R₁ : X₁ → Y₁ → Prop} {simulate₀ : Y₀ → C → PMF (T₀ × Z₀)} {simulate₁ : Y₁ → C → PMF (T₁ × Z₁)} (h₀ : P₀.Complete R₀) (h₁ : P₁.Complete R₁) (hs₀ : P₀.SpecialHVZK R₀ simulate₀) (hs₁ : P₁.SpecialHVZK R₁ simulate₁) : (P₀.orProof P₁ simulate₀ simulate₁).Complete (orRelation R₀ R₁)

Theorem 19.19 of [BS23]: completeness. It uses that both simulators output accepting conversations.

theorem Cslib.Crypto.Protocols.SigmaProtocol.orProof_specialSoundness {X₀ Y₀ T₀ Z₀ X₁ Y₁ T₁ Z₁ C : Type u} [AddCommGroup C] [Fintype C] {P₀ : SigmaProtocol X₀ Y₀ T₀ C Z₀} {P₁ : SigmaProtocol X₁ Y₁ T₁ C Z₁} {R₀ : X₀ → Y₀ → Prop} {R₁ : X₁ → Y₁ → Prop} {simulate₀ : Y₀ → C → PMF (T₀ × Z₀)} {simulate₁ : Y₁ → C → PMF (T₁ × Z₁)} [DecidableEq C] {extract₀ : Y₀ → T₀ → C → Z₀ → C → Z₀ → X₀} {extract₁ : Y₁ → T₁ → C → Z₁ → C → Z₁ → X₁} (h₀ : P₀.SpecialSoundness R₀ extract₀) (h₁ : P₁.SpecialSoundness R₁ extract₁) : (P₀.orProof P₁ simulate₀ simulate₁).SpecialSoundness (orRelation R₀ R₁) (orExtract extract₀ extract₁)

Theorem 19.19 of [BS23]: special soundness. Distinct challenges differ on the first side's challenge or on the second side's.

theorem Cslib.Crypto.Protocols.SigmaProtocol.orProof_specialHVZK {X₀ Y₀ T₀ Z₀ X₁ Y₁ T₁ Z₁ C : Type u} [AddCommGroup C] [Fintype C] {P₀ : SigmaProtocol X₀ Y₀ T₀ C Z₀} {P₁ : SigmaProtocol X₁ Y₁ T₁ C Z₁} {R₀ : X₀ → Y₀ → Prop} {R₁ : X₁ → Y₁ → Prop} {simulate₀ : Y₀ → C → PMF (T₀ × Z₀)} {simulate₁ : Y₁ → C → PMF (T₁ × Z₁)} (hs₀ : P₀.SpecialHVZK R₀ simulate₀) (hs₁ : P₁.SpecialHVZK R₁ simulate₁) : (P₀.orProof P₁ simulate₀ simulate₁).SpecialHVZK (orRelation R₀ R₁) (orSimulate simulate₀ simulate₁)

Theorem 19.19 of [BS23]: special honest-verifier zero knowledge. The honest prover's own-side challenge c - c' is uniform, and its own-side transcript is replaced by a simulation.