Hashing isolates preimages

Given an image f x, a universal hash can isolate x among its other preimages. On successful isolation, every predicate of x is determined by the revealed information. Consequently, the remaining conditional entropy of a bit is bounded by the probability of a hash collision inside the fiber. The seed stays public; a predicate may depend on it, so it can include a fresh parity query as well as the hash matrix.

Main results

• Cslib.Probability.IsTwoUniversal.fiber_collision_le: failure to isolate a preimage.
• Cslib.Probability.IsTwoUniversal.conditionalEntropy_hash_le: entropy bounded by collisions.
• Cslib.Probability.conditionalEntropy_random_hash_le: entropy averaged over public hash lengths.

References

• T. Holenstein, Pseudorandom Generators from One-Way Functions: A Simple Construction for Any Hardness, Section 4, proof of Lemma 3. The isolation and averaged entropy bounds allow arbitrary two-universal families and input distributions, retaining the sampled hash length as public information.

Adapted from Probability/HashIsolation.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

theorem Cslib.Probability.IsTwoUniversal.fiber_collision_le {Seed : Type u_1} {Input : Type u_2} {Image : Type u_3} {Output : Type u_4} [Fintype Seed] [Fintype Input] [Fintype Output] {seed : PMF Seed} {hash : Seed → Input → Output} (hhash : IsTwoUniversal seed hash) (f : Input → Image) (x : Input) : (∑ s : Seed, if ∃ (y : Input), y ≠ x ∧ f y = f x ∧ hash s y = hash s x then (seed s).toReal else 0) ≤ min 1 (↑(Nat.card { y : Input // f y = f x } - 1) / ↑(Fintype.card Output))

The chance that a hash fails to isolate a preimage is at most the number of its competitors divided by the hash alphabet size, capped at one. No assumption on the fiber sizes is needed.

theorem Cslib.Probability.IsTwoUniversal.conditionalEntropy_hash_le {Seed : Type u_1} {Input : Type u_2} {Image : Type u_3} {Output : Type u_4} [Fintype Seed] [Fintype Input] [Finite Image] [Fintype Output] {seed : PMF Seed} {hash : Seed → Input → Output} (hhash : IsTwoUniversal seed hash) (source : PMF Input) (f : Input → Image) (predicate : Seed → Input → Bool) : PMF.conditionalEntropy (seed.bind fun (s : Seed) => PMF.map (fun (x : Input) => ((s, f x, hash s x), predicate s x)) source) ≤ ∑ x : Input, (source x).toReal * min 1 (↑(Nat.card { y : Input // f y = f x } - 1) / ↑(Fintype.card Output))

Conditional entropy after revealing the seed, the function image, and the hash value is bounded by the expected probability that the hash leaves more than one possible preimage.

theorem Cslib.Probability.conditionalEntropy_random_hash_le {Seed : Type u_1} {Input : Type u_2} {Image : Type u_3} [Fintype Seed] [Fintype Input] [Finite Image] (count : ℕ) [NeZero count] (seed : PMF Seed) (source : PMF Input) (f : Input → Image) (hash : (i : Fin count) → Seed → Input → Fin (↑i + 1) → Bool) (hhash : ∀ (i : Fin count), IsTwoUniversal seed (hash i)) (predicate : Fin count → Seed → Input → Bool) : PMF.conditionalEntropy ((PMF.uniformOfFintype (Fin count)).bind fun (i : Fin count) => seed.bind fun (s : Seed) => PMF.map (fun (x : Input) => (⟨i, (s, f x, hash i s x)⟩, predicate i s x)) source) ≤ (∑ x : Input, (source x).toReal * Real.logb 2 ↑(Nat.card { y : Input // f y = f x }) + 2) / ↑count

The averaged bound applies to the actual joint experiment with a public uniform hash length. The dependent observation type records exactly the number of revealed hash bits.