Commitment Schemes: Perfect Hiding and Perfect Binding

A commitment scheme lets a sender commit to a message m — publishing a commitment c that hides m — and later open it by revealing m together with the randomness r. Following Rosulek, The Joy of Cryptography (Chapter on commitment schemes), the two security goals are:

• hiding — the commitment c reveals nothing about the committed message;
• binding — the sender cannot open a single commitment to two different messages.

This file defines a minimal CommScheme structure, the hiding game (phrased over the core AdvantageA), and the perfect-binding predicate, then instantiates two schemes over Bool:

• MaskComm — the one-time-pad / masking commitment commit(m; r) = m ⊕ r with r uniform. A uniform mask makes the commitment uniform and independent of m, so the hiding advantage of every adversary is exactly 0 (perfect hiding).
• IdComm — the trivial deterministic commitment commit(m; r) = m, which is perfectly binding.

The two examples witness the information-theoretic tension Rosulek highlights: a commitment scheme cannot be simultaneously perfectly hiding and perfectly binding. MaskComm is the OTP argument on the hiding side; IdComm shows the binding predicate is inhabited.

Main definitions

• CommScheme — a commitment scheme (commit, verify, uniform randomness).
• Hiding_Game / Hiding_Adv — the hiding game and its advantage.
• CommScheme.PerfectlyBinding — no commitment opens to two distinct messages.
• MaskComm, IdComm — the masking and identity commitments over Bool.

Main results

• maskComm_correct — an honest opening of a MaskComm commitment verifies.
• maskComm_perfect_hiding — the masking commitment is perfectly hiding: Hiding_Adv MaskComm m₀ m₁ A = 0 for every adversary A.
• idComm_perfectly_binding — the identity commitment is perfectly binding.

References

• [Rosulek, The Joy of Cryptography, Chapter on commitment schemes]
• [Shannon, Communication Theory of Secrecy Systems, 1949]

Commitment Scheme

structure CatCrypt.Examples.Commitment.CommScheme : Type 1

A (non-interactive) commitment scheme.

• Message, Randomness, Commitment are the data types.
• commit r m produces the commitment to message m under randomness r.
• verify c m r checks that (m, r) is a valid opening of the commitment c.

Randomness is required finite and nonempty so it can be sampled uniformly in the hiding game.

• Message : Type

  Message (committed value) type

• Randomness : Type

  Randomness (opening) type

• Commitment : Type

  Commitment type

• finRand : Fintype self.Randomness

  Randomness is finite (for uniform sampling)

• neRand : Nonempty self.Randomness

  Randomness is nonempty (for uniform sampling)

• commit : self.Randomness → self.Message → self.Commitment

  Deterministic commitment function

• verify : self.Commitment → self.Message → self.Randomness → Bool

  Opening verification: is (m, r) a valid opening of c?

def CatCrypt.Examples.Commitment.CommScheme.Correct (C : CommScheme) : Prop

Correctness: an honestly produced commitment opens back to its message.

Equations

• C.Correct = ∀ (r : C.Randomness) (m : C.Message), C.verify (C.commit r m) m r = true

def CatCrypt.Examples.Commitment.CommScheme.PerfectlyBinding (C : CommScheme) : Prop

Perfect binding: no commitment can be opened to two distinct messages. That is, if (m₀, r₀) and (m₁, r₁) both verify against the same commitment c, then m₀ = m₁.

Equations

• C.PerfectlyBinding = ∀ (c : C.Commitment) (m₀ m₁ : C.Message) (r₀ r₁ : C.Randomness), C.verify c m₀ r₀ = true → C.verify c m₁ r₁ = true → m₀ = m₁

Hiding Game

noncomputable def CatCrypt.Examples.Commitment.Hiding_Game (C : CommScheme) (m₀ m₁ : C.Message) (b : Bool) : Core.SPComp C.Commitment

The hiding game for a commitment scheme.

The challenger samples fresh randomness r and returns the commitment to m₀ (when b = true) or m₁ (when b = false). The adversary is given the commitment and tries to guess b.

• Hiding_Game C m₀ m₁ true — commits to m₀ (left)
• Hiding_Game C m₀ m₁ false — commits to m₁ (right)

Equations

• CatCrypt.Examples.Commitment.Hiding_Game C m₀ m₁ b = do let r ← CatCrypt.Core.SPComp.sample C.Randomness CatCrypt.Core.SPComp.pure (C.commit r (if b = true then m₀ else m₁))

noncomputable def CatCrypt.Examples.Commitment.Hiding_Adv (C : CommScheme) (m₀ m₁ : C.Message) (A : C.Commitment → Core.SPComp Bool) : ENNReal

Hiding advantage: the probability with which an adversary distinguishes a commitment to m₀ from a commitment to m₁.

Equations

• CatCrypt.Examples.Commitment.Hiding_Adv C m₀ m₁ A = CatCrypt.Crypto.AdvantageA (CatCrypt.Examples.Commitment.Hiding_Game C m₀ m₁ true) (CatCrypt.Examples.Commitment.Hiding_Game C m₀ m₁ false) A

Masking Commitment: Perfect Hiding

commit(m; r) = m ⊕ r, the one-time-pad commitment.

noncomputable def CatCrypt.Examples.Commitment.MaskComm : CommScheme

The masking commitment over Bool: commit r m = r ⊕ m, opened by revealing (m, r). This is the one-time-pad commitment.

Equations

• One or more equations did not get rendered due to their size.

theorem CatCrypt.Examples.Commitment.maskComm_correct : MaskComm.Correct

The masking commitment is correct: an honest opening verifies.

theorem CatCrypt.Examples.Commitment.maskComm_hiding_coupling (m₀ m₁ : Bool) : Relational.rHoare Relational.eqPre (Hiding_Game MaskComm m₀ m₁ true) (Hiding_Game MaskComm m₀ m₁ false) Relational.eqPost

Coupling: the two hiding games for the masking commitment are equidistributed.

For a uniform mask r, both r ⊕ m₀ and r ⊕ m₁ are uniformly distributed (XOR-by-a-fixed-bit is a bijection of the mask). The bijection boolXorBij (m₀ ⊕ m₁) re-labels the mask on the right so the two commitments coincide, coupling the games under eqPost.

theorem CatCrypt.Examples.Commitment.maskComm_perfect_hiding (m₀ m₁ : Bool) (A : MaskComm.Commitment → Core.SPComp Bool) : Hiding_Adv MaskComm m₀ m₁ A = 0

The masking commitment is perfectly hiding: every adversary has hiding advantage exactly 0.

Reflection into the Package / UC Stack

The shallow maskComm_perfect_hiding bounds a single distinguisher applied to the two hiding-game bodies. This section lifts it to a composable statement about deep nominal packages linked with an arbitrary adversary package, following the stack shallow game → rawCode% → NomPackage.ofOracle → DeepNomAdvantage → sdist → UC via the shared CatCryptCore.Deep.ReflectUCHelpers combinators. The masking commitment commit r m = r ⊕ m is heap-independent, so the shallow coupling maskComm_hiding_coupling upgrades to a full SPComp equality of the two reflected bodies (spcomp_eq_of_isPure_coupling), and the whole stack follows with no purity bridge on the adversary.

noncomputable def CatCrypt.Examples.Commitment.maskGameRaw (m₀ m₁ b : Bool) : Deep.RawCode Bool

The reflected masking-commitment hiding-game body for bit b: sample a uniform mask r and return the one-time-pad commitment r ⊕ (if b then m₀ else m₁).

Equations

• CatCrypt.Examples.Commitment.maskGameRaw m₀ m₁ b = (CatCrypt.Deep.RawCode.sample Bool).bind fun (r : Bool) => CatCrypt.Deep.RawCode.ret (r ^^ if b = true then m₀ else m₁)

instance CatCrypt.Examples.Commitment.instValidMaskGameRaw (m₀ m₁ b : Bool) : Deep.IsValid ∅ (maskGameRaw m₀ m₁ b)

theorem CatCrypt.Examples.Commitment.maskGameRaw_eval_shallow (m₀ m₁ b : Bool) : (maskGameRaw m₀ m₁ b).eval = Hiding_Game MaskComm m₀ m₁ b

The reflected body evaluates back to the shallow hiding game.

theorem CatCrypt.Examples.Commitment.mask_game_isPure (m₀ m₁ b : Bool) : (Hiding_Game MaskComm m₀ m₁ b).IsPure

The hiding game is heap-independent (a uniform mask then a pure commitment).

theorem CatCrypt.Examples.Commitment.maskGameRaw_eval_eq (m₀ m₁ : Bool) : (maskGameRaw m₀ m₁ true).eval = (maskGameRaw m₀ m₁ false).eval

The two reflected bodies (commit to m₀ vs. m₁) have equal evaluations: the heap-independent coupling maskComm_hiding_coupling upgrades to SPComp equality.

noncomputable def CatCrypt.Examples.Commitment.maskGameTrue (m₀ m₁ : Bool) : Deep.NomPackage

Real hiding game as an oracle-exporting nominal package (commits to m₀).

Equations

• CatCrypt.Examples.Commitment.maskGameTrue m₀ m₁ = CatCrypt.Deep.NomPackage.ofOracle 1 Unit Bool fun (x : Unit) => CatCrypt.Examples.Commitment.maskGameRaw m₀ m₁ true

noncomputable def CatCrypt.Examples.Commitment.maskGameFalse (m₀ m₁ : Bool) : Deep.NomPackage

Ideal hiding game as an oracle-exporting nominal package (commits to m₁).

Equations

• CatCrypt.Examples.Commitment.maskGameFalse m₀ m₁ = CatCrypt.Deep.NomPackage.ofOracle 1 Unit Bool fun (x : Unit) => CatCrypt.Examples.Commitment.maskGameRaw m₀ m₁ false

theorem CatCrypt.Examples.Commitment.mask_deepnom_zero (m₀ m₁ : Bool) (A : Deep.NomPackage) : Crypto.DeepNomAdvantage (maskGameTrue m₀ m₁) (maskGameFalse m₀ m₁) A = 0

Zero deep-nominal advantage against every adversary package.

theorem CatCrypt.Examples.Commitment.mask_sdist_zero (m₀ m₁ : Bool) : (Crypto.sdist (fun (A : Deep.NomPackage) => Crypto.runPkg (A.pkg.link (maskGameTrue m₀ m₁).pkg)) fun (A : Deep.NomPackage) => Crypto.runPkg (A.pkg.link (maskGameFalse m₀ m₁).pkg)) = 0

Statistical distance zero between the two linked-game families.

theorem CatCrypt.Examples.Commitment.mask_nompkg_secure (m₀ m₁ : Bool) : Crypto.NomPkgSecure (maskGameTrue m₀ m₁) (maskGameFalse m₀ m₁) fun (x : Deep.NomPackage) => 0

Package-level perfect hiding (NomPkgSecure).

theorem CatCrypt.Examples.Commitment.mask_uc (m₀ m₁ : Bool) : Crypto.UCEmulates 0 { hon := Deep.NomPackage, out := Bool, leak := Empty, sim_if := Empty, view := Bool } (fun (A : { hon := Deep.NomPackage, out := Bool, leak := Empty, sim_if := Empty, view := Bool }.hon) => Core.SPComp.map Sum.inl (Crypto.runPkg (A.pkg.link (maskGameTrue m₀ m₁).pkg))) fun (A : { hon := Deep.NomPackage, out := Bool, leak := Empty, sim_if := Empty, view := Bool }.hon) => Core.SPComp.map Sum.inl (Crypto.runPkg (A.pkg.link (maskGameFalse m₀ m₁).pkg))

Perfect UC emulation of the linked-game families over the trivial-leak interface (out = Bool, leak = Empty) with the identity simulator (composition plumbing).

theorem CatCrypt.Examples.Commitment.mask_deepnom_forward_eq_adv (m₀ m₁ : Bool) : Crypto.DeepNomAdvantage (maskGameTrue m₀ m₁) (maskGameFalse m₀ m₁) Deep.forwardAdv = Hiding_Adv MaskComm m₀ m₁ Core.SPComp.pure

Reflection mirrors the shallow game. Against the forwarding adversary, the deep-nominal advantage equals the shallow hiding advantage under the identity distinguisher — which is 0 by maskComm_perfect_hiding.

Identity Commitment: Perfect Binding

commit(m; r) = m — a deterministic commitment that ignores its randomness. It provides no hiding, but it is perfectly binding: the commitment is the message, so it can only be opened to that one message. This witnesses the hiding/binding tension: no scheme achieves both perfectly.

noncomputable def CatCrypt.Examples.Commitment.IdComm : CommScheme

The identity commitment over Bool: commit r m = m, opened by revealing m (the randomness is irrelevant).

Equations

• One or more equations did not get rendered due to their size.

theorem CatCrypt.Examples.Commitment.idComm_correct : IdComm.Correct

The identity commitment is correct.

theorem CatCrypt.Examples.Commitment.idComm_perfectly_binding : IdComm.PerfectlyBinding

The identity commitment is perfectly binding: since the commitment equals the committed message, any two valid openings expose the same message.