Abstract Commitment Schemes

This file defines the abstract structure for commitment schemes and their security games (correctness, hiding, binding).

Main definitions

• CommitmentScheme — Structure for a commitment scheme with setup, commit, verify
• Correct_Game — Correctness game
• Hiding_Game₀/₁ — Hiding games (real/ideal)
• Binding_Game — Binding game

References

• SSProve/Commitments — Com.v
• [Kate, Zaverucha, Goldberg 2010 — §3]

Commitment Scheme Structure

structure CatCrypt.Examples.Commitments.CommitmentScheme : Type 1

An abstract commitment scheme.

A commitment scheme consists of:

• A setup algorithm producing public parameters
• A commit algorithm producing a commitment and opening
• A verify algorithm checking validity

• Key : Type

  Public parameters / key type

• Message : Type

  Message space

• Commitment : Type

  Commitment type

• Opening : Type

  Opening / decommitment type

• instFintypeKey : Fintype self.Key
• instNonemptyKey : Nonempty self.Key
• instDecEqKey : DecidableEq self.Key
• instFintypeMessage : Fintype self.Message
• instNonemptyMessage : Nonempty self.Message
• instDecEqMessage : DecidableEq self.Message
• instFintypeCommitment : Fintype self.Commitment
• instNonemptyCommitment : Nonempty self.Commitment
• instDecEqCommitment : DecidableEq self.Commitment
• instFintypeOpening : Fintype self.Opening
• instNonemptyOpening : Nonempty self.Opening
• instDecEqOpening : DecidableEq self.Opening
• setup : Core.SPComp self.Key

  Probabilistic setup algorithm

• commit : self.Key → self.Message → Core.SPComp (self.Commitment × self.Opening)

  Probabilistic commitment: (commitment, opening)

• verify : self.Key → self.Message → self.Commitment → self.Opening → Bool

  Deterministic verification

Correctness

noncomputable def CatCrypt.Examples.Commitments.Correct_Game (S : CommitmentScheme) (m : S.Message) : Core.SPComp Bool

Correctness game: setup, commit, then verify. Returns true if verify accepts the honest commitment.

Equations

• CatCrypt.Examples.Commitments.Correct_Game S m = do let k ← S.setup let __x ← S.commit k m match __x with | (c, o) => CatCrypt.Core.SPComp.pure (S.verify k m c o)

def CatCrypt.Examples.Commitments.IsCorrect (S : CommitmentScheme) : Prop

A commitment scheme is correct if for all messages, the correctness game always returns true.

Equations

• CatCrypt.Examples.Commitments.IsCorrect S = ∀ (m : S.Message), CatCrypt.Crypto.prTrue (CatCrypt.Examples.Commitments.Correct_Game S m) CatCrypt.Core.Heap.empty = 1

Hiding

structure CatCrypt.Examples.Commitments.HidingAdversary (S : CommitmentScheme) : Type

Type of hiding adversary: chooses two messages, then distinguishes

• choose : S.Key → Core.SPComp (S.Message × S.Message)

  Choose two messages given the public key

• distinguish : S.Commitment → Core.SPComp Bool

  Distinguish given commitment

noncomputable def CatCrypt.Examples.Commitments.Hiding_Game (S : CommitmentScheme) (A : HidingAdversary S) (b : Bool) : Core.SPComp Bool

Hiding game with bit b: commit to m_b

Equations

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

noncomputable def CatCrypt.Examples.Commitments.Hiding_Advantage (S : CommitmentScheme) (A : HidingAdversary S) : ENNReal

Hiding advantage

Equations

• CatCrypt.Examples.Commitments.Hiding_Advantage S A = CatCrypt.Crypto.Advantage (CatCrypt.Examples.Commitments.Hiding_Game S A false) (CatCrypt.Examples.Commitments.Hiding_Game S A true)

Binding

@[reducible, inline]

abbrev CatCrypt.Examples.Commitments.BindingAdversary (S : CommitmentScheme) : Type

Type of binding adversary: given key, output two valid openings for different messages

Equations

• CatCrypt.Examples.Commitments.BindingAdversary S = (S.Key → CatCrypt.Core.SPComp (S.Message × S.Opening × S.Message × S.Opening × S.Commitment))

noncomputable def CatCrypt.Examples.Commitments.Binding_Game (S : CommitmentScheme) (A : BindingAdversary S) : Core.SPComp Bool

Binding game: adversary wins if it finds two valid openings for the same commitment but different messages

Equations

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

noncomputable def CatCrypt.Examples.Commitments.Binding_Advantage (S : CommitmentScheme) (A : BindingAdversary S) : ENNReal

Binding advantage

Equations

• CatCrypt.Examples.Commitments.Binding_Advantage S A = CatCrypt.Crypto.prTrue (CatCrypt.Examples.Commitments.Binding_Game S A) CatCrypt.Core.Heap.empty