Documentation

Complexity.Crypto.Computational.Homomorphic.FixedKey.Reduction

The fixed-key security reduction #

The public-artifact game allows adaptive message selection after the entire encrypted-secret vector is visible. In the zero-vector experiment, a concrete base adversary samples an independent key only to learn the common supported secret length. It encrypts that many zero bits under the challenge public key and preserves both stages of the target adversary.

The unknown challenge secret is never available to the reduction. The supported-width premise is used only in the exact game identity, not by the algorithm or its native runtime certificate.

Main definitions #

Main results #

References #

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

Choose messages after seeing the complete artifact, then encrypt under its base public key and retain the adversary's exact saved state.

Instances For
    source
    def Cslib.Crypto.Homomorphic.FixedKey.zeroAdversary (E : Scheme) (adversary : Encryption.Adversary) :
    Encryption.Adversary

    Build the zero-vector public artifact from the challenge public key. An independently generated secret supplies only its length; the challenge secret is neither read nor saved.

    Instances For
      source
      theorem Cslib.Crypto.Homomorphic.FixedKey.isPPTOn_publicKeyGame {E : Scheme} (hencrypt : 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) => E.encrypt p.1 p.2.1 p.2.2) {adversary : Encryption.Adversary} (hadversary : adversary.IsPPT) (bit : Bool) :
      Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary encPublicKey) Turing.MultiTapeTM.encBool fun (p : ℕ × List Bool × List (List Bool)) => publicKeyGame E adversary bit p.1 p.2

      Both adversary stages and the complete public encoding have native certificates.

      source
      theorem Cslib.Crypto.Homomorphic.FixedKey.isPPT_zeroAdversary {E : Scheme} (hencrypt : 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) => E.encrypt p.1 p.2.1 p.2.2) {adversary : Encryption.Adversary} (hadversary : adversary.IsPPT) (hkeyGen : Probability.IsPPTOn Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) E.keyGen) :
      (zeroAdversary E adversary).IsPPT

      The reduction is uniform strict PPT without any width-computability premise.

      source
      theorem Cslib.Crypto.Homomorphic.FixedKey.eval_zeroAdversary (E : Scheme) (adversary : Encryption.Adversary) (bit : Bool) (n width : ℕ) (hwidth : ∀ keys ∈ (E.keyGen n).eval.support, keys.2.length = width) :
      (Encryption.game E.keyGen E.encrypt (zeroAdversary E adversary) bit n).eval = (Encryption.circularPublicKey E.keyGen E.encrypt false n >>= publicKeyGame E adversary bit n).eval

      A supported auxiliary key supplies exactly the challenge secret's length. Removing that unused auxiliary sample then gives the complete zero-vector chosen-message experiment.