Bitwise encryption hybrids

Replace an initial segment of a word by zeros before encrypting its bits. A simulator samples the surrounding ciphertexts and inserts one challenge ciphertext at the selected coordinate. The exact distributional identities retain every other ciphertext and its independent encryption randomness. They also apply inside a larger randomized context.

Main definitions

• Cslib.Crypto.Homomorphic.Scheme.encryptBitsHybrid: encrypt a word with a zero prefix.
• Cslib.Crypto.Homomorphic.Scheme.spliceEncryptedBit: insert a bit-encryption challenge.

Main results

• Cslib.Crypto.Homomorphic.Scheme.eval_spliceEncryptedBit_original: the original bit gives the earlier adjacent hybrid.
• Cslib.Crypto.Homomorphic.Scheme.eval_spliceEncryptedBit_zero: a zero bit gives the next adjacent hybrid.

References

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

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

Encrypt a word after replacing its first cut bits by zeros. The word's length is preserved even when the requested cut is beyond its end.

def Cslib.Crypto.Homomorphic.Scheme.spliceEncryptedBit (E : Scheme) (n : ℕ) (pk : List Bool) (before : ℕ) (after challenge : List Bool) : ProbComp (List (List Bool))

Encrypt the zero prefix and the original suffix, inserting the supplied ciphertext between them. The challenge is already encrypted and is not encrypted again.

@[simp]

theorem Cslib.Crypto.Homomorphic.Scheme.encryptBitsHybrid_zero (E : Scheme) (n : ℕ) (pk bits : List Bool) : E.encryptBitsHybrid n pk bits 0 = E.encryptBits n pk bits

The initial bit hybrid is the actual bitwise encryption sampler.

theorem Cslib.Crypto.Homomorphic.Scheme.encryptBitsHybrid_length (E : Scheme) (n : ℕ) (pk bits : List Bool) : E.encryptBitsHybrid n pk bits bits.length = E.encryptBits n pk (List.replicate bits.length false)

The final bit hybrid encrypts an equal-length zero word.

theorem Cslib.Crypto.Homomorphic.Scheme.eval_spliceEncryptedBit_original (E : Scheme) (n : ℕ) (pk bits : List Bool) (cut : ℕ) (hcut : cut < bits.length) : (do let challenge ← E.encrypt n pk (bits.getD cut false) E.spliceEncryptedBit n pk cut (List.drop (cut + 1) bits) challenge).eval = (E.encryptBitsHybrid n pk bits cut).eval

An encryption of the selected original bit supplies the earlier adjacent hybrid.

theorem Cslib.Crypto.Homomorphic.Scheme.eval_spliceEncryptedBit_zero (E : Scheme) (n : ℕ) (pk bits : List Bool) (cut : ℕ) (hcut : cut < bits.length) : (do let challenge ← E.encrypt n pk false E.spliceEncryptedBit n pk cut (List.drop (cut + 1) bits) challenge).eval = (E.encryptBitsHybrid n pk bits (cut + 1)).eval

An encryption of zero supplies the next adjacent hybrid.