Uniform polynomial-time key-chain generation

The actual key-chain sampler from [Gentry2009, Section 2] is strict PPT when key generation and bit encryption are uniformly strict PPT. Both the security parameter and the requested depth are encoded in unary. The certificates charge every key, every secret-key bit encryption, and the complete nested output encoding. They impose no correctness, fixed-width, or security assumption.

Main results

• Cslib.Crypto.Homomorphic.Scheme.isPPTOn_generateKeys: sample all levels of keys.
• Cslib.Crypto.Homomorphic.Scheme.isPPTOn_encryptKeyLinks: encrypt adjacent secret-key links.
• Cslib.Crypto.Homomorphic.Scheme.isPPTOn_generateKeyChain: the complete sampler is strict PPT.

References

• C. Gentry, Fully homomorphic encryption using ideal lattices

theorem Cslib.Crypto.Homomorphic.Scheme.isPPTOn_generateKeys {E : Scheme} (hkeyGen : Probability.IsPPTOn Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) E.keyGen) {α : Type} {input : α ↪ List Bool} {n depth : α → ℕ} (hn : Turing.MultiTapeTM.ComputableTidilyInPolyTime n input Turing.MultiTapeTM.encUnary) (hdepth : Turing.MultiTapeTM.ComputableTidilyInPolyTime depth input Turing.MultiTapeTM.encUnary) : Probability.IsPPTOn input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) fun (a : α) => E.generateKeys (n a) (depth a)

Generate an efficiently computed unary number of keys using bounded repetition.

theorem Cslib.Crypto.Homomorphic.Scheme.isPPTOn_encryptKeyLinks {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) {α : Type} {input : α ↪ List Bool} {n : α → ℕ} {keys : α → List (List Bool × List Bool)} (hn : Turing.MultiTapeTM.ComputableTidilyInPolyTime n input Turing.MultiTapeTM.encUnary) (hkeys : Turing.MultiTapeTM.ComputableTidilyInPolyTime keys input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits))) : Probability.IsPPTOn input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) fun (a : α) => E.encryptKeyLinks (n a) (keys a)

Encrypt every adjacent secret-key link, including all copied public keys and key bits.

theorem Cslib.Crypto.Homomorphic.Scheme.isPPTOn_generateKeyChain {E : Scheme} (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) {α : Type} {input : α ↪ List Bool} {n depth : α → ℕ} (hn : Turing.MultiTapeTM.ComputableTidilyInPolyTime n input Turing.MultiTapeTM.encUnary) (hdepth : Turing.MultiTapeTM.ComputableTidilyInPolyTime depth input Turing.MultiTapeTM.encUnary) : Probability.IsPPTOn input (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits))) fun (a : α) => E.generateKeyChain (n a) (depth a)

Generate the keys and their encrypted links with one uniform polynomial clock in the full encoded input. No correctness or output-width premise is used to bound the sampled keys.