Abstract Public-Key Encryption Scheme and CPA Games

This file defines an abstract public-key encryption (PKE) scheme and the CPA$ security games, following the framework from "Mechanizing Nested Hybrid Arguments" (Larsen & Schurmann, CSF 2025, Fig. 5).

Overview

The CPA$ game (ciphertext indistinguishability) has two variants:

• Real (b = true): Encrypt the queried message
• Ideal (b = false): Return a random ciphertext

This is equivalent to the standard IND-CPA definition but more convenient for hybrid arguments, as each encryption query can be independently switched.

Main Definitions

• PKEScheme - Abstract PKE scheme record
• OT_CPA_real / OT_CPA_ideal - One-time CPA$ games (single query)
• OT_CPA_Advantage - One-time CPA$ advantage
• MT_CPA_real / MT_CPA_ideal - Many-time CPA$ games (q queries)
• hybrid_game - Hybrid game indexed by switch position
• MT_CPA_bound - Main reduction: MT-CPA advantage ≤ q * OT-CPA advantage

References

• [Larsen & Schurmann, Mechanizing Nested Hybrid Arguments, CSF 2025, Fig. 5-9]
• [Bellare et al., Relations Among Notions of Security for PKE]

PKE Scheme Definition

structure CatCrypt.Examples.PKE.PKEScheme : Type 1

Abstract public-key encryption scheme.

Following the CSF 2025 paper (Fig. 5):

• keygen produces a (secret key, public key) pair
• enc encrypts a message under a public key (probabilistic)
• dec decrypts a ciphertext under a secret key
• sampleCip samples a random ciphertext (for the ideal CPA$ game)

• SK : Type

  Secret key type

• PK : Type

  Public key type

• M : Type

  Message type

• C : Type

  Ciphertext type

• finSK : Fintype self.SK

  Secret keys are finite

• neSK : Nonempty self.SK

  Secret keys are nonempty

• finPK : Fintype self.PK

  Public keys are finite

• nePK : Nonempty self.PK

  Public keys are nonempty

• finM : Fintype self.M

  Messages are finite

• neM : Nonempty self.M

  Messages are nonempty

• finC : Fintype self.C

  Ciphertexts are finite

• neC : Nonempty self.C

  Ciphertexts are nonempty

• keygen : Core.SPComp (self.SK × self.PK)

  Probabilistic key generation

• enc : self.PK → self.M → Core.SPComp self.C

  Probabilistic encryption

• dec : self.SK → self.C → Core.SPComp (Option self.M)

  Decryption (may fail)

• sampleCip : Core.SPComp self.C

  Random ciphertext sampling (for CPA$ ideal game)

Correctness

def CatCrypt.Examples.PKE.PKEScheme.Correct (P : PKEScheme) : Prop

Perfect correctness: decryption always recovers the message.

Equations

• One or more equations did not get rendered due to their size.

One-Time CPA$ Games

noncomputable def CatCrypt.Examples.PKE.OT_CPA_real (P : PKEScheme) (pk : P.PK) (m : P.M) : Core.SPComp P.C

One-time CPA$ real game: encrypt the message under the public key.

Equations

• CatCrypt.Examples.PKE.OT_CPA_real P pk m = P.enc pk m

noncomputable def CatCrypt.Examples.PKE.OT_CPA_ideal (P : PKEScheme) (_pk : P.PK) (_m : P.M) : Core.SPComp P.C

One-time CPA$ ideal game: return a random ciphertext.

Equations

• CatCrypt.Examples.PKE.OT_CPA_ideal P _pk _m = P.sampleCip

noncomputable def CatCrypt.Examples.PKE.OT_CPA_Advantage (P : PKEScheme) (pk : P.PK) (m : P.M) (A : P.C → Core.SPComp Bool) : ENNReal

One-time CPA$ advantage for a fixed public key and message.

Equations

• CatCrypt.Examples.PKE.OT_CPA_Advantage P pk m A = CatCrypt.Crypto.AdvantageA (CatCrypt.Examples.PKE.OT_CPA_real P pk m) (CatCrypt.Examples.PKE.OT_CPA_ideal P pk m) A

Hybrid Games (SLIDE Construction)

The hybrid game at index `i` samples random ciphertexts for positions `< i`
and encrypts the real message for positions `≥ i`. This is the SLIDE construction
from the CSF 2025 paper (Fig. 9).

We define this recursively with an explicit position counter. 

noncomputable def CatCrypt.Examples.PKE.hybridLoop (P : PKEScheme) (pk : P.PK) (i : ℕ) : ℕ → List P.M → Core.SPComp (List P.C)

Helper: process messages with position counter. For position j: if j < i then sample random, else encrypt.

Equations

• One or more equations did not get rendered due to their size.
• CatCrypt.Examples.PKE.hybridLoop P pk i x✝ [] = CatCrypt.Core.SPComp.pure []

noncomputable def CatCrypt.Examples.PKE.hybrid_game (P : PKEScheme) (pk : P.PK) (msgs : List P.M) (i : ℕ) : Core.SPComp (List P.C)

Hybrid game: first i ciphertexts are random, remaining are encrypted.

• hybrid_game pk msgs 0 = all encrypted (real game)
• hybrid_game pk msgs msgs.length = all random (ideal game)

Equations

• CatCrypt.Examples.PKE.hybrid_game P pk msgs i = CatCrypt.Examples.PKE.hybridLoop P pk i 0 msgs

Many-Time CPA$ Games

The many-time game allows `q` encryption queries (one per message in the list).
These are defined recursively to match `hybridLoop`'s structure. 

noncomputable def CatCrypt.Examples.PKE.MT_CPA_real (P : PKEScheme) (pk : P.PK) : List P.M → Core.SPComp (List P.C)

Many-time CPA$ real game: encrypt all messages under the public key.

Equations

• CatCrypt.Examples.PKE.MT_CPA_real P pk [] = CatCrypt.Core.SPComp.pure []
• CatCrypt.Examples.PKE.MT_CPA_real P pk (m :: ms) = do let c ← P.enc pk m let cs ← CatCrypt.Examples.PKE.MT_CPA_real P pk ms CatCrypt.Core.SPComp.pure (c :: cs)

noncomputable def CatCrypt.Examples.PKE.MT_CPA_ideal (P : PKEScheme) : List P.M → Core.SPComp (List P.C)

Many-time CPA$ ideal game: return random ciphertexts for all queries.

Equations

• CatCrypt.Examples.PKE.MT_CPA_ideal P [] = CatCrypt.Core.SPComp.pure []
• CatCrypt.Examples.PKE.MT_CPA_ideal P (m :: ms) = do let c ← P.sampleCip let cs ← CatCrypt.Examples.PKE.MT_CPA_ideal P ms CatCrypt.Core.SPComp.pure (c :: cs)

noncomputable def CatCrypt.Examples.PKE.MT_CPA_Advantage (P : PKEScheme) (pk : P.PK) (msgs : List P.M) (A : List P.C → Core.SPComp Bool) : ENNReal

Many-time CPA$ advantage.

Equations

• CatCrypt.Examples.PKE.MT_CPA_Advantage P pk msgs A = CatCrypt.Crypto.AdvantageA (CatCrypt.Examples.PKE.MT_CPA_real P pk msgs) (CatCrypt.Examples.PKE.MT_CPA_ideal P msgs) A

Boundary Conditions

theorem CatCrypt.Examples.PKE.hybridLoop_zero_eq_real (P : PKEScheme) (pk : P.PK) (j : ℕ) (msgs : List P.M) : hybridLoop P pk 0 j msgs = MT_CPA_real P pk msgs

Helper: hybridLoop with threshold 0 equals MT_CPA_real.

theorem CatCrypt.Examples.PKE.hybrid_game_zero (P : PKEScheme) (pk : P.PK) (msgs : List P.M) : hybrid_game P pk msgs 0 = MT_CPA_real P pk msgs

Boundary: hybrid at 0 = all encrypted (real game).

theorem CatCrypt.Examples.PKE.hybridLoop_length_eq_ideal (P : PKEScheme) (pk : P.PK) (j : ℕ) (msgs : List P.M) : hybridLoop P pk (j + msgs.length) j msgs = MT_CPA_ideal P msgs

Helper: hybridLoop at full length equals MT_CPA_ideal.

theorem CatCrypt.Examples.PKE.hybrid_game_length (P : PKEScheme) (pk : P.PK) (msgs : List P.M) : hybrid_game P pk msgs msgs.length = MT_CPA_ideal P msgs

Boundary: hybrid at length = all random (ideal game).

Adjacent Hybrid Lemmas

Key structural lemma: adjacent hybrids differ only at position i.

For positions `j < i`: both games sample random (identical).
For position `j = i`: game i encrypts, game i+1 samples random.
For positions `j > i`: both games encrypt (identical).

This means the advantage between adjacent hybrids reduces to a single
OT-CPA$ query at position i. 

theorem CatCrypt.Examples.PKE.hybridLoop_agree_prefix (P : PKEScheme) (pk : P.PK) (i j : ℕ) (msgs : List P.M) (hj : j + msgs.length ≤ i) : hybridLoop P pk i j msgs = hybridLoop P pk (i + 1) j msgs

Helper: hybridLoop agrees on positions where the condition is the same.

theorem CatCrypt.Examples.PKE.hybridLoop_agree_suffix (P : PKEScheme) (pk : P.PK) (i j : ℕ) (msgs : List P.M) (hj : i < j) : hybridLoop P pk i j msgs = hybridLoop P pk (i + 1) j msgs

Helper: hybridLoop agrees on positions after the switch point.

Pure PKE Schemes

structure CatCrypt.Examples.PKE.PKEScheme.IsPure (P : PKEScheme) : Prop

A PKE scheme is pure if its encryption and random ciphertext sampling don't depend on or modify the heap.

• enc_isPure (pk : P.PK) (m : P.M) : (P.enc pk m).IsPure
• sampleCip_isPure : P.sampleCip.IsPure

IsPure for Many-Time Games

theorem CatCrypt.Examples.PKE.MT_CPA_real_isPure (P : PKEScheme) (hP : P.IsPure) (pk : P.PK) (msgs : List P.M) : (MT_CPA_real P pk msgs).IsPure

Many-time CPA$ real game is pure when the scheme is pure.

theorem CatCrypt.Examples.PKE.MT_CPA_ideal_isPure (P : PKEScheme) (hP : P.IsPure) (msgs : List P.M) : (MT_CPA_ideal P msgs).IsPure

Many-time CPA$ ideal game is pure when the scheme is pure.

theorem CatCrypt.Examples.PKE.hybridLoop_isPure (P : PKEScheme) (hP : P.IsPure) (pk : P.PK) (i j : ℕ) (msgs : List P.M) : (hybridLoop P pk i j msgs).IsPure

The hybrid game is pure when the scheme is pure.

theorem CatCrypt.Examples.PKE.hybrid_game_isPure (P : PKEScheme) (hP : P.IsPure) (pk : P.PK) (msgs : List P.M) (i : ℕ) : (hybrid_game P pk msgs i).IsPure

Main Reduction Theorem

theorem CatCrypt.Examples.PKE.MT_CPA_bound (P : PKEScheme) (pk : P.PK) (msgs : List P.M) (A : List P.C → Core.SPComp Bool) (ε : ENNReal) (hstep : ∀ i < msgs.length, Crypto.AdvantageA (hybrid_game P pk msgs i) (hybrid_game P pk msgs (i + 1)) A ≤ ε) : MT_CPA_Advantage P pk msgs A ≤ ↑msgs.length * ε

Many-time to one-time CPA$ reduction (CSF 2025, Theorem 1).

The many-time CPA$ advantage is bounded by q * ε where q = msgs.length and ε bounds each per-step hybrid advantage.

This uses the general advantage_hybrid_uniform theorem from HybridArgument.lean.

theorem CatCrypt.Examples.PKE.MT_CPA_dep_bound (P : PKEScheme) (pk : P.PK) (msgs : List P.M) (A : List P.C → Core.SPComp Bool) (ε : ℕ → ENNReal) (hstep : ∀ i < msgs.length, Crypto.AdvantageA (hybrid_game P pk msgs i) (hybrid_game P pk msgs (i + 1)) A ≤ ε i) : MT_CPA_Advantage P pk msgs A ≤ ∑ i ∈ Finset.range msgs.length, ε i

Many-time to one-time CPA$ reduction with dependent bounds.

When per-step bounds differ, the total advantage is bounded by their sum.

theorem CatCrypt.Examples.PKE.MT_CPA_perfect (P : PKEScheme) (pk : P.PK) (msgs : List P.M) (hperf : ∀ i < msgs.length, Relational.rHoare Relational.eqPre (hybrid_game P pk msgs i) (hybrid_game P pk msgs (i + 1)) Relational.eqPost) (A : List P.C → Core.SPComp Bool) : MT_CPA_Advantage P pk msgs A = 0

Perfect security for many-time CPA$: when all hybrid steps are perfectly indistinguishable, the many-time advantage is 0.