Statistical hiding of GSW ciphertexts under a uniform public matrix

The public matrix is sampled uniformly and remains visible to the adversary. Independent binary rows of encryption coins share this one matrix. Their joint leftover-hash bound applies to the actual encryptWithCoins ciphertext. The first adversarial stage may inspect the public matrix, choose both messages, and retain arbitrary randomized state for the final guess.

This is the unconditional statistical step of the GSW security reduction. It supplies neither a decision-LWE assumption, security of generated public keys, native runtime certificates, nor bootstrappability.

Main definitions

• uniformPublicGame: the adaptive two-stage experiment with a uniform public matrix.
• idealGame: retain the first-stage state and replace the ciphertext by independent uniform modular coefficients followed by decomposition.

Main results

• dist_uniformPublicGame_ideal_le: the shared-matrix statistical bound preserves saved state.
• uniformPublicGame_advantage_le: the two chosen-message games differ by at most N * sqrt(2^(w * (n + 1)) / 2^m), where N = (n + 1) * w.

References

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

theorem Cslib.Crypto.Homomorphic.GSW.uniform_decomposeMatrix_add {n w : ℕ} (shift : Matrix (Fin (n + 1) × Fin w) (Fin (n + 1)) (ZMod (2 ^ w))) : PMF.map (fun (U : Matrix (Fin (n + 1) × Fin w) (Fin (n + 1)) (ZMod (2 ^ w))) => decomposeMatrix w (shift + U)) (Probability.PMF.uniformOfFintype (Matrix (Fin (n + 1) × Fin w) (Fin (n + 1)) (ZMod (2 ^ w)))) = PMF.map (decomposeMatrix w) (Probability.PMF.uniformOfFintype (Matrix (Fin (n + 1) × Fin w) (Fin (n + 1)) (ZMod (2 ^ w))))

Adding any fixed modular message shift preserves the decomposed uniform distribution.

noncomputable def Cslib.Crypto.Homomorphic.GSW.uniformPublicGame {n m w : ℕ} {State : Type} (choose : Matrix (Fin m) (Fin (n + 1)) (ZMod (2 ^ w)) → PMF ((Bool × Bool) × State)) (guess : State → Ciphertext n w → PMF Bool) (bit : Bool) : PMF Bool

The first stage sees the public matrix before choosing two bits and retaining its state. The second stage receives that same state and the actual challenge ciphertext.

noncomputable def Cslib.Crypto.Homomorphic.GSW.idealGame {n m w : ℕ} {State : Type} (choose : Matrix (Fin m) (Fin (n + 1)) (ZMod (2 ^ w)) → PMF ((Bool × Bool) × State)) (guess : State → Ciphertext n w → PMF Bool) : PMF Bool

The common ideal experiment retains the first-stage state. Its ciphertext no longer depends on either chosen message. The state type need not be finite.

theorem Cslib.Crypto.Homomorphic.GSW.dist_uniformPublicGame_ideal_le {n m w : ℕ} {State : Type} (choose : Matrix (Fin m) (Fin (n + 1)) (ZMod (2 ^ w)) → PMF ((Bool × Bool) × State)) (guess : State → Ciphertext n w → PMF Bool) (bit : Bool) : dist (uniformPublicGame choose guess bit) (idealGame choose guess) ≤ ↑((n + 1) * w) * √(2 ^ (w * (n + 1)) / 2 ^ m) / 2

The entire adaptive experiment is close to one common ideal game. No efficiency or finite state assumption is imposed on either adversarial stage.

theorem Cslib.Crypto.Homomorphic.GSW.uniformPublicGame_advantage_le {n m w : ℕ} {State : Type} (choose : Matrix (Fin m) (Fin (n + 1)) (ZMod (2 ^ w)) → PMF ((Bool × Bool) × State)) (guess : State → Ciphertext n w → PMF Bool) : |((uniformPublicGame choose guess false) true).toReal - ((uniformPublicGame choose guess true) true).toReal| ≤ ↑((n + 1) * w) * √(2 ^ (w * (n + 1)) / 2 ^ m)

Under a uniform public matrix, arbitrary adaptive message selection and saved state give acceptance probabilities differing by at most N * sqrt(2^(w * (n + 1)) / 2^m). This concerns the uniform-matrix world, not the public-key distribution generated from LWE.