Documentation

Complexity.Crypto.Computational.Homomorphic.Leveled.Encoding

Encodings for acyclic leveled encryption #

The public artifact contains the list of public keys and the adjacent encrypted secret-key links. The private artifact contains only the initial and final secrets. Both use existing framed encodings and total polynomial-time decoders; no private key is part of the public data.

Main definitions #

References #

The acyclic key chain follows Gentry, Section 2. Retaining two private endpoints supports both fresh and evaluated decryption through the same bit-string scheme interface.

source
def Cslib.Crypto.Homomorphic.Leveled.encPublicKey :
List (List Bool) × List (List (List Bool)) ↪ List Bool

Encode every public key and adjacent encrypted link, with no unencrypted secret key.

Instances For
    source
    def Cslib.Crypto.Homomorphic.Leveled.publicKeyDecoder :
    Turing.MultiTapeTM.Decoder encPublicKey

    Decode every public string; framing errors retain the standard total-decoder behavior.

    Instances For
      source
      def Cslib.Crypto.Homomorphic.Leveled.encSecretKey :
      List Bool × List Bool ↪ List Bool

      Encode the initial and final secret, independently of the length of the public key chain.

      Instances For
        source
        def Cslib.Crypto.Homomorphic.Leveled.secretKeyDecoder :
        Turing.MultiTapeTM.Decoder encSecretKey

        Decode the two private endpoint secrets from any bit string.

        Instances For
          source
          @[simp]
          theorem Cslib.Crypto.Homomorphic.Leveled.publicKeyDecoder_decode_enc (keys : List (List Bool)) (links : List (List (List Bool))) :
          publicKeyDecoder.decode (encPublicKey (keys, links)) = (keys, links)
          source
          @[simp]
          theorem Cslib.Crypto.Homomorphic.Leveled.secretKeyDecoder_decode_enc (first last : List Bool) :
          secretKeyDecoder.decode (encSecretKey (first, last)) = (first, last)
          source
          @[simp]
          theorem Cslib.Crypto.Homomorphic.Leveled.length_encSecretKey (first last : List Bool) :
          (encSecretKey (first, last)).length = 2 * first.length + 1 + last.length

          The private representation charges the framing of its first endpoint.