Native runtime of encrypted-key chain hybrids

The actual hybrid samplers charge every public and private key supplied as input, every bit encryption, and their full nested output. Counters are unary. These certificates require only the native key-generation and encryption certificates, with no correctness, fixed-width or security assumptions.

Main results

• Cslib.Crypto.Homomorphic.Scheme.isPPTOn_encryptZeroKeyLinks: encrypt zero words of the supplied secret keys' actual lengths.
• Cslib.Crypto.Homomorphic.Scheme.isPPTOn_encryptKeyLinksHybrid: sample the real prefix and zero suffix.
• Cslib.Crypto.Homomorphic.Scheme.isPPTOn_publicKeyChainHybrid: generate keys and return only the public keys and hybrid links.
• Cslib.Crypto.Homomorphic.Scheme.isPPTOn_encryptKeyLinkHybrid: refine the boundary link one bit at a time while sampling both surrounding link segments.
• Cslib.Crypto.Homomorphic.Scheme.isPPTOn_spliceEncryptedKeyLink: insert a supplied ciphertext into the boundary link while sampling the surrounding bits and links.

References

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

theorem Cslib.Crypto.Homomorphic.Scheme.isPPTOn_encryptZeroKeyLinks {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) {α : Type} {input : α ↪ List Bool} {n : α → ℕ} {keys : α → List (List Bool × List Bool)} (hn : Turing.MultiTapeTM.ComputableTidilyInPolyTime n input Turing.MultiTapeTM.encUnary) (hkeys : Turing.MultiTapeTM.ComputableTidilyInPolyTime keys input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits))) : Probability.IsPPTOn input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) fun (a : α) => E.encryptZeroKeyLinks (n a) (keys a)

Encrypt every zero link, using the actual length of each supplied secret key.

theorem Cslib.Crypto.Homomorphic.Scheme.isPPTOn_encryptKeyLinksHybrid {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) {α : Type} {input : α ↪ List Bool} {n cut : α → ℕ} {keys : α → List (List Bool × List Bool)} (hn : Turing.MultiTapeTM.ComputableTidilyInPolyTime n input Turing.MultiTapeTM.encUnary) (hcut : Turing.MultiTapeTM.ComputableTidilyInPolyTime cut input Turing.MultiTapeTM.encUnary) (hkeys : Turing.MultiTapeTM.ComputableTidilyInPolyTime keys input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits))) : Probability.IsPPTOn input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) fun (a : α) => E.encryptKeyLinksHybrid (n a) (cut a) (keys a)

Sample the actual real-prefix/zero-suffix hybrid for every unary boundary, including boundaries beyond the supplied list.

theorem Cslib.Crypto.Homomorphic.Scheme.isPPTOn_publicKeyChainHybrid {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) {α : Type} {input : α ↪ List Bool} {n depth cut : α → ℕ} (hn : Turing.MultiTapeTM.ComputableTidilyInPolyTime n input Turing.MultiTapeTM.encUnary) (hdepth : Turing.MultiTapeTM.ComputableTidilyInPolyTime depth input Turing.MultiTapeTM.encUnary) (hcut : Turing.MultiTapeTM.ComputableTidilyInPolyTime cut input Turing.MultiTapeTM.encUnary) : Probability.IsPPTOn input (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits))) fun (a : α) => E.publicKeyChainHybrid (n a) (depth a) (cut a)

Generate independent keys and hybrid links, charging the full public artifact.

theorem Cslib.Crypto.Homomorphic.Scheme.isPPTOn_encryptKeyLinkHybrid {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) {α : Type} {input : α ↪ List Bool} {n cut : α → ℕ} {before after : α → List (List Bool × List Bool)} {predecessor next : α → List Bool × List Bool} (hn : Turing.MultiTapeTM.ComputableTidilyInPolyTime n input Turing.MultiTapeTM.encUnary) (hbefore : Turing.MultiTapeTM.ComputableTidilyInPolyTime before input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits))) (hpredecessor : Turing.MultiTapeTM.ComputableTidilyInPolyTime predecessor input (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) (hnext : Turing.MultiTapeTM.ComputableTidilyInPolyTime next input (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) (hafter : Turing.MultiTapeTM.ComputableTidilyInPolyTime after input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits))) (hcut : Turing.MultiTapeTM.ComputableTidilyInPolyTime cut input Turing.MultiTapeTM.encUnary) : Probability.IsPPTOn input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) fun (a : α) => E.encryptKeyLinkHybrid (n a) (before a) (predecessor a) (next a) (after a) (cut a)

Refine one link's plaintext while sampling the real prefix and zero suffix.

theorem Cslib.Crypto.Homomorphic.Scheme.isPPTOn_spliceEncryptedKeyLink {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) {α : Type} {input : α ↪ List Bool} {n cut : α → ℕ} {before after : α → List (List Bool × List Bool)} {predecessor next : α → List Bool × List Bool} {challenge : α → List Bool} (hn : Turing.MultiTapeTM.ComputableTidilyInPolyTime n input Turing.MultiTapeTM.encUnary) (hbefore : Turing.MultiTapeTM.ComputableTidilyInPolyTime before input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits))) (hpredecessor : Turing.MultiTapeTM.ComputableTidilyInPolyTime predecessor input (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) (hnext : Turing.MultiTapeTM.ComputableTidilyInPolyTime next input (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) (hafter : Turing.MultiTapeTM.ComputableTidilyInPolyTime after input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits))) (hcut : Turing.MultiTapeTM.ComputableTidilyInPolyTime cut input Turing.MultiTapeTM.encUnary) (hchallenge : Turing.MultiTapeTM.ComputableTidilyInPolyTime challenge input Turing.MultiTapeTM.encBits) : Probability.IsPPTOn input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) fun (a : α) => E.spliceEncryptedKeyLink (n a) (before a) (predecessor a) (next a) (after a) (cut a) (challenge a)

Insert the full challenge ciphertext into the actual boundary-link simulation.