Collision Resistance (CR) Assumptions

Centralized definitions of collision resistance for hash functions. These are used by Merkle trees, FAEST vector commitments, XMSS, and SLH-DSA.

Main definitions

Search-style CR (standard)

• HashScheme — abstract hash function with typed input/output
• CR_Search_Game — adversary finds two inputs with the same hash
• CR_Search_Advantage — probability of finding a collision
• CRSearchSecure — CR hardness assumption

Distinguishing-style CR (for game-hopping)

• CRDef — compression function with keyed input sampling
• CR_Dist_Game_Real / CR_Dist_Game_Ideal — real/ideal games
• CR_Dist_Advantage — distinguishing advantage

Target Collision Resistance (TCR)

• TCR_Game — adversary finds a second preimage for a given target
• TCR_Advantage — probability of finding a target collision

Preimage Resistance (Pre)

• Pre_Game — adversary inverts the hash on a random output
• Pre_Advantage — probability of finding a preimage
• PreSecure — preimage resistance assumption

Reductions

• CRSecure_implies_TCRSecure — CR implies TCR (Rogaway-Shrimpton Prop. 7)
• CRSecure_implies_PreSecure — CR implies Pre for fixed-length hashes (KL Prop. 8.4)

Cross-Validation

Notion	This file	Rogaway-Shrimpton 2004	BS	KL
CR (search)	CR_Search_Game	Def. 1	§8.1	Def. 5.1
CR (distinguishing)	CR_Dist_Game	—	§8.1	—
TCR	TCR_Game	Def. 5	—	§8.1
Pre	Pre_Game	Def. 3	§8.1	§8.1
CR⟹TCR	CRSecure_implies_TCRSecure	Prop. 7	—	Prop. 8.3
CR⟹Pre	CRSecure_implies_PreSecure	—	—	Prop. 8.4

Equivalent formalizations:

• EasyCrypt: CRHash.ec (search CR + indistinguishability variant), KeyedHashFunctions.eca (TCR, SPR, PRE, CR, DSPR, UD, ITSR)
• SSProve (Rocq): CR in MerkleTree/Reduction.lean (distinguishing form), TCR in CramerShoup.lean

References

• Rogaway & Shrimpton, Cryptographic Hash-Function Basics, FSE 2004.
• Boneh & Shoup, A Graduate Course in Applied Cryptography, §8.1.
• Katz & Lindell, Introduction to Modern Cryptography, §8.1, Props. 8.3–8.4.

Hash Function Scheme

structure CatCrypt.Crypto.Assumptions.HashScheme : Type 1

Abstract hash function with typed input and output.

• Input : Type

  Input type

• Output : Type

  Output type

• instFintypeOut : Fintype self.Output
• instNeOut : Nonempty self.Output
• instDecEqOut : DecidableEq self.Output
• instDecEqIn : DecidableEq self.Input
• hash : self.Input → self.Output

  The hash function

Search-Style Collision Resistance

The standard formulation: adversary produces two distinct inputs that hash to the same output.

noncomputable def CatCrypt.Crypto.Assumptions.CR_Search_Game (h : HashScheme) (A : Core.SPComp (h.Input × h.Input)) : Core.SPComp Bool

CR search game: adversary finds a collision (x₁, x₂) with hash(x₁) = hash(x₂) and x₁ ≠ x₂.

Equations

• CatCrypt.Crypto.Assumptions.CR_Search_Game h A = do let __discr ← A match __discr with | (x₁, x₂) => CatCrypt.Core.SPComp.pure (decide (h.hash x₁ = h.hash x₂ ∧ x₁ ≠ x₂))

noncomputable def CatCrypt.Crypto.Assumptions.CR_Search_Advantage (h : HashScheme) (A : Core.SPComp (h.Input × h.Input)) : ENNReal

CR search advantage: probability that adversary finds a collision.

Equations

• CatCrypt.Crypto.Assumptions.CR_Search_Advantage h A = CatCrypt.Crypto.prTrue (CatCrypt.Crypto.Assumptions.CR_Search_Game h A) CatCrypt.Core.Heap.empty

class CatCrypt.Crypto.Assumptions.CRSearchSecure (h : HashScheme) (ε : ENNReal) : Prop

CR hardness (search form).

• cr_bound (A : Core.SPComp (h.Input × h.Input)) : CR_Search_Advantage h A ≤ ε

Distinguishing-Style Collision Resistance

Used for game-hopping proofs (e.g., Merkle tree reductions): adversary distinguishes hash(x, y) from a random value. A collision implies distinguishing, so this captures CR.

structure CatCrypt.Crypto.Assumptions.CRDef (W : Type) [SampleableType W] : Type

Collision resistance definition for a compression function, modeled as a distinguishing game analogous to DDH.

• hashPair x y : the 2-to-1 compression function H(x, y)
• keygen : sampling the input pair (left child, right child)

The game: sample (x, y), give adversary either (x, y, hashPair(x, y)) (real) or (x, y, random) (ideal).

• hashPair : W → W → W

  Hash compression: H(left, right)

• keygen : Core.SPComp (W × W)

  Input pair sampling

• keygen_isPure : self.keygen.IsPure

  Sampling is heap-independent

@[reducible, inline]

abbrev CatCrypt.Crypto.Assumptions.CR_Dist_Adversary (W : Type) : Type

CR distinguishing adversary: receives both inputs and the challenge.

Equations

• CatCrypt.Crypto.Assumptions.CR_Dist_Adversary W = (W → W → W → CatCrypt.Core.SPComp Bool)

noncomputable def CatCrypt.Crypto.Assumptions.CR_Dist_Game_Real {W : Type} [CryptoWord W] (C : CRDef W) (A : CR_Dist_Adversary W) : Core.SPComp Bool

CR real game: adversary receives (x, y, hashPair(x, y)).

Equations

• CatCrypt.Crypto.Assumptions.CR_Dist_Game_Real C A = C.keygen.bind fun (p : W × W) => A p.1 p.2 (C.hashPair p.1 p.2)

noncomputable def CatCrypt.Crypto.Assumptions.CR_Dist_Game_Ideal {W : Type} [CryptoWord W] (C : CRDef W) (A : CR_Dist_Adversary W) : Core.SPComp Bool

CR ideal game: adversary receives (x, y, random).

Equations

• CatCrypt.Crypto.Assumptions.CR_Dist_Game_Ideal C A = C.keygen.bind fun (p : W × W) => (CatCrypt.Core.SPComp.sample W).bind fun (r : W) => A p.1 p.2 r

noncomputable def CatCrypt.Crypto.Assumptions.CR_Dist_Advantage {W : Type} [CryptoWord W] (C : CRDef W) (A : CR_Dist_Adversary W) : ENNReal

CR distinguishing advantage.

Equations

• CatCrypt.Crypto.Assumptions.CR_Dist_Advantage C A = CatCrypt.Crypto.Advantage (CatCrypt.Crypto.Assumptions.CR_Dist_Game_Real C A) (CatCrypt.Crypto.Assumptions.CR_Dist_Game_Ideal C A)

Target Collision Resistance (TCR)

Second-preimage resistance: given x, find x' ≠ x with hash(x') = hash(x). Weaker than CR.

noncomputable def CatCrypt.Crypto.Assumptions.TCR_Game (h : HashScheme) [SampleableType h.Input] (A : h.Input → h.Output → Core.SPComp h.Input) : Core.SPComp Bool

TCR game: adversary receives (x, hash(x)) and must find x' ≠ x with hash(x') = hash(x).

Equations

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

noncomputable def CatCrypt.Crypto.Assumptions.TCR_Advantage (h : HashScheme) [SampleableType h.Input] (A : h.Input → h.Output → Core.SPComp h.Input) : ENNReal

TCR advantage: probability of finding a target collision.

Equations

• CatCrypt.Crypto.Assumptions.TCR_Advantage h A = CatCrypt.Crypto.prTrue (CatCrypt.Crypto.Assumptions.TCR_Game h A) CatCrypt.Core.Heap.empty

class CatCrypt.Crypto.Assumptions.TCRSecure (h : HashScheme) [SampleableType h.Input] (ε : ENNReal) : Prop

TCR hardness assumption.

• tcr_bound (A : h.Input → h.Output → Core.SPComp h.Input) : TCR_Advantage h A ≤ ε

Preimage Resistance (Pre)

Given a hash output y = hash(x) for random x, find any x' with hash(x') = y. Weaker than both CR and TCR.

noncomputable def CatCrypt.Crypto.Assumptions.Pre_Game (h : HashScheme) [SampleableType h.Input] (A : h.Output → Core.SPComp h.Input) : Core.SPComp Bool

Pre game: sample random x, give hash(x) to adversary, check if adversary's output x' satisfies hash(x') = hash(x).

Equations

• CatCrypt.Crypto.Assumptions.Pre_Game h A = do let x ← CatCrypt.Core.SPComp.sample h.Input have y : h.Output := h.hash x let x' ← A y CatCrypt.Core.SPComp.pure (decide (h.hash x' = y))

noncomputable def CatCrypt.Crypto.Assumptions.Pre_Advantage (h : HashScheme) [SampleableType h.Input] (A : h.Output → Core.SPComp h.Input) : ENNReal

Pre advantage: probability of finding a preimage.

Equations

• CatCrypt.Crypto.Assumptions.Pre_Advantage h A = CatCrypt.Crypto.prTrue (CatCrypt.Crypto.Assumptions.Pre_Game h A) CatCrypt.Core.Heap.empty

class CatCrypt.Crypto.Assumptions.PreSecure (h : HashScheme) [SampleableType h.Input] (ε : ENNReal) : Prop

Preimage resistance hardness assumption.

• pre_bound (A : h.Output → Core.SPComp h.Input) : Pre_Advantage h A ≤ ε

Reductions

theorem CatCrypt.Crypto.Assumptions.CRSecure_implies_TCRSecure (h : HashScheme) [SampleableType h.Input] (ε : ENNReal) [hCR : CRSearchSecure h ε] : TCRSecure h ε

CR implies TCR: a collision finder trivially finds target collisions. Given a target x and hash(x), a CR adversary can find x' ≠ x with hash(x') = hash(x) by finding any collision and checking if one element matches.

Bound: TCR_Advantage ≤ CR_Search_Advantage.

Reference: Rogaway-Shrimpton 2004 Prop. 7, Katz-Lindell Prop. 8.3.

class CatCrypt.Crypto.Assumptions.CRImpliesPre (h : HashScheme) [SampleableType h.Input] : Prop

CR implies preimage resistance (for fixed-length hash functions). If an adversary can find a preimage x' of y = hash(x), then with probability ≥ 1/2, x' ≠ x, giving a collision.

Bound: Pre_Advantage ≤ CR_Search_Advantage.

Reference: Katz-Lindell Prop. 8.4.

The compression hypothesis Fintype.card h.Input > Fintype.card h.Output is essential: for injective hash, CR holds trivially but Pre may not.

• bound {ε : ENNReal} (h_compress : Fintype.card h.Input > Fintype.card h.Output) (hCR : CRSearchSecure h ε) (A : h.Output → Core.SPComp h.Input) : Pre_Advantage h A ≤ ε

theorem CatCrypt.Crypto.Assumptions.CRSecure_implies_PreSecure (h : HashScheme) [SampleableType h.Input] [CRImpliesPre h] (ε : ENNReal) [hCR : CRSearchSecure h ε] (h_compress : Fintype.card h.Input > Fintype.card h.Output) : PreSecure h ε