Homomorphic encryption on bit strings

This module records the algorithms and perfect correctness of bit-encryption schemes with a specified family of permitted Boolean circuits, following [Gentry2009, Definitions 1 and 5]. Algorithms are terminating probabilistic programs. Uniform efficiency and semantic security are separate obligations; neither follows from this interface or its correctness property.

Homomorphic correctness is required on pointwise supported fresh encryptions. Inputs may share randomness or repeat a ciphertext, as happens when the same encrypted secret key is used twice in an augmented decryption circuit. No independence hypothesis is imposed on these inputs.

Scheme.FixedWidth describes a padded representation whose ciphertext width depends only on the security parameter. It asserts a representation bound, not that the width is polynomial.

Main definitions

• Cslib.Crypto.Homomorphic.Scheme: encryption algorithms and permitted circuits.
• Cslib.Crypto.Homomorphic.Scheme.FreshInputs: matching plaintexts and fresh ciphertexts.
• Cslib.Crypto.Homomorphic.Scheme.Correct: perfect encryption and evaluation correctness.
• Cslib.Crypto.Homomorphic.Scheme.FixedWidth: fixed secret-key and ciphertext widths.
• Cslib.Crypto.Homomorphic.Scheme.encryptBits: encrypt each bit of a public word.

Main results

• Cslib.Crypto.Homomorphic.Scheme.mem_support_encryptBits_iff: the exact support of bitwise encryption, including the empty word.

References

• C. Gentry, Fully homomorphic encryption using ideal lattices

structure Cslib.Crypto.Homomorphic.Scheme : Type

Algorithms of a bit-encryption scheme, with a unary security parameter. evaluate receives an actual Boolean circuit and an ordered list of ciphertexts. Correctness, uniform efficiency, and security are separate properties.

• keyGen : ℕ → ProbComp (List Bool × List Bool)

  Sample a public and secret key, in that order.

• encrypt : ℕ → List Bool → Bool → ProbComp (List Bool)

  Encrypt one bit under a public key.

• decrypt : ℕ → List Bool → List Bool → Bool

  Decrypt a ciphertext under a secret key.

• evaluate : ℕ → List Bool → (m : ℕ) × Circuits.Circuit Circuits.Boolean.signature m 1 → List (List Bool) → ProbComp (List Bool)

  Evaluate a circuit on encrypted inputs; malformed input lists are allowed but have no correctness guarantee.

• permitted : ℕ → (m : ℕ) × Circuits.Circuit Circuits.Boolean.signature m 1 → Prop

  Circuits for which homomorphic correctness is guaranteed at a security parameter.

def Cslib.Crypto.Homomorphic.Scheme.FreshInputs (E : Scheme) (n : ℕ) (pk bits : List Bool) (inputs : List (List Bool)) : Prop

Each ciphertext is a supported fresh encryption of the corresponding plaintext bit. The relation implies equal list lengths, and permits repeated ciphertexts.

structure Cslib.Crypto.Homomorphic.Scheme.Correct (E : Scheme) : Prop

Perfect correctness of encryption and evaluation of permitted circuits on fresh inputs. The evaluator need not accept its own outputs as inputs: bootstrapping will derive that closure.

• decrypt_encrypt (n : ℕ) (keys : List Bool × List Bool) : keys ∈ (E.keyGen n).eval.support → ∀ (b : Bool), ∀ c ∈ (E.encrypt n keys.1 b).eval.support, E.decrypt n keys.2 c = b

  Fresh ciphertexts decrypt to the encrypted bit under every supported key pair.

• decrypt_evaluate (n : ℕ) (keys : List Bool × List Bool) : keys ∈ (E.keyGen n).eval.support → ∀ (C : (m : ℕ) × Circuits.Circuit Circuits.Boolean.signature m 1), E.permitted n C → ∀ (bits : List Bool) (inputs : List (List Bool)), bits.length = C.fst → E.FreshInputs n keys.1 bits inputs → ∀ c ∈ (E.evaluate n keys.1 C inputs).eval.support, E.decrypt n keys.2 c = C.snd.eval Circuits.Boolean.interpretation (BitString.ofList C.fst bits) 0

  Permitted circuits evaluate correctly on any pointwise supported fresh encryptions.

structure Cslib.Crypto.Homomorphic.Scheme.FixedWidth (E : Scheme) (secretWidth ciphertextWidth : ℕ → ℕ) : Prop

A fixed-width representation for supported keys and ciphertexts. Both fresh encryption and evaluation outputs have the same width, independent of circuit size and evaluation depth. Polynomial bounds on these width functions are a separate efficiency obligation.

• secret_length (n : ℕ) (keys : List Bool × List Bool) : keys ∈ (E.keyGen n).eval.support → keys.2.length = secretWidth n

  Supported secret keys have the stated width.

• encrypt_length (n : ℕ) (keys : List Bool × List Bool) : keys ∈ (E.keyGen n).eval.support → ∀ (b : Bool), ∀ c ∈ (E.encrypt n keys.1 b).eval.support, c.length = ciphertextWidth n

  Supported fresh encryptions have the stated ciphertext width.

• evaluate_length (n : ℕ) (keys : List Bool × List Bool) : keys ∈ (E.keyGen n).eval.support → ∀ (C : (m : ℕ) × Circuits.Circuit Circuits.Boolean.signature m 1), E.permitted n C → ∀ (bits : List Bool) (inputs : List (List Bool)), bits.length = C.fst → E.FreshInputs n keys.1 bits inputs → ∀ c ∈ (E.evaluate n keys.1 C inputs).eval.support, c.length = ciphertextWidth n

  The base evaluator returns the same ciphertext width, even after a nontrivial circuit.

def Cslib.Crypto.Homomorphic.Scheme.encryptBits (E : Scheme) (n : ℕ) (pk bits : List Bool) : ProbComp (List (List Bool))

Encrypt every bit of a public word using a fresh call to the base encryption algorithm.

theorem Cslib.Crypto.Homomorphic.Scheme.mem_support_encryptBits_iff (E : Scheme) (n : ℕ) (pk bits : List Bool) (inputs : List (List Bool)) : inputs ∈ (E.encryptBits n pk bits).eval.support ↔ E.FreshInputs n pk bits inputs

Bitwise encryption has exactly the pointwise fresh-encryption support.