Integer noise witnesses for GSW encryption

The modular ciphertext equations use explicit integer errors. A binary matrix sends an error vector to a subset sum in each row. Fresh encryption therefore has error at most the sum of the input magnitudes. For NAND, the first ciphertext multiplies the second error, and the second message multiplies the first error. These bounds use the structural Boolean-entry invariant.

Main definitions

• encryptionError: the integer subset sums selected by the encryption coins.
• nandError: the exact propagated integer error for the NAND operation.

Main results

• encryptionError_natAbs_le: m errors bounded by B give fresh error at most m * B.
• nandError_natAbs_le: errors bounded by B₁, B₂ give NAND error at most B₁ + N * B₂.

References

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

def Cslib.Crypto.Homomorphic.GSW.encryptionError {ι : Type u_1} {κ : Type u_2} [Fintype κ] (R : Matrix ι κ Bool) (error : κ → ℤ) : ι → ℤ

The integer error selected by each binary row of encryption coins.

theorem Cslib.Crypto.Homomorphic.GSW.encryptionError_natAbs_le_sum {ι : Type u_1} {κ : Type u_2} [Fintype κ] (R : Matrix ι κ Bool) (error : κ → ℤ) (i : ι) : (encryptionError R error i).natAbs ≤ ∑ j : κ, (error j).natAbs

Each fresh error is bounded by the sum of the original integer error magnitudes.

theorem Cslib.Crypto.Homomorphic.GSW.encryptionError_natAbs_le {ι : Type u_1} {κ : Type u_2} [Fintype κ] (R : Matrix ι κ Bool) (error : κ → ℤ) {bound : ℕ} (herror : ∀ (j : κ), (error j).natAbs ≤ bound) (i : ι) : (encryptionError R error i).natAbs ≤ Fintype.card κ * bound

A uniform bound on the input errors gives the usual fresh-encryption noise bound.

theorem Cslib.Crypto.Homomorphic.GSW.bitMatrix_mulVec_intCast {ι : Type u_1} {κ : Type u_2} [Fintype κ] (w : ℕ) (R : Matrix ι κ Bool) (error : κ → ℤ) : ((bitMatrix (ZMod (2 ^ w)) R).mulVec fun (j : κ) => ↑(error j)) = fun (i : ι) => ↑(encryptionError R error i)

Casting the integer subset sums agrees with the modular matrix computation.

def Cslib.Crypto.Homomorphic.GSW.nandError {ι : Type u_1} [Fintype ι] (C₁ : Matrix ι ι Bool) (μ₂ : Bool) (error₁ error₂ : ι → ℤ) : ι → ℤ

The exact NAND error: the second message scales the first error, while the first ciphertext multiplies the second error.

theorem Cslib.Crypto.Homomorphic.GSW.nandError_natAbs_le {ι : Type u_1} [Fintype ι] (C₁ : Matrix ι ι Bool) (μ₂ : Bool) (error₁ error₂ : ι → ℤ) {bound₁ bound₂ : ℕ} (herror₁ : ∀ (i : ι), (error₁ i).natAbs ≤ bound₁) (herror₂ : ∀ (i : ι), (error₂ i).natAbs ≤ bound₂) (i : ι) : (nandError C₁ μ₂ error₁ error₂ i).natAbs ≤ bound₁ + Fintype.card ι * bound₂

NAND increases error from B₁, B₂ to at most B₁ + N * B₂.