Averaging acyclic key-chain hybrids

The signed gap of a key-chain experiment telescopes over links, then over secret-key bits. Both coordinates are averaged over fixed dyadic ranges. Unused coordinates reject in both worlds, including zero links and empty secret words. No parameter-dependent best coordinate is selected.

These are exact game identities. Connecting the averaged game to an actual native IND-CPA adversary is a separate reduction obligation.

Main definitions

• Cslib.Crypto.Homomorphic.Scheme.keyChainHybridGame: the two-coordinate hybrid average.

Main results

• Cslib.Crypto.Homomorphic.Scheme.publicKeyLinkHybrid_gap: signed bitwise telescoping.
• Cslib.Crypto.Homomorphic.Scheme.publicKeyChainHybrid_gap: the full signed two-coordinate identity with its explicit dyadic loss.

References

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

theorem Cslib.Crypto.Homomorphic.Scheme.publicKeyLinkHybrid_gap (E : Scheme) (n beforeCount afterCount width capacity : ℕ) (hwidth : ∀ keys ∈ (E.keyGen n).eval.support, keys.2.length = width) (hcapacity : width ≤ capacity) (test : List (List Bool) × List (List (List Bool)) → ProbComp Bool) : ↑(Game.succProbability (E.publicKeyChainHybrid n (beforeCount + afterCount + 1) (beforeCount + 1) >>= test).eval) - ↑(Game.succProbability (E.publicKeyChainHybrid n (beforeCount + afterCount + 1) beforeCount >>= test).eval) = ↑(Probability.dyadicSize capacity) * (↑(Game.succProbability ((Probability.PMF.uniformOfFintype (Fin (Probability.dyadicSize capacity))).bind fun (j : Fin (Probability.dyadicSize capacity)) => if ↑j < width then (E.publicKeyLinkHybrid n beforeCount afterCount ↑j >>= test).eval else PMF.pure false)) - ↑(Game.succProbability ((Probability.PMF.uniformOfFintype (Fin (Probability.dyadicSize capacity))).bind fun (j : Fin (Probability.dyadicSize capacity)) => if ↑j < width then (E.publicKeyLinkHybrid n beforeCount afterCount (↑j + 1) >>= test).eval else PMF.pure false)))

Telescope the bit hybrids of one link. The cap can be any upper bound on the common supported secret length; it need not equal that length.

noncomputable def Cslib.Crypto.Homomorphic.Scheme.keyChainHybridGame (E : Scheme) (n depth width capacity : ℕ) (test : List (List Bool) × List (List (List Bool)) → ProbComp Bool) (bit : Bool) : Game

Average reverse link indices and forward bit indices. Inactive coordinates return the same constant in both worlds. This is a distributional definition, not an unchecked sampler.

theorem Cslib.Crypto.Homomorphic.Scheme.publicKeyChainHybrid_gap (E : Scheme) (n depth width capacity : ℕ) (hwidth : ∀ keys ∈ (E.keyGen n).eval.support, keys.2.length = width) (hcapacity : width ≤ capacity) (test : List (List Bool) × List (List (List Bool)) → ProbComp Bool) : ↑(Game.succProbability (E.publicKeyChainHybrid n depth depth >>= test).eval) - ↑(Game.succProbability (E.publicKeyChainHybrid n depth 0 >>= test).eval) = ↑(Probability.dyadicSize depth) * ↑(Probability.dyadicSize capacity) * (↑(E.keyChainHybridGame n depth width capacity test false).succProbability - ↑(E.keyChainHybridGame n depth width capacity test true).succProbability)

The real-to-zero public-key gap is the signed gap of one uniformly selected link/bit hybrid, multiplied by the two dyadic range sizes.