Naor's bit commitment scheme from pseudorandom generators

Naor's statistically binding, computationally hiding bit commitment scheme [Nao91] commits to a bit b : Bool under a receiver string r : List Bool and a uniform seed seed : List Bool of length n using a pseudorandom generator generator: naorCommit generator r b seed outputs generator seed when b = false, and BitString.listXor (generator seed).length [generator seed, r] when b = true.

Main definitions

• Cslib.Crypto.naorCommit: commit to a single bit using a generator, receiver string, and seed.
• Cslib.Crypto.naorCommitEnsemble: the commitment distribution for a family of receiver strings and bits.
• Cslib.Crypto.CommitmentReceiver, Cslib.Crypto.CommitmentReceiver.IsPPT: a two-stage randomized stateful PPT receiver that outputs ((r, (b₀, b₁)), state) in the first stage and distinguishes (state, c) in the second stage.
• Cslib.Crypto.commitmentHidingGame, Cslib.Crypto.StatefulHiding: the two-stage commitment hiding game and computational hiding against randomized stateful PPT receivers.
• Cslib.Crypto.naorReceiverDistinguisher: PRG distinguisher induced by a stateful commitment receiver.
• Cslib.Crypto.NaorBinding: statistical binding at seed length n for receiver string r, requiring that no two seeds of length n open to false and true with the same commitment.
• Cslib.Crypto.naorBindingProb, Cslib.Crypto.naorBindingError: the probability over a uniform receiver string r of length length n that NaorBinding generator n r fails.
• Cslib.Crypto.BitCommitmentScheme: a two-message statistically binding, computationally hiding bit commitment scheme.

Main results

• Cslib.Crypto.OneWay.exists_pseudorandomGenerator_three_mul: any one-way function yields a pseudorandom generator with expansion fun n => 3 * n + 1.
• Cslib.Crypto.uniformList_map_naorCommit_id: replacing the generator output with a uniform word of length m makes the commitment distribution exactly BitString.uniformList m for every receiver string r and committed bit b.
• Cslib.Crypto.PseudorandomGenerator.naorCommit_indistinguishable_uniform, Cslib.Crypto.PseudorandomGenerator.naorCommit_hiding: computational hiding of Naor commitments for deterministic polynomial-time families of receiver strings r : ℕ → List Bool and bit families b₀ b₁ : ℕ → Bool.
• Cslib.Crypto.advantage_commitmentHidingGame_naorCommit_le, Cslib.Crypto.PseudorandomGenerator.naorStatefulHiding: computational hiding of Naor commitments against randomized stateful PPT receivers, and Cslib.Crypto.StatefulHiding.computational_hiding connecting stateful-receiver hiding to the deterministic-family interface.
• Cslib.Crypto.naorBindingProb_le, Cslib.Crypto.naorBindingProb_le_of_three_mul_add_one, Cslib.Crypto.negligible_naorBindingError: statistical binding when 3 * n ≤ length n.
• Cslib.Crypto.PseudorandomGenerator.naorBitCommitment, Cslib.Crypto.OneWay.exists_bitCommitmentScheme: packaged Naor bit commitment scheme from a pseudorandom generator or one-way function.

References

• M. Naor, Bit Commitment Using Pseudorandomness
• O. Goldreich, Foundations of Cryptography: Volume 1, Basic Tools, Section 4.4.1.

Stretching a one-way function to 3 * n + 1 bits

theorem Cslib.Crypto.OneWay.exists_pseudorandomGenerator_three_mul {f : List Bool → List Bool} (hf : OneWay f) : ∃ (generator : List Bool → List Bool), PseudorandomGenerator generator fun (n : ℕ) => 3 * n + 1

Any one-way function yields a pseudorandom generator stretching n bits to 3 * n + 1 bits.

Naor bit commitment

def Cslib.Crypto.naorCommit (generator : List Bool → List Bool) (r : List Bool) (b : Bool) (seed : List Bool) : List Bool

Naor's bit commitment: evaluate generator seed, and XOR with r when b = true.

@[simp]

theorem Cslib.Crypto.naorCommit_false (generator : List Bool → List Bool) (r seed : List Bool) : naorCommit generator r false seed = generator seed

@[simp]

theorem Cslib.Crypto.naorCommit_true (generator : List Bool → List Bool) (r seed : List Bool) : naorCommit generator r true seed = BitString.listXor (generator seed).length [generator seed, r]

theorem Cslib.Crypto.naorCommit_eq_comp_id (generator : List Bool → List Bool) (r : List Bool) (b : Bool) (seed : List Bool) : naorCommit generator r b seed = naorCommit id r b (generator seed)

naorCommit factors through the identity generator naorCommit id r b.

@[simp]

theorem Cslib.Crypto.length_naorCommit (generator : List Bool → List Bool) (r : List Bool) (b : Bool) (seed : List Bool) : (naorCommit generator r b seed).length = (generator seed).length

theorem Cslib.Crypto.computableTidilyInPolyTime_naorCommit {α : Type} {input : α ↪ List Bool} {generator : List Bool → List Bool} {r : α → List Bool} {b : α → Bool} {seed : α → List Bool} (hg : Turing.MultiTapeTM.ComputableTidilyInPolyTime generator Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (hr : Turing.MultiTapeTM.ComputableTidilyInPolyTime r input Turing.MultiTapeTM.encBits) (hb : Turing.MultiTapeTM.ComputableTidilyInPolyTime b input Turing.MultiTapeTM.encBool) (hseed : Turing.MultiTapeTM.ComputableTidilyInPolyTime seed input Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => naorCommit generator (r a) (b a) (seed a)) input Turing.MultiTapeTM.encBits

Naor commitment is computable in polynomial time when its inputs are.

theorem Cslib.Crypto.computableInPolyTime_naorCommit {α : Type} {input : α ↪ List Bool} {generator : List Bool → List Bool} {r : α → List Bool} {b : α → Bool} {seed : α → List Bool} (hg : Turing.MultiTapeTM.ComputableInPolyTime generator Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (hr : Turing.MultiTapeTM.ComputableInPolyTime r input Turing.MultiTapeTM.encBits) (hb : Turing.MultiTapeTM.ComputableInPolyTime b input Turing.MultiTapeTM.encBool) (hseed : Turing.MultiTapeTM.ComputableInPolyTime seed input Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => naorCommit generator (r a) (b a) (seed a)) input Turing.MultiTapeTM.encBits

Naor commitment is computable in plain polynomial time when its inputs are.

Algebraic and distributional laws

@[simp]

theorem Cslib.Crypto.uniformList_map_naorCommit_id (m : ℕ) (r : List Bool) (b : Bool) : PMF.map (naorCommit id r b) (BitString.uniformList m) = BitString.uniformList m

Applying naorCommit id r b to a uniform m-bit word yields a uniform m-bit word for every receiver string r and bit b.

Computational hiding

noncomputable def Cslib.Crypto.naorCommitEnsemble (generator : List Bool → List Bool) (r : ℕ → List Bool) (b : ℕ → Bool) (n : ℕ) : PMF (List Bool)

The commitment ensemble on a uniform n-bit seed for receiver string r n and bit b n.

theorem Cslib.Crypto.naorCommitEnsemble_eq_map (generator : List Bool → List Bool) (r : ℕ → List Bool) (b : ℕ → Bool) (n : ℕ) : naorCommitEnsemble generator r b n = PMF.map (naorCommit id (r n) (b n)) (generatorEnsemble generator n)

theorem Cslib.Crypto.PseudorandomGenerator.naorCommit_indistinguishable_uniform {generator : List Bool → List Bool} {length : ℕ → ℕ} (hG : PseudorandomGenerator generator length) {r : ℕ → List Bool} {b : ℕ → Bool} (hr : Turing.MultiTapeTM.ComputableTidilyInPolyTime r Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) (hb : Turing.MultiTapeTM.ComputableTidilyInPolyTime b Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool) : ComputationallyIndistinguishable (naorCommitEnsemble generator r b) fun (n : ℕ) => BitString.uniformList (length n)

For any polynomial-time receiver family r and bit family b, the Naor commitment ensemble is computationally indistinguishable from uniform words of length length n.

theorem Cslib.Crypto.PseudorandomGenerator.naorCommit_hiding {generator : List Bool → List Bool} {length : ℕ → ℕ} (hG : PseudorandomGenerator generator length) {r : ℕ → List Bool} {b₀ b₁ : ℕ → Bool} (hr : Turing.MultiTapeTM.ComputableTidilyInPolyTime r Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) (hb₀ : Turing.MultiTapeTM.ComputableTidilyInPolyTime b₀ Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool) (hb₁ : Turing.MultiTapeTM.ComputableTidilyInPolyTime b₁ Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool) : ComputationallyIndistinguishable (naorCommitEnsemble generator r b₀) (naorCommitEnsemble generator r b₁)

Computational hiding of Naor bit commitment (deterministic-family formulation). Commitments to any two deterministic polynomial-time bit families b₀ and b₁ under any deterministic polynomial-time receiver string family r : ℕ → List Bool are computationally indistinguishable against uniform strict PPT distinguishers. See PseudorandomGenerator.naorStatefulHiding below for hiding against a randomized stateful PPT receiver.

Stateful-receiver commitment hiding

structure Cslib.Crypto.CommitmentReceiver : Type

A two-stage randomized stateful receiver for a bit commitment scheme [Naor1991, Goldreich2001]. In the first stage, choose n aux receives the unary security parameter n and auxiliary input aux, and outputs a receiver challenge string r, two challenge bits (b₀, b₁), and an internal state passed to the second stage. In the second stage, guess n state c receives the security parameter n, the saved state, and the commitment c, and outputs a distinguishing bit.

• choose : ℕ → List Bool → ProbComp ((List Bool × Bool × Bool) × List Bool)

  First stage: output ((r, (b₀, b₁)), state).

• guess : ℕ → List Bool → List Bool → ProbComp Bool

  Second stage: distinguish the commitment c using the saved state.

structure Cslib.Crypto.CommitmentReceiver.IsPPT (receiver : CommitmentReceiver) : Prop

A commitment receiver is strict PPT if both stages run in polynomial time in their full encoded inputs (charging for the auxiliary input aux in choose and for the saved state and commitment c in guess).

• choose : Probability.IsPPT (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBool Turing.MultiTapeTM.encBool)) Turing.MultiTapeTM.encBits) receiver.choose

  The first stage is a strict PPT family from (n, aux) to ((r, (b₀, b₁)), state).

• guess : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBool fun (p : ℕ × List Bool × List Bool) => receiver.guess p.1 p.2.1 p.2.2

  The second stage is strict PPT on (n, state, c).

noncomputable def Cslib.Crypto.commitmentHidingGame (commit : List Bool → Bool → List Bool → List Bool) (receiver : CommitmentReceiver) (aux : List Bool) (bit : Bool) (n : ℕ) : ProbComp Bool

The two-stage commitment-hiding experiment against a stateful receiver receiver with auxiliary input aux and hidden bit selector bit : Bool at security parameter n. The receiver outputs ((r, (b₀, b₁)), state) ← receiver.choose n aux, the challenger samples a uniform n-bit seed seed ← BitString.sampleList n and commits to b₁ (when bit = true) or b₀ (when bit = false) under r, and receiver.guess n state c outputs a guess bit.

theorem Cslib.Crypto.isPPTOn_commitmentHidingGame {commit : List Bool → Bool → List Bool → List Bool} {receiver : CommitmentReceiver} (hcommit : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List Bool × Bool × List Bool) => commit p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBool Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits) (hR : receiver.IsPPT) : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool)) Turing.MultiTapeTM.encBool fun (p : ℕ × List Bool × Bool) => commitmentHidingGame commit receiver p.2.1 p.2.2 p.1

The commitment-hiding experiment runs in strict PPT on (n, aux, bit) whenever commit is computable in plain polynomial time and receiver is strict PPT.

theorem Cslib.Crypto.isPPT_commitmentHidingGame {commit : List Bool → Bool → List Bool → List Bool} {receiver : CommitmentReceiver} (hcommit : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List Bool × Bool × List Bool) => commit p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBool Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits) (hR : receiver.IsPPT) (bit : Bool) : Probability.IsPPT Turing.MultiTapeTM.encBool fun (n : ℕ) (aux : List Bool) => commitmentHidingGame commit receiver aux bit n

For any fixed challenge selector bit, the commitment-hiding experiment is a strict PPT indexed family on (n, aux).

theorem Cslib.Crypto.isPPTOn_commitmentHidingGame_aux {commit : List Bool → Bool → List Bool → List Bool} {receiver : CommitmentReceiver} {aux : ℕ → List Bool} (hcommit : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List Bool × Bool × List Bool) => commit p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBool Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits) (hR : receiver.IsPPT) (haux : Turing.MultiTapeTM.ComputableInPolyTime aux Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) (bit : Bool) : Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool fun (n : ℕ) => commitmentHidingGame commit receiver (aux n) bit n

For any polynomial-time auxiliary family aux, the commitment-hiding experiment is strict PPT in the unary security parameter n.

def Cslib.Crypto.StatefulHiding (commit : List Bool → Bool → List Bool → List Bool) : Prop

Computational hiding against a randomized stateful PPT receiver: for every polynomial-time auxiliary family aux : ℕ → List Bool, no strict PPT CommitmentReceiver can distinguish commitments to its first chosen bit (bit = false) from commitments to its second chosen bit (bit = true) with non-negligible advantage.

theorem Cslib.Crypto.StatefulHiding.empty {commit : List Bool → Bool → List Bool → List Bool} (h : StatefulHiding commit) : Game.Indistinguishable (fun (receiver : CommitmentReceiver) (n : ℕ) => (commitmentHidingGame commit receiver [] false n).eval) (fun (receiver : CommitmentReceiver) (n : ℕ) => (commitmentHidingGame commit receiver [] true n).eval) CommitmentReceiver.IsPPT

Specialization of StatefulHiding to the empty auxiliary string [].

def Cslib.Crypto.CommitmentReceiver.ofDeterministic (r : ℕ → List Bool) (b₀ b₁ : ℕ → Bool) (D : Distinguisher) : CommitmentReceiver

Package deterministic families (r, b₀, b₁) and a distinguisher D as a stateless CommitmentReceiver.

theorem Cslib.Crypto.CommitmentReceiver.isPPT_ofDeterministic {r : ℕ → List Bool} {b₀ b₁ : ℕ → Bool} {D : Distinguisher} (hr : Turing.MultiTapeTM.ComputableInPolyTime r Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) (hb₀ : Turing.MultiTapeTM.ComputableInPolyTime b₀ Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool) (hb₁ : Turing.MultiTapeTM.ComputableInPolyTime b₁ Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool) (hD : Probability.IsPPT Turing.MultiTapeTM.encBool D) : (ofDeterministic r b₀ b₁ D).IsPPT

CommitmentReceiver.ofDeterministic r b₀ b₁ D is strict PPT whenever r, b₀, b₁ are computable in plain polynomial time and D is a strict PPT distinguisher.

@[simp]

theorem Cslib.Crypto.eval_commitmentHidingGame_ofDeterministic (commit : List Bool → Bool → List Bool → List Bool) (r : ℕ → List Bool) (b₀ b₁ : ℕ → Bool) (D : Distinguisher) (aux : List Bool) (bit : Bool) (n : ℕ) : (commitmentHidingGame commit (CommitmentReceiver.ofDeterministic r b₀ b₁ D) aux bit n).eval = distinguishingGame (PMF.map (commit (r n) (if bit = true then b₁ n else b₀ n)) (BitString.uniformList n)) (D n)

theorem Cslib.Crypto.StatefulHiding.computational_hiding {commit : List Bool → Bool → List Bool → List Bool} (h : StatefulHiding commit) {r : ℕ → List Bool} {b₀ b₁ : ℕ → Bool} (hr : Turing.MultiTapeTM.ComputableInPolyTime r Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) (hb₀ : Turing.MultiTapeTM.ComputableInPolyTime b₀ Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool) (hb₁ : Turing.MultiTapeTM.ComputableInPolyTime b₁ Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool) : ComputationallyIndistinguishable (fun (n : ℕ) => PMF.map (commit (r n) (b₀ n)) (BitString.uniformList n)) fun (n : ℕ) => PMF.map (commit (r n) (b₁ n)) (BitString.uniformList n)

Stateful-receiver hiding implies the deterministic-family hiding interface: any commitment function satisfying StatefulHiding hides commitments for all deterministic polynomial-time families r : ℕ → List Bool and b₀ b₁ : ℕ → Bool.

noncomputable def Cslib.Crypto.naorReceiverDistinguisher (receiver : CommitmentReceiver) (aux : ℕ → List Bool) (bit : Bool) : Distinguisher

PRG distinguisher induced by a stateful commitment receiver receiver, auxiliary input family aux, and hidden bit selector bit. On security parameter n and candidate pad pad, it runs choice ← receiver.choose n (aux n), forms the commitment naorCommit id r b_bit pad, and runs receiver.guess n choice.2 c.

theorem Cslib.Crypto.isPPT_naorReceiverDistinguisher {receiver : CommitmentReceiver} {aux : ℕ → List Bool} (hR : receiver.IsPPT) (haux : Turing.MultiTapeTM.ComputableInPolyTime aux Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) (bit : Bool) : Probability.IsPPT Turing.MultiTapeTM.encBool (naorReceiverDistinguisher receiver aux bit)

naorReceiverDistinguisher receiver aux bit is a strict PPT distinguisher whenever receiver is strict PPT and aux is computable in plain polynomial time.

theorem Cslib.Crypto.eval_commitmentHidingGame_naorCommit (generator : List Bool → List Bool) (receiver : CommitmentReceiver) (aux : ℕ → List Bool) (bit : Bool) (n : ℕ) : (commitmentHidingGame (naorCommit generator) receiver (aux n) bit n).eval = distinguishingGame (generatorEnsemble generator n) (naorReceiverDistinguisher receiver aux bit n)

Running commitmentHidingGame (naorCommit generator) against receiver coincides with running naorReceiverDistinguisher receiver aux bit against the PRG output generatorEnsemble generator n.

theorem Cslib.Crypto.distinguishingGame_uniformList_naorReceiverDistinguisher (m : ℕ) (receiver : CommitmentReceiver) (aux : ℕ → List Bool) (bit : Bool) (n : ℕ) : distinguishingGame (BitString.uniformList m) (naorReceiverDistinguisher receiver aux bit n) = (receiver.choose n (aux n)).eval.bind fun (choice : (List Bool × Bool × Bool) × List Bool) => (BitString.uniformList m).bind fun (c : List Bool) => (receiver.guess n choice.2 c).eval

On a truly uniform m-bit pad, naorReceiverDistinguisher receiver aux bit n presents an independent uniform m-bit commitment to receiver.guess regardless of the receiver's chosen challenge string r and bit selector bit.

theorem Cslib.Crypto.distinguishingGame_uniformList_naorReceiverDistinguisher_false_eq_true (m : ℕ) (receiver : CommitmentReceiver) (aux : ℕ → List Bool) (n : ℕ) : distinguishingGame (BitString.uniformList m) (naorReceiverDistinguisher receiver aux false n) = distinguishingGame (BitString.uniformList m) (naorReceiverDistinguisher receiver aux true n)

Under a truly uniform m-bit pad, the false and true commitment-hiding experiments are identically distributed for every stateful receiver receiver.

theorem Cslib.Crypto.advantage_commitmentHidingGame_naorCommit_le (generator : List Bool → List Bool) (m : ℕ) (receiver : CommitmentReceiver) (aux : ℕ → List Bool) (n : ℕ) : Game.advantage (commitmentHidingGame (naorCommit generator) receiver (aux n) false n).eval (commitmentHidingGame (naorCommit generator) receiver (aux n) true n).eval ≤ (distinguishingGame (generatorEnsemble generator n) (naorReceiverDistinguisher receiver aux false n)).advantage (distinguishingGame (BitString.uniformList m) (naorReceiverDistinguisher receiver aux false n)) + (distinguishingGame (generatorEnsemble generator n) (naorReceiverDistinguisher receiver aux true n)).advantage (distinguishingGame (BitString.uniformList m) (naorReceiverDistinguisher receiver aux true n))

Quantitative stateful-receiver hiding bound for Naor's bit commitment scheme: the commitment-hiding advantage of any stateful receiver receiver at security parameter n is bounded by the sum of the PRG distinguishing advantages of naorReceiverDistinguisher receiver aux false and naorReceiverDistinguisher receiver aux true against BitString.uniformList m.

theorem Cslib.Crypto.PseudorandomGenerator.naorStatefulHiding {generator : List Bool → List Bool} {length : ℕ → ℕ} (hG : PseudorandomGenerator generator length) : StatefulHiding (naorCommit generator)

Stateful-receiver computational hiding of Naor bit commitment [Nao91]: for any pseudorandom generator generator, naorCommit generator satisfies StatefulHiding against all randomized stateful PPT receivers.

Statistical binding

def Cslib.Crypto.NaorBinding (generator : List Bool → List Bool) (n : ℕ) (r : List Bool) : Prop

A receiver string r is binding for seed length n if no two seeds of length n produce the same commitment for false and true.

theorem Cslib.Crypto.naorBinding_iff_bitString (generator : List Bool → List Bool) (n : ℕ) (r : List Bool) : NaorBinding generator n r ↔ ∀ (s₀ s₁ : BitString n), naorCommit generator r false (List.ofFn s₀) ≠ naorCommit generator r true (List.ofFn s₁)

Equivalence between NaorBinding on lists of length n and on BitString n.

@[instance_reducible]

instance Cslib.Crypto.decidablePredNaorBinding (generator : List Bool → List Bool) (n : ℕ) : DecidablePred (NaorBinding generator n)

theorem Cslib.Crypto.NaorBinding.eq_of_naorCommit_eq {generator : List Bool → List Bool} {n : ℕ} {r : List Bool} (hbind : NaorBinding generator n r) {b₀ b₁ : Bool} {s₀ s₁ : List Bool} (hs₀ : s₀.length = n) (hs₁ : s₁.length = n) (heq : naorCommit generator r b₀ s₀ = naorCommit generator r b₁ s₁) : b₀ = b₁

If a commitment opened as false with s₀ equals a commitment opened as true with s₁, then s₀ and s₁ must open to the same bit whenever NaorBinding holds.

def Cslib.Crypto.naorBadShift (generator : List Bool → List Bool) (m n : ℕ) (pair : BitString n × BitString n) : BitString m

The bad receiver string determined by a pair of seeds (s₀, s₁).

theorem Cslib.Crypto.mem_image_naorBadShift_of_not_naorBinding {generator : List Bool → List Bool} {length : ℕ → ℕ} (hlen : ∀ (s : List Bool), (generator s).length = length s.length) {n : ℕ} {r : List Bool} (hnot : ¬NaorBinding generator n r) : BitString.ofList (length n) r ∈ Finset.image (naorBadShift generator (length n) n) Finset.univ

If NaorBinding generator n r fails, then ofList (length n) r is the XOR of two generator outputs on n-bit seeds.

theorem Cslib.Crypto.card_not_naorBinding_le {generator : List Bool → List Bool} {length : ℕ → ℕ} (hlen : ∀ (s : List Bool), (generator s).length = length s.length) (n : ℕ) : {r : BitString (length n) | ¬NaorBinding generator n (List.ofFn r)}.card ≤ 2 ^ (2 * n)

At most 2 ^ (2 * n) receiver strings of length length n violate NaorBinding.

noncomputable def Cslib.Crypto.naorBindingProb (generator : List Bool → List Bool) (length : ℕ → ℕ) (n : ℕ) : ENNReal

The ENNReal probability that a uniform receiver string of length length n fails to be binding for n-bit seeds.

noncomputable def Cslib.Crypto.naorBindingError (generator : List Bool → List Bool) (length : ℕ → ℕ) (n : ℕ) : NNReal

The nonnegative real probability that a uniform receiver string of length length n fails to be binding for n-bit seeds.

theorem Cslib.Crypto.naorBindingProb_le {generator : List Bool → List Bool} {length : ℕ → ℕ} (hlen : ∀ (s : List Bool), (generator s).length = length s.length) (n : ℕ) : naorBindingProb generator length n ≤ 2 ^ (2 * n) / 2 ^ length n

The binding failure probability is at most 2 ^ (2 * n) / 2 ^ (length n).

theorem Cslib.Crypto.naorBindingProb_le_of_three_mul {generator : List Bool → List Bool} {length : ℕ → ℕ} (hlen : ∀ (s : List Bool), (generator s).length = length s.length) (n : ℕ) (hstretch : 3 * n ≤ length n) : naorBindingProb generator length n ≤ (1 / 2) ^ n

When 3 * n ≤ length n, the binding failure probability is at most (1 / 2) ^ n.

theorem Cslib.Crypto.naorBindingProb_le_of_three_mul_add_one {generator : List Bool → List Bool} {length : ℕ → ℕ} (hlen : ∀ (s : List Bool), (generator s).length = length s.length) (n : ℕ) (hstretch : 3 * n + 1 ≤ length n) : naorBindingProb generator length n ≤ (1 / 2) ^ (n + 1)

When 3 * n + 1 ≤ length n, the binding failure probability is at most (1 / 2) ^ (n + 1).

theorem Cslib.Crypto.naorBindingError_le_of_three_mul {generator : List Bool → List Bool} {length : ℕ → ℕ} (hlen : ∀ (s : List Bool), (generator s).length = length s.length) (n : ℕ) (hstretch : 3 * n ≤ length n) : naorBindingError generator length n ≤ (1 / 2) ^ n

When 3 * n ≤ length n, the nonnegative real binding failure probability is at most (1 / 2) ^ n.

theorem Cslib.Crypto.negligible_naorBindingError {generator : List Bool → List Bool} {length : ℕ → ℕ} (hlen : ∀ (s : List Bool), (generator s).length = length s.length) (hstretch : ∀ (n : ℕ), 3 * n ≤ length n) : Negligible (naorBindingError generator length)

Statistical binding of Naor bit commitment. When 3 * n ≤ length n for all n, the binding failure probability is negligible.

Selective-opening batch commitments

def Cslib.Crypto.naorCommitAt (generator : List Bool → List Bool) (r : List Bool) (openFlag b : Bool) (seed pad : List Bool) : List Bool

Commit to one bit using seed when openFlag = true, or a pre-expanded pad when openFlag = false.

@[simp]

theorem Cslib.Crypto.naorCommitAt_true (generator : List Bool → List Bool) (r : List Bool) (b : Bool) (seed pad : List Bool) : naorCommitAt generator r true b seed pad = naorCommit generator r b seed

@[simp]

theorem Cslib.Crypto.naorCommitAt_false (generator : List Bool → List Bool) (r : List Bool) (b : Bool) (seed pad : List Bool) : naorCommitAt generator r false b seed pad = naorCommit id r b pad

theorem Cslib.Crypto.computableTidilyInPolyTime_naorCommitAt {α : Type} {input : α ↪ List Bool} {generator : List Bool → List Bool} {r : α → List Bool} {openFlag b : α → Bool} {seed pad : α → List Bool} (hg : Turing.MultiTapeTM.ComputableTidilyInPolyTime generator Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (hr : Turing.MultiTapeTM.ComputableTidilyInPolyTime r input Turing.MultiTapeTM.encBits) (hopen : Turing.MultiTapeTM.ComputableTidilyInPolyTime openFlag input Turing.MultiTapeTM.encBool) (hb : Turing.MultiTapeTM.ComputableTidilyInPolyTime b input Turing.MultiTapeTM.encBool) (hseed : Turing.MultiTapeTM.ComputableTidilyInPolyTime seed input Turing.MultiTapeTM.encBits) (hpad : Turing.MultiTapeTM.ComputableTidilyInPolyTime pad input Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => naorCommitAt generator (r a) (openFlag a) (b a) (seed a) (pad a)) input Turing.MultiTapeTM.encBits

theorem Cslib.Crypto.uniformList_map_naorCommitAt (m : ℕ) (generator : List Bool → List Bool) (r : List Bool) (openFlag b : Bool) (seed : List Bool) : PMF.map (naorCommitAt generator r openFlag b seed) (BitString.uniformList m) = PMF.map (naorCommitAt generator r openFlag (openFlag && b) seed) (BitString.uniformList m)

When the unopened pad is drawn uniformly from BitString.uniformList m, the committed bit at an unopened coordinate is information-theoretically hidden and may be replaced by openFlag && b.

def Cslib.Crypto.naorMaskBits : List Bool → List Bool → List Bool

Keep the bits at opened coordinates and zero out unopened coordinates to false.

@[simp]

theorem Cslib.Crypto.length_naorMaskBits (openFlags bits : List Bool) : (naorMaskBits openFlags bits).length = bits.length

theorem Cslib.Crypto.getD_naorMaskBits (openFlags bits : List Bool) (i : ℕ) : (naorMaskBits openFlags bits).getD i false = (openFlags.getD i false && bits.getD i false)

theorem Cslib.Crypto.naorMaskBits_eq_map (openFlags bits : List Bool) : naorMaskBits openFlags bits = List.map (fun (i : ℕ) => openFlags.getD i false && bits.getD i false) (List.range bits.length)

theorem Cslib.Crypto.computableTidilyInPolyTime_naorMaskBits {α : Type} {input : α ↪ List Bool} {openFlags bits : α → List Bool} (hopen : Turing.MultiTapeTM.ComputableTidilyInPolyTime openFlags input Turing.MultiTapeTM.encBits) (hbits : Turing.MultiTapeTM.ComputableTidilyInPolyTime bits input Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => naorMaskBits (openFlags a) (bits a)) input Turing.MultiTapeTM.encBits

def Cslib.Crypto.naorCommitSplit (generator : List Bool → List Bool) (r : List Bool) : List Bool → List Bool → List (List Bool) → List (List Bool) → List (List Bool)

Batch commitment using seeds at opened coordinates and pre-expanded pads at unopened coordinates.

@[simp]

theorem Cslib.Crypto.length_naorCommitSplit (generator : List Bool → List Bool) (r openFlags bits : List Bool) (seeds pads : List (List Bool)) : (naorCommitSplit generator r openFlags bits seeds pads).length = bits.length

theorem Cslib.Crypto.getD_naorCommitSplit (generator : List Bool → List Bool) (r openFlags bits : List Bool) (seeds pads : List (List Bool)) (i : ℕ) (hi : i < bits.length) : (naorCommitSplit generator r openFlags bits seeds pads).getD i [] = naorCommitAt generator r (openFlags.getD i false) (bits.getD i false) (seeds.getD i []) (pads.getD i [])

theorem Cslib.Crypto.naorCommitSplit_eq_map (generator : List Bool → List Bool) (r openFlags bits : List Bool) (seeds pads : List (List Bool)) : naorCommitSplit generator r openFlags bits seeds pads = List.map (fun (i : ℕ) => naorCommitAt generator r (openFlags.getD i false) (bits.getD i false) (seeds.getD i []) (pads.getD i [])) (List.range bits.length)

theorem Cslib.Crypto.computableTidilyInPolyTime_naorCommitSplit {α : Type} {input : α ↪ List Bool} {generator : List Bool → List Bool} {r openFlags bits : α → List Bool} {seeds pads : α → List (List Bool)} (hg : Turing.MultiTapeTM.ComputableTidilyInPolyTime generator Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (hr : Turing.MultiTapeTM.ComputableTidilyInPolyTime r input Turing.MultiTapeTM.encBits) (hopen : Turing.MultiTapeTM.ComputableTidilyInPolyTime openFlags input Turing.MultiTapeTM.encBits) (hbits : Turing.MultiTapeTM.ComputableTidilyInPolyTime bits input Turing.MultiTapeTM.encBits) (hseeds : Turing.MultiTapeTM.ComputableTidilyInPolyTime seeds input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) (hpads : Turing.MultiTapeTM.ComputableTidilyInPolyTime pads input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => naorCommitSplit generator (r a) (openFlags a) (bits a) (seeds a) (pads a)) input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)

theorem Cslib.Crypto.eval_replicate_map_naorCommitSplit (m : ℕ) (generator : List Bool → List Bool) (r openFlags bits : List Bool) (seeds : List (List Bool)) : (naorCommitSplit generator r openFlags bits seeds <$> OracleComp.replicate bits.length (BitString.sampleList m)).eval = (naorCommitSplit generator r openFlags (naorMaskBits openFlags bits) seeds <$> OracleComp.replicate bits.length (BitString.sampleList m)).eval

When the unopened pads are drawn independently from BitString.sampleList m, the distribution of naorCommitSplit depends only on the masked bits naorMaskBits openFlags bits.

theorem Cslib.Crypto.naorMaskBits_append {flags₁ flags₂ bits₁ bits₂ : List Bool} (h : flags₁.length = bits₁.length) : naorMaskBits (flags₁ ++ flags₂) (bits₁ ++ bits₂) = naorMaskBits flags₁ bits₁ ++ naorMaskBits flags₂ bits₂

naorMaskBits distributes over list append when the first segments have equal length.

theorem Cslib.Crypto.naorCommitSplit_append (generator : List Bool → List Bool) (r : List Bool) {flags₁ flags₂ bits₁ bits₂ : List Bool} {seeds₁ seeds₂ pads₁ pads₂ : List (List Bool)} (hflags : flags₁.length = bits₁.length) (hseeds : seeds₁.length = bits₁.length) (hpads : pads₁.length = bits₁.length) : naorCommitSplit generator r (flags₁ ++ flags₂) (bits₁ ++ bits₂) (seeds₁ ++ seeds₂) (pads₁ ++ pads₂) = naorCommitSplit generator r flags₁ bits₁ seeds₁ pads₁ ++ naorCommitSplit generator r flags₂ bits₂ seeds₂ pads₂

naorCommitSplit distributes over list append when the first segments have equal length.

def Cslib.Crypto.naorSelectSeeds (s : ℕ) : List Bool → List Bool → List (List Bool) → List (List Bool)

Select seeds of width s at opened coordinates and pad unopened coordinates with s false bits.

@[simp]

theorem Cslib.Crypto.length_naorSelectSeeds (s : ℕ) (openFlags bits : List Bool) (seeds : List (List Bool)) : (naorSelectSeeds s openFlags bits seeds).length = bits.length

theorem Cslib.Crypto.length_mem_naorSelectSeeds {s : ℕ} {openFlags bits : List Bool} {seeds : List (List Bool)} {w : List Bool} (hw : w ∈ naorSelectSeeds s openFlags bits seeds) : w.length = s

theorem Cslib.Crypto.getD_naorSelectSeeds (s : ℕ) (openFlags bits : List Bool) (seeds : List (List Bool)) (i : ℕ) (hi : i < bits.length) : (naorSelectSeeds s openFlags bits seeds).getD i [] = if openFlags.getD i false = true then BitString.listRow s 0 (seeds.getD i []) else List.replicate s false

theorem Cslib.Crypto.naorSelectSeeds_eq_map (s : ℕ) (openFlags bits : List Bool) (seeds : List (List Bool)) : naorSelectSeeds s openFlags bits seeds = List.map (fun (i : ℕ) => if openFlags.getD i false = true then BitString.listRow s 0 (seeds.getD i []) else List.replicate s false) (List.range bits.length)

@[simp]

theorem Cslib.Crypto.naorSelectSeeds_naorMaskBits (s : ℕ) (openFlags bits : List Bool) (seeds : List (List Bool)) : naorSelectSeeds s openFlags (naorMaskBits openFlags bits) seeds = naorSelectSeeds s openFlags bits seeds

theorem Cslib.Crypto.computableTidilyInPolyTime_naorSelectSeeds {α : Type} {input : α ↪ List Bool} {s : α → ℕ} {openFlags bits : α → List Bool} {seeds : α → List (List Bool)} (hs : Turing.MultiTapeTM.ComputableTidilyInPolyTime s input Turing.MultiTapeTM.encUnary) (hopen : Turing.MultiTapeTM.ComputableTidilyInPolyTime openFlags input Turing.MultiTapeTM.encBits) (hbits : Turing.MultiTapeTM.ComputableTidilyInPolyTime bits input Turing.MultiTapeTM.encBits) (hseeds : Turing.MultiTapeTM.ComputableTidilyInPolyTime seeds input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => naorSelectSeeds (s a) (openFlags a) (bits a) (seeds a)) input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)

def Cslib.Crypto.naorSelectPads (generator : List Bool → List Bool) : List Bool → List Bool → List (List Bool) → List (List Bool) → List (List Bool)

Select generator seed at opened coordinates and pad at unopened coordinates.

theorem Cslib.Crypto.naorCommitSplit_eq_naorSelectPads (generator : List Bool → List Bool) (r openFlags bits : List Bool) (seeds pads : List (List Bool)) : naorCommitSplit generator r openFlags bits seeds pads = naorCommitSplit id r (List.replicate bits.length false) bits [] (naorSelectPads generator openFlags bits seeds pads)

naorCommitSplit depends on seeds and pads only through naorSelectPads.

theorem Cslib.Crypto.eval_replicate_naorSelectPads (s : ℕ) (generator : List Bool → List Bool) (openFlags bits : List Bool) : (do let seeds ← OracleComp.replicate bits.length (BitString.sampleList s) let pads ← OracleComp.replicate bits.length (generator <$> BitString.sampleList s) pure (naorSelectPads generator openFlags bits seeds pads, naorSelectSeeds s openFlags bits seeds)).eval = ((fun (seeds : List (List Bool)) => (naorSelectPads generator (List.replicate bits.length true) bits seeds [], naorSelectSeeds s openFlags bits seeds)) <$> OracleComp.replicate bits.length (BitString.sampleList s)).eval

When pads are drawn from generator <$> BitString.sampleList s and seeds from BitString.sampleList s, the joint law of (naorSelectPads, naorSelectSeeds) is identical to using seeds at all coordinates (openFlags = List.replicate bits.length true).

Packaged bit commitment scheme

def Cslib.Crypto.naorVerify (generator : List Bool → List Bool) (n : ℕ) (r c : List Bool) (b : Bool) (seed : List Bool) : Bool

Verification of a Naor bit commitment opening (b, seed) against seed length n, receiver string r, and commitment c.

theorem Cslib.Crypto.computableTidilyInPolyTime_naorVerify {α : Type} {input : α ↪ List Bool} {generator : List Bool → List Bool} {n : α → ℕ} {r c : α → List Bool} {b : α → Bool} {seed : α → List Bool} (hg : Turing.MultiTapeTM.ComputableTidilyInPolyTime generator Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (hn : Turing.MultiTapeTM.ComputableTidilyInPolyTime n input Turing.MultiTapeTM.encUnary) (hr : Turing.MultiTapeTM.ComputableTidilyInPolyTime r input Turing.MultiTapeTM.encBits) (hc : Turing.MultiTapeTM.ComputableTidilyInPolyTime c input Turing.MultiTapeTM.encBits) (hb : Turing.MultiTapeTM.ComputableTidilyInPolyTime b input Turing.MultiTapeTM.encBool) (hseed : Turing.MultiTapeTM.ComputableTidilyInPolyTime seed input Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => naorVerify generator (n a) (r a) (c a) (b a) (seed a)) input Turing.MultiTapeTM.encBool

theorem Cslib.Crypto.computableInPolyTime_naorVerify {α : Type} {input : α ↪ List Bool} {generator : List Bool → List Bool} {n : α → ℕ} {r c : α → List Bool} {b : α → Bool} {seed : α → List Bool} (hg : Turing.MultiTapeTM.ComputableInPolyTime generator Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (hn : Turing.MultiTapeTM.ComputableInPolyTime n input Turing.MultiTapeTM.encUnary) (hr : Turing.MultiTapeTM.ComputableInPolyTime r input Turing.MultiTapeTM.encBits) (hc : Turing.MultiTapeTM.ComputableInPolyTime c input Turing.MultiTapeTM.encBits) (hb : Turing.MultiTapeTM.ComputableInPolyTime b input Turing.MultiTapeTM.encBool) (hseed : Turing.MultiTapeTM.ComputableInPolyTime seed input Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => naorVerify generator (n a) (r a) (c a) (b a) (seed a)) input Turing.MultiTapeTM.encBool

Naor commitment verification is computable in plain polynomial time when its inputs are.

theorem Cslib.Crypto.naorVerify_naorCommit {generator : List Bool → List Bool} {n : ℕ} (r : List Bool) (b : Bool) {seed : List Bool} (hseed : seed.length = n) : naorVerify generator n r (naorCommit generator r b seed) b seed = true

theorem Cslib.Crypto.eq_naorCommit_of_naorVerify {generator : List Bool → List Bool} {n : ℕ} {r c : List Bool} {b : Bool} {seed : List Bool} (h : naorVerify generator n r c b seed = true) : seed.length = n ∧ c = naorCommit generator r b seed

structure Cslib.Crypto.BitCommitmentScheme : Type

A two-message statistically binding, computationally hiding bit commitment scheme [Nao91]. At security parameter n, the receiver sends a uniform challenge string r of length challengeLength n, the committer commits to b : Bool using a uniform seed seed of length n via commit r b seed of length commitLength n, and openings are verified by verify n r c b seed. Hiding (stateful_hiding) holds against any two-stage randomized stateful PPT receiver (CommitmentReceiver).

• challengeLength : ℕ → ℕ

  Length of the receiver's first-round challenge at security parameter n.

• commitLength : ℕ → ℕ

  Length of the commitment string at security parameter n.

• commit : List Bool → Bool → List Bool → List Bool

  Commitment function taking receiver string r, bit b, and n-bit seed seed.

• verify : ℕ → List Bool → List Bool → Bool → List Bool → Bool

  Verification of an opening (b, seed) against (n, r, c).

• polyTime_challengeLength : Turing.MultiTapeTM.ComputableInPolyTime self.challengeLength Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary

  challengeLength is computable in plain polynomial time in unary.

• polyTime_commitLength : Turing.MultiTapeTM.ComputableInPolyTime self.commitLength Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary

  commitLength is computable in plain polynomial time in unary.

• polyTime_commit : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List Bool × Bool × List Bool) => self.commit p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBool Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits

  commit is computable in plain polynomial time.

• polyTime_verify : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool × List Bool × Bool × List Bool) => self.verify p.1 p.2.1 p.2.2.1 p.2.2.2.1 p.2.2.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBool Turing.MultiTapeTM.encBits)))) Turing.MultiTapeTM.encBool

  verify is computable in plain polynomial time.

• length_commit (n : ℕ) (r : List Bool) (b : Bool) (seed : List Bool) : seed.length = n → (self.commit r b seed).length = self.commitLength n

  Honest commitments have length commitLength n when seed.length = n.

• verify_commit (n : ℕ) (r : List Bool) (b : Bool) (seed : List Bool) : seed.length = n → self.verify n r (self.commit r b seed) b seed = true

  Correctness: an honest commitment is accepted by verify.

• eq_commit_of_verify {n : ℕ} {r c : List Bool} {b : Bool} {seed : List Bool} : self.verify n r c b seed = true → seed.length = n ∧ c = self.commit r b seed

  Soundness of verify: if verify n r c b seed = true, then seed.length = n and c = commit r b seed.

• statistical_binding : Negligible fun (n : ℕ) => ((BitString.uniformList (self.challengeLength n)).toOuterMeasure {r : List Bool | ¬∀ (s₀ s₁ : List Bool), s₀.length = n → s₁.length = n → self.commit r false s₀ ≠ self.commit r true s₁}).toNNReal

  Statistical binding: the probability over a uniform receiver challenge r of length challengeLength n that two n-bit seeds open to false and true with the same commitment is negligible in n.

• stateful_hiding : StatefulHiding self.commit

  Computational hiding against a randomized stateful PPT receiver: for every polynomial-time auxiliary family aux : ℕ → List Bool, no strict PPT CommitmentReceiver can distinguish commitments to its first chosen bit (bit = false) from commitments to its second chosen bit (bit = true) with non-negligible advantage.

theorem Cslib.Crypto.BitCommitmentScheme.computational_hiding (h : BitCommitmentScheme) (r : ℕ → List Bool) (b₀ b₁ : ℕ → Bool) : Turing.MultiTapeTM.ComputableInPolyTime r Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits → Turing.MultiTapeTM.ComputableInPolyTime b₀ Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool → Turing.MultiTapeTM.ComputableInPolyTime b₁ Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool → ComputationallyIndistinguishable (fun (n : ℕ) => PMF.map (h.commit (r n) (b₀ n)) (BitString.uniformList n)) fun (n : ℕ) => PMF.map (h.commit (r n) (b₁ n)) (BitString.uniformList n)

Deterministic-family computational hiding derived from BitCommitmentScheme.stateful_hiding: for every deterministic polynomial-time family of receiver strings r : ℕ → List Bool and any two deterministic polynomial-time families of committed bits b₀ b₁ : ℕ → Bool, the commitment ensembles for b₀ and b₁ are computationally indistinguishable against uniform strict PPT distinguishers.

theorem Cslib.Crypto.BitCommitmentScheme.polyTime_challengeLength_tidy (h : BitCommitmentScheme) : Turing.MultiTapeTM.ComputableTidilyInPolyTime h.challengeLength Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary

The equivalent tidy contract used internally by compositional proofs.

theorem Cslib.Crypto.BitCommitmentScheme.polyTime_commitLength_tidy (h : BitCommitmentScheme) : Turing.MultiTapeTM.ComputableTidilyInPolyTime h.commitLength Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary

The equivalent tidy contract used internally by compositional proofs.

theorem Cslib.Crypto.BitCommitmentScheme.polyTime_commit_tidy (h : BitCommitmentScheme) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (p : List Bool × Bool × List Bool) => h.commit p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBool Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits

The equivalent tidy contract used internally by compositional proofs.

theorem Cslib.Crypto.BitCommitmentScheme.polyTime_verify_tidy (h : BitCommitmentScheme) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (p : ℕ × List Bool × List Bool × Bool × List Bool) => h.verify p.1 p.2.1 p.2.2.1 p.2.2.2.1 p.2.2.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBool Turing.MultiTapeTM.encBits)))) Turing.MultiTapeTM.encBool

The equivalent tidy contract used internally by compositional proofs.

theorem Cslib.Crypto.BitCommitmentScheme.computational_hiding_tidy (h : BitCommitmentScheme) (r : ℕ → List Bool) (b₀ b₁ : ℕ → Bool) : Turing.MultiTapeTM.ComputableTidilyInPolyTime r Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits → Turing.MultiTapeTM.ComputableTidilyInPolyTime b₀ Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool → Turing.MultiTapeTM.ComputableTidilyInPolyTime b₁ Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool → ComputationallyIndistinguishable (fun (n : ℕ) => PMF.map (h.commit (r n) (b₀ n)) (BitString.uniformList n)) fun (n : ℕ) => PMF.map (h.commit (r n) (b₁ n)) (BitString.uniformList n)

The equivalent tidy contract used internally by compositional proofs.

def Cslib.Crypto.PseudorandomGenerator.naorBitCommitment {generator : List Bool → List Bool} {length : ℕ → ℕ} (hG : PseudorandomGenerator generator length) (hstretch : ∀ (n : ℕ), 3 * n ≤ length n) : BitCommitmentScheme

Naor's bit commitment scheme built from any pseudorandom generator with stretch at least 3 * n [Nao91].

theorem Cslib.Crypto.OneWay.exists_bitCommitmentScheme {f : List Bool → List Bool} (hf : OneWay f) : Nonempty BitCommitmentScheme

Existence of bit commitments from one-way functions [Nao91]: if a one-way function exists, then there exists a statistically binding, computationally hiding bit commitment scheme (with hiding against randomized stateful PPT receivers, BitCommitmentScheme.stateful_hiding).