Exact chosen-message games of leveled encryption

The actual serialized scheme experiment is the real public-chain hybrid followed by adaptive message selection. At the zero-link endpoint, one base IND-CPA challenge simulates the entire experiment, including the adversary's retained state and the fresh-ciphertext tag.

Combining the two encrypted-link hybrid reductions (E.linkAdversary for the false and message-swapped true challenge worlds) with the dyadically weighted zeroLinkAdversary yields leveledAdversary, whose base IND-CPA game achieves the exact concrete-security loss 4 * dyadicSize (2 * budget n) * dyadicSize (capacity n), bounded between 4 * (2 * budget n + 1) * (capacity n + 1) and 16 * (2 * budget n + 1) * (capacity n + 1) and therefore matching Gentry's Theorem 4 loss ℓ(d + 1) up to a constant factor ([Gen09], Section 2, Theorem 4, p. 171; the constant arises from the 2 * budget n encrypted links, dyadic power-of-two index rounding, and the four-way branch selector with one inactive branch).

Main results

• Cslib.Crypto.Homomorphic.Leveled.eval_keyGen_public: the exact serialized public marginal.
• Cslib.Crypto.Homomorphic.Leveled.eval_game_keyGen: the actual scheme game is the real-chain public-artifact experiment.
• Cslib.Crypto.Homomorphic.Leveled.eval_zeroLinkAdversary: an exact simulation of the zero-chain chosen-message experiment, including depth zero.
• Cslib.Crypto.Homomorphic.Leveled.eval_leveledAdversary: exact distributional decomposition of the unified base reduction leveledAdversary.
• Cslib.Crypto.Homomorphic.Leveled.gap_leveledAdversary: signed telescoping identity relating the leveled scheme's chosen-message gap to leveledAdversary.
• Cslib.Crypto.Homomorphic.Leveled.advantage_game_eq_leveledAdversary: exact unsigned advantage identity with factor 4 * dyadicSize (2 * budget n) * dyadicSize (capacity n).
• Cslib.Crypto.Homomorphic.Leveled.advantage_game_le_mul_leveledAdversary: concrete polynomial loss bound 16 * (2 * budget n + 1) * (capacity n + 1) (Gentry's Theorem 4 up to a constant factor).

References

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

theorem Cslib.Crypto.Homomorphic.Leveled.eval_keyGen_public (E : Scheme) (n budget : ℕ) : PMF.map Prod.fst (keyGen E n budget).eval = PMF.map (⇑encPublicKey) (E.publicKeyChainHybrid n (2 * budget) (2 * budget)).eval

The actual key generator's public marginal is the serialized real-chain hybrid.

theorem Cslib.Crypto.Homomorphic.Leveled.eval_game_keyGen (E : Scheme) (budget : ℕ → ℕ) (adversary : Encryption.Adversary) (bit : Bool) (n : ℕ) : (Encryption.game (fun (n : ℕ) => keyGen E n (budget n)) (encrypt E) adversary bit n).eval = (E.publicKeyChainHybrid n (2 * budget n) (2 * budget n) >>= publicKeyGame E adversary bit n).eval

The public artifact and tagged challenge in the actual scheme game agree with the real chain experiment; intermediate and endpoint secrets remain hidden.

theorem Cslib.Crypto.Homomorphic.Leveled.eval_zeroLinkAdversary (E : Scheme) (depth : ℕ → ℕ) (adversary : Encryption.Adversary) (bit : Bool) (n width : ℕ) (hwidth : ∀ keys ∈ (E.keyGen n).eval.support, keys.2.length = width) : (Encryption.game E.keyGen E.encrypt (zeroLinkAdversary E depth adversary) bit n).eval = (E.publicKeyChainHybrid n (depth n) 0 >>= publicKeyGame E adversary bit n).eval

The zero-link base adversary simulates the entire adaptive chosen-message experiment. When the chain is nonempty, a generated secret supplies the unknown first secret's length; when it is empty, no secret length is used.

theorem Cslib.Crypto.Homomorphic.Leveled.eval_leveledAdversary (E : Scheme) (depth capacity : ℕ → ℕ) (adversary : Encryption.Adversary) (bit : Bool) (n : ℕ) : (Encryption.game E.keyGen E.encrypt (leveledAdversary E depth capacity adversary) bit n).eval = (Probability.PMF.uniformOfFintype Bool).bind fun (first : Bool) => (Probability.PMF.uniformOfFintype Bool).bind fun (second : Bool) => if first = true then if second = true then PMF.pure false else (ProbComp.sampleDyadicCoin (depth n) 1).eval.bind fun (keepLink : Bool) => if keepLink = true then (ProbComp.sampleDyadicCoin (capacity n) 1).eval.bind fun (keepBit : Bool) => if keepBit = true then (Encryption.game E.keyGen E.encrypt (zeroLinkAdversary E depth adversary) bit n).eval else PMF.pure false else PMF.pure false else if second = true then (Encryption.game E.keyGen E.encrypt (E.linkAdversary depth capacity (publicKeyGame E adversary true)) (!bit) n).eval else (Encryption.game E.keyGen E.encrypt (E.linkAdversary depth capacity (publicKeyGame E adversary false)) bit n).eval

The unified base reduction's encryption game is the fair four-branch average over the false-world linkAdversary, the message-swapped true-world linkAdversary, the dyadically weighted zeroLinkAdversary, and an inactive rejecting branch.

theorem Cslib.Crypto.Homomorphic.Leveled.succProbability_leveledAdversary (E : Scheme) (depth capacity : ℕ → ℕ) (adversary : Encryption.Adversary) (bit : Bool) (n : ℕ) : 4 * ↑(Probability.dyadicSize (depth n)) * ↑(Probability.dyadicSize (capacity n)) * ↑(Game.succProbability (Encryption.game E.keyGen E.encrypt (leveledAdversary E depth capacity adversary) bit n).eval) = ↑(Probability.dyadicSize (depth n)) * ↑(Probability.dyadicSize (capacity n)) * ↑(Game.succProbability (Encryption.game E.keyGen E.encrypt (E.linkAdversary depth capacity (publicKeyGame E adversary false)) bit n).eval) + ↑(Probability.dyadicSize (depth n)) * ↑(Probability.dyadicSize (capacity n)) * ↑(Game.succProbability (Encryption.game E.keyGen E.encrypt (E.linkAdversary depth capacity (publicKeyGame E adversary true)) (!bit) n).eval) + ↑(Game.succProbability (Encryption.game E.keyGen E.encrypt (zeroLinkAdversary E depth adversary) bit n).eval)

The exact scaled acceptance probability of leveledAdversary equals the sum of the two dyadic-grid-scaled linkAdversary acceptance probabilities and the zeroLinkAdversary acceptance probability.

theorem Cslib.Crypto.Homomorphic.Leveled.gap_leveledAdversary (E : Scheme) (budget capacity : ℕ → ℕ) (adversary : Encryption.Adversary) (n width : ℕ) (hwidth : ∀ keys ∈ (E.keyGen n).eval.support, keys.2.length = width) (hcapacity : width ≤ capacity n) : ↑(Game.succProbability (Encryption.game (fun (n : ℕ) => keyGen E n (budget n)) (encrypt E) adversary false n).eval) - ↑(Game.succProbability (Encryption.game (fun (n : ℕ) => keyGen E n (budget n)) (encrypt E) adversary true n).eval) = 4 * ↑(Probability.dyadicSize (2 * budget n)) * ↑(Probability.dyadicSize (capacity n)) * (↑(Game.succProbability (Encryption.game E.keyGen E.encrypt (leveledAdversary E (fun (n : ℕ) => 2 * budget n) capacity adversary) false n).eval) - ↑(Game.succProbability (Encryption.game E.keyGen E.encrypt (leveledAdversary E (fun (n : ℕ) => 2 * budget n) capacity adversary) true n).eval))

The signed chosen-message gap of the actual serialized leveled scheme equals the exact dyadic loss 4 * dyadicSize (2 * budget n) * dyadicSize (capacity n) times the signed gap of leveledAdversary against the base encryption scheme ([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_game_eq_leveledAdversary (E : Scheme) (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 (fun (n : ℕ) => keyGen E n (budget n)) (encrypt E) adversary false n).eval (Encryption.game (fun (n : ℕ) => keyGen E n (budget n)) (encrypt E) 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 unsigned concrete-security identity for the actual serialized leveled scheme: its chosen-message advantage equals 4 * dyadicSize (2 * budget n) * dyadicSize (capacity n) times the base chosen-message advantage of 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_game_le_mul_leveledAdversary (E : Scheme) (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 (fun (n : ℕ) => keyGen E n (budget n)) (encrypt E) adversary false n).eval (Encryption.game (fun (n : ℕ) => keyGen E n (budget n)) (encrypt E) 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 actual serialized leveled scheme in terms of the chain length 2 * budget n and secret-width bound capacity n: rounding both dyadic ranges via dyadicSize_le bounds the single-adversary reduction loss by 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).