Binary subset-sum hashing

A binary word selects a subset of independently uniform elements of a finite additive group. Distinct words give a uniformly distributed difference, and hence collide with probability exactly 1 / |G|. In particular, the output group may be a finite power of ZMod q for any positive modulus; no prime-modulus hypothesis is needed.

Main definitions

• Cslib.BitString.SubsetSum.hash: sum the weights selected by a binary word.
• Cslib.BitString.SubsetSum.hashRows: hash every binary row with the same weights.

Main results

• Cslib.BitString.SubsetSum.uniform_hash_sub: distinct words give a uniform difference.
• Cslib.BitString.SubsetSum.collision_probability: the exact collision probability.
• Cslib.BitString.SubsetSum.isDeltaUniversalHash, Cslib.BitString.SubsetSum.isTwoUniversal: the binary subset-sum family is 1 / |G|-Δ-universal, hence universal.
• Cslib.BitString.SubsetSum.dist_hashRows_le: many independent binary rows with one public seed.

References

• [C. Gentry, A. Sahai and B. Waters, Homomorphic Encryption from Learning with Errors: Conceptually-Simpler, Asymptotically-Faster, Attribute-Based, Section 3.2] [GSW13]

The proof reuses the finite-group uniformity lemmas in Probability.Uniform.

def Cslib.BitString.SubsetSum.hash {ι : Type u_1} {G : Type u_2} [Fintype ι] [AddCommGroup G] (weights : ι → G) (input : ι → Bool) : G

Sum the weights at the coordinates selected by a binary word.

theorem Cslib.BitString.SubsetSum.uniform_hash_sub {ι : Type u_1} {G : Type u_2} [Fintype ι] [AddCommGroup G] [Fintype G] [DecidableEq ι] (x y : ι → Bool) (hxy : x ≠ y) : PMF.map (fun (weights : ι → G) => hash weights x - hash weights y) (Probability.PMF.uniformOfFintype (ι → G)) = Probability.PMF.uniformOfFintype G

Distinct binary words give a uniform difference, including for composite-modulus groups.

theorem Cslib.BitString.SubsetSum.collision_probability {ι : Type u_1} {G : Type u_2} [Fintype ι] [AddCommGroup G] [Fintype G] [DecidableEq ι] (x y : ι → Bool) (hxy : x ≠ y) : (∑ weights : ι → G, if hash weights x = hash weights y then ((Probability.PMF.uniformOfFintype (ι → G)) weights).toReal else 0) = (↑(Fintype.card G))⁻¹

The collision probability is exactly the reciprocal output-group cardinality.

theorem Cslib.BitString.SubsetSum.isDeltaUniversalHash {ι : Type u_1} {G : Type u_2} [Fintype ι] [AddCommGroup G] [Fintype G] [DecidableEq ι] : Probability.IsDeltaUniversalHash (Probability.PMF.uniformOfFintype (ι → G)) hash (↑(Fintype.card G))⁻¹

Uniform group weights form a 1 / |G|-Δ-universal family on binary words: the difference of two hashes is uniform.

theorem Cslib.BitString.SubsetSum.isTwoUniversal {ι : Type u_1} {G : Type u_2} [Fintype ι] [AddCommGroup G] [Fintype G] [DecidableEq ι] : Probability.IsTwoUniversal (Probability.PMF.uniformOfFintype (ι → G)) hash

Uniform group weights form a universal family on binary words.

def Cslib.BitString.SubsetSum.hashRows {ι : Type u_1} {G : Type u_2} [Fintype ι] [AddCommGroup G] {κ : Type u_3} (weights : ι → G) (inputs : κ → ι → Bool) : κ → G

Apply the same public weights to every binary row.

theorem Cslib.BitString.SubsetSum.dist_hashRows_le {ι : Type u_1} {G : Type u_2} [Fintype ι] [AddCommGroup G] [Fintype G] [DecidableEq ι] {κ : Type u_3} [Fintype κ] [DecidableEq κ] : dist (Probability.seededHash (Probability.PMF.uniformOfFintype (ι → G)) (Probability.PMF.uniformOfFintype (κ → ι → Bool)) hashRows) ((Probability.PMF.uniformOfFintype (ι → G)).bind fun (weights : ι → G) => PMF.map (fun (x : κ → G) => (weights, x)) (Probability.PMF.uniformOfFintype (κ → G))) ≤ ↑(Fintype.card κ) * √(↑(Fintype.card G) / 2 ^ Fintype.card ι) / 2

Independent uniform binary rows become jointly close to uniform while their shared weights remain public. The loss is linear in the row count; the complete row family is not assumed to be two-universal.