Generated-key GSW security from the exact decision-LWE assumption

The actual serialized key generator and encryption program satisfy chosen-message security under decision LWE for their precise centered-binomial error law. A single uniform adversary reduction has loss two; the remaining statistical error comes from the shared uniform public matrix. Every runtime premise concerns the actual serialized program on its complete input.

Main definitions

• hidingError: the explicit statistical term in the chosen-message advantage bound.
• lweDistinguisher: the uniform hidden-bit reduction using actual serialized encryption.

Main results

• advantage_game_le: twice the decision-LWE advantage plus the explicit statistical term.
• indCPA_of_decisionLWE: negligible chosen-message advantage under an eventual entropy margin.
• Parameters.indCPA: the concrete positive-noise family instantiates all runtime and entropy requirements, leaving only its specified decision-LWE assumption.

This is ordinary single-challenge public-key security against uniform classical strict PPT adversaries. It does not provide circular security, a quantum worst-case lattice reduction, or a bootstrappability theorem.

References

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

noncomputable def Cslib.Crypto.Homomorphic.GSW.hidingError (n m w : ℕ) : NNReal

The shared-public-matrix statistical term, with N = (n + 1) * w ciphertext rows.

noncomputable def Cslib.Crypto.Homomorphic.GSW.lweDistinguisher (n m w : ℕ → ℕ) (adversary : Encryption.Adversary) : Distinguisher

The reduction uses the actual serialized encryption algorithm, including total decoding of arbitrary challenge words. Its hidden fair bit is not supplied to either adversary stage.

theorem Cslib.Crypto.Homomorphic.GSW.isPPT_lweDistinguisher {n m w : ℕ → ℕ} {adversary : Encryption.Adversary} (hn : Turing.MultiTapeTM.ComputableTidilyInPolyTime n Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hm : Turing.MultiTapeTM.ComputableTidilyInPolyTime m Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hw : Turing.MultiTapeTM.ComputableTidilyInPolyTime w Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hadversary : adversary.IsPPT) : Probability.IsPPT Turing.MultiTapeTM.encBool (lweDistinguisher n m w adversary)

Efficient parameter functions instantiate the actual reduction's uniform native certificate.

theorem Cslib.Crypto.Homomorphic.GSW.publicKeyGame_uniformEnsemble (n m w : ℕ → ℕ) (adversary : Encryption.Adversary) (bit : Bool) (security : ℕ) : Encryption.publicKeyGame (LWE.uniformEnsemble n m w security) (fun (k : ℕ) => encryptSerialized (n k) (m k) (w k)) adversary bit security = uniformPublicGame (fun (A : Matrix (Fin (m security)) (Fin (n security + 1)) (ZMod (2 ^ w security))) => (adversary.choose security (serializePublicMatrix A)).eval) (fun (state : List Bool) (ciphertext : Ciphertext (n security) (w security)) => (adversary.guess security state (serializeCiphertext ciphertext)).eval) bit

In the uniform-matrix experiment, serialized message selection, encryption and guessing agree with the typed adaptive hiding game, including the full saved word.

theorem Cslib.Crypto.Homomorphic.GSW.advantage_uniformEnsemble_le (n m w : ℕ → ℕ) (adversary : Encryption.Adversary) (security : ℕ) : (Encryption.publicKeyGame (LWE.uniformEnsemble n m w security) (fun (k : ℕ) => encryptSerialized (n k) (m k) (w k)) adversary false security).advantage (Encryption.publicKeyGame (LWE.uniformEnsemble n m w security) (fun (k : ℕ) => encryptSerialized (n k) (m k) (w k)) adversary true security) ≤ hidingError (n security) (m security) (w security)

The uniform public-key word gives the typed hiding theorem's full adaptive bound.

theorem Cslib.Crypto.Homomorphic.GSW.advantage_game_le (n m w η : ℕ → ℕ) (adversary : Encryption.Adversary) (security : ℕ) : Game.advantage (Encryption.game (fun (k : ℕ) => keyGenSerialized (n k) (m k) (w k) (η k)) (fun (k : ℕ) => encryptSerialized (n k) (m k) (w k)) adversary false security).eval (Encryption.game (fun (k : ℕ) => keyGenSerialized (n k) (m k) (w k) (η k)) (fun (k : ℕ) => encryptSerialized (n k) (m k) (w k)) adversary true security).eval ≤ 2 * (distinguishingGame (LWE.realEnsemble n m w (fun (k : ℕ) => noiseLaw (w k) (η k)) security) (lweDistinguisher n m w adversary security)).advantage (distinguishingGame (LWE.uniformEnsemble n m w security) (lweDistinguisher n m w adversary security)) + hidingError (n security) (m security) (w security)

One uniform reduction bounds actual chosen-message advantage by twice its exact decision-LWE advantage plus the shared-public-matrix statistical error. No efficiency is needed for this law.

theorem Cslib.Crypto.Homomorphic.GSW.indCPA_of_decisionLWE {n m w η : ℕ → ℕ} (hn : Turing.MultiTapeTM.ComputableTidilyInPolyTime n Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hm : Turing.MultiTapeTM.ComputableTidilyInPolyTime m Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hw : Turing.MultiTapeTM.ComputableTidilyInPolyTime w Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hmargin : ∀ᶠ (security : ℕ) in Filter.atTop, (n security + 1) * w security + 2 * security ≤ m security) (hLWE : DecisionLWE n m w fun (k : ℕ) => noiseLaw (w k) (η k)) : Encryption.INDCPA (fun (k : ℕ) => keyGenSerialized (n k) (m k) (w k) (η k)) fun (k : ℕ) => encryptSerialized (n k) (m k) (w k)

The actual encryption scheme is IND-CPA secure under its exact decision-LWE assumption, provided efficient dimensions have an eventual entropy surplus of twice the security parameter.

theorem Cslib.Crypto.Homomorphic.GSW.Parameters.indCPA (hLWE : DecisionLWE dimension samples width fun (k : ℕ) => noiseLaw (width k) (noise k)) : Encryption.INDCPA (fun (k : ℕ) => keyGenSerialized (dimension k) (samples k) (width k) (noise k)) fun (k : ℕ) => encryptSerialized (dimension k) (samples k) (width k)

The positive-noise parameter family supplies every dimension/runtime/entropy premise. Only decision LWE for its precise centered-binomial law remains a security assumption.