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, and zeroLinkAdversary simulates the intervening zero-link experiment. The unified two-stage reduction leveledAdversary combines all three hops into a single base IND-CPA adversary with concrete loss 4 * dyadicSize (2 * budget n) * dyadicSize (capacity n) ≤ 16 * (2 * budget n + 1) * (capacity n + 1), matching Gentry's Theorem 4 ([Gen09], Section 2, p. 171) up to a constant factor from power-of-two coin sampling and NAND-compiled depth 2 * d, with asymptotic IsPPT rather than a multiplicative runtime bound relative to the adversary. 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.advantage_scheme_eq_leveledAdversary: exact concrete-security identity for scheme D budget via leveledAdversary.
• Cslib.Crypto.Homomorphic.Leveled.advantage_scheme_le_mul_leveledAdversary: concrete polynomial loss bound 16 * (2 * budget n + 1) * (capacity n + 1) for scheme D budget.
• 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.advantage_scheme_eq_leveledAdversary {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (budget capacity : ℕ → ℕ) (adversary : Encryption.Adversary) (n width : ℕ) (hwidth : ∀ keys ∈ (E.keyGen n).eval.support, keys.2.length = width) (hcapacity : width ≤ capacity n) : Game.advantage (Encryption.game (scheme D budget).keyGen (scheme D budget).encrypt adversary false n).eval (Encryption.game (scheme D budget).keyGen (scheme D budget).encrypt adversary true n).eval = 4 * ↑(Probability.dyadicSize (2 * budget n)) * ↑(Probability.dyadicSize (capacity n)) * Game.advantage (Encryption.game E.keyGen E.encrypt (leveledAdversary E (fun (n : ℕ) => 2 * budget n) capacity adversary) false n).eval (Encryption.game E.keyGen E.encrypt (leveledAdversary E (fun (n : ℕ) => 2 * budget n) capacity adversary) true n).eval

Exact chosen-message advantage of the depth-budgeted scheme scheme D budget in terms of the unified two-stage base reduction leveledAdversary ([Gen09], Section 2, Theorem 4, p. 171, up to a constant factor in the loss; the running-time clause is not formalized).

theorem Cslib.Crypto.Homomorphic.Leveled.advantage_scheme_le_mul_leveledAdversary {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (budget capacity : ℕ → ℕ) (adversary : Encryption.Adversary) (n width : ℕ) (hwidth : ∀ keys ∈ (E.keyGen n).eval.support, keys.2.length = width) (hcapacity : width ≤ capacity n) : Game.advantage (Encryption.game (scheme D budget).keyGen (scheme D budget).encrypt adversary false n).eval (Encryption.game (scheme D budget).keyGen (scheme D budget).encrypt adversary true n).eval ≤ 16 * (2 * ↑(budget n) + 1) * (↑(capacity n) + 1) * Game.advantage (Encryption.game E.keyGen E.encrypt (leveledAdversary E (fun (n : ℕ) => 2 * budget n) capacity adversary) false n).eval (Encryption.game E.keyGen E.encrypt (leveledAdversary E (fun (n : ℕ) => 2 * budget n) capacity adversary) true n).eval

Polynomial concrete-security bound for the depth-budgeted scheme scheme D budget with explicit factor 16 * (2 * budget n + 1) * (capacity n + 1) ([Gen09], Section 2, Theorem 4, p. 171, up to a constant factor in the loss; the running-time clause is not formalized).

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