CPA Security from a PRF: the Perfect Instantiation

The canonical construction of an IND-CPA-secure symmetric encryption scheme from a pseudorandom function. Following Rosulek, The Joy of Cryptography, §7 (CPA security).

Encrypt a message m as (r, F(k, r) ⊕ m) for a fresh uniform r: the keyed value F(k, r) acts as a one-time pad on m. Decryption recomputes F(k, r) from the transmitted r and un-pads. In the standard argument an IND-CPA distinguisher reduces to a PRF distinguisher, so the IND-CPA advantage is bounded by the PRF advantage.

The perfect instantiation

Instantiating the PRF by a bijection family — for each input r, a bijection bij r : Key ≃ Output — makes the underlying PRF perfect (CatCrypt.Examples.PRF, bijPRF_perfect): over a uniform key, F(k, r) = bij r k is uniform on Output. Consequently the pad F(k, r) ⊕ m is uniform regardless of m, and the two IND-CPA games (encrypting m₀ vs. m₁) are perfectly indistinguishable: the IND-CPA advantage of every adversary is exactly 0.

Overview

The security argument is the bijection-coupling technique of the one-time pad (CatCrypt.Examples.OTP), lifted through the fresh randomness r. First the two independent samples (key and randomness) are reordered so r is drawn first (SPComp.swap_sample_sample); then r is synchronized across the two games (rHoare_same_step); finally, at each fixed r, the key is coupled by the bijection keyEquiv r m₀ m₁ : Key ≃ Key chosen so that bij r k ⊕ m₀ = bij r (keyEquiv r m₀ m₁ k) ⊕ m₁, forcing the two ciphertexts to coincide (rHoare_bij_step).

Main definitions

• BijCPAScheme — a symmetric scheme (r, bij r k ⊕ m) built from a bijection family together with an involutive XOR on the output space.
• BijCPAScheme.toEncScheme — the induced core EncScheme.
• BijCPAScheme.toBijPRFFamily — the underlying (perfect) bijection-family PRF.

Main results

• bijCPA_correct — the scheme is correct (decryption recovers the message).
• bijCPA_prf_perfect — the underlying PRF has perfect PRF security.
• bijCPA_indcpa_coupling — the two IND-CPA games couple with eqPost.
• bijCPA_perfect_indcpa — perfect IND-CPA security: INDCPA_Adv B.toEncScheme m₀ m₁ A = 0 for every adversary A.
• boolXorCPA_perfect_indcpa — the Bool instantiation (r, (k ⊕ r) ⊕ m).

References

• [Rosulek, The Joy of Cryptography, §7 (CPA security)]

The Bijection-Family CPA Scheme

structure CatCrypt.Examples.CPAFromPRF.BijCPAScheme : Type 1

A symmetric encryption scheme encrypting m as (r, (bij r k) ⊕ m).

bij r : Key ≃ Output is a family of key→output bijections (one per randomness value r), and xorOut is an involutive combining operation on Output playing the role of XOR. For a uniform key the pad bij r k is uniform, which is the source of perfect security.

• Key : Type

  Key type

• Input : Type

  Randomness / PRF-input type

• Output : Type

  Output / message type

• finKey : Fintype self.Key
• neKey : Nonempty self.Key
• finInput : Fintype self.Input
• neInput : Nonempty self.Input
• finOutput : Fintype self.Output
• neOutput : Nonempty self.Output
• bij : self.Input → self.Key ≃ self.Output

  For each randomness value, a bijection from keys to outputs

• xorOut : self.Output → self.Output → self.Output

  The XOR-like combining operation on outputs

• xorOut_cancel (a b : self.Output) : self.xorOut (self.xorOut a b) b = a

  xorOut · b is involutive: un-padding with the same pad recovers the value

• xorOut_cancel' (a b : self.Output) : self.xorOut a (self.xorOut a b) = b

  xorOut a · is involutive: decryption recovers the message

noncomputable def CatCrypt.Examples.CPAFromPRF.BijCPAScheme.toEncScheme (B : BijCPAScheme) : Crypto.EncScheme

The core EncScheme induced by a bijection-family CPA scheme.

• Key, Plaintext = Output, Ciphertext = Input × Output
• keyGen samples a uniform key
• encrypt k m = do r ← sample Input; pure (r, (bij r k) ⊕ m)
• decrypt k (r, c) = pure (some ((bij r k) ⊕ c))

Equations

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

def CatCrypt.Examples.CPAFromPRF.BijCPAScheme.toBijPRFFamily (B : BijCPAScheme) : PRF.BijPRFFamily

The underlying bijection-family PRF F(k, r) = bij r k.

Equations

• B.toBijPRFFamily = { Key := B.Key, Input := B.Input, Output := B.Output, finKey := B.finKey, neKey := ⋯, finOutput := B.finOutput, neOutput := ⋯, bij := B.bij }

Correctness

theorem CatCrypt.Examples.CPAFromPRF.bijCPA_correct (B : BijCPAScheme) : B.toEncScheme.Correct

The scheme is correct: decrypting (r, (bij r k) ⊕ m) recovers m.

The Underlying PRF Is Perfect

theorem CatCrypt.Examples.CPAFromPRF.bijCPA_prf_perfect (B : BijCPAScheme) (x : B.Input) (A : B.toBijPRFFamily.toPRFScheme.Output → Core.SPComp Bool) : Crypto.SecurityDefs.PRF_Adv B.toBijPRFFamily.toPRFScheme x A = 0

The bijection-family PRF underlying the scheme has perfect PRF security.

Perfect IND-CPA Security

def CatCrypt.Examples.CPAFromPRF.BijCPAScheme.keyEquiv (B : BijCPAScheme) (r : B.Input) (m₀ m₁ : B.Output) : B.Key ≃ B.Key

The key-space bijection coupling the two IND-CPA games at a fixed randomness r: it maps k to the unique key whose pad differs from bij r k by m₀ ⊕ m₁, so that bij r k ⊕ m₀ and bij r (keyEquiv r m₀ m₁ k) ⊕ m₁ agree.

Equations

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

theorem CatCrypt.Examples.CPAFromPRF.bijCPA_game_eq (B : BijCPAScheme) (m₀ m₁ : B.Output) (b : Bool) : Crypto.SecurityDefs.INDCPA_Game B.toEncScheme m₀ m₁ b = (Core.SPComp.sample B.Input).bind fun (r : B.Input) => (Core.SPComp.sample B.Key).bind fun (k : B.Key) => Core.SPComp.pure (r, B.xorOut ((B.bij r) k) (if b = true then m₀ else m₁))

Reordered form of the IND-CPA game: sample the randomness r first, then the key, then output (r, (bij r k) ⊕ (if b then m₀ else m₁)).

theorem CatCrypt.Examples.CPAFromPRF.bijCPA_indcpa_coupling (B : BijCPAScheme) (m₀ m₁ : B.Output) : Relational.rHoare Relational.eqPre (Crypto.SecurityDefs.INDCPA_Game B.toEncScheme m₀ m₁ true) (Crypto.SecurityDefs.INDCPA_Game B.toEncScheme m₀ m₁ false) Relational.eqPost

Coupling: the two IND-CPA games for the scheme are equidistributed.

At each fixed randomness r, over a uniform key the pad bij r k is uniform, so bij r k ⊕ m₀ and bij r k ⊕ m₁ have the same distribution; keyEquiv r m₀ m₁ couples the two keys so the ciphertexts agree pointwise.

theorem CatCrypt.Examples.CPAFromPRF.bijCPA_perfect_indcpa (B : BijCPAScheme) (m₀ m₁ : B.Output) (A : B.toEncScheme.Ciphertext → Core.SPComp Bool) : Crypto.SecurityDefs.INDCPA_Adv B.toEncScheme m₀ m₁ A = 0

The scheme has perfect IND-CPA security: every adversary has IND-CPA advantage exactly 0.

Example: the XOR CPA scheme over Bool

Enc(k, m) = (r, (k ⊕ r) ⊕ m) with a fresh bit r, built from the XOR PRF F(k, r) = k ⊕ r (CatCrypt.Examples.PRF, boolXorPRF).

def CatCrypt.Examples.CPAFromPRF.boolXorCPA : BijCPAScheme

The XOR CPA scheme over Bool: bij r = boolXorBij r, xorOut = xor.

Equations

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

theorem CatCrypt.Examples.CPAFromPRF.boolXorCPA_correct : boolXorCPA.toEncScheme.Correct

The XOR CPA scheme over Bool is correct.

theorem CatCrypt.Examples.CPAFromPRF.boolXorCPA_perfect_indcpa (m₀ m₁ : Bool) (A : boolXorCPA.toEncScheme.Ciphertext → Core.SPComp Bool) : Crypto.SecurityDefs.INDCPA_Adv boolXorCPA.toEncScheme m₀ m₁ A = 0

The XOR CPA scheme over Bool has perfect IND-CPA security.

Reflection into the Package / UC Stack

The shallow bijCPA_perfect_indcpa bounds a single distinguisher applied to the two IND-CPA game bodies. This section lifts it to a composable statement about deep nominal packages linked with an arbitrary adversary package, following the stack shallow game → rawCode% → NomPackage.ofOracle → DeepNomAdvantage → sdist → UC via the shared CatCryptCore.Deep.ReflectUCHelpers combinators. The IND-CPA game samples the key and randomness then returns a pure ciphertext (heap-independent), so the shallow coupling bijCPA_indcpa_coupling upgrades to a full SPComp equality of the two reflected bodies (spcomp_eq_of_isPure_coupling), and the whole stack follows with no purity bridge on the adversary. Applies verbatim to the Bool instantiation boolXorCPA.

noncomputable def CatCrypt.Examples.CPAFromPRF.bijCpaGameRaw (B : BijCPAScheme) (m₀ m₁ : B.Output) (b : Bool) : Deep.RawCode (B.Input × B.Output)

The reflected IND-CPA game body for bit b: sample a key k and randomness r, then return the ciphertext (r, (bij r k) ⊕ (if b then m₀ else m₁)).

Equations

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

instance CatCrypt.Examples.CPAFromPRF.instValidBijCpaGameRaw (B : BijCPAScheme) (m₀ m₁ : B.Output) (b : Bool) : Deep.IsValid ∅ (bijCpaGameRaw B m₀ m₁ b)

theorem CatCrypt.Examples.CPAFromPRF.bijCpaGameRaw_eval_shallow (B : BijCPAScheme) (m₀ m₁ : B.Output) (b : Bool) : (bijCpaGameRaw B m₀ m₁ b).eval = Crypto.SecurityDefs.INDCPA_Game B.toEncScheme m₀ m₁ b

The reflected body evaluates back to the shallow IND-CPA game.

theorem CatCrypt.Examples.CPAFromPRF.bijCpa_game_isPure (B : BijCPAScheme) (m₀ m₁ : B.Output) (b : Bool) : (Crypto.SecurityDefs.INDCPA_Game B.toEncScheme m₀ m₁ b).IsPure

The IND-CPA game is heap-independent (two uniform samples then a pure ciphertext).

theorem CatCrypt.Examples.CPAFromPRF.bijCpaGameRaw_eval_eq (B : BijCPAScheme) (m₀ m₁ : B.Output) : (bijCpaGameRaw B m₀ m₁ true).eval = (bijCpaGameRaw B m₀ m₁ false).eval

The two reflected bodies (encrypting m₀ vs. m₁) have equal evaluations: the heap-independent coupling bijCPA_indcpa_coupling upgrades to SPComp equality.

noncomputable def CatCrypt.Examples.CPAFromPRF.bijCpaGameTrue (B : BijCPAScheme) (m₀ m₁ : B.Output) : Deep.NomPackage

Real IND-CPA game as an oracle-exporting nominal package (encrypts m₀).

Equations

• CatCrypt.Examples.CPAFromPRF.bijCpaGameTrue B m₀ m₁ = CatCrypt.Deep.NomPackage.ofOracle 1 Unit (B.Input × B.Output) fun (x : Unit) => CatCrypt.Examples.CPAFromPRF.bijCpaGameRaw B m₀ m₁ true

noncomputable def CatCrypt.Examples.CPAFromPRF.bijCpaGameFalse (B : BijCPAScheme) (m₀ m₁ : B.Output) : Deep.NomPackage

Ideal IND-CPA game as an oracle-exporting nominal package (encrypts m₁).

Equations

• CatCrypt.Examples.CPAFromPRF.bijCpaGameFalse B m₀ m₁ = CatCrypt.Deep.NomPackage.ofOracle 1 Unit (B.Input × B.Output) fun (x : Unit) => CatCrypt.Examples.CPAFromPRF.bijCpaGameRaw B m₀ m₁ false

theorem CatCrypt.Examples.CPAFromPRF.bijCpa_deepnom_zero (B : BijCPAScheme) (m₀ m₁ : B.Output) (A : Deep.NomPackage) : Crypto.DeepNomAdvantage (bijCpaGameTrue B m₀ m₁) (bijCpaGameFalse B m₀ m₁) A = 0

Zero deep-nominal advantage against every adversary package.

theorem CatCrypt.Examples.CPAFromPRF.bijCpa_sdist_zero (B : BijCPAScheme) (m₀ m₁ : B.Output) : (Crypto.sdist (fun (A : Deep.NomPackage) => Crypto.runPkg (A.pkg.link (bijCpaGameTrue B m₀ m₁).pkg)) fun (A : Deep.NomPackage) => Crypto.runPkg (A.pkg.link (bijCpaGameFalse B m₀ m₁).pkg)) = 0

Statistical distance zero between the two linked-game families.

theorem CatCrypt.Examples.CPAFromPRF.bijCpa_nompkg_secure (B : BijCPAScheme) (m₀ m₁ : B.Output) : Crypto.NomPkgSecure (bijCpaGameTrue B m₀ m₁) (bijCpaGameFalse B m₀ m₁) fun (x : Deep.NomPackage) => 0

Package-level perfect IND-CPA security (NomPkgSecure).

theorem CatCrypt.Examples.CPAFromPRF.bijCpa_uc (B : BijCPAScheme) (m₀ m₁ : B.Output) : Crypto.UCEmulates 0 { hon := Deep.NomPackage, out := Bool, leak := Empty, sim_if := Empty, view := Bool } (fun (A : { hon := Deep.NomPackage, out := Bool, leak := Empty, sim_if := Empty, view := Bool }.hon) => Core.SPComp.map Sum.inl (Crypto.runPkg (A.pkg.link (bijCpaGameTrue B m₀ m₁).pkg))) fun (A : { hon := Deep.NomPackage, out := Bool, leak := Empty, sim_if := Empty, view := Bool }.hon) => Core.SPComp.map Sum.inl (Crypto.runPkg (A.pkg.link (bijCpaGameFalse B m₀ m₁).pkg))

Perfect UC emulation of the linked-game families over the trivial-leak interface (out = Bool, leak = Empty) with the identity simulator (composition plumbing).

The Computational Reduction: IND-CPA ≤ PRF advantage

The perfect result above instantiates the PRF by a bijection family, making the underlying PRF information-theoretically secure. We now give the genuine computational result: for an arbitrary pseudorandom function F, the encryption Enc(k, m) = (r, F(k, r) ⊕ m) is IND-CPA secure with advantage bounded by the PRF advantage of F.

The argument is the standard single-reduction game hop through the one-time-pad world otpGame, in which the keyed pad F(k, r) is replaced by a fresh uniform output u:

Step	Transition	Bound
PRF-swap	Enc game ↔ otpGame (both worlds)	ε_prf (PRF assumption)
OTP	otpGame m₀ ↔ otpGame m₁	0 (one-time pad is perfect)

The OTP hop is perfect: over a fresh uniform pad the two ciphertext distributions coincide (otp_advantage_zero, proved by the bind_vcgen change-of-variables tactic). The PRF-swap hop is the cryptographic reduction; its soundness — that distinguishing the real encryption from the one-time-pad world is no easier than distinguishing F from random — is taken as the hypothesis hswap, bounded through the PRFAssumption. The two hops compose by the advantage triangle inequality into INDCPA_Adv ≤ ε_prf.

structure CatCrypt.Examples.CPAFromPRF.PRFEncScheme : Type 1

A PRF-based symmetric encryption scheme: Enc(k, m) = (r, F.eval k r ⊕ m) for a fresh uniform r, where ⊕ is the involutive xorOut on outputs. Unlike BijCPAScheme, the PRF F is arbitrary (no bijection assumption); security is therefore computational, resting on a PRFAssumption for F.

• F : Crypto.SecurityDefs.PRFScheme

  The underlying pseudorandom function family.

• finInput : Fintype self.F.Input
• neInput : Nonempty self.F.Input
• xorOut : self.F.Output → self.F.Output → self.F.Output

  The XOR-like combining operation on outputs.

• xorOut_cancel (a b : self.F.Output) : self.xorOut (self.xorOut a b) b = a

  xorOut · b is involutive: un-padding with the same pad recovers the value.

• xorOut_cancel' (a b : self.F.Output) : self.xorOut a (self.xorOut a b) = b

  xorOut a · is involutive: decryption recovers the message.

noncomputable def CatCrypt.Examples.CPAFromPRF.PRFEncScheme.toEncScheme (P : PRFEncScheme) : Crypto.EncScheme

The core EncScheme induced by a PRF-based scheme: Enc(k, m) = (r, F(k,r) ⊕ m).

Equations

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

noncomputable def CatCrypt.Examples.CPAFromPRF.PRFEncScheme.otpGame (P : PRFEncScheme) (m₀ m₁ : P.F.Output) (b : Bool) : Core.SPComp (P.F.Input × P.F.Output)

The one-time-pad world: the game obtained from the IND-CPA game by replacing the keyed pad F(k, r) with a fresh uniform output u. Encrypting if b then m₀ else m₁ as (r, u ⊕ (if b then m₀ else m₁)).

Equations

• P.otpGame m₀ m₁ b = do let r ← CatCrypt.Core.SPComp.sample P.F.Input let u ← CatCrypt.Core.SPComp.sample P.F.Output CatCrypt.Core.SPComp.pure (r, P.xorOut u (if b = true then m₀ else m₁))

def CatCrypt.Examples.CPAFromPRF.PRFEncScheme.xorEquiv (P : PRFEncScheme) (m : P.F.Output) : P.F.Output ≃ P.F.Output

The involution u ↦ xorOut u m as a self-bijection of the output space (its own inverse by xorOut_cancel). This is the change of variables that collapses a uniform pad to a plain uniform sample.

Equations

• P.xorEquiv m = { toFun := fun (u : P.F.Output) => P.xorOut u m, invFun := fun (u : P.F.Output) => P.xorOut u m, left_inv := ⋯, right_inv := ⋯ }

theorem CatCrypt.Examples.CPAFromPRF.PRFEncScheme.otpGame_true_eq_false (P : PRFEncScheme) (m₀ m₁ : P.F.Output) : P.otpGame m₀ m₁ true = P.otpGame m₀ m₁ false

Over a fresh uniform pad the padded ciphertext distribution is independent of the message: the two one-time-pad worlds are the same SPComp computation. Proved by the bind_vcgen run-to-completion tactic, feeding it the change-of-variables xorEquiv that rewrites the uniform pad into a plain uniform sample.

theorem CatCrypt.Examples.CPAFromPRF.PRFEncScheme.otp_advantage_zero (P : PRFEncScheme) (m₀ m₁ : P.F.Output) (A : P.F.Input × P.F.Output → Core.SPComp Bool) : Crypto.AdvantageA (P.otpGame m₀ m₁ true) (P.otpGame m₀ m₁ false) A = 0

The OTP hop is perfect: over a fresh uniform pad, no adversary distinguishes the m₀- from the m₁-world. Its advantage is exactly 0.

theorem CatCrypt.Examples.CPAFromPRF.cpa_from_prf_bound (P : PRFEncScheme) (H : Crypto.PRFAssumption P.F) (m₀ m₁ : P.F.Output) (A : P.F.Input × P.F.Output → Core.SPComp Bool) (x : P.F.Input) (Ared : P.F.Output → Core.SPComp Bool) (hswap : Crypto.AdvantageA (Crypto.SecurityDefs.INDCPA_Game P.toEncScheme m₀ m₁ true) (P.otpGame m₀ m₁ true) A + Crypto.AdvantageA (P.otpGame m₀ m₁ false) (Crypto.SecurityDefs.INDCPA_Game P.toEncScheme m₀ m₁ false) A ≤ Crypto.SecurityDefs.PRF_Adv P.F x Ared) : Crypto.SecurityDefs.INDCPA_Adv P.toEncScheme m₀ m₁ A ≤ H.ε

IND-CPA security from a PRF assumption (the computational headline).

For the PRF-based encryption Enc(k, m) = (r, F(k, r) ⊕ m), the IND-CPA advantage of any adversary A is bounded by the PRF advantage H.ε of the underlying function F.

The proof composes two hops by the advantage triangle inequality, routing through the one-time-pad world otpGame:

• the PRF-swap hop hswap — the reduction's soundness: distinguishing the real encryption from the one-time-pad world (in both challenge worlds) is bounded by a single PRF distinguisher's advantage PRF_Adv F x Ared, hence by H.ε via the assumption; and
• the perfect-OTP hop otp_advantage_zero — a one-time pad on a fresh uniform pad leaks nothing, contributing 0.

x/Ared are the reduction's PRF-distinguisher witness. The hswap hypothesis packages the (large) explicit-reduction construction, exactly as the cascade bound CatCrypt.Examples.PRF.cascade_prf_bound exposes its hop bounds as hypotheses.

The Synthesized Reduction: discharging the PRF-swap hop

cpa_from_prf_bound takes the PRF-swap soundness hswap as a hypothesis. We now build the concrete PRF distinguisher and prove the swap hops outright, so the computational IND-CPA bound rests only on the PRFAssumption — no assumed hop.

The single-challenge IND-CPA game samples a fresh randomness r and pads with F(k, r), whereas the single-query PRF game PRF_Real F x fixes its input x. The two are reconciled by conditioning on r: after reordering the game so r is sampled first (indcpa_game_eq), each fixed-r slice is literally a PRF distinguishing experiment — the distinguisher is cpaReduction r m A, which pads its oracle output with m at randomness r and runs A. This gives the exact per-slice identity slice_eq; averaging over r with advantageA_sample_bind bounds each swap hop by H.ε (indcpa_otp_hop).

The IND-CPA advantage then decomposes by the triangle inequality through the two one-time-pad worlds into two such swap hops (plus the perfect OTP hop), yielding the 2 · H.ε bound of cpa_from_prf_reduction_gamehop. The factor two is the two independent PRF replacements (one per challenge world) inherent to the left-right advantage formulation, matching Rosulek §7.

def CatCrypt.Examples.CPAFromPRF.PRFEncScheme.cpaReduction (P : PRFEncScheme) (r : P.F.Input) (m : P.F.Output) (A : P.F.Input × P.F.Output → Core.SPComp Bool) : P.F.Output → Core.SPComp Bool

The PRF-distinguisher reduction built from the IND-CPA adversary A.

Given the challenge randomness r and message m, cpaReduction r m A is the single-query PRF distinguisher that receives a candidate pad y — either the keyed value F(k, r) in the PRF real game, or a fresh uniform output in the ideal game — forms the challenge ciphertext (r, y ⊕ m), runs A on it, and returns A's guess. With a real pad it reproduces the IND-CPA game at randomness r; with a uniform pad, the one-time-pad world at r.

Equations

• P.cpaReduction r m A y = A (r, P.xorOut y m)

theorem CatCrypt.Examples.CPAFromPRF.PRFEncScheme.indcpa_game_eq (P : PRFEncScheme) (m₀ m₁ : P.F.Output) (b : Bool) : Crypto.SecurityDefs.INDCPA_Game P.toEncScheme m₀ m₁ b = (Core.SPComp.sample P.F.Input).bind fun (r : P.F.Input) => (Core.SPComp.sample P.F.Key).bind fun (k : P.F.Key) => Core.SPComp.pure (r, P.xorOut (P.F.eval k r) (if b = true then m₀ else m₁))

Reordered form of the IND-CPA game for the PRF scheme: sample the randomness r first, then the key k, then output (r, F(k, r) ⊕ (if b then m₀ else m₁)). The reorder is the Fubini commutation of the two independent samples (SPComp.swap_sample_sample).

theorem CatCrypt.Examples.CPAFromPRF.PRFEncScheme.slice_eq (P : PRFEncScheme) (r : P.F.Input) (m : P.F.Output) (A : P.F.Input × P.F.Output → Core.SPComp Bool) : Crypto.AdvantageA ((Core.SPComp.sample P.F.Key).bind fun (k : P.F.Key) => Core.SPComp.pure (r, P.xorOut (P.F.eval k r) m)) ((Core.SPComp.sample P.F.Output).bind fun (u : P.F.Output) => Core.SPComp.pure (r, P.xorOut u m)) A = Crypto.SecurityDefs.PRF_Adv P.F r (P.cpaReduction r m A)

The per-randomness slice is exactly a PRF distinguishing advantage.

At a fixed challenge randomness r, the advantage between the keyed-pad game (sample k; (r, F(k, r) ⊕ m)) and the uniform-pad game (sample u; (r, u ⊕ m)) against A equals the PRF advantage of the built distinguisher cpaReduction r m A. This is a definitional identity: A's view after either game is exactly the reduction's view after the corresponding PRF game.

theorem CatCrypt.Examples.CPAFromPRF.PRFEncScheme.indcpa_otp_hop (P : PRFEncScheme) (H : Crypto.PRFAssumption P.F) (m₀ m₁ : P.F.Output) (A : P.F.Input × P.F.Output → Core.SPComp Bool) (b : Bool) : Crypto.AdvantageA (Crypto.SecurityDefs.INDCPA_Game P.toEncScheme m₀ m₁ b) (P.otpGame m₀ m₁ b) A ≤ H.ε

The PRF-swap hop, discharged by the built reduction.

For each challenge world b, distinguishing the real PRF encryption from the one-time-pad world is bounded by H.ε: reorder so the randomness r is sampled first (indcpa_game_eq), then average the per-r slices (advantageA_sample_bind), each of which equals PRF_Adv P.F r (cpaReduction r · A) (slice_eq) and is hence ≤ H.ε by the PRF assumption. No hop is assumed.

theorem CatCrypt.Examples.CPAFromPRF.cpa_from_prf_reduction_gamehop (P : PRFEncScheme) (H : Crypto.PRFAssumption P.F) (m₀ m₁ : P.F.Output) (A : P.F.Input × P.F.Output → Core.SPComp Bool) : Crypto.SecurityDefs.INDCPA_Adv P.toEncScheme m₀ m₁ A ≤ 2 * H.ε

IND-CPA security from a PRF, fully synthesized (no assumed swap hop).

For the PRF-based encryption Enc(k, m) = (r, F(k, r) ⊕ m), the IND-CPA advantage of any adversary A is at most 2 · H.ε, resting only on the PRFAssumption H. The adv_game_hop tactic composes, by the advantage triangle inequality through the two one-time-pad worlds:

• the two PRF-swap hops indcpa_otp_hop (each ≤ H.ε), proved from the concrete distinguisher cpaReduction rather than assumed; and
• the perfect-OTP hop otp_advantage_zero (= 0).

The factor two is the two independent PRF replacements — one per challenge world — that the left-right advantage genuinely requires; it cannot be collapsed to a single H.ε without assuming a combined distinguisher whose advantage exceeds the PRF bound (Rosulek §7).