Hybrids for an acyclic encrypted-key chain

The link hybrid retains real secret-key encryptions before a boundary and encrypts zero words after it. Moving the boundary towards the initial key erases links from the end of the chain. This order is essential: when a reduction embeds a challenge public key, the outgoing link that would contain its unknown secret has already been replaced by an encryption of zeros.

These are actual sampling programs and exact distributional identities. They do not assume or establish computational indistinguishability on their own.

Main definitions

• Cslib.Crypto.Homomorphic.Scheme.encryptZeroKeyLinks: encrypt equal-length zero words.
• Cslib.Crypto.Homomorphic.Scheme.encryptKeyLinksHybrid: retain a prefix of real links.
• Cslib.Crypto.Homomorphic.Scheme.publicKeyChainHybrid: sample the complete public artifact.
• Cslib.Crypto.Homomorphic.Scheme.publicKeyLinkHybrid: refine one boundary link bit by bit.
• Cslib.Crypto.Homomorphic.Scheme.spliceEncryptedKeyLink: insert the base challenge ciphertext.

Main results

• Cslib.Crypto.Homomorphic.Scheme.eval_generateKeys_splice: sampling the challenge key first preserves the complete joint key distribution.
• Cslib.Crypto.Homomorphic.Scheme.eval_spliceEncryptedKeyLink_original, .eval_spliceEncryptedKeyLink_zero: exact laws for the two challenge worlds.
• Cslib.Crypto.Homomorphic.Scheme.eval_publicKeyLinkHybrid_zero, .eval_publicKeyLinkHybrid_length: bit-hybrid endpoints are the adjacent link hybrids.

References

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

theorem Cslib.Crypto.Homomorphic.Scheme.eval_generateKeys_splice (E : Scheme) (n beforeCount afterCount : ℕ) : (do let next ← E.keyGen n let before ← OracleComp.replicate beforeCount (E.keyGen n) let predecessor ← E.keyGen n let after ← OracleComp.replicate afterCount (E.keyGen n) pure (before ++ predecessor :: next :: after)).eval = (E.generateKeys n (beforeCount + afterCount + 1)).eval

Draw the target key first, then independently draw the keys before and after its predecessor. Splicing them restores the complete original key-generation distribution.

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

Replace every secret-key plaintext by a zero word of the same length. The public keys, number of links and number of bit encryptions in each link are retained.

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

Encrypt real secrets in the first cut links, and zero words in the remaining links. The two key segments overlap at their boundary key; each link is sampled exactly once.

theorem Cslib.Crypto.Homomorphic.Scheme.encryptKeyLinks_append_cons (E : Scheme) (n : ℕ) (before : List (List Bool × List Bool)) (middle : List Bool × List Bool) (after : List (List Bool × List Bool)) : E.encryptKeyLinks n (before ++ middle :: after) = do let front ← E.encryptKeyLinks n (before ++ [middle]) let back ← E.encryptKeyLinks n (middle :: after) pure (front ++ back)

Splitting a real-link traversal keeps its shared boundary key in both segments.

theorem Cslib.Crypto.Homomorphic.Scheme.encryptZeroKeyLinks_append_cons (E : Scheme) (n : ℕ) (before : List (List Bool × List Bool)) (middle : List Bool × List Bool) (after : List (List Bool × List Bool)) : E.encryptZeroKeyLinks n (before ++ middle :: after) = do let front ← E.encryptZeroKeyLinks n (before ++ [middle]) let back ← E.encryptZeroKeyLinks n (middle :: after) pure (front ++ back)

Splitting a zero-link traversal also keeps the shared boundary key.

@[simp]

theorem Cslib.Crypto.Homomorphic.Scheme.encryptZeroKeyLinks_nil (E : Scheme) (n : ℕ) : E.encryptZeroKeyLinks n [] = pure []

@[simp]

theorem Cslib.Crypto.Homomorphic.Scheme.encryptZeroKeyLinks_singleton (E : Scheme) (n : ℕ) (key : List Bool × List Bool) : E.encryptZeroKeyLinks n [key] = pure []

theorem Cslib.Crypto.Homomorphic.Scheme.encryptZeroKeyLinks_cons_cons (E : Scheme) (n : ℕ) (first second : List Bool × List Bool) (rest : List (List Bool × List Bool)) : E.encryptZeroKeyLinks n (first :: second :: rest) = do let link ← E.encryptBits n second.1 (List.replicate first.2.length false) List.cons link <$> E.encryptZeroKeyLinks n (second :: rest)

Expose the first zero link, retaining ordinary independent bit encryption.

theorem Cslib.Crypto.Homomorphic.Scheme.encryptZeroKeyLinks_cons_congr (E : Scheme) (n : ℕ) (first replacement : List Bool × List Bool) (rest : List (List Bool × List Bool)) (hlength : first.2.length = replacement.2.length) : E.encryptZeroKeyLinks n (first :: rest) = E.encryptZeroKeyLinks n (replacement :: rest)

The first zero link uses only the length of the first secret. Its public key is unused.

@[simp]

theorem Cslib.Crypto.Homomorphic.Scheme.encryptKeyLinksHybrid_zero (E : Scheme) (n : ℕ) (keys : List (List Bool × List Bool)) : E.encryptKeyLinksHybrid n 0 keys = E.encryptZeroKeyLinks n keys

A boundary at zero erases every secret-key plaintext.

theorem Cslib.Crypto.Homomorphic.Scheme.encryptKeyLinksHybrid_of_length_le_succ (E : Scheme) (n cut : ℕ) (keys : List (List Bool × List Bool)) (hcut : keys.length ≤ cut + 1) : E.encryptKeyLinksHybrid n cut keys = E.encryptKeyLinks n keys

A boundary after the last link also retains every original link.

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

Sample the independent keys and a link hybrid, returning only public data.

theorem Cslib.Crypto.Homomorphic.Scheme.eval_publicKeyChainHybrid_depth (E : Scheme) (n depth : ℕ) : (E.publicKeyChainHybrid n depth depth).eval = PMF.map (fun (chain : List (List Bool × List Bool) × List (List (List Bool))) => (List.map Prod.fst chain.1, chain.2)) (E.generateKeyChain n depth).eval

The final boundary is the exact public marginal of the original key-chain sampler.

theorem Cslib.Crypto.Homomorphic.Scheme.publicKeyChainHybrid_zero (E : Scheme) (n depth : ℕ) : E.publicKeyChainHybrid n depth 0 = do let keys ← E.generateKeys n depth let links ← E.encryptZeroKeyLinks n keys pure (List.map Prod.fst keys, links)

The initial boundary samples the same public keys with zero plaintexts in every link.

def Cslib.Crypto.Homomorphic.Scheme.encryptKeyLinkHybrid (E : Scheme) (n : ℕ) (before : List (List Bool × List Bool)) (predecessor next : List Bool × List Bool) (after : List (List Bool × List Bool)) (cut : ℕ) : ProbComp (List (List (List Bool)))

Refine the boundary link bit by bit, leaving earlier links real and later links zeroed. predecessor is the key whose secret is encrypted under next.1.

theorem Cslib.Crypto.Homomorphic.Scheme.encryptKeyLinkHybrid_zero (E : Scheme) (n : ℕ) (before : List (List Bool × List Bool)) (predecessor next : List Bool × List Bool) (after : List (List Bool × List Bool)) : E.encryptKeyLinkHybrid n before predecessor next after 0 = E.encryptKeyLinksHybrid n (before.length + 1) (before ++ predecessor :: next :: after)

Before erasing any bit, the boundary link is still real.

theorem Cslib.Crypto.Homomorphic.Scheme.encryptKeyLinkHybrid_length (E : Scheme) (n : ℕ) (before : List (List Bool × List Bool)) (predecessor next : List Bool × List Bool) (after : List (List Bool × List Bool)) : E.encryptKeyLinkHybrid n before predecessor next after predecessor.2.length = E.encryptKeyLinksHybrid n before.length (before ++ predecessor :: next :: after)

After erasing every bit, the boundary link is part of the zeroed suffix.

theorem Cslib.Crypto.Homomorphic.Scheme.encryptKeyLinkHybrid_secret_congr (E : Scheme) (n : ℕ) (before : List (List Bool × List Bool)) (predecessor : List Bool × List Bool) (pk secret replacement : List Bool) (after : List (List Bool × List Bool)) (cut : ℕ) (hlength : secret.length = replacement.length) : E.encryptKeyLinkHybrid n before predecessor (pk, secret) after cut = E.encryptKeyLinkHybrid n before predecessor (pk, replacement) after cut

Once its outgoing link is zeroed, replacing the target key's secret by an equal-length word does not change the intermediate sampler. Its public key is retained.

def Cslib.Crypto.Homomorphic.Scheme.spliceEncryptedKeyLink (E : Scheme) (n : ℕ) (before : List (List Bool × List Bool)) (predecessor next : List Bool × List Bool) (after : List (List Bool × List Bool)) (cut : ℕ) (challenge : List Bool) : ProbComp (List (List (List Bool)))

Sample the surrounding encrypted links and insert one ciphertext into the boundary link.

theorem Cslib.Crypto.Homomorphic.Scheme.eval_spliceEncryptedKeyLink_original (E : Scheme) (n : ℕ) (before : List (List Bool × List Bool)) (predecessor next : List Bool × List Bool) (after : List (List Bool × List Bool)) (cut : ℕ) (hcut : cut < predecessor.2.length) : (do let challenge ← E.encrypt n next.1 (predecessor.2.getD cut false) E.spliceEncryptedKeyLink n before predecessor next after cut challenge).eval = (E.encryptKeyLinkHybrid n before predecessor next after cut).eval

The bit challenge is sampled independently of every surrounding link. An original-bit challenge recovers the full earlier hybrid distribution.

theorem Cslib.Crypto.Homomorphic.Scheme.eval_spliceEncryptedKeyLink_zero (E : Scheme) (n : ℕ) (before : List (List Bool × List Bool)) (predecessor next : List Bool × List Bool) (after : List (List Bool × List Bool)) (cut : ℕ) (hcut : cut < predecessor.2.length) : (do let challenge ← E.encrypt n next.1 false E.spliceEncryptedKeyLink n before predecessor next after cut challenge).eval = (E.encryptKeyLinkHybrid n before predecessor next after (cut + 1)).eval

A zero-bit challenge recovers the full next hybrid distribution, retaining all other encrypted links and their randomness.

def Cslib.Crypto.Homomorphic.Scheme.publicKeyLinkHybrid (E : Scheme) (n beforeCount afterCount cut : ℕ) : ProbComp (List (List Bool) × List (List (List Bool)))

Sample an intermediate bit hybrid with the target key drawn first. Only public keys and encrypted links are returned. This sampling order matches the single-challenge reduction.

theorem Cslib.Crypto.Homomorphic.Scheme.eval_publicKeyLinkHybrid_zero (E : Scheme) (n beforeCount afterCount : ℕ) : (E.publicKeyLinkHybrid n beforeCount afterCount 0).eval = (E.publicKeyChainHybrid n (beforeCount + afterCount + 1) (beforeCount + 1)).eval

The initial bit boundary is the corresponding real-link boundary in the original key sampling order. This is an equality of complete public distributions.

theorem Cslib.Crypto.Homomorphic.Scheme.eval_publicKeyLinkHybrid_length (E : Scheme) (n beforeCount afterCount width : ℕ) (hwidth : ∀ keys ∈ (E.keyGen n).eval.support, keys.2.length = width) : (E.publicKeyLinkHybrid n beforeCount afterCount width).eval = (E.publicKeyChainHybrid n (beforeCount + afterCount + 1) beforeCount).eval

With a fixed supported secret length, the final bit boundary is the preceding link boundary. No efficiency or ciphertext-width assumption is needed for this exact law.