Commitment Schemes

Basic results about information-theoretic commitment schemes.

The main result is the hiding–binding trade-off: a perfectly binding scheme places the commitment distributions of distinct messages at the maximum statistical distance, so it cannot be statistically hiding for any error below one. Hiding and binding can therefore not both hold unconditionally; real schemes make at most one side information-theoretic and settle for a computational version of the other.

Main results

• Scheme.subsingleton_of_statisticallyHiding_of_perfectlyBinding: a scheme cannot be both statistically hiding with error below one and perfectly binding unless any two messages are equal
• Scheme.PerfectlyBinding.dist_commitmentDist_eq_one: perfect binding forces distinct messages' commitment distributions to the maximum statistical distance
• Scheme.subsingleton_of_perfectlyHiding_of_perfectlyBinding: the perfect hiding case, with no finiteness assumption on commitments
• Scheme.perfectlyHiding_iff_statisticallyHiding_zero: perfect hiding is statistical hiding with zero error

theorem Cslib.Crypto.Protocols.Commitment.Scheme.perfectlyHiding_iff_statisticallyHiding_zero {Message : Type u_1} {Commitment : Type u_2} {Opening : Type u_3} [Fintype Commitment] (scheme : Scheme Message Commitment Opening) : scheme.PerfectlyHiding ↔ scheme.StatisticallyHiding 0

Perfect hiding is exactly statistical hiding with zero error.

theorem Cslib.Crypto.Protocols.Commitment.Scheme.StatisticallyHiding.mono {Message : Type u_1} {Commitment : Type u_2} {Opening : Type u_3} [Fintype Commitment] {scheme : Scheme Message Commitment Opening} : Monotone scheme.StatisticallyHiding

Enlarging the permitted error preserves statistical hiding.

theorem Cslib.Crypto.Protocols.Commitment.Scheme.PerfectlyBinding.disjoint_support_commitmentDist {Message : Type u_1} {Commitment : Type u_2} {Opening : Type u_3} {scheme : Scheme Message Commitment Opening} (hbind : scheme.PerfectlyBinding) {message₀ message₁ : Message} (hne : message₀ ≠ message₁) : Disjoint (scheme.commitmentDist message₀).support (scheme.commitmentDist message₁).support

Distinct messages of a perfectly binding scheme have disjoint sets of possible commitments.

theorem Cslib.Crypto.Protocols.Commitment.Scheme.PerfectlyBinding.dist_commitmentDist_eq_one {Message : Type u_1} {Commitment : Type u_2} {Opening : Type u_3} [Fintype Commitment] {scheme : Scheme Message Commitment Opening} (hbind : scheme.PerfectlyBinding) {message₀ message₁ : Message} (hne : message₀ ≠ message₁) : dist (scheme.commitmentDist message₀) (scheme.commitmentDist message₁) = 1

In a perfectly binding scheme, the commitment distributions of distinct messages are at the maximum statistical distance: an unbounded observer can read the message off the commitment.

theorem Cslib.Crypto.Protocols.Commitment.Scheme.subsingleton_of_statisticallyHiding_of_perfectlyBinding {Message : Type u_1} {Commitment : Type u_2} {Opening : Type u_3} [Fintype Commitment] (scheme : Scheme Message Commitment Opening) {ε : NNReal} (hε : ε < 1) (hhide : scheme.StatisticallyHiding ε) (hbind : scheme.PerfectlyBinding) : Subsingleton Message

The hiding–binding trade-off. A scheme cannot be both statistically hiding with error below one and perfectly binding unless any two messages are equal. The error bound is sharp: statistical hiding with error one holds vacuously for every scheme.

theorem Cslib.Crypto.Protocols.Commitment.Scheme.subsingleton_of_perfectlyHiding_of_perfectlyBinding {Message : Type u_1} {Commitment : Type u_2} {Opening : Type u_3} (scheme : Scheme Message Commitment Opening) (hhide : scheme.PerfectlyHiding) (hbind : scheme.PerfectlyBinding) : Subsingleton Message

A scheme cannot be both perfectly hiding and perfectly binding unless any two messages are equal. Unlike the statistical version, this needs no finiteness assumption on the commitment type.