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.
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.
References #
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.