A single-key circular-security assumption

The public experiment samples one key pair and encrypts every secret-key bit under its own public key, or encrypts the same number of zero bits. The complete vector and public key are jointly visible. CircularSecure asserts computational indistinguishability of these two serialized experiments against uniform native strict PPT tests.

For fixed supported secret width, this is a one-key, bitwise specialization of the real-versus-zero KDM experiment of [Boneh, Halevi, Hamburg and Ostrovsky, Section 2.1] [BHHO08]. The definition also permits varying supported lengths, in which case the public vector reveals that length. It does not assert general adaptive KDM security. Ordinary chosen-message security is a separate premise; neither definition mentions a derived homomorphic scheme. The single public sample can be reused by efficient computations without assuming independent copies of its contents.

Main definitions

• Cslib.Crypto.Encryption.encCircularPublicKey: a public key and its encrypted secret vector.
• Cslib.Crypto.Encryption.circularPublicKey: the actual self-encryption or zero experiment.
• Cslib.Crypto.Encryption.CircularSecure: joint one-key self-encryption indistinguishability.

References

• D. Boneh, S. Halevi, M. Hamburg, R. Ostrovsky, Circular-Secure Encryption from Decision Diffie-Hellman, Section 2.1.
• C. Gentry, Fully homomorphic encryption using ideal lattices, Section 2.

def Cslib.Crypto.Encryption.encCircularPublicKey : List Bool × List (List Bool) ↪ List Bool

Encode the public key and the complete vector of encrypted key bits, with no plaintext secret component.

def Cslib.Crypto.Encryption.circularPublicKey (keyGen : ℕ → ProbComp (List Bool × List Bool)) (encrypt : ℕ → List Bool → Bool → ProbComp (List Bool)) (real : Bool) (n : ℕ) : ProbComp (List Bool × List (List Bool))

Sample one key pair, then independently encrypt either every secret bit or equally many zero bits under that same public key. The result retains their full joint distribution.

def Cslib.Crypto.Encryption.CircularSecure (keyGen : ℕ → ProbComp (List Bool × List Bool)) (encrypt : ℕ → List Bool → Bool → ProbComp (List Bool)) : Prop

The complete self-encryption vector is indistinguishable from equal-length zero encryptions, jointly with its public key. This is an explicit additional assumption, not a consequence of ordinary IND-CPA and not a security claim about a constructed output scheme.