Keyed collision-resistant hash families and compression functions

In the uniform PPT model, an unkeyed deterministic function H : List Bool → List Bool with unrestricted inputs (valid := fun _ _ => true, or any domain predicate that accepts a fixed pair at every security parameter n) cannot be collision-resistant whenever a single colliding pair (m₁, m₂) exists, because one uniform algorithm can hardcode (m₁, m₂) as a constant and win for every n. (In the length-indexed compression setting validCompressionInput n x := (x.length == 2 * n), by contrast, a single hardcoded pair has fixed length and is valid at most at one parameter n.) Standard uniform formulations therefore index both compression and hash families H : List Bool → List Bool → List Bool by a public key k ← {0, 1}^n sampled uniformly at security parameter n; the adversary receives (1^n, k) and wins by outputting a pair (m₁, m₂) of valid inputs with m₁ ≠ m₂ and H k m₁ = H k m₂ ([BS23], Sections 8.1–8.2; [KL20], Section 5.1).

Parameterizing the experiment by a validity predicate valid : ℕ → List Bool → Bool accommodates both fixed-input-length compression families (validCompressionInput n x := (x.length == 2 * n), mapping 2n-bit inputs to n-bit outputs under an n-bit key) and arbitrary-input-length hash families (valid := fun _ _ => true).

Main definitions

• Cslib.Crypto.CollisionFinder: uniform adversary taking (n, k) and outputting candidate messages (m₁, m₂).
• Cslib.Crypto.isCollision, Cslib.Crypto.collisionGame: Boolean collision test and keyed collision-finding experiment.
• Cslib.Crypto.CollisionResistantOn, Cslib.Crypto.CollisionResistant: negligible collision probability against every uniform strict PPT adversary.
• Cslib.Crypto.validCompressionInput, Cslib.Crypto.CompressionFamily: 2n → n collision- resistant compression families.
• Cslib.Crypto.HashFamily: unrestricted collision-resistant hash families on arbitrary bit strings.

Main results

• Cslib.Crypto.isPPTOn_collisionGame, Cslib.Crypto.isPPT_collisionGame: strict PPT certificates for the collision experiment.
• Cslib.Crypto.CollisionResistantOn.negligible, Cslib.Crypto.CollisionResistantOn.of_negligible: equivalence with negligible collision-finding probability.
• Cslib.Crypto.succProbability_collisionGame_le_of_extract, Cslib.Crypto.CollisionResistantOn.of_extract: deterministic polynomial-time collision extraction transfers collision resistance between hash families.
• Cslib.Crypto.CollisionResistantOn.mono: restricting the valid input domain preserves collision resistance.
• Cslib.Crypto.not_collisionResistantOn_of_le_succProbability: finding collisions with probability bounded away from zero refutes collision resistance.

References

• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Section 8.1.
• J. Katz, Y. Lindell, Introduction to Modern Cryptography, Section 5.1.

@[reducible, inline]

abbrev Cslib.Crypto.CollisionFinder : Type

A collision finder receives the unary security parameter n and public hash key k and outputs a pair (m₁, m₂) of candidate colliding messages.

def Cslib.Crypto.isCollision (H : List Bool → List Bool → List Bool) (valid : ℕ → List Bool → Bool) (n : ℕ) (k m₁ m₂ : List Bool) : Bool

Test whether (m₁, m₂) is a valid collision for H k at security parameter n under the domain predicate valid.

@[simp]

theorem Cslib.Crypto.isCollision_eq_true_iff {H : List Bool → List Bool → List Bool} {valid : ℕ → List Bool → Bool} {n : ℕ} {k m₁ m₂ : List Bool} : isCollision H valid n k m₁ m₂ = true ↔ valid n m₁ = true ∧ valid n m₂ = true ∧ m₁ ≠ m₂ ∧ H k m₁ = H k m₂

theorem Cslib.Crypto.isCollision_comm (H : List Bool → List Bool → List Bool) (valid : ℕ → List Bool → Bool) (n : ℕ) (k m₁ m₂ : List Bool) : isCollision H valid n k m₁ m₂ = isCollision H valid n k m₂ m₁

Collision testing is symmetric in the two candidate messages.

@[simp]

theorem Cslib.Crypto.isCollision_self (H : List Bool → List Bool → List Bool) (valid : ℕ → List Bool → Bool) (n : ℕ) (k m : List Bool) : isCollision H valid n k m m = false

theorem Cslib.Crypto.computableInPolyTime_isCollision {H : List Bool → List Bool → List Bool} {valid : ℕ → List Bool → Bool} (hH : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List Bool × List Bool) => H p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hvalid : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool) => valid p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool × List Bool × List Bool) => isCollision H valid p.1 p.2.1 p.2.2.1 p.2.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits))) Turing.MultiTapeTM.encBool

Testing whether (m₁, m₂) is a valid collision is polynomial-time when H and valid are polynomial-time.

noncomputable def Cslib.Crypto.collisionGame (H : List Bool → List Bool → List Bool) (valid : ℕ → List Bool → Bool) (adversary : CollisionFinder) (n : ℕ) : ProbComp Bool

The keyed collision-finding experiment: sample a uniform n-bit key k, run adversary n k to obtain a candidate pair (m₁, m₂), and accept when isCollision H valid n k m₁ m₂ holds.

theorem Cslib.Crypto.isPPTOn_collisionGame {H : List Bool → List Bool → List Bool} {valid : ℕ → List Bool → Bool} {adversary : CollisionFinder} (hH : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List Bool × List Bool) => H p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hvalid : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool) => valid p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) (ha : Probability.IsPPT (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) adversary) : Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool (collisionGame H valid adversary)

Run the complete collision experiment on its unary security parameter.

theorem Cslib.Crypto.isPPT_collisionGame {H : List Bool → List Bool → List Bool} {valid : ℕ → List Bool → Bool} {adversary : CollisionFinder} (hH : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List Bool × List Bool) => H p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hvalid : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool) => valid p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) (ha : Probability.IsPPT (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) adversary) : Probability.IsPPT Turing.MultiTapeTM.encBool fun (n : ℕ) (x : List Bool) => collisionGame H valid adversary n

The collision experiment is uniformly strict PPT, independently of unused auxiliary input.

def Cslib.Crypto.CollisionResistantOn (H : List Bool → List Bool → List Bool) (valid : ℕ → List Bool → Bool) : Prop

Collision resistance of a keyed hash family H on the valid input domain valid: every uniform strict PPT collision finder has negligible success probability.

@[reducible, inline]

abbrev Cslib.Crypto.CollisionResistant (H : List Bool → List Bool → List Bool) : Prop

Unrestricted collision resistance on all bit strings List Bool.

theorem Cslib.Crypto.CollisionResistantOn.negligible {H : List Bool → List Bool → List Bool} {valid : ℕ → List Bool → Bool} (h : CollisionResistantOn H valid) (adversary : CollisionFinder) (hPPT : Probability.IsPPT (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) adversary) : Negligible fun (n : ℕ) => Game.succProbability (collisionGame H valid adversary n).eval

Collision resistance gives negligible collision-finding probability for every strict PPT adversary.

theorem Cslib.Crypto.CollisionResistantOn.of_negligible {H : List Bool → List Bool → List Bool} {valid : ℕ → List Bool → Bool} (h : ∀ (adversary : CollisionFinder), Probability.IsPPT (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) adversary → Negligible fun (n : ℕ) => Game.succProbability (collisionGame H valid adversary n).eval) : CollisionResistantOn H valid

Establish collision resistance by bounding every strict PPT adversary's success probability.

theorem Cslib.Crypto.succProbability_collisionGame_le_of_extract {H₁ H₂ : List Bool → List Bool → List Bool} {valid₁ valid₂ : ℕ → List Bool → Bool} (extract : ℕ → List Bool → List Bool → List Bool → List Bool × List Bool) (adversary : CollisionFinder) (n : ℕ) (himp : ∀ (k : List Bool), k.length = n → ∀ (m₁ m₂ : List Bool), isCollision H₁ valid₁ n k m₁ m₂ = true → isCollision H₂ valid₂ n k (extract n k m₁ m₂).1 (extract n k m₁ m₂).2 = true) : Game.succProbability (collisionGame H₁ valid₁ adversary n).eval ≤ Game.succProbability (collisionGame H₂ valid₂ (fun (m : ℕ) (k : List Bool) => do let pair ← adversary m k pure (extract m k pair.1 pair.2)) n).eval

If a deterministic map extract turns every valid H₁-collision under an n-bit key k into a valid H₂-collision under k, then postprocessing adversary by extract at parameter n never decreases the collision success probability.

theorem Cslib.Crypto.CollisionResistantOn.of_extract {H₁ H₂ : List Bool → List Bool → List Bool} {valid₁ valid₂ : ℕ → List Bool → Bool} (hCR : CollisionResistantOn H₂ valid₂) (extract : ℕ → List Bool → List Bool → List Bool → List Bool × List Bool) (hextract : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool × List Bool × List Bool) => extract p.1 p.2.1 p.2.2.1 p.2.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits))) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) (himp : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (k : List Bool), k.length = n → ∀ (m₁ m₂ : List Bool), isCollision H₁ valid₁ n k m₁ m₂ = true → isCollision H₂ valid₂ n k (extract n k m₁ m₂).1 (extract n k m₁ m₂).2 = true) : CollisionResistantOn H₁ valid₁

Deterministic collision-extraction reduction: if a polynomial-time function extract turns every H₁-collision at parameter n (for all sufficiently large n and n-bit keys k) into an H₂-collision under the same key k, then collision resistance of H₂ implies collision resistance of H₁.

theorem Cslib.Crypto.CollisionResistantOn.mono {H : List Bool → List Bool → List Bool} {valid₁ valid₂ : ℕ → List Bool → Bool} (hCR : CollisionResistantOn H valid₂) (hsub : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (m : List Bool), valid₁ n m = true → valid₂ n m = true) : CollisionResistantOn H valid₁

Restricting the valid input domain preserves collision resistance.

theorem Cslib.Crypto.not_collisionResistantOn_of_le_succProbability {H : List Bool → List Bool → List Bool} {valid : ℕ → List Bool → Bool} {c : NNReal} (hc : c ≠ 0) (adversary : CollisionFinder) (hPPT : Probability.IsPPT (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) adversary) (h : ∀ (n : ℕ), c ≤ Game.succProbability (collisionGame H valid adversary n).eval) : ¬CollisionResistantOn H valid

Finding collisions with probability bounded away from zero refutes collision resistance: a strict PPT adversary whose success probability is at least a fixed c > 0 at every security parameter.

def Cslib.Crypto.validCompressionInput (n : ℕ) (x : List Bool) : Bool

Validity predicate for a fixed-input-length 2n → n compression family: at security parameter n, valid inputs have length 2 * n.

@[simp]

theorem Cslib.Crypto.validCompressionInput_eq_true_iff {n : ℕ} {x : List Bool} : validCompressionInput n x = true ↔ x.length = 2 * n

theorem Cslib.Crypto.computableInPolyTime_validCompressionInput : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool) => validCompressionInput p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

Testing whether an input has length 2 * n is computable in plain polynomial time.

structure Cslib.Crypto.CompressionFamily (h : List Bool → List Bool → List Bool) : Prop

A keyed 2n → n collision-resistant compression family ([BS23], Section 8.2): computable in deterministic polynomial time, mapping 2n-bit inputs under an n-bit key to n-bit outputs, and collision-resistant on 2n-bit inputs.

• polyTime : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List Bool × List Bool) => h p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits

  Deterministic polynomial-time evaluation of (k, x) ↦ h k x.

• length_eq (k x : List Bool) : x.length = 2 * k.length → (h k x).length = k.length

  Compressing a 2n-bit input under an n-bit key produces an n-bit digest.

• collisionResistant : CollisionResistantOn h validCompressionInput

  Finding two distinct 2n-bit inputs with the same digest under a uniform n-bit key is hard for every uniform strict PPT adversary.

structure Cslib.Crypto.HashFamily (H : List Bool → List Bool → List Bool) : Prop

A keyed collision-resistant hash family on arbitrary-length bit strings (List Bool), mapping every message under an n-bit key to an n-bit digest.

• polyTime : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List Bool × List Bool) => H p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits

  Deterministic polynomial-time evaluation of (k, msg) ↦ H k msg.

• length_eq (k msg : List Bool) : (H k msg).length = k.length

  Hashing any message under an n-bit key produces an n-bit digest.

• collisionResistant : CollisionResistant H

  Finding two distinct bit strings of any lengths with the same digest under a uniform n-bit key is hard for every uniform strict PPT adversary.