The decision-LWE distribution of generated GSW public keys

The public marginal of the actual key generator is exactly the decision-LWE law with independent centered-binomial errors reduced modulo 2 ^ w. The joint key generator still retains its secret; the equality below exposes only the public marginal, as required by the security experiment.

Main definitions

• noiseLaw: the precise modular error law supplied to the decision-LWE hypothesis.

Main results

• eval_errorVector_mod: independently sampled integer errors give the independent modular law.
• eval_keyGen_publicMatrix: the actual generated public matrix has the stated decision-LWE law.
• eval_keyGenSerialized_publicWord: the serialized key generator exposes that exact word ensemble.

References

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

noncomputable def Cslib.Crypto.Homomorphic.GSW.noiseLaw (w η : ℕ) : PMF (ZMod (2 ^ w))

Reduce the difference of two independent η-bit counts modulo the actual modulus.

theorem Cslib.Crypto.Homomorphic.GSW.eval_errorVector_mod (m w η : ℕ) : PMF.map (fun (error : Fin m → ℤ) (i : Fin m) => ↑(error i)) (ProbComp.eval (OracleComp.replicateFin m (Probability.sampleCenteredBinomial η))) = Probability.PMF.pi fun (x : Fin m) => noiseLaw w η

Reducing independent integer errors preserves the complete independent modular error law.

theorem Cslib.Crypto.Homomorphic.GSW.eval_keyGen_publicMatrix (n m w η : ℕ) : PMF.map Prod.fst (keyGen n m w η).eval = LWE.publicMatrixLaw n m w (noiseLaw w η)

The generated public matrix is an exact decision-LWE sample. This equality neither reveals the generated secret nor asserts that any parameter or error family is computationally hard.

theorem Cslib.Crypto.Homomorphic.GSW.eval_keyGen_publicWord (n m w η : ℕ → ℕ) (security : ℕ) : PMF.map (fun (keys : Matrix (Fin (m security)) (Fin (n security + 1)) (ZMod (2 ^ w security)) × (Fin (n security) → ZMod (2 ^ w security))) => Matrix.toBinary keys.1) (keyGen (n security) (m security) (w security) (η security)).eval = LWE.realEnsemble n m w (fun (k : ℕ) => noiseLaw (w k) (η k)) security

Encoding the actual public marginal gives the exact word ensemble in the hardness hypothesis, with no secret or error coordinates appended to the adversary's input.

theorem Cslib.Crypto.Homomorphic.GSW.eval_keyGenSerialized_publicWord (n m w η : ℕ → ℕ) (security : ℕ) : PMF.map Prod.fst (keyGenSerialized (n security) (m security) (w security) (η security)).eval = LWE.realEnsemble n m w (fun (k : ℕ) => noiseLaw (w k) (η k)) security

The actual serialized key generator has precisely the public marginal used by decision LWE. The encoded secret is discarded before the distinguisher is called.