Uniform native certificates for the depth-budgeted scheme #

These certificates compose the actual sampler, serializers, total decoders, circuit compiler, identity padding, encrypted evaluator and tags. Both the security parameter and depth budget use unary encodings. The same polynomial bound therefore applies as the budget varies; the proofs do not fix a different hidden clock for each budget. Efficient unary budget families can then be substituted for the second parameter.

The bounds charge the complete key artifacts, circuit code and input ciphertext lists. They also cover malformed keys, wrong-width ciphertexts, and circuits exceeding the budget. No correctness or valid-input premise supplies a runtime bound. Total decryption executes the generated circuit, so no separate runtime assumption on the base decryption function is needed.

Main results #

Cslib.Crypto.Homomorphic.Leveled.isPPTOn_keyGen: uniform generation in the parameter and budget.
Cslib.Crypto.Homomorphic.Leveled.isPPTOn_encrypt: fresh tagged encryption.
Cslib.Crypto.Homomorphic.Leveled.computableTidilyInPolyTime_decrypt: total tagged decryption.
Cslib.Crypto.Homomorphic.Leveled.isPPTOn_evaluate: uniform evaluation of the complete circuit.
Cslib.Crypto.Homomorphic.Leveled.polynomiallyBounded_widths: polynomial secret-key and ciphertext widths follow from the native decryption-circuit generator.

References #

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

source

theorem Cslib.Crypto.Homomorphic.Leveled.computableTidilyInPolyTime_keyPair {α : Type} {input : α ↪ List Bool} {depth : α → ℕ} {keys : α → List (List Bool × List Bool)} {links : α → List (List (List Bool))} (hdepth : Turing.MultiTapeTM.ComputableTidilyInPolyTime depth input Turing.MultiTapeTM.encUnary) (hkeys : Turing.MultiTapeTM.ComputableTidilyInPolyTime keys input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits))) (hlinks : Turing.MultiTapeTM.ComputableTidilyInPolyTime links input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits))) :

Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => keyPair (depth a) (keys a) (links a)) input (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)

Serialize public projections and two secret endpoints, including the complete output words.

source

Probability.IsPPTOn input (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) fun (a : α) => keyGen E (n a) (budget a)

The key sampler has one native clock uniform in both unary parameters.

source

Probability.IsPPTOn input Turing.MultiTapeTM.encBits fun (a : α) => encrypt E (n a) (pk a) (bit a)

Decode every public word, encrypt under its initial key, and add the fresh tag.

source

theorem Cslib.Crypto.Homomorphic.Leveled.computableTidilyInPolyTime_decrypt {α : Type} {input : α ↪ List Bool} {E : Scheme} {n : α → ℕ} {sk ciphertext : α → List Bool} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (hD : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (n : ℕ) => ⟨secretWidth n + ciphertextWidth n, D.circuit n⟩) Turing.MultiTapeTM.encUnary (Circuits.Boolean.encCircuit 1)) (hn : Turing.MultiTapeTM.ComputableTidilyInPolyTime n input Turing.MultiTapeTM.encUnary) (hsk : Turing.MultiTapeTM.ComputableTidilyInPolyTime sk input Turing.MultiTapeTM.encBits) (hc : Turing.MultiTapeTM.ComputableTidilyInPolyTime ciphertext input Turing.MultiTapeTM.encBits) :

Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => decrypt D (n a) (sk a) (ciphertext a)) input Turing.MultiTapeTM.encBool

Decryption is polynomial time on every encoded input and contains no budget parameter.

source

Probability.IsPPTOn input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits) fun (a : α) => evaluateCircuit D (n a) (budget a) (publicKeys a) (links a) (inputs a) (inputCount a) (code a)

Compile, pad, evaluate and select outputs uniformly in the full raw code and unary budget.

source

Probability.IsPPTOn input Turing.MultiTapeTM.encBits fun (a : α) => evaluate D (n a) (budget a) (pk a) (c a) (inputs a)

The actual scheme evaluator is strict PPT, including on malformed artifacts and on circuits outside the chosen depth budget. The native certificate charges the complete circuit input.

source

theorem Cslib.Crypto.Homomorphic.Leveled.polynomiallyBounded_widths {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (hD : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (n : ℕ) => ⟨secretWidth n + ciphertextWidth n, D.circuit n⟩) Turing.MultiTapeTM.encUnary (Circuits.Boolean.encCircuit 1)) :

(PolynomiallyBounded fun (n : ℕ) => 3 * secretWidth n + 1) ∧ PolynomiallyBounded fun (n : ℕ) => ciphertextWidth n + 1

The circuit generator emits its input arity in unary. Its native runtime certificate therefore bounds both base widths and the two derived widths polynomially in n, independently of the depth budget. No separate polynomial-width assumption is needed.

source

Probability.IsPPTOn Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (scheme D budget).keyGen

Substitute an efficiently computed unary depth budget into the constructed key generator.

source

theorem Cslib.Crypto.Homomorphic.Leveled.isPPTOn_scheme_encrypt {E : Scheme} (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) {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (budget : ℕ → ℕ) :

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) => (scheme D budget).encrypt p.1 p.2.1 p.2.2

The constructed scheme's encryption certificate does not depend on computing its budget.

source

theorem Cslib.Crypto.Homomorphic.Leveled.computableTidilyInPolyTime_scheme_decrypt {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (hD : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (n : ℕ) => ⟨secretWidth n + ciphertextWidth n, D.circuit n⟩) Turing.MultiTapeTM.encUnary (Circuits.Boolean.encCircuit 1)) (budget : ℕ → ℕ) :

Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (p : ℕ × List Bool × List Bool) => (scheme D budget).decrypt p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBool

The constructed decryption algorithm and its polynomial clock are independent of the budget.

source

theorem Cslib.Crypto.Homomorphic.Leveled.isPPTOn_scheme_evaluate {E : Scheme} (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) {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (hD : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (n : ℕ) => ⟨secretWidth n + ciphertextWidth n, D.circuit n⟩) Turing.MultiTapeTM.encUnary (Circuits.Boolean.encCircuit 1)) (hevaluate : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair (Circuits.Boolean.encCircuit 1) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)))) Turing.MultiTapeTM.encBits fun (p : ℕ × List Bool × ((n : ℕ) × Circuits.Circuit Circuits.Boolean.signature n 1) × List (List Bool)) => E.evaluate p.1 p.2.1 p.2.2.1 p.2.2.2) (budget : ℕ → ℕ) (hbudget : Turing.MultiTapeTM.ComputableTidilyInPolyTime budget Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) :

Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair (Circuits.Boolean.encCircuit 1) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)))) Turing.MultiTapeTM.encBits fun (p : ℕ × List Bool × ((n : ℕ) × Circuits.Circuit Circuits.Boolean.signature n 1) × List (List Bool)) => (scheme D budget).evaluate p.1 p.2.1 p.2.2.1 p.2.2.2

An efficient unary budget yields one uniform certificate for the constructed evaluator.

Documentation

Complexity.Crypto.Computational.Homomorphic.Leveled.PolyTime

Uniform native certificates for the depth-budgeted scheme #

Main results #

References #