Uniform polynomial-time homomorphic refresh

Strict PPT encryption and evaluation, together with a uniform polynomial-time generator for actual decryption circuits, suffice to implement refresh and NAND refresh in strict PPT. The certificates charge the full encodings of the public key, encrypted secret key, ciphertexts, and generated circuits. In particular, the NAND augmentation is constructed by a certified code transformation rather than supplied as an independently assumed efficient operation.

These are computation certificates for Gentry's refresh construction [Gentry2009, Section 2]. They do not establish security or a leveled evaluator. Correctness and fixed output width have separate hypotheses and are proved in Homomorphic.Refresh.

Main results

• Cslib.Crypto.Homomorphic.Scheme.isPPTOn_encryptBits: encrypt a computed list of bits.
• Cslib.Crypto.Homomorphic.Scheme.isPPTOn_refresh: uniform strict PPT refresh.
• Cslib.Crypto.Homomorphic.Scheme.isPPTOn_refreshNand: uniform strict PPT NAND refresh.

References

• C. Gentry, Fully homomorphic encryption using ideal lattices

theorem Cslib.Crypto.Homomorphic.Scheme.isPPTOn_encryptBits {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 : α → ℕ} {pk bits : α → List Bool} (hn : Turing.MultiTapeTM.ComputableTidilyInPolyTime n input Turing.MultiTapeTM.encUnary) (hpk : Turing.MultiTapeTM.ComputableTidilyInPolyTime pk input Turing.MultiTapeTM.encBits) (hbits : Turing.MultiTapeTM.ComputableTidilyInPolyTime bits input Turing.MultiTapeTM.encBits) : Probability.IsPPTOn input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits) fun (a : α) => E.encryptBits (n a) (pk a) (bits a)

Encrypt all bits of an efficiently computed word, charging repeated copies of the key.

theorem Cslib.Crypto.Homomorphic.Scheme.isPPTOn_refresh {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) (hevaluate : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair (Circuits.Boolean.encCircuit 1) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)))) Turing.MultiTapeTM.encBits fun (p : ℕ × List Bool × ((n : ℕ) × Circuits.Circuit Circuits.Boolean.signature n 1) × List (List Bool)) => E.evaluate p.1 p.2.1 p.2.2.1 p.2.2.2) {α : Type} {input : α ↪ List Bool} {n : α → ℕ} {pk bits : α → List Bool} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (hD : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (n : ℕ) => ⟨secretWidth n + ciphertextWidth n, D.circuit n⟩) Turing.MultiTapeTM.encUnary (Circuits.Boolean.encCircuit 1)) {encryptedKey : α → List (List Bool)} (hn : Turing.MultiTapeTM.ComputableTidilyInPolyTime n input Turing.MultiTapeTM.encUnary) (hpk : Turing.MultiTapeTM.ComputableTidilyInPolyTime pk input Turing.MultiTapeTM.encBits) (hek : Turing.MultiTapeTM.ComputableTidilyInPolyTime encryptedKey input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) (hc : Turing.MultiTapeTM.ComputableTidilyInPolyTime bits input Turing.MultiTapeTM.encBits) : Probability.IsPPTOn input Turing.MultiTapeTM.encBits fun (a : α) => refresh D (n a) (pk a) (encryptedKey a) (bits a)

Refresh is strict PPT from the base algorithm certificates and uniform decryption-circuit construction. No refresh algorithm or refresh runtime bound is assumed.

theorem Cslib.Crypto.Homomorphic.Scheme.isPPTOn_refreshNand {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) (hevaluate : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair (Circuits.Boolean.encCircuit 1) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)))) Turing.MultiTapeTM.encBits fun (p : ℕ × List Bool × ((n : ℕ) × Circuits.Circuit Circuits.Boolean.signature n 1) × List (List Bool)) => E.evaluate p.1 p.2.1 p.2.2.1 p.2.2.2) {α : Type} {input : α ↪ List Bool} {n : α → ℕ} {pk : α → List Bool} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (hD : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (n : ℕ) => ⟨secretWidth n + ciphertextWidth n, D.circuit n⟩) Turing.MultiTapeTM.encUnary (Circuits.Boolean.encCircuit 1)) {encryptedKey : α → List (List Bool)} {first second : α → List Bool} (hn : Turing.MultiTapeTM.ComputableTidilyInPolyTime n input Turing.MultiTapeTM.encUnary) (hpk : Turing.MultiTapeTM.ComputableTidilyInPolyTime pk input Turing.MultiTapeTM.encBits) (hek : Turing.MultiTapeTM.ComputableTidilyInPolyTime encryptedKey input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) (hfirst : Turing.MultiTapeTM.ComputableTidilyInPolyTime first input Turing.MultiTapeTM.encBits) (hsecond : Turing.MultiTapeTM.ComputableTidilyInPolyTime second input Turing.MultiTapeTM.encBits) : Probability.IsPPTOn input Turing.MultiTapeTM.encBits fun (a : α) => refreshNand D (n a) (pk a) (encryptedKey a) (first a) (second a)

NAND refresh is strict PPT. The certificate constructs the augmented circuit and charges both bit-encryption traversals and both copies of the encrypted secret key.