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 — random-oracle spec with domain X and range Y.
• 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'). The experiment runs the adversary inside cachingOracle, then 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.

@[reducible, inline]

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

The random-oracle spec with domain X and range Y: each input x : X is a distinct oracle index returning a value in Y.

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 X Y) (Bool × (ROMHashSpec X Y).QueryCache)

ROM collision-resistance experiment: run the adversary inside cachingOracle 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.

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.