Completeness and soundness of the 3-copy GMW protocol

This module proves perfect completeness (acceptProb_gmwVerifier_gmwProver) and unconditional soundness (acceptProb_gmwVerifier_le) for Cslib.Crypto.GMW.gmwVerifier.

• Completeness. When ThreeSAT.verifier (f a, w) = true, every selectively opened copy of the honest prover's committed bits matches simBits (naorMaskBits_realBits) and passes verifyCopyBits and verifyCommitments, so gmwVerifier accepts gmwProver with probability 1.
• Soundness. Whenever Naor's commitment scheme is statistically binding on the first-round receiver string r (NaorBinding generator s (BitString.listRow m 0 r)), if a prover can produce accepting second-round openings for two distinct 3-bit challenges x₁ ≠ x₂ on the same first-round commitment transcript commitReply, then those two challenges differ in at least one coordinate j ∈ {0, 1, 2}: one transcript opens copy j under challenge false (revealing m and the full clause truth tables tableBits φ m) and the other opens copy j under challenge true (revealing v and confirming that the active entry gmwActiveIdx of every clause is true), while binding forces the opened active entries to agree with tableBits φ m. Consequently v ⊕ m satisfies φ (mem_ThreeSAT_of_verifyTranscript_ne), so when f a ∉ ThreeSAT at most one of the 8 challenges can be answered after any binding r, bounding the acceptance probability by naorBindingProb + 1 / 8 ≤ 1 / 3 (acceptProb_gmwVerifier_le).

Main results

• Cslib.Crypto.GMW.acceptProb_gmwVerifier_gmwProver: perfect completeness (acceptProb = 1) for any valid ThreeSAT witness.
• Cslib.Crypto.GMW.mem_ThreeSAT_of_verifyTranscript_ne: witness extraction from two accepting transcripts with distinct 3-bit challenges on a binding receiver string.
• Cslib.Crypto.GMW.acceptProb_gmwVerifier_le: soundness bound acceptProb ≤ 1 / 3 when f a ∉ ThreeSAT and ∀ k, 3 * k + 1 ≤ length k.

References

• O. Goldreich, S. Micali, A. Wigderson, Proofs that Yield Nothing But Their Validity, or All Languages in NP Have Zero-Knowledge Proof Systems
• M. Naor, Bit Commitment Using Pseudorandomness

Completeness of gmwVerifier with gmwProver

theorem Cslib.Crypto.GMW.acceptProb_gmwVerifier_gmwProver {α : Type} {generator : List Bool → List Bool} {length : ℕ → ℕ} (hlen : ∀ (seed : List Bool), (generator seed).length = length seed.length) (f : α → Logic.PL.CNF ℕ) (n : ℕ) (a : α) {w : List Bool} (hw : Complexity.ThreeSAT.verifier (f a, w) = true) : Complexity.acceptProb (gmwVerifier generator length f n a) (gmwProver generator (n + 7) (length (n + 7)) (f a) w) = 1

Completeness of the GMW protocol. When ThreeSAT.verifier (f a, w) = true, the honest prover gmwProver makes gmwVerifier accept with probability 1.

Soundness of gmwVerifier against arbitrary provers

theorem Cslib.Crypto.GMW.mem_ThreeSAT_of_verifyTranscript_ne {generator : List Bool → List Bool} {s m : ℕ} {φ : Logic.PL.CNF ℕ} {r commitReply openReply₁ openReply₂ : List Bool} {x₁ x₂ : BitString 3} (hbind : NaorBinding generator s (BitString.listRow m 0 r)) (hne : x₁ ≠ x₂) (hv₁ : verifyTranscript generator s m φ r commitReply (List.ofFn x₁) openReply₁ = true) (hv₂ : verifyTranscript generator s m φ r commitReply (List.ofFn x₂) openReply₂ = true) : φ ∈ Complexity.ThreeSAT

If a first-round commitment transcript commitReply under a binding receiver string r admits accepting second-round openings for two distinct 3-bit challenges x₁ ≠ x₂, then φ ∈ ThreeSAT.

theorem Cslib.Crypto.GMW.acceptProb_gmwVerifier_le {α : Type} {generator : List Bool → List Bool} {length : ℕ → ℕ} (hlen : ∀ (seed : List Bool), (generator seed).length = length seed.length) (hstretch : ∀ (k : ℕ), 3 * k + 1 ≤ length k) (f : α → Logic.PL.CNF ℕ) (n : ℕ) (a : α) (hnot : f a ∉ Complexity.ThreeSAT) (P : Complexity.Prover Unit) : Complexity.acceptProb (gmwVerifier generator length f n a) P ≤ 1 / 3

Soundness of the GMW protocol. When f a ∉ ThreeSAT and 3 * k + 1 ≤ length k for all k, no unbounded stateful prover P makes gmwVerifier accept with probability greater than 1 / 3.