Exact games of the encrypted-link reduction

The concrete two-stage reduction simulates the full public key-chain distribution. Its saved state contains only keys that it generated and the public challenge key. Fixed supported secret length justifies replacing the unknown challenge secret by an equally long zero word after its outgoing link has been erased.

Main results

• Cslib.Crypto.Homomorphic.Scheme.eval_guessLink_active: exact simulation after inserting a challenge ciphertext.
• Cslib.Crypto.Homomorphic.Scheme.eval_linkAdversaryAt: the complete base encryption game at a supplied link and bit coordinate, including rejection of padding coordinates.
• Cslib.Crypto.Homomorphic.Scheme.eval_linkAdversary: exact uniform averaging of the concrete two-stage adversary.
• Cslib.Crypto.Homomorphic.Scheme.publicKeyChainHybrid_advantage_linkAdversary: the exact unsigned reduction loss for the complete public artifact.

References

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

theorem Cslib.Crypto.Homomorphic.Scheme.eval_guessLink_active (E : Scheme) (test : ℕ → List (List Bool) × List (List (List Bool)) → ProbComp Bool) (n : ℕ) (before : List (List Bool × List Bool)) (predecessor next : List Bool × List Bool) (after : List (List Bool × List Bool)) (cut : ℕ) (bit : Bool) (hcut : cut < predecessor.2.length) (hlength : next.2.length = predecessor.2.length) : (do let challenge ← E.encrypt n next.1 (if bit = true then false else predecessor.2.getD cut false) E.guessLink test n (activeLinkState before predecessor next.1 after cut) challenge).eval = (do let links ← E.encryptKeyLinkHybrid n before predecessor next after (cut + if bit = true then 1 else 0) test n (List.map Prod.fst (before ++ predecessor :: next :: after), links)).eval

An active reduction reconstructs the corresponding complete bit hybrid. The target secret is used only in this specification; the algorithm knows its length from the predecessor.

theorem Cslib.Crypto.Homomorphic.Scheme.eval_linkAdversaryAt (E : Scheme) (beforeCount afterCount bitIndex : ℕ → ℕ) (test : ℕ → List (List Bool) × List (List (List Bool)) → ProbComp Bool) (n width : ℕ) (bit : Bool) (hwidth : ∀ keys ∈ (E.keyGen n).eval.support, keys.2.length = width) : (Encryption.game E.keyGen E.encrypt (E.linkAdversaryAt beforeCount afterCount bitIndex test) bit n).eval = if bitIndex n < width then (E.publicKeyLinkHybrid n (beforeCount n) (afterCount n) (bitIndex n + if bit = true then 1 else 0) >>= test n).eval else PMF.pure false

The real single-challenge encryption game equals the chosen bit hybrid. The fixed-width hypothesis ranges only over honestly generated keys; no decryption correctness is assumed.

theorem Cslib.Crypto.Homomorphic.Scheme.eval_linkAdversary (E : Scheme) (depth capacity : ℕ → ℕ) (test : ℕ → List (List Bool) × List (List (List Bool)) → ProbComp Bool) (n width : ℕ) (bit : Bool) (hwidth : ∀ keys ∈ (E.keyGen n).eval.support, keys.2.length = width) : (Encryption.game E.keyGen E.encrypt (E.linkAdversary depth capacity test) bit n).eval = E.keyChainHybridGame n (depth n) width (capacity n) (test n) bit

The actual uniformly sampled two-stage reduction realizes the exact two-coordinate game. Every random choice and every saved-state computation is part of the concrete adversary.

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

The public key-chain gap is exactly the concrete base adversary's signed gap, with the explicit dyadic sampling loss. No maximizing coordinate or nonuniform advice is selected.

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

The exact unsigned reduction loss for the full public artifact. Padding contributes no gap, including when there are no links or no secret bits.