Security from a single self-encrypted key

The circular premise concerns the actual joint public artifact: one public key and the complete vector encrypting its own secret bits. Native public-artifact postprocessing lets an adversary choose its messages after seeing that artifact and retain its full saved state.

The proof replaces self-encryptions by zero encryptions in each challenge world, and reduces the middle comparison to ordinary base IND-CPA. The zero-world simulator obtains the fixed supported secret length from an independent key sample. No efficient width function, correctness or bootstrappability premise is needed for this security transfer.

Main results

• Cslib.Crypto.Homomorphic.FixedKey.negligible_publicKeyGame: replacing the self-encrypted public vector by zero encryptions changes either adaptive challenge world negligibly.
• Cslib.Crypto.Homomorphic.FixedKey.indCPA_scheme: the actual fixed-key scheme preserves IND-CPA under the explicit additional one-key circular premise.

References

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

theorem Cslib.Crypto.Homomorphic.FixedKey.eval_keyGen_public (E : Scheme) (n : ℕ) : PMF.map Prod.fst (keyGen E n).eval = PMF.map (⇑encPublicKey) (Encryption.circularPublicKey E.keyGen E.encrypt true n).eval

The actual public marginal is the serialized self-encryption experiment.

theorem Cslib.Crypto.Homomorphic.FixedKey.eval_game_keyGen (E : Scheme) (adversary : Encryption.Adversary) (bit : Bool) (n : ℕ) : (Encryption.game (keyGen E) (encrypt E) adversary bit n).eval = (Encryption.circularPublicKey E.keyGen E.encrypt true n >>= publicKeyGame E adversary bit n).eval

The actual scheme challenge is the real public artifact followed by adaptive message selection. The private secret component is never passed to the adversary.

theorem Cslib.Crypto.Homomorphic.FixedKey.publicKey_indistinguishable_zero {E : Scheme} (hcircular : Encryption.CircularSecure E.keyGen E.encrypt) : ComputationallyIndistinguishable (fun (n : ℕ) => PMF.map Prod.fst (keyGen E n).eval) fun (n : ℕ) => PMF.map (⇑encPublicKey) (Encryption.circularPublicKey E.keyGen E.encrypt false n).eval

The circular premise applies to the exact serialized public artifact of the construction.

theorem Cslib.Crypto.Homomorphic.FixedKey.negligible_publicKeyGame {E : Scheme} (hcircular : Encryption.CircularSecure E.keyGen E.encrypt) (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) {adversary : Encryption.Adversary} (hadversary : adversary.IsPPT) (bit : Bool) : Negligible fun (n : ℕ) => Game.advantage (Encryption.circularPublicKey E.keyGen E.encrypt true n >>= publicKeyGame E adversary bit n).eval (Encryption.circularPublicKey E.keyGen E.encrypt false n >>= publicKeyGame E adversary bit n).eval

The circular premise protects either adaptive chosen-message experiment. Honest encryption and both adversary stages are certified on their complete inputs.

theorem Cslib.Crypto.Homomorphic.FixedKey.indCPA_keyGen {E : Scheme} (hsecure : Encryption.INDCPA E.keyGen E.encrypt) (hcircular : Encryption.CircularSecure E.keyGen E.encrypt) (hkeyGen : Probability.IsPPTOn Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) E.keyGen) (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) {width : ℕ → ℕ} (hwidth : ∀ (n : ℕ), ∀ keys ∈ (E.keyGen n).eval.support, keys.2.length = width n) : Encryption.INDCPA (keyGen E) (encrypt E)

Self-encrypted evaluation keys preserve adaptive IND-CPA under ordinary base IND-CPA and the separate joint circular premise. Fixed supported secret length is semantic; the reduction learns it from an independent key sample and needs no computable width function.

theorem Cslib.Crypto.Homomorphic.FixedKey.indCPA_scheme {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (hsecure : Encryption.INDCPA E.keyGen E.encrypt) (hcircular : Encryption.CircularSecure E.keyGen E.encrypt) (hkeyGen : Probability.IsPPTOn Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) E.keyGen) (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) {width : ℕ → ℕ} (hwidth : ∀ (n : ℕ), ∀ keys ∈ (E.keyGen n).eval.support, keys.2.length = width n) : Encryption.INDCPA (scheme D).keyGen (scheme D).encrypt

The actual all-circuit fixed-key scheme is conditionally IND-CPA secure. The decryption family identifies the construction but contributes no security assumption.