Commitment Schemes: Syntax and Correctness

The syntax of a commitment scheme ([BS23], Section 8.12): committing to a message samples a commitment-opening pair (c, o), verification of a claimed opening is deterministic, and honestly generated pairs always verify.

The algorithms are plain functions, with no efficiency or finiteness assumptions. Security notions live in separate definitions, so the same syntax can carry perfect, statistical, or computational security.

Main definitions

• Scheme: commitment syntax with perfect correctness
• Scheme.commitmentDist: the public commitment distribution for a message
• Scheme.mem_support_commitmentDist_iff: a commitment is possible exactly when it has a possible opening
• Scheme.Accepts: the verifier's acceptance relation

References

• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Version 0.6

structure Cslib.Crypto.Protocols.Commitment.Scheme (Message : Type u_1) (Commitment : Type u_2) (Opening : Type u_3) : Type (max (max u_1 u_2) u_3)

A noninteractive, unkeyed commitment scheme over message, commitment, and opening types ([BS23], Section 8.12).

Committing is randomized and produces the commitment and opening together, since the two may be correlated. Correctness requires that every commitment-opening pair the honest committer can output is accepted by the verifier; for a PMF, this says honest openings verify with probability one.

• commit (message : Message) : PMF (Commitment × Opening)

  Randomized commitment and opening generation.

• verify (message : Message) (commitment : Commitment) (opening : Opening) : Bool

  Deterministic verification of a claimed opening.

• correct (message : Message) (commitment : Commitment) (opening : Opening) : (commitment, opening) ∈ (self.commit message).support → self.verify message commitment opening = true

  Every honestly generated commitment-opening pair verifies.

noncomputable def Cslib.Crypto.Protocols.Commitment.Scheme.commitmentDist {Message : Type u_1} {Commitment : Type u_2} {Opening : Type u_3} (scheme : Scheme Message Commitment Opening) (message : Message) : PMF Commitment

The public commitment distribution obtained by forgetting the opening.

Equations

• scheme.commitmentDist message = PMF.map Prod.fst (scheme.commit message)

theorem Cslib.Crypto.Protocols.Commitment.Scheme.mem_support_commitmentDist_iff {Message : Type u_1} {Commitment : Type u_2} {Opening : Type u_3} (scheme : Scheme Message Commitment Opening) {message : Message} {commitment : Commitment} : commitment ∈ (scheme.commitmentDist message).support ↔ ∃ (opening : Opening), (commitment, opening) ∈ (scheme.commit message).support

A commitment lies in the public distribution's support exactly when some opening makes the corresponding pair an honest possible output.

def Cslib.Crypto.Protocols.Commitment.Scheme.Accepts {Message : Type u_1} {Commitment : Type u_2} {Opening : Type u_3} (scheme : Scheme Message Commitment Opening) (message : Message) (commitment : Commitment) (opening : Opening) : Prop

The proposition that an opening is accepted for a commitment and message.

Equations

• scheme.Accepts message commitment opening = (scheme.verify message commitment opening = true)

theorem Cslib.Crypto.Protocols.Commitment.Scheme.accepts_of_mem_support {Message : Type u_1} {Commitment : Type u_2} {Opening : Type u_3} (scheme : Scheme Message Commitment Opening) {message : Message} {commitment : Commitment} {opening : Opening} (h : (commitment, opening) ∈ (scheme.commit message).support) : scheme.Accepts message commitment opening

Every pair in the support of an honest commitment is accepted.

noncomputable def Cslib.Crypto.Protocols.Commitment.Scheme.ofPure {Message : Type u_1} {Commitment : Type u_2} {Opening : Type u_3} (commit : Message → Commitment × Opening) (verify : Message → Commitment → Opening → Bool) (correct : ∀ (message : Message), verify message (commit message).1 (commit message).2 = true) : Scheme Message Commitment Opening

Build a commitment scheme from a deterministic commitment generation.

Equations

• Cslib.Crypto.Protocols.Commitment.Scheme.ofPure commit verify correct = { commit := fun (message : Message) => PMF.pure (commit message), verify := verify, correct := ⋯ }