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).

Following [BS23], Section 8.1.1 (Definition 8.2 and Fig. 8.3, printed pp. 290–291), we define the general setup-parameterized notions CollisionFinderFor, isCollisionFor, collisionGameFor, CollisionResistantForOn, and CollisionResistantFor for hash families H : (d : Param) → List Bool → Digest d indexed by a public system parameter d ← setup n (where setup : ℕ → PMF Param need not be efficiently sampleable, matching PrimeOrderGroupFamily in DiscreteLog and DiffieHellman, and where d subsumes any hash key per footnote 1 on printed p. 290). Standard keyed word-level collision resistance (CollisionFinder, CollisionResistantOn, CollisionResistant) is the abbrev specialization Param = List Bool, Digest _ = List Bool, encParam = encBits, setup n = ProbComp.eval (BitString.sampleList n).

Main definitions

• Cslib.Crypto.CollisionFinderFor, Cslib.Crypto.isCollisionFor, Cslib.Crypto.collisionGameFor, Cslib.Crypto.CollisionResistantForOn, Cslib.Crypto.CollisionResistantFor: setup-parameterized collision-finding experiment and collision resistance for families H : (d : Param) → List Bool → Digest d indexed by a public setup parameter d ← setup n (used for group-indexed $\mathbb{Z}_q$-valued hashes such as $H' : \mathbb{G}^3 \to \mathbb{Z}_q$ in Cramer–Shoup).
• Cslib.Crypto.CollisionFinder, Cslib.Crypto.isCollision, Cslib.Crypto.collisionGame, Cslib.Crypto.CollisionResistantOn, Cslib.Crypto.CollisionResistant: uniform keyed word-level collision resistance (Param = List Bool, setup n = ProbComp.eval (BitString.sampleList n)).
• 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.CollisionResistantForOn.negligible, Cslib.Crypto.CollisionResistantForOn.of_negligible, Cslib.Crypto.not_collisionResistantForOn_of_le_succProbability, Cslib.Crypto.succProbability_collisionGameFor_map_le, Cslib.Crypto.CollisionResistantForOn.of_map, Cslib.Crypto.CollisionResistantOn.collisionResistantForOn: setup-parameterized collision resistance properties and injective-digest reductions (including the specialization from word-level CollisionResistantOn).
• Cslib.Crypto.isPPTOn_collisionGame, Cslib.Crypto.isPPT_collisionGame: strict PPT certificates for the keyed word-level 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, Version 0.6, Section 8.1 (Definition 8.2 and Fig. 8.3, printed pp. 290–291).
• J. Katz, Y. Lindell, Introduction to Modern Cryptography, Section 5.1.

Setup-parameterized collision-resistant hash families ([BS23], Section 8.1.1)

Verbatim from [BS23], Section 8.1.1 (printed pp. 290–291):

Definition 8.2 (Keyless hash functions). A (keyless) hash function is an efficient algorithm $H$, along with two families of spaces with system parameterization $P$: $$\mathcal{M} = \{\mathcal{M}_{\lambda, \Lambda}\}_{\lambda, \Lambda}, \quad \text{and} \quad \mathcal{T} = \{\mathcal{T}_{\lambda, \Lambda}\}_{\lambda, \Lambda},$$ such that

1. $\mathcal{M}$, and $\mathcal{T}$ are efficiently recognizable.
2. Algorithm $H$ is an efficient deterministic algorithm that on input $\lambda \in \mathbb{Z}_{\ge 1}$, $\Lambda \in \text{Supp}(P(\lambda))$, and $m \in \mathcal{M}_{\lambda, \Lambda}$, outputs an element of $\mathcal{T}_{\lambda, \Lambda}$.

In defining collision resistance, we parameterize Attack Game 8.1 by the security parameter $\lambda$. The asymptotic game is shown in Fig. 8.3. The advantage $\text{CRadv}[\mathcal{A}, H]$ is then a function of $\lambda$. Definition 8.1 should be read as saying that $\text{CRadv}[\mathcal{A}, H](\lambda)$ is a negligible function.

@[reducible, inline]

abbrev Cslib.Crypto.CollisionFinderFor (Param : Type) : Type

A setup-parameterized collision finder receives the unary security parameter n and the public system parameter d : Param (which may be a hash key k : List Bool, a group description d : F.Desc, or a pair (d, k)), and outputs a candidate colliding pair (m₁, m₂).

def Cslib.Crypto.isCollisionFor {Param : Type} {Digest : Param → Type} [(d : Param) → DecidableEq (Digest d)] (H : (d : Param) → List Bool → Digest d) (valid : ℕ → Param → List Bool → Bool) (n : ℕ) (d : Param) (m₁ m₂ : List Bool) : Bool

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

@[simp]

theorem Cslib.Crypto.isCollisionFor_eq_true_iff {Param : Type} {Digest : Param → Type} [(d : Param) → DecidableEq (Digest d)] {H : (d : Param) → List Bool → Digest d} {valid : ℕ → Param → List Bool → Bool} {n : ℕ} {d : Param} {m₁ m₂ : List Bool} : isCollisionFor H valid n d m₁ m₂ = true ↔ valid n d m₁ = true ∧ valid n d m₂ = true ∧ m₁ ≠ m₂ ∧ H d m₁ = H d m₂

theorem Cslib.Crypto.isCollisionFor_comm {Param : Type} {Digest : Param → Type} [(d : Param) → DecidableEq (Digest d)] (H : (d : Param) → List Bool → Digest d) (valid : ℕ → Param → List Bool → Bool) (n : ℕ) (d : Param) (m₁ m₂ : List Bool) : isCollisionFor H valid n d m₁ m₂ = isCollisionFor H valid n d m₂ m₁

Parameterized collision testing is symmetric in the two candidate messages.

@[simp]

theorem Cslib.Crypto.isCollisionFor_self {Param : Type} {Digest : Param → Type} [(d : Param) → DecidableEq (Digest d)] (H : (d : Param) → List Bool → Digest d) (valid : ℕ → Param → List Bool → Bool) (n : ℕ) (d : Param) (m : List Bool) : isCollisionFor H valid n d m m = false

noncomputable def Cslib.Crypto.collisionGameFor {Param : Type} {Digest : Param → Type} [(d : Param) → DecidableEq (Digest d)] (setup : ℕ → PMF Param) (H : (d : Param) → List Bool → Digest d) (valid : ℕ → Param → List Bool → Bool) (adversary : CollisionFinderFor Param) (n : ℕ) : Game

The setup-parameterized collision-finding experiment ([BS23], Section 8.1.1, Definition 8.2 and Fig. 8.3, printed pp. 290–291): draw d ← setup n (where setup is an arbitrary setup distribution and need not be efficiently sampleable, matching DiscreteLog and DDH), run adversary n d to obtain (m₁, m₂), and accept when isCollisionFor H valid n d m₁ m₂ holds.

def Cslib.Crypto.CollisionResistantForOn {Param : Type} {Digest : Param → Type} [(d : Param) → DecidableEq (Digest d)] (encParam : Param ↪ List Bool) (setup : ℕ → PMF Param) (H : (d : Param) → List Bool → Digest d) (valid : ℕ → Param → List Bool → Bool) : Prop

Collision resistance of a setup-parameterized hash family H on valid against every uniform strict PPT collision finder ([BS23], Section 8.1.1, Definition 8.2 and Fig. 8.3, printed pp. 290–291). The setup distribution setup : ℕ → PMF Param need not be efficiently sampleable.

@[reducible, inline]

abbrev Cslib.Crypto.CollisionResistantFor {Param : Type} {Digest : Param → Type} [(d : Param) → DecidableEq (Digest d)] (encParam : Param ↪ List Bool) (setup : ℕ → PMF Param) (H : (d : Param) → List Bool → Digest d) : Prop

Unrestricted collision resistance of a setup-parameterized hash family H.

theorem Cslib.Crypto.CollisionResistantForOn.negligible {Param : Type} {Digest : Param → Type} [(d : Param) → DecidableEq (Digest d)] {encParam : Param ↪ List Bool} {setup : ℕ → PMF Param} {H : (d : Param) → List Bool → Digest d} {valid : ℕ → Param → List Bool → Bool} (h : CollisionResistantForOn encParam setup H valid) (adversary : CollisionFinderFor Param) (hPPT : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary encParam) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) fun (p : ℕ × Param) => adversary p.1 p.2) : Negligible fun (n : ℕ) => (collisionGameFor setup H valid adversary n).succProbability

Setup-parameterized collision resistance gives negligible collision-finding probability for every strict PPT collision finder.

theorem Cslib.Crypto.CollisionResistantForOn.of_negligible {Param : Type} {Digest : Param → Type} [(d : Param) → DecidableEq (Digest d)] {encParam : Param ↪ List Bool} {setup : ℕ → PMF Param} {H : (d : Param) → List Bool → Digest d} {valid : ℕ → Param → List Bool → Bool} (h : ∀ (adversary : CollisionFinderFor Param), (Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary encParam) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) fun (p : ℕ × Param) => adversary p.1 p.2) → Negligible fun (n : ℕ) => (collisionGameFor setup H valid adversary n).succProbability) : CollisionResistantForOn encParam setup H valid

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

theorem Cslib.Crypto.not_collisionResistantForOn_of_le_succProbability {Param : Type} {Digest : Param → Type} [(d : Param) → DecidableEq (Digest d)] {encParam : Param ↪ List Bool} {setup : ℕ → PMF Param} {H : (d : Param) → List Bool → Digest d} {valid : ℕ → Param → List Bool → Bool} {c : NNReal} (hc : c ≠ 0) (adversary : CollisionFinderFor Param) (hPPT : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary encParam) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) fun (p : ℕ × Param) => adversary p.1 p.2) (h : ∀ (n : ℕ), c ≤ (collisionGameFor setup H valid adversary n).succProbability) : ¬CollisionResistantForOn encParam setup H valid

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

theorem Cslib.Crypto.succProbability_collisionGameFor_map_le {Param₁ Param₂ : Type} {Digest₁ : Param₁ → Type} {Digest₂ : Param₂ → Type} [(p₁ : Param₁) → DecidableEq (Digest₁ p₁)] [(p₂ : Param₂) → DecidableEq (Digest₂ p₂)] (setup₁ : ℕ → PMF Param₁) (f : ℕ → Param₁ → Param₂) (H₁ : (p₁ : Param₁) → List Bool → Digest₁ p₁) (H₂ : (p₂ : Param₂) → List Bool → Digest₂ p₂) (valid₁ : ℕ → Param₁ → List Bool → Bool) (valid₂ : ℕ → Param₂ → List Bool → Bool) (adversary : CollisionFinderFor Param₂) (n : ℕ) (hinj : ∀ p₁ ∈ (setup₁ n).support, ∀ (m₁ m₂ : List Bool), valid₂ n (f n p₁) m₁ = true → valid₂ n (f n p₁) m₂ = true → H₂ (f n p₁) m₁ = H₂ (f n p₁) m₂ → valid₁ n p₁ m₁ = true ∧ valid₁ n p₁ m₂ = true ∧ H₁ p₁ m₁ = H₁ p₁ m₂) : (collisionGameFor (fun (m : ℕ) => PMF.map (f m) (setup₁ m)) H₂ valid₂ adversary n).succProbability ≤ (collisionGameFor setup₁ H₁ valid₁ (fun (m : ℕ) (p₁ : Param₁) => adversary m (f m p₁)) n).succProbability

Pushing a setup distribution setup₁ n forward along f n : Param₁ → Param₂ and post-composing H₁ with a digest map that is injective on valid H₁ p₁-outputs for p₁ ∈ (setup₁ n).support never increases collision-finding success probability.

theorem Cslib.Crypto.CollisionResistantForOn.of_map {Param₁ Param₂ : Type} {Digest₁ : Param₁ → Type} {Digest₂ : Param₂ → Type} [(p₁ : Param₁) → DecidableEq (Digest₁ p₁)] [(p₂ : Param₂) → DecidableEq (Digest₂ p₂)] {encParam₁ : Param₁ ↪ List Bool} {encParam₂ : Param₂ ↪ List Bool} {setup₁ : ℕ → PMF Param₁} {f : ℕ → Param₁ → Param₂} {H₁ : (p₁ : Param₁) → List Bool → Digest₁ p₁} {H₂ : (p₂ : Param₂) → List Bool → Digest₂ p₂} {valid₁ : ℕ → Param₁ → List Bool → Bool} {valid₂ : ℕ → Param₂ → List Bool → Bool} (hCR : CollisionResistantForOn encParam₁ setup₁ H₁ valid₁) (hf : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × Param₁) => f p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary encParam₁) encParam₂) (hinj : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ p₁ ∈ (setup₁ n).support, ∀ (m₁ m₂ : List Bool), valid₂ n (f n p₁) m₁ = true → valid₂ n (f n p₁) m₂ = true → H₂ (f n p₁) m₁ = H₂ (f n p₁) m₂ → valid₁ n p₁ m₁ = true ∧ valid₁ n p₁ m₂ = true ∧ H₁ p₁ m₁ = H₁ p₁ m₂) : CollisionResistantForOn encParam₂ (fun (m : ℕ) => PMF.map (f m) (setup₁ m)) H₂ valid₂

Parameter-map and injective-digest reduction for CollisionResistantForOn: if f is computable in polynomial time and every H₂ (f n p₁)-collision on p₁ ∈ (setup₁ n).support is a valid H₁ p₁-collision, then CollisionResistantForOn for H₁ implies CollisionResistantForOn for H₂ under fun n => (setup₁ n).map (f n).

Keyed word-level collision-resistant hash families (Param = List Bool)

@[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₂

@[simp]

theorem Cslib.Crypto.isCollisionFor_eq_isCollision (H : List Bool → List Bool → List Bool) (valid : ℕ → List Bool → Bool) (n : ℕ) (k m₁ m₂ : List Bool) : isCollisionFor H (fun (m : ℕ) (x : List Bool) => valid m) n k m₁ m₂ = isCollision H valid n k m₁ 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.collisionGameFor_sampleList_eq (H : List Bool → List Bool → List Bool) (valid : ℕ → List Bool → Bool) (adversary : CollisionFinder) (n : ℕ) : collisionGameFor (fun (m : ℕ) => (BitString.sampleList m).eval) H (fun (m : ℕ) (x : List Bool) => valid m) adversary n = (collisionGame H valid adversary n).eval

The keyed collisionGame is the Param = List Bool, setup n = ProbComp.eval (sampleList n) specialization of collisionGameFor.

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.

@[reducible, inline]

abbrev 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: specialization of CollisionResistantForOn to Param = List Bool, Digest _ = List Bool, encParam = encBits, and setup n = ProbComp.eval (BitString.sampleList n).

@[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.

theorem Cslib.Crypto.CollisionResistantOn.collisionResistantForOn {Param : Type} {Digest : Param → Type} [(d : Param) → DecidableEq (Digest d)] {encParam : Param ↪ List Bool} {d : ℕ → Param} {H : List Bool → List Bool → List Bool} {toDigest : (p : Param) → List Bool → Digest p} {valid : ℕ → List Bool → Bool} (hCR : CollisionResistantOn H valid) (hd : Turing.MultiTapeTM.ComputableInPolyTime d Turing.MultiTapeTM.encUnary encParam) (hinj : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (k : List Bool), k.length = n → ∀ (m₁ m₂ : List Bool), valid n m₁ = true → valid n m₂ = true → toDigest (d n) (H k m₁) = toDigest (d n) (H k m₂) → H k m₁ = H k m₂) : CollisionResistantForOn (Turing.MultiTapeTM.encPair encParam Turing.MultiTapeTM.encBits) (fun (m : ℕ) => PMF.map (fun (k : List Bool) => (d m, k)) (BitString.sampleList m).eval) (fun (pk : Param × List Bool) (x : List Bool) => toDigest pk.1 (H pk.2 x)) fun (m : ℕ) (x : Param × List Bool) (x_1 : List Bool) => valid m x_1

Bridge from word-level CollisionResistantOn to CollisionResistantForOn over (d n, k) : Param × List Bool: when d : ℕ → Param is computable in polynomial time and toDigest (d n) is eventually injective on valid H k-outputs for n-bit keys k, collision resistance of H implies parameterized collision resistance of fun pk x => toDigest pk.1 (H pk.2 x) under setup n = (ProbComp.eval (BitString.sampleList n)).map (fun k => (d n, k)).

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.