Documentation

Complexity.Crypto.Computational.Homomorphic.GSW.DepthParameters.Scheme

GSW evaluates its own augmented decryption circuit #

The serialized GSW algorithms at the logarithmic-depth parameter family form a bit-encryption Scheme. A circuit is permitted when its two NAND layers per De Morgan level fit depthBudget. Fresh encryption and evaluation of every permitted circuit are perfectly correct, with fixed key and ciphertext widths. The actual raw-input decryption circuit and its NAND augmentation are permitted, so the scheme is bootstrappable in Gentry's sense [Gentry2009, Definitions 4 and 5]. These are the premises of the generic constructions in Leveled and FixedKey apart from security. All four algorithms and the decryption-circuit generator have uniform native polynomial-time certificates.

IND-CPA security of the same algorithms assumes decision LWE for exactly this family. Correctness, bootstrappability and the runtime certificates use no computational assumption, and circular security is not asserted.

Main definitions #

Main results #

References #

source
def Cslib.Crypto.Homomorphic.GSW.DepthParameters.secretWidth (security : ℕ) :
ℕ

Secret words hold dimension residues of width bits.

Instances For
    source
    def Cslib.Crypto.Homomorphic.GSW.DepthParameters.ciphertextWidth (security : ℕ) :
    ℕ

    Ciphertext words hold a square bit matrix with rows rows and columns.

    Instances For
      source
      noncomputable def Cslib.Crypto.Homomorphic.GSW.DepthParameters.scheme :
      Scheme

      GSW at the logarithmic-depth family. Evaluation is the deterministic layered evaluator and reads no key. The permitted circuits are those of depth at most depthBudget / 2, the depth whose compiled NAND schedule the noise margin covers.

      Instances For
        source
        theorem Cslib.Crypto.Homomorphic.GSW.DepthParameters.correct :
        scheme.Correct

        Encryption and evaluation of every permitted circuit are perfectly correct.

        source
        theorem Cslib.Crypto.Homomorphic.GSW.DepthParameters.fixedWidth :
        scheme.FixedWidth secretWidth ciphertextWidth

        Secret keys, fresh ciphertexts and evaluation outputs have fixed widths.

        source
        def Cslib.Crypto.Homomorphic.GSW.DepthParameters.decryptionCircuits :
        DecryptionCircuits scheme secretWidth ciphertextWidth

        The actual raw-input GSW decryption circuits, secret bits first.

        Instances For
          source
          theorem Cslib.Crypto.Homomorphic.GSW.DepthParameters.bootstrappable :
          Scheme.Bootstrappable decryptionCircuits

          The decryption circuit and its NAND augmentation are permitted at every security parameter, so GSW is bootstrappable for the identity and NAND gates [Gentry2009, Definition 5].

          source
          theorem Cslib.Crypto.Homomorphic.GSW.DepthParameters.isPPTOn_keyGen :
          Probability.IsPPTOn Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) scheme.keyGen

          Key generation is strict PPT in the unary security parameter.

          source
          theorem Cslib.Crypto.Homomorphic.GSW.DepthParameters.isPPTOn_encrypt :
          Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool)) Turing.MultiTapeTM.encBits fun (p : ℕ × List Bool × Bool) => scheme.encrypt p.1 p.2.1 p.2.2

          Encryption is strict PPT on every public word and message.

          source
          theorem Cslib.Crypto.Homomorphic.GSW.DepthParameters.computableInPolyTime_decrypt :
          Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool × List Bool) => scheme.decrypt p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBool

          Decryption runs in native polynomial time on every raw secret and ciphertext word.

          source
          theorem Cslib.Crypto.Homomorphic.GSW.DepthParameters.isPPTOn_evaluate :
          Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair (Circuits.Boolean.encCircuit 1) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)))) Turing.MultiTapeTM.encBits fun (p : ℕ × List Bool × ((n : ℕ) × Circuits.Circuit Circuits.Boolean.signature n 1) × List (List Bool)) => scheme.evaluate p.1 p.2.1 p.2.2.1 p.2.2.2

          Evaluation is strict PPT on every security parameter, public word, circuit and input list; it samples no coins.

          source
          theorem Cslib.Crypto.Homomorphic.GSW.DepthParameters.computableInPolyTime_decryptionCircuits :
          Turing.MultiTapeTM.ComputableInPolyTime (fun (security : ℕ) => ⟨secretWidth security + ciphertextWidth security, decryptionCircuits.circuit security⟩) Turing.MultiTapeTM.encUnary (Circuits.Boolean.encCircuit 1)

          The decryption circuits, with their unary input arity, have a native generator.

          source
          theorem Cslib.Crypto.Homomorphic.GSW.DepthParameters.indCPA_scheme (hLWE : DecisionLWE Parameters.dimension samples width fun (k : ℕ) => noiseLaw (width k) (Parameters.noise k)) :
          Encryption.INDCPA scheme.keyGen scheme.encrypt

          The scheme's key generation and encryption are IND-CPA under decision LWE for exactly this family's dimensions, modulus and centered-binomial noise.