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.ComputableInPolyTime n input Turing.MultiTapeTM.encUnary) (hkeys : Turing.MultiTapeTM.ComputableInPolyTime 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.ComputableInPolyTime n input Turing.MultiTapeTM.encUnary) (hcut : Turing.MultiTapeTM.ComputableInPolyTime cut input Turing.MultiTapeTM.encUnary) (hkeys : Turing.MultiTapeTM.ComputableInPolyTime 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.ComputableInPolyTime n input Turing.MultiTapeTM.encUnary) (hdepth : Turing.MultiTapeTM.ComputableInPolyTime depth input Turing.MultiTapeTM.encUnary) (hcut : Turing.MultiTapeTM.ComputableInPolyTime 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.ComputableInPolyTime n input Turing.MultiTapeTM.encUnary) (hbefore : Turing.MultiTapeTM.ComputableInPolyTime before input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits))) (hpredecessor : Turing.MultiTapeTM.ComputableInPolyTime predecessor input (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) (hnext : Turing.MultiTapeTM.ComputableInPolyTime next input (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) (hafter : Turing.MultiTapeTM.ComputableInPolyTime after input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits))) (hcut : Turing.MultiTapeTM.ComputableInPolyTime 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.ComputableInPolyTime n input Turing.MultiTapeTM.encUnary) (hbefore : Turing.MultiTapeTM.ComputableInPolyTime before input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits))) (hpredecessor : Turing.MultiTapeTM.ComputableInPolyTime predecessor input (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) (hnext : Turing.MultiTapeTM.ComputableInPolyTime next input (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) (hafter : Turing.MultiTapeTM.ComputableInPolyTime after input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits))) (hcut : Turing.MultiTapeTM.ComputableInPolyTime cut input Turing.MultiTapeTM.encUnary) (hchallenge : Turing.MultiTapeTM.ComputableInPolyTime 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.