Native runtime of the leveled security reductions

The public-artifact test charges both adaptive adversary stages and the complete tagged challenge. The zero-link adversary charges the generated key list, all zero-link encryptions, public serialization and the adversary's saved state. isPPT_leveledAdversary certifies the asymptotic runtime consequence of [Gentry2009, Section 2, Theorem 4, p. 171]: the unified two-stage reduction is uniform strict PPT whenever the adversary, base scheme, depth and capacity are (without proving the multiplicative poly(ℓ, d) runtime factor relative to the adversary).

Main results

• Cslib.Crypto.Homomorphic.Leveled.isPPTOn_publicKeyGame: native public-artifact postprocessing.
• Cslib.Crypto.Homomorphic.Leveled.isPPT_zeroLinkAdversary: native zero-link base-game admissibility.
• Cslib.Crypto.Homomorphic.Leveled.isPPT_leveledAdversary: native admissibility of the unified leveled reduction.

References

• C. Gentry, Fully homomorphic encryption using ideal lattices, Section 2, Theorem 4

theorem Cslib.Crypto.Homomorphic.Leveled.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 (List Bool) × List (List (List Bool))) => publicKeyGame E adversary bit p.1 p.2

Both stages of the adversary run after complete public-artifact serialization.

theorem Cslib.Crypto.Homomorphic.Leveled.isPPT_zeroLinkAdversary {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) {depth : ℕ → ℕ} (hdepth : Turing.MultiTapeTM.ComputableInPolyTime depth Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) : (zeroLinkAdversary E depth adversary).IsPPT

The all-zero simulation is strict PPT with the parameter, complete input public key and saved state charged. The supported-width hypothesis is needed only for the semantic proof.

theorem Cslib.Crypto.Homomorphic.Leveled.isPPT_leveledAdversary {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) {depth capacity : ℕ → ℕ} (hdepth : Turing.MultiTapeTM.ComputableInPolyTime depth Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hcapacity : Turing.MultiTapeTM.ComputableInPolyTime capacity Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) : (leveledAdversary E depth capacity adversary).IsPPT

The unified leveled reduction is native strict PPT: its message selection charges both selector coins, the dyadic index coins, and the selected sub-reduction (zeroLinkAdversary or E.linkAdversary), while its guessing stage inspects the two prefix bits and charges the forwarded saved state and challenge ciphertext.