Correct, compact and secure acyclic leveled encryption #
The independently proved correctness, exact width, native runtime and IND-CPA results apply to
the same constructed scheme. This module assembles correctness, budget-independent polynomial
widths and security without assuming those conclusions for the output scheme. Native certificates
for its algorithms remain available in Leveled.PolyTime.
Leveled.exists_decrypt_circuits, Leveled.exists_uniform_decrypt_circuits and
Leveled.exists_decrypt_parameter_bound give one decryption circuit family (with a native
polynomial-time circuit generator when secretWidth is computable in polynomial time in unary) and
one parameter-only resource bound shared by all budgets. These include the complete tagged decoder
and are chosen independently of the requested depth family.
The contract evaluates fresh ciphertexts under an efficiently computed unary depth budget. It does not promise arbitrary reuse of evaluated wrapper ciphertexts, circuit privacy, a concrete base scheme, or fixed-key evaluation without a predetermined budget.
Main results #
Cslib.Crypto.Homomorphic.Leveled.correct_fixedWidth_indCPA: a correct, secure constructed scheme with exact polynomial secret and ciphertext widths independent of the depth budget.Cslib.Crypto.Homomorphic.Leveled.exists_scheme_of_polynomiallyBounded: every polynomially bounded depth family is covered by an actual efficient and secure scheme, without requiring the requested family to be computable.Cslib.Crypto.Homomorphic.Leveled.schemeFamily_spec: the depth-indexed familyfun d => scheme D (fun _ => d)satisfies Gentry's Definition 3 with one uniform polynomial clock in(n, d)jointly across all depths.
References #
Assemble the actual construction's correctness, exact compact widths and IND-CPA security.
The native decryption-circuit generator bounds both widths; no output property is an input
hypothesis. Evaluation runtime additionally uses the base evaluator certificate, as stated by
isPPTOn_scheme_evaluate.
Every polynomially bounded depth family is covered by one actual leveled scheme with polynomial widths, native algorithms and IND-CPA security. The selected unary budget dominates the requested depth at every parameter, including its finite prefix. The requested depth family itself need not be computable: only the selected polynomial majorant is executed.
The depth-indexed family fun d => scheme D (fun _ => d) ({E^(d) : d ∈ ℕ} in
[Gentry2009, Definition 3, p. 170]) shares one uniform strict PPT clock jointly in (n, d)
for key generation, encryption and evaluation, and one deterministic polynomial clock jointly in
(n, d) for decryption. Any budget-specific scheme scheme D budget is obtained by substituting
d = budget n at each parameter n.