Collision-Resistant Hash Functions

This file defines collision resistance for unkeyed hash functions and for keyed hash function families, together with their security experiments.

Collision Resistance

A function f : X → Y is collision-resistant if no efficient adversary can find two distinct inputs x ≠ x' with f x = f x'.

Keyed Hash Function Families

A keyed hash family samples a public key k : K and the adversary must find a collision under f k. This is the form used in practical constructions and in the Merkle-tree / FRI commitment-scheme setting where the hash key is a protocol parameter.

Main Definitions

• CRAdversary X — an adversary outputting a candidate collision pair.
• crExp — the collision-resistance experiment.
• crAdvantage — the advantage of a CR adversary.
• KeyedHashFamily K X Y — a keyed hash family.
• KeyedCRAdversary K X — an adversary for the keyed variant.
• keyedCRExp — the keyed collision-resistance experiment.
• keyedCRAdvantage — the advantage of a keyed CR adversary.
• ROMHashSpec X Y — adversary-facing random-oracle spec; carries no probability instances.
• ROMHashSpec.cached X Y — post-simulation companion; defeq to ROMHashSpec X Y but with the IsUniformSpec instance attached.
• ROMHashSpec.cachingOracle — QueryImpl bridge that consumes pre-spec queries and dispatches them through the generic cachingOracle on the cached spec. The spec transition happens only via simulateQ.
• ROMCRAdversary X Y — an adversary for the ROM variant.
• romCRExp — the ROM collision-resistance experiment.
• romCRAdvantage — the advantage of a ROM-CR adversary.
• romCRAdvantage_le_birthday — birthday bound on ROM-CR advantage.

See also

• VCVio/CryptoFoundations/CommitmentScheme.lean — binding for commitment schemes; collision resistance of the underlying hash is the standard-model source of binding for hash-based commitments.
• VCVio/OracleComp/QueryTracking/Collision.lean — CacheHasCollision predicates and birthday bounds used to bound ROM-level collision probability.

Unkeyed Collision Resistance

def CollisionResistance.CRAdversary (X : Type) : Type

A collision-resistance adversary outputs a candidate pair of inputs that it hopes form a collision under the target hash function.

def CollisionResistance.crExp {X Y : Type} [DecidableEq X] [DecidableEq Y] (f : X → Y) (adversary : CRAdversary X) : ProbComp Bool

Collision-resistance experiment: the adversary proposes a pair (x, x'), and the experiment returns true iff the two inputs are distinct and map to the same image under f.

noncomputable def CollisionResistance.crAdvantage {X Y : Type} [DecidableEq X] [DecidableEq Y] (f : X → Y) (adversary : CRAdversary X) : ENNReal

Collision-resistance advantage: the probability that the adversary produces a valid collision for f.

Keyed Hash Function Families

structure CollisionResistance.KeyedHashFamily (K X Y : Type) : Type

A keyed hash family with key space K, domain X, and range Y. The key-sampling algorithm is probabilistic; the hash itself is a deterministic function of the key and input.

• keygen : ProbComp K
• hash : K → X → Y

def CollisionResistance.KeyedCRAdversary (K X : Type) : Type

A keyed CR adversary receives the public key and outputs a candidate collision pair.

def CollisionResistance.keyedCRExp {X Y K : Type} [DecidableEq X] [DecidableEq Y] (H : KeyedHashFamily K X Y) (adversary : KeyedCRAdversary K X) : ProbComp Bool

Keyed collision-resistance experiment: sample a key, run the adversary on the key, and return true iff the adversary's pair is a valid collision under H.hash k.

noncomputable def CollisionResistance.keyedCRAdvantage {X Y K : Type} [DecidableEq X] [DecidableEq Y] (H : KeyedHashFamily K X Y) (adversary : KeyedCRAdversary K X) : ENNReal

Keyed collision-resistance advantage: the probability of producing a valid collision under the sampled key.

ROM-Level Collision Resistance

Companion section modelling collision resistance directly in the random-oracle model. A ROM-CR adversary is an oracle computation outputting a candidate collision pair (x, x'), expressed in the adversary-facing ROMHashSpec X Y which carries no probability instances. The experiment lifts the adversary into the post-simulation companion ROMHashSpec.cached X Y (defeq, distinct head symbol) where IsUniformSpec is in scope, then runs it inside cachingOracle and queries the random oracle on both candidates sharing the same cache; it wins iff x ≠ x' and the queried outputs coincide.

For any t-query ROM-CR adversary the advantage is bounded by the birthday term (t+2) * (t+1) / (2 * |Y|) — a (t+2)-query game once the two verification queries are accounted for.

Closes one of the layers requested in Verified-zkEVM/VCV-io#284.

def CollisionResistance.ROMHashSpec (X Y : Type) : OracleSpec X

The random-oracle spec with domain X and range Y, as seen by the adversary. Each input x : X is a distinct oracle index returning a value in Y. This pre-cache spec carries no probability instances: a ROM-CR adversary is a syntactic object, and probability semantics only attach to the post-simulation spec ROMHashSpec.cached (defeq, distinct head symbol).

@[implicit_reducible]

instance CollisionResistance.instDecidableEqROMHashSpecOfDecidableEq {X Y : Type} [DecidableEq X] [DecidableEq Y] : (ROMHashSpec X Y).DecidableEq

def CollisionResistance.ROMHashSpec.cached (X Y : Type) : OracleSpec X

The post-simulation companion to ROMHashSpec: definitionally the same OracleSpec X, but with a distinct head symbol so the IsUniformSpec instance below is opted into only where probability reasoning is intended. The adversary's pre-cache computation is converted into a post-cache computation only via simulateQ ROMHashSpec.cachingOracle.

@[implicit_reducible]

instance CollisionResistance.instFintypeCachedOfFintype {X Y : Type} [Fintype Y] : (ROMHashSpec.cached X Y).Fintype

@[implicit_reducible]

instance CollisionResistance.instInhabitedCachedOfInhabited {X Y : Type} [Inhabited Y] : (ROMHashSpec.cached X Y).Inhabited

@[implicit_reducible]

instance CollisionResistance.instDecidableEqCachedOfDecidableEq {X Y : Type} [DecidableEq X] [DecidableEq Y] : (ROMHashSpec.cached X Y).DecidableEq

@[implicit_reducible]

noncomputable instance CollisionResistance.instIsUniformSpecCachedOfFintypeOfInhabited {X Y : Type} [Fintype Y] [Inhabited Y] : (ROMHashSpec.cached X Y).IsUniformSpec

@[reducible, inline]

def CollisionResistance.ROMHashSpec.cachingOracle {X Y : Type} [DecidableEq X] : QueryImpl (ROMHashSpec X Y) (StateT (cached X Y).QueryCache (OracleComp (cached X Y)))

Bridge caching oracle: a QueryImpl that takes adversary-facing ROMHashSpec X Y queries and dispatches them through the generic cachingOracle on the post-cache spec ROMHashSpec.cached X Y. The spec transition from pre to cached happens only here, via simulateQ.

@[simp]

theorem CollisionResistance.ROMHashSpec.simulateQ_cachingOracle_query {X Y : Type} [DecidableEq X] (x : X) : simulateQ cachingOracle (liftM (OracleSpec.query x)) = OracleSpec.cachingOracle x

Specialised simulateQ_query lemma for the bridge: simulating a single pre-spec query through ROMHashSpec.cachingOracle is the generic cachingOracle action at the post-cache spec. True by rfl because the two specs are definitionally equal as OracleSpec X.

def CollisionResistance.ROMCRAdversary (X Y : Type) : Type

A ROM-CR adversary is an oracle computation outputting a candidate collision pair under the random oracle.

structure CollisionResistance.BoundedROMCRAdversary (X Y : Type) (t : ℕ) : Type

A ROM-CR adversary bundled with a total query bound.

• run : ROMCRAdversary X Y

  The adversary's oracle computation.

• queryBound : OracleComp.IsTotalQueryBound self.run t

  The adversary makes at most t total queries.

def CollisionResistance.romCRExp {X Y : Type} [DecidableEq X] [DecidableEq Y] {t : ℕ} (A : BoundedROMCRAdversary X Y t) : OracleComp (ROMHashSpec.cached X Y) (Bool × (ROMHashSpec.cached X Y).QueryCache)

ROM collision-resistance experiment: run the adversary inside the ROMHashSpec.cachingOracle bridge from the empty cache, then query the random oracle on both candidate inputs (verification queries share the cache). Win iff the inputs are distinct and the queried outputs coincide. The bridge takes the entire computation from OracleComp (ROMHashSpec X Y) into OracleComp (ROMHashSpec.cached X Y) in one step — no separate oracle-comp lift is needed.

noncomputable def CollisionResistance.romCRAdvantage {X Y : Type} [DecidableEq X] [DecidableEq Y] [Fintype Y] [Inhabited Y] {t : ℕ} (A : BoundedROMCRAdversary X Y t) : ENNReal

ROM collision-resistance advantage: probability that the adversary produces a valid collision under the random oracle.

theorem CollisionResistance.romCRAdvantage_le_birthday {X Y : Type} [DecidableEq X] [DecidableEq Y] [Fintype Y] [Inhabited X] [Inhabited Y] {t : ℕ} (hY : 0 < Fintype.card Y) (A : BoundedROMCRAdversary X Y t) : romCRAdvantage A ≤ ↑((t + 2) * (t + 1)) / (2 * ↑(Fintype.card Y))

ROM Collision Resistance birthday bound: for any t-query ROM-CR adversary A over a hash range of cardinality |Y| > 0, the advantage is bounded by (t+2) * (t+1) / (2 * |Y|). The two extra queries account for the experiment's verification queries, which share the adversary's cache.