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.

Main results

• Cslib.Crypto.Homomorphic.Leveled.isPPTOn_publicKeyGame: native public-artifact postprocessing.
• Cslib.Crypto.Homomorphic.Leveled.isPPT_zeroLinkAdversary: native base-game admissibility.

References

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

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.ComputableTidilyInPolyTime 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.