Homomorphic refresh from decryption circuits

Gentry's refresh algorithm encrypts the public bits of an old ciphertext and evaluates a decryption circuit using those encryptions and an encrypted old secret key. Connecting two decryption circuits to NAND derives a homomorphic NAND operation [Gentry2009, Section 2].

The old ciphertexts need only have the declared width: they may be outputs of earlier homomorphic evaluations. The base evaluation guarantee applies because its immediate inputs are fresh encryptions of bits. The two copies of the encrypted secret key may be identical.

Bootstrappable asserts membership of the actual circuits in the permitted set. Refresh is constructed below, and its correctness is proved rather than bundled into that assumption. These results establish functional correctness and fixed output width. They do not yet establish uniform polynomial running time, a leveled evaluator, IND-CPA security, or fixed-key FHE.

Main definitions

• Cslib.Crypto.Homomorphic.DecryptionCircuits: circuits computing the base decryption algorithm.
• Cslib.Crypto.Homomorphic.Scheme.Bootstrappable: permitted decryption and NAND augmentations.
• Cslib.Crypto.Homomorphic.Scheme.refresh, .refreshNand: explicit probabilistic programs.

Main results

• Cslib.Crypto.Homomorphic.Scheme.decrypt_refresh: refresh preserves the decrypted bit.
• Cslib.Crypto.Homomorphic.Scheme.decrypt_refreshNand: NAND refresh computes NAND of decrypted bits, including for old ciphertexts outside the support of fresh encryption.
• Cslib.Crypto.Homomorphic.Scheme.length_refresh, .length_refreshNand: refreshed ciphertexts have the same width as base ciphertexts, independent of prior evaluation depth.

References

• C. Gentry, Fully homomorphic encryption using ideal lattices

structure Cslib.Crypto.Homomorphic.DecryptionCircuits (E : Scheme) (secretWidth ciphertextWidth : ℕ → ℕ) : Type

Actual circuits computing decryption on the specified fixed-width inputs. Existence alone does not certify uniform circuit generation; that is a separate computational obligation.

• circuit (n : ℕ) : Circuits.Circuit Circuits.Boolean.signature (secretWidth n + ciphertextWidth n) 1

  Secret-key bits precede ciphertext bits.

• correct (n : ℕ) (sk c : List Bool) : sk.length = secretWidth n → c.length = ciphertextWidth n → (self.circuit n).eval Circuits.Boolean.interpretation (BitString.ofList (secretWidth n + ciphertextWidth n) (sk ++ c)) 0 = E.decrypt n sk c

  The circuit computes decryption on all well-sized keys and ciphertexts, including outputs of earlier homomorphic evaluations.

structure Cslib.Crypto.Homomorphic.Scheme.Bootstrappable {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) : Prop

Gentry's permitted-circuit condition for identity and NAND augmentations. This condition does not postulate a refresh algorithm or a correctness theorem for one.

• decrypt_mem (n : ℕ) : E.permitted n ⟨secretWidth n + ciphertextWidth n, D.circuit n⟩

  The identity augmentation is the decryption circuit itself.

• nand_mem (n : ℕ) : E.permitted n ⟨secretWidth n + ciphertextWidth n + (secretWidth n + ciphertextWidth n), augmentNand (D.circuit n)⟩

  NAND of two decryptions is permitted by the base evaluator.

def Cslib.Crypto.Homomorphic.Scheme.refresh {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (n : ℕ) (pk : List Bool) (encryptedKey : List (List Bool)) (ciphertext : List Bool) : ProbComp (List Bool)

Refresh an old ciphertext using its public bits and an encrypted old secret key.

def Cslib.Crypto.Homomorphic.Scheme.refreshNand {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (n : ℕ) (pk : List Bool) (encryptedKey : List (List Bool)) (first second : List Bool) : ProbComp (List Bool)

Refresh and NAND two old ciphertexts. The same encrypted secret key is used in both blocks.

theorem Cslib.Crypto.Homomorphic.Scheme.decrypt_refresh {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (hE : E.Correct) (hD : Bootstrappable D) (n : ℕ) (keys : List Bool × List Bool) (hkeys : keys ∈ (E.keyGen n).eval.support) (sk ciphertext : List Bool) (hsk : sk.length = secretWidth n) (hc : ciphertext.length = ciphertextWidth n) (encryptedKey : List (List Bool)) (hek : E.FreshInputs n keys.1 sk encryptedKey) (result : List Bool) (hresult : result ∈ (refresh D n keys.1 encryptedKey ciphertext).eval.support) : E.decrypt n keys.2 result = E.decrypt n sk ciphertext

Refresh preserves decryption of every well-sized old ciphertext, whether fresh or evaluated.

theorem Cslib.Crypto.Homomorphic.Scheme.decrypt_refreshNand {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (hE : E.Correct) (hD : Bootstrappable D) (n : ℕ) (keys : List Bool × List Bool) (hkeys : keys ∈ (E.keyGen n).eval.support) (sk first second : List Bool) (hsk : sk.length = secretWidth n) (hfirst : first.length = ciphertextWidth n) (hsecond : second.length = ciphertextWidth n) (encryptedKey : List (List Bool)) (hek : E.FreshInputs n keys.1 sk encryptedKey) (result : List Bool) (hresult : result ∈ (refreshNand D n keys.1 encryptedKey first second).eval.support) : E.decrypt n keys.2 result = !(E.decrypt n sk first && E.decrypt n sk second)

NAND refresh computes NAND of the old decryptions. No fresh-encryption hypothesis is needed for either old ciphertext, and the encrypted secret key is shared between the two input blocks.

theorem Cslib.Crypto.Homomorphic.Scheme.length_refresh {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (hE : E.FixedWidth secretWidth ciphertextWidth) (hD : Bootstrappable D) (n : ℕ) (keys : List Bool × List Bool) (hkeys : keys ∈ (E.keyGen n).eval.support) (sk ciphertext : List Bool) (hsk : sk.length = secretWidth n) (hc : ciphertext.length = ciphertextWidth n) (encryptedKey : List (List Bool)) (hek : E.FreshInputs n keys.1 sk encryptedKey) (result : List Bool) (hresult : result ∈ (refresh D n keys.1 encryptedKey ciphertext).eval.support) : result.length = ciphertextWidth n

Refresh has the same output width as the base scheme.

theorem Cslib.Crypto.Homomorphic.Scheme.length_refreshNand {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (hE : E.FixedWidth secretWidth ciphertextWidth) (hD : Bootstrappable D) (n : ℕ) (keys : List Bool × List Bool) (hkeys : keys ∈ (E.keyGen n).eval.support) (sk first second : List Bool) (hsk : sk.length = secretWidth n) (hfirst : first.length = ciphertextWidth n) (hsecond : second.length = ciphertextWidth n) (encryptedKey : List (List Bool)) (hek : E.FreshInputs n keys.1 sk encryptedKey) (result : List Bool) (hresult : result ∈ (refreshNand D n keys.1 encryptedKey first second).eval.support) : result.length = ciphertextWidth n

NAND refresh has the same output width as the base scheme, independent of prior depth.