Security of an acyclic encrypted-key chain

Base IND-CPA security hides every secret-key bit encrypted in the public acyclic chain. The reduction replaces links from the end of the chain and bits from the beginning of each secret. Its two coordinates are sampled uniformly from polynomially bounded dyadic ranges.

The secret-width function need not be computable. A native key-generation certificate supplies an executable polynomial cap, while equality of supported secret lengths justifies the unknown target-secret substitution. The reduction contains no parameter-dependent advice and requires no decryption correctness or bootstrappability assumption.

Main results

• Cslib.Crypto.Homomorphic.Scheme.negligible_publicKeyChainHybrid: every native uniform test has negligible advantage between the actual public chain and its all-zero-link hybrid.

References

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

theorem Cslib.Crypto.Homomorphic.Scheme.negligible_publicKeyChainHybrid {E : Scheme} (hsecure : Encryption.INDCPA E.keyGen E.encrypt) (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) {width depth : ℕ → ℕ} (hwidth : ∀ (n : ℕ), ∀ keys ∈ (E.keyGen n).eval.support, keys.2.length = width n) (hdepth : Turing.MultiTapeTM.ComputableTidilyInPolyTime depth Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) {test : ℕ → List (List Bool) × List (List (List Bool)) → ProbComp Bool} (htest : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)))) Turing.MultiTapeTM.encBool fun (p : ℕ × List (List Bool) × List (List (List Bool))) => test p.1 p.2) : Negligible fun (n : ℕ) => Game.advantage (E.publicKeyChainHybrid n (depth n) (depth n) >>= test n).eval (E.publicKeyChainHybrid n (depth n) 0 >>= test n).eval

Encrypting an acyclic chain of fixed-length secrets is indistinguishable from encrypting zero words. The complete public keys and every encrypted link are given to the native test.