Native runtime of the encrypted-link reduction

The actual two-stage reduction is uniform strict PPT. Message selection charges every generated key and the encoded saved context. Guessing charges total parsing on every saved word, the zero replacement secret, all simulated encryptions and the complete public artifact passed to its test. No security, correctness or fixed-width hypothesis is used in these runtime certificates.

Main results

• Cslib.Crypto.Homomorphic.Scheme.isPPTOn_chooseLinkAt: sample a complete reduction context.
• Cslib.Crypto.Homomorphic.Scheme.isPPTOn_guessLink: run the response on arbitrary saved words.
• Cslib.Crypto.Homomorphic.Scheme.isPPT_linkAdversaryAt: admissibility at efficient indices.
• Cslib.Crypto.Homomorphic.Scheme.isPPT_linkAdversary: admissibility of uniform dyadic selection.

References

• C. Gentry, Fully homomorphic encryption using ideal lattices, Section 2
• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Section 11.2

theorem Cslib.Crypto.Homomorphic.Scheme.isPPTOn_chooseLinkAt {E : Scheme} (hkeyGen : Probability.IsPPTOn Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) E.keyGen) {α : Type} {input : α ↪ List Bool} {n beforeCount afterCount bitIndex : α → ℕ} {challengePk : α → List Bool} (hn : Turing.MultiTapeTM.ComputableTidilyInPolyTime n input Turing.MultiTapeTM.encUnary) (hbefore : Turing.MultiTapeTM.ComputableTidilyInPolyTime beforeCount input Turing.MultiTapeTM.encUnary) (hafter : Turing.MultiTapeTM.ComputableTidilyInPolyTime afterCount input Turing.MultiTapeTM.encUnary) (hindex : Turing.MultiTapeTM.ComputableTidilyInPolyTime bitIndex input Turing.MultiTapeTM.encUnary) (hpk : Turing.MultiTapeTM.ComputableTidilyInPolyTime challengePk input Turing.MultiTapeTM.encBits) : Probability.IsPPTOn input (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBool Turing.MultiTapeTM.encBool) Turing.MultiTapeTM.encBits) fun (a : α) => E.chooseLinkAt (n a) (beforeCount a) (afterCount a) (bitIndex a) (challengePk a)

Sample all known keys and encode the actual context, charging every saved secret bit.

theorem Cslib.Crypto.Homomorphic.Scheme.isPPTOn_guessLink {E : Scheme} (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) {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) {α : Type} {input : α ↪ List Bool} {n : α → ℕ} {state challengeCiphertext : α → List Bool} (hn : Turing.MultiTapeTM.ComputableTidilyInPolyTime n input Turing.MultiTapeTM.encUnary) (hstate : Turing.MultiTapeTM.ComputableTidilyInPolyTime state input Turing.MultiTapeTM.encBits) (hchallenge : Turing.MultiTapeTM.ComputableTidilyInPolyTime challengeCiphertext input Turing.MultiTapeTM.encBits) : Probability.IsPPTOn input Turing.MultiTapeTM.encBool fun (a : α) => E.guessLink test (n a) (state a) (challengeCiphertext a)

The guessing stage is native strict PPT on every saved string, including malformed ones.

theorem Cslib.Crypto.Homomorphic.Scheme.isPPT_linkAdversaryAt {E : Scheme} (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) {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) {beforeCount afterCount bitIndex : ℕ → ℕ} (hbefore : Turing.MultiTapeTM.ComputableTidilyInPolyTime beforeCount Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hafter : Turing.MultiTapeTM.ComputableTidilyInPolyTime afterCount Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hindex : Turing.MultiTapeTM.ComputableTidilyInPolyTime bitIndex Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) : (E.linkAdversaryAt beforeCount afterCount bitIndex test).IsPPT

Efficient unary index families give one admissible chosen-message adversary.

theorem Cslib.Crypto.Homomorphic.Scheme.isPPT_linkAdversary {E : Scheme} (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) {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) {depth capacity : ℕ → ℕ} (hdepth : Turing.MultiTapeTM.ComputableTidilyInPolyTime depth Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hcapacity : Turing.MultiTapeTM.ComputableTidilyInPolyTime capacity Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) : (E.linkAdversary depth capacity test).IsPPT

Uniform dyadic link and bit selection remains strict PPT, including rejected padding.