Documentation

Complexity.Crypto.Computational.Homomorphic.Leveled.Reduction

Chosen-message experiments for the leveled construction #

The public-artifact experiment lets the adversary choose its messages after receiving the entire serialized key chain. The zero-link reduction places the base challenge public key first and generates every later key itself. A generated secret supplies the first zero link's length; when the chain has no links, that length is unused. Its guessing stage retains the adversary's exact state and adds the ordinary fresh-ciphertext tag to the base challenge.

leveledAdversary combines the two encrypted-link hybrid reductions (E.linkAdversary for the false and message-swapped true challenge worlds) and the dyadically weighted zeroLinkAdversary into a single two-stage base IND-CPA adversary, realizing Gentry's Theorem 4 concrete-security reduction up to a constant factor ([Gen09], Section 2, Theorem 4, p. 171): writing d = budget n and ℓ = capacity n, the exact loss is 4 * dyadicSize (2 * d) * dyadicSize ℓ (between 4 * (2 * d + 1) * (ℓ + 1) and 16 * (2 * d + 1) * (ℓ + 1), so within a constant factor of Gentry's ℓ * (d + 1)). isPPT_leveledAdversary proves the asymptotic efficiency consequence that the reduction is uniform strict PPT whenever the adversary, base scheme, depth and capacity are; the multiplicative runtime bound (poly(ℓ, d) times that of the adversary) is not proved here.

Main definitions #

References #

source
def Cslib.Crypto.Homomorphic.Leveled.publicKeyGame (E : Scheme) (adversary : Encryption.Adversary) (bit : Bool) (n : ℕ) (artifact : List (List Bool) × List (List (List Bool))) :
ProbComp Bool

Choose both messages after seeing every public key and encrypted link, then give the tagged challenge ciphertext to the guessing stage together with its unchanged saved state.

Instances For
    source
    def Cslib.Crypto.Homomorphic.Leveled.zeroLinkAdversary (E : Scheme) (depth : ℕ → ℕ) (adversary : Encryption.Adversary) :
    Encryption.Adversary

    Simulate the all-zero chain using the challenge key as its initial public key. The unknown challenge secret is never read or saved; only independently generated secrets supply lengths.

    Instances For
      source
      def Cslib.Crypto.Homomorphic.Leveled.tagLeveledChoice (first second : Bool) (choice : (Bool × Bool) × List Bool) :
      (Bool × Bool) × List Bool

      Prefix two selector bits onto the saved state of a chosen-message choice.

      Instances For
        source
        def Cslib.Crypto.Homomorphic.Leveled.swapLeveledChoice (choice : (Bool × Bool) × List Bool) :
        (Bool × Bool) × List Bool

        Swap the two challenge messages of a chosen-message choice while keeping its saved state.

        Instances For
          source
          def Cslib.Crypto.Homomorphic.Leveled.rejectLeveledChoice :
          (Bool × Bool) × List Bool

          Fixed inactive choice for rejected dyadic coordinates or the unused selector branch.

          Instances For
            source
            noncomputable def Cslib.Crypto.Homomorphic.Leveled.leveledAdversary (E : Scheme) (depth capacity : ℕ → ℕ) (adversary : Encryption.Adversary) :
            Encryption.Adversary

            Unified two-stage base IND-CPA reduction for the acyclic leveled construction ([Gen09], Section 2, Theorem 4, p. 171, up to a constant factor in the loss; the running-time clause is not formalized). Two fair selector bits choose between:

            • (false, false): the false-world encrypted-link reduction E.linkAdversary,
            • (false, true): the message-swapped true-world encrypted-link reduction E.linkAdversary,
            • (true, false): the zero-link reduction zeroLinkAdversary, weighted by the inverse dyadic grid size (dyadicSize (depth n) * dyadicSize (capacity n))⁻¹ via sampleDyadicCoin,
            • (true, true): an inactive branch returning false.
            Instances For