Acyclic chains of encrypted secret keys

The sampler generates one more key pair than the requested depth, then encrypts each secret key under the next public key. This is the acyclic construction of [Gentry2009, Section 2], indexed in evaluation order. Sampling and support are explicit; no security claim is made here. The returned key pairs retain the secret keys as private correctness witnesses. Public evaluation uses only the public-key projection and encrypted links. Acyclicity refers to positions in the chain; sampled key values may coincide.

Main definitions

• Cslib.Crypto.Homomorphic.Scheme.generateKeys: independently sample the key pairs.
• Cslib.Crypto.Homomorphic.Scheme.encryptKeyLinks: encrypt secrets between adjacent keys.
• Cslib.Crypto.Homomorphic.Scheme.generateKeyChain: sample the keys and their encrypted links.
• Cslib.Crypto.Homomorphic.Scheme.ValidLinks: the links are pointwise fresh encryptions.

Main results

• Cslib.Crypto.Homomorphic.Scheme.mem_support_generateKeyChain_iff: exact supported keys, key count, and encrypted links of the actual sampler.

References

• C. Gentry, Fully homomorphic encryption using ideal lattices

def Cslib.Crypto.Homomorphic.Scheme.generateKeys (E : Scheme) (n depth : ℕ) : ProbComp (List (List Bool × List Bool))

Independently sample one key pair for each level, including the initial level.

def Cslib.Crypto.Homomorphic.Scheme.encryptKeyLinks (E : Scheme) (n : ℕ) (keys : List (List Bool × List Bool)) : ProbComp (List (List (List Bool)))

Encrypt each old secret key under the next public key. Empty and singleton lists have no links.

def Cslib.Crypto.Homomorphic.Scheme.generateKeyChain (E : Scheme) (n depth : ℕ) : ProbComp (List (List Bool × List Bool) × List (List (List Bool)))

Sample all key pairs before encrypting their adjacent secret-key links. The result retains private secret-key witnesses and is not the public key artifact.

def Cslib.Crypto.Homomorphic.Scheme.ValidLinks (E : Scheme) (n : ℕ) (keys : List (List Bool × List Bool)) (links : List (List (List Bool))) : Prop

Each link freshly encrypts the preceding secret key under the following public key.

theorem Cslib.Crypto.Homomorphic.Scheme.mem_support_generateKeys_iff (E : Scheme) (n depth : ℕ) (keys : List (List Bool × List Bool)) : keys ∈ (E.generateKeys n depth).eval.support ↔ keys.length = depth + 1 ∧ ∀ key ∈ keys, key ∈ (E.keyGen n).eval.support

Sampling the keys fixes their number and requires exactly pointwise key-generation support.

theorem Cslib.Crypto.Homomorphic.Scheme.mem_support_encryptKeyLinks_iff (E : Scheme) (n : ℕ) (keys : List (List Bool × List Bool)) (links : List (List (List Bool))) : links ∈ (E.encryptKeyLinks n keys).eval.support ↔ E.ValidLinks n keys links

Supported outputs of the link sampler are exactly the valid links.

theorem Cslib.Crypto.Homomorphic.Scheme.ValidLinks.length_eq {E : Scheme} {n : ℕ} {keys : List (List Bool × List Bool)} {links : List (List (List Bool))} (h : E.ValidLinks n keys links) : links.length = keys.length - 1

A valid chain has one fewer encrypted link than key pairs.

theorem Cslib.Crypto.Homomorphic.Scheme.ValidLinks.getD {E : Scheme} {n : ℕ} {keys : List (List Bool × List Bool)} {links : List (List (List Bool))} (h : E.ValidLinks n keys links) {i : ℕ} (hi : i < links.length) : E.FreshInputs n (keys.getD (i + 1) ([], [])).1 (keys.getD i ([], [])).2 (links.getD i [])

At each link index, the link freshly encrypts that level's secret under the next public key. The bounds ensure that none of the default values is used.

theorem Cslib.Crypto.Homomorphic.Scheme.mem_support_generateKeyChain_iff (E : Scheme) (n depth : ℕ) (keys : List (List Bool × List Bool)) (links : List (List (List Bool))) : (keys, links) ∈ (E.generateKeyChain n depth).eval.support ↔ keys.length = depth + 1 ∧ (∀ key ∈ keys, key ∈ (E.keyGen n).eval.support) ∧ E.ValidLinks n keys links

The actual key-chain sampler produces exactly supported keys and valid encrypted links.

theorem Cslib.Crypto.Homomorphic.Scheme.lengths_of_mem_support_generateKeyChain (E : Scheme) {n depth : ℕ} {keys : List (List Bool × List Bool)} {links : List (List (List Bool))} (h : (keys, links) ∈ (E.generateKeyChain n depth).eval.support) : keys.length = depth + 1 ∧ links.length = depth

Every supported key chain has the requested number of transitions and one additional key.

theorem Cslib.Crypto.Homomorphic.Scheme.key_mem_support_of_generatedChain (E : Scheme) {n depth : ℕ} {keys : List (List Bool × List Bool)} {links : List (List (List Bool))} (h : (keys, links) ∈ (E.generateKeyChain n depth).eval.support) {i : ℕ} (hi : i ≤ depth) : keys.getD i ([], []) ∈ (E.keyGen n).eval.support

Every position through the final level of a generated chain is a supported base key pair. The index bound ensures that the default pair is never used.