IND-CPA security of the acyclic leveled construction

Every native two-stage adversary against the actual serialized leveled scheme has negligible advantage, assuming base IND-CPA security, native base key generation and encryption, fixed supported secret length, and an efficient unary depth budget. The public key includes the complete encrypted-key chain, and message selection occurs after the adversary sees it.

Two public-artifact hybrids replace secret encryptions by zero encryptions in the two challenge worlds. A concrete base adversary simulates the intervening zero-link experiment. This proves qualitative single-challenge security with explicit uniform reductions; it does not assert Gentry's exact concrete-security loss. Correctness, evaluation efficiency, compactness, a concrete base cryptosystem and fixed-key unbounded-depth bootstrapping are separate results or obligations.

Main results

• Cslib.Crypto.Homomorphic.Leveled.publicKey_indistinguishable_zero: the serialized public artifact is indistinguishable from its zero-link hybrid.
• Cslib.Crypto.Homomorphic.Leveled.indCPA_keyGen: security of the actual key generation and tagged encryption algorithms.
• Cslib.Crypto.Homomorphic.Leveled.indCPA_scheme: security of the actual depth-budgeted scheme.

References

• C. Gentry, Fully homomorphic encryption using ideal lattices, Section 2, Theorem 4
• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Section 11.2

theorem Cslib.Crypto.Homomorphic.Leveled.publicKey_indistinguishable_zero {E : Scheme} (hsecure : Encryption.INDCPA E.keyGen E.encrypt) (hkeyGen : Probability.IsPPTOn Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) E.keyGen) (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) {width budget : ℕ → ℕ} (hwidth : ∀ (n : ℕ), ∀ keys ∈ (E.keyGen n).eval.support, keys.2.length = width n) (hbudget : Turing.MultiTapeTM.ComputableTidilyInPolyTime budget Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) : ComputationallyIndistinguishable (fun (n : ℕ) => PMF.map Prod.fst (keyGen E n (budget n)).eval) fun (n : ℕ) => PMF.map (⇑encPublicKey) (E.publicKeyChainHybrid n (2 * budget n) 0).eval

The actual serialized public key is computationally indistinguishable from the same independent public keys with equal-length zero plaintexts in every encrypted link.

theorem Cslib.Crypto.Homomorphic.Leveled.indCPA_keyGen {E : Scheme} (hsecure : Encryption.INDCPA E.keyGen E.encrypt) (hkeyGen : Probability.IsPPTOn Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) E.keyGen) (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) {width budget : ℕ → ℕ} (hwidth : ∀ (n : ℕ), ∀ keys ∈ (E.keyGen n).eval.support, keys.2.length = width n) (hbudget : Turing.MultiTapeTM.ComputableTidilyInPolyTime budget Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) : Encryption.INDCPA (fun (n : ℕ) => keyGen E n (budget n)) (encrypt E)

The actual serialized acyclic public key and fresh tagged encryption preserve IND-CPA. Both adversary stages are uniform strict PPT, with arbitrary polynomial saved state.

theorem Cslib.Crypto.Homomorphic.Leveled.indCPA_scheme {E : Scheme} (hsecure : Encryption.INDCPA E.keyGen E.encrypt) (hkeyGen : Probability.IsPPTOn Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) E.keyGen) (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) {width budget : ℕ → ℕ} (hwidth : ∀ (n : ℕ), ∀ keys ∈ (E.keyGen n).eval.support, keys.2.length = width n) (hbudget : Turing.MultiTapeTM.ComputableTidilyInPolyTime budget Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) : Encryption.INDCPA (scheme D budget).keyGen (scheme D budget).encrypt

The actual depth-budgeted scheme is IND-CPA secure. The decryption circuit family identifies the scheme but supplies no security premise; only base security and the stated native hypotheses are used.