Commitment Schemes

This file defines non-interactive commitment schemes and their standard security properties: correctness, hiding, and binding.

Main Definitions

• CommitmentScheme PP M C D — a commitment scheme with public parameters PP, message space M, commitment space C, and opening (decommitment) space D.
• CommitmentScheme.PerfectlyCorrect — honestly generated parameters and commitments always verify.
• CommitmentScheme.PerfectlyHiding — under honestly generated parameters, commitment distribution is independent of the message.
• CommitmentScheme.hidingExp — computational hiding experiment (IND-style).
• CommitmentScheme.bindingExp — computational binding experiment.
• TrapdoorExtractor PP TD C M — trapdoor-based message extraction algorithm.
• CommitmentScheme.extractExp — extraction experiment (game-based, allows error).

structure CommitmentScheme (PP M C D : Type) : Type

A non-interactive commitment scheme with public parameters PP, message space M, commitment space C, and opening (decommitment) space D.

• setup : ProbComp PP

  Generate public parameters (e.g. a common reference string).

• commit (pp : PP) (m : M) : ProbComp (C × D)

  Commit to a message, producing a commitment and an opening.

• verify (pp : PP) (m : M) (c : C) (d : D) : Bool

  Deterministic verification that an opening is valid.

def CommitmentScheme.PerfectlyCorrect {PP M C D : Type} (cs : CommitmentScheme PP M C D) : Prop

A commitment scheme is perfectly correct if every honestly generated public parameter and commitment-opening pair passes verification.

def CommitmentScheme.PerfectlyHiding {PP M C D : Type} (cs : CommitmentScheme PP M C D) : Prop

A commitment scheme is perfectly hiding if, for every honestly generated public parameter, the commitment (first component) has the same distribution regardless of the committed message.

Computational hiding

structure CommitmentScheme.HidingAdv (PP M C : Type) : Type 1

A two-phase hiding adversary: phase 1 chooses two messages given the public parameters; phase 2 receives the commitment and tries to guess which message was committed. State carries information between the two phases.

• State : Type
• chooseMessages : PP → ProbComp (M × M × self.State)
• distinguish : self.State → C → ProbComp Bool

def CommitmentScheme.hidingExp {PP M C D : Type} (cs : CommitmentScheme PP M C D) (adversary : HidingAdv PP M C) : ProbComp Bool

Hiding experiment: the adversary chooses two messages, the challenger commits to one at random, and the adversary tries to guess which.

noncomputable def CommitmentScheme.hidingAdvantage {PP M C D : Type} (cs : CommitmentScheme PP M C D) (adversary : HidingAdv PP M C) : ℝ

Computational binding

def CommitmentScheme.BindingAdv (PP M C D : Type) : Type

A binding adversary outputs a commitment with two openings to different messages.

def CommitmentScheme.bindingExp {PP M C D : Type} [DecidableEq M] (cs : CommitmentScheme PP M C D) (adversary : BindingAdv PP M C D) : ProbComp Bool

Binding experiment: the adversary tries to open a single commitment to two distinct messages. Succeeds iff both openings verify and the messages differ.

noncomputable def CommitmentScheme.bindingAdvantage {PP M C D : Type} [DecidableEq M] (cs : CommitmentScheme PP M C D) (adversary : BindingAdv PP M C D) : ENNReal

Trapdoor extractability

structure CommitmentScheme.TrapdoorExtractor (PP TD C M : Type) : Type

A trapdoor extractor for a commitment scheme: bundles an alternative setup that produces a trapdoor alongside the public parameters, and a (potentially probabilistic) extraction algorithm that recovers the committed message from the commitment using the trapdoor.

Named TrapdoorExtractor specifically to leave room for other extraction paradigms (e.g. rewinding-based extraction).

• setupExtract : ProbComp (PP × TD)
• extract : TD → C → ProbComp M

def CommitmentScheme.TrapdoorExtractor.SetupConsistent {PP M C D TD : Type} (extractor : TrapdoorExtractor PP TD C M) (cs : CommitmentScheme PP M C D) : Prop

The extraction setup produces the same public parameter distribution as the scheme's normal setup. Required for reductions that swap in the trapdoor setup without the adversary noticing.

def CommitmentScheme.extractExp {PP M C D : Type} [DecidableEq M] (cs : CommitmentScheme PP M C D) {TD : Type} (extractor : TrapdoorExtractor PP TD C M) (m : M) : ProbComp Bool

Extraction experiment: generate parameters with trapdoor, honestly commit to message m, then check whether the extractor recovers m from the commitment.

Downstream code decides how much error to tolerate:

• Perfect extraction: ∀ m, Pr[= true | extractExp cs ext m] = 1
• Computational: bound 1 - Pr[= true | extractExp cs ext m]