Counter (CTR) Mode: the Perfect Single-Block Instantiation

Counter mode turns a block cipher / PRF into an IND-CPA-secure symmetric encryption scheme. Following Rosulek, The Joy of Cryptography, §8 (block cipher modes).

A single message block m is encrypted as (nonce, E(k, nonce) ⊕ m) for a fresh uniform nonce (the initial counter value): the keystream block E(k, nonce) acts as a one-time pad. Decryption recomputes E(k, nonce) from the transmitted nonce and un-pads. This single-block CTR construction is exactly the CPA-from-PRF construction (CatCrypt.Examples.CPAFromPRF) with the PRF input specialized to the counter/nonce, so we obtain its security for free.

The perfect instantiation

Model the block cipher in CTR mode as a bijection family: for each counter value ctr, the keystream map keystream ctr : Key ≃ Block, k ↦ E(k, ctr), is a bijection from keys to blocks (the ideal-cipher / perfect-PRF model). Over a uniform key the keystream block E(k, nonce) is then uniform on Block, independent of the message, so the pad E(k, nonce) ⊕ m is uniform regardless of m. The two IND-CPA games (encrypting m₀ vs. m₁) are perfectly indistinguishable: the IND-CPA advantage of every adversary is exactly 0.

Scope

This file proves the single-block statement, which is the clean core-provable case (it coincides with CPA-from-PRF). Genuine multi-block CTR — encrypting (m₁, …, mₙ) as (nonce, E(k, nonce+0) ⊕ m₁, …, E(k, nonce+n-1) ⊕ mₙ) — needs a product-of-bijections (independent-keystream-block) argument not developed in core, and is deliberately out of scope here.

Main definitions

• CTRBlockScheme — single-block CTR data: a keystream bijection family keystream : Block → (Key ≃ Block) together with an involutive XOR on blocks.
• CTRBlockScheme.toBijCPAScheme — the equivalent CPA-from-PRF scheme (nonce as PRF input); every result is inherited through it.
• CTRBlockScheme.toEncScheme — the induced core EncScheme.

Main results

• ctr_correct — the scheme is correct (decryption recovers the message).
• ctr_perfect_indcpa — perfect IND-CPA security: INDCPA_Adv C.toEncScheme m₀ m₁ A = 0 for every adversary A.
• boolCTR_perfect_indcpa — the Bool instantiation with block cipher E(k, n) = k ⊕ n, i.e. Enc(k, m) = (n, (k ⊕ n) ⊕ m).

References

• [Rosulek, The Joy of Cryptography, §8 (block cipher modes)]

The Single-Block CTR Scheme

structure CatCrypt.Examples.CTRMode.CTRBlockScheme : Type 1

Data for single-block CTR-mode encryption Enc(k, m) = (nonce, E(k, nonce) ⊕ m).

keystream ctr : Key ≃ Block is the counter-indexed keystream map k ↦ E(k, ctr), required to be a bijection for each counter value (the ideal-cipher / perfect-PRF model), and xorBlock is an involutive XOR on blocks. For a uniform key the keystream block keystream nonce k is uniform, which is the source of perfect security.

• Key : Type

  Key type

• Block : Type

  Block / message type (also the nonce / counter type)

• finKey : Fintype self.Key
• neKey : Nonempty self.Key
• finBlock : Fintype self.Block
• neBlock : Nonempty self.Block
• keystream : self.Block → self.Key ≃ self.Block

  For each counter value, the keystream map k ↦ E(k, ctr) is a bijection

• xorBlock : self.Block → self.Block → self.Block

  The XOR-like combining operation on blocks

• xorBlock_cancel (a b : self.Block) : self.xorBlock (self.xorBlock a b) b = a

  xorBlock · b is involutive: un-padding with the same keystream recovers the value

• xorBlock_cancel' (a b : self.Block) : self.xorBlock a (self.xorBlock a b) = b

  xorBlock a · is involutive: decryption recovers the message

def CatCrypt.Examples.CTRMode.CTRBlockScheme.toBijCPAScheme (C : CTRBlockScheme) : CPAFromPRF.BijCPAScheme

Single-block CTR is CPA-from-PRF with the PRF input taken to be the nonce: Input = Output = Block, bij = keystream, xorOut = xorBlock.

Equations

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

noncomputable def CatCrypt.Examples.CTRMode.CTRBlockScheme.toEncScheme (C : CTRBlockScheme) : Crypto.EncScheme

The core EncScheme induced by a single-block CTR scheme: encrypt k m = do nonce ← sample Block; pure (nonce, (keystream nonce k) ⊕ m).

Equations

• C.toEncScheme = C.toBijCPAScheme.toEncScheme

Correctness

theorem CatCrypt.Examples.CTRMode.ctr_correct (C : CTRBlockScheme) : C.toEncScheme.Correct

The scheme is correct: decrypting (nonce, (keystream nonce k) ⊕ m) recovers m.

Perfect IND-CPA Security

theorem CatCrypt.Examples.CTRMode.ctr_perfect_indcpa (C : CTRBlockScheme) (m₀ m₁ : C.toEncScheme.Plaintext) (A : C.toEncScheme.Ciphertext → Core.SPComp Bool) : Crypto.SecurityDefs.INDCPA_Adv C.toEncScheme m₀ m₁ A = 0

Single-block CTR mode has perfect IND-CPA security: every adversary has IND-CPA advantage exactly 0.

Over a uniform key the keystream block keystream nonce k is uniform on Block (bijection family), so the pad keystream nonce k ⊕ m is uniform regardless of m; the two IND-CPA games are therefore perfectly indistinguishable.

Example: single-block CTR over Bool

Block cipher E(k, n) = k ⊕ n (keystream n = boolXorBij n), giving Enc(k, m) = (n, (k ⊕ n) ⊕ m) for a fresh bit n.

def CatCrypt.Examples.CTRMode.boolCTR : CTRBlockScheme

Single-block CTR over Bool with block cipher E(k, n) = k ⊕ n.

Equations

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

theorem CatCrypt.Examples.CTRMode.boolCTR_correct : boolCTR.toEncScheme.Correct

The Bool CTR scheme is correct.

theorem CatCrypt.Examples.CTRMode.boolCTR_perfect_indcpa (m₀ m₁ : boolCTR.toEncScheme.Plaintext) (A : boolCTR.toEncScheme.Ciphertext → Core.SPComp Bool) : Crypto.SecurityDefs.INDCPA_Adv boolCTR.toEncScheme m₀ m₁ A = 0

The Bool CTR scheme has perfect IND-CPA security.

The Computational IND-CPA Bound from the Block Cipher's PRF Security

The perfect result above models the block cipher in CTR mode as an ideal cipher (a bijection family), giving IND-CPA advantage exactly 0. The standard computational reduction that a real block cipher would use bounds the CTR IND-CPA advantage by the block cipher's PRF advantage ε_prf, via the two-hop game walk

Hop	Transition	Bound
PRF-swap	real challenge game → ctrIdealGame (keystream E(k,·) → random function)	ε_prf (PRFAssumption)
perfect	ctrIdealGame → other challenge world (random pad is message-independent)	0

The perfect hop is an SPComp game equality proved by bind_vcgen; the PRF-swap hop is the reduction's soundness, taken as a hypothesis and discharged by the PRFAssumption. Composition is the advantage triangle inequality.

noncomputable def CatCrypt.Examples.CTRMode.ctrIdealGame (C : CTRBlockScheme) : Core.SPComp (C.Block × C.Block)

The message-independent ideal CTR game: output a fresh nonce and a fresh uniform pad (nonce, pad). This is CTR encryption with the keystream E(k,·) replaced by a random function; being independent of the message, both IND-CPA challenge worlds collapse onto it.

Equations

• CatCrypt.Examples.CTRMode.ctrIdealGame C = do let nonce ← CatCrypt.Core.SPComp.sample C.Block let pad ← CatCrypt.Core.SPComp.sample C.Block CatCrypt.Core.SPComp.pure (nonce, pad)

def CatCrypt.Examples.CTRMode.CTRBlockScheme.padEquiv (C : CTRBlockScheme) (r msg : C.Block) : C.Key ≃ C.Block

At a fixed nonce r, the keystream-then-XOR map k ↦ E(k, r) ⊕ msg is a bijection Key ≃ Block: compose the keystream bijection keystream r with the involutive XOR by msg. This is the change of variables that turns the (uniform key) pad into a uniform block, i.e. the coupling behind the perfect hop.

Equations

• C.padEquiv r msg = { toFun := fun (k : C.Key) => C.xorBlock ((C.keystream r) k) msg, invFun := fun (b : C.Block) => (C.keystream r).symm (C.xorBlock b msg), left_inv := ⋯, right_inv := ⋯ }

theorem CatCrypt.Examples.CTRMode.ctr_game_eq_ideal (C : CTRBlockScheme) (m₀ m₁ : C.toEncScheme.Plaintext) (b : Bool) : Crypto.SecurityDefs.INDCPA_Game C.toEncScheme m₀ m₁ b = ctrIdealGame C

Perfect hop. Each concrete IND-CPA challenge game equals the message-independent ctrIdealGame: sampling the nonce first (via bijCPA_game_eq) and then changing variables k ↦ E(k, r) ⊕ msg through padEquiv collapses the keyed pad to a fresh uniform block. Proved by bind_vcgen using the coupling bijection.

theorem CatCrypt.Examples.CTRMode.ctr_indcpa_bound (C : CTRBlockScheme) {F : Crypto.SecurityDefs.PRFScheme} (H : Crypto.PRFAssumption F) (m₀ m₁ : C.toEncScheme.Plaintext) (A : C.toEncScheme.Ciphertext → Core.SPComp Bool) (x : F.Input) (Ared : F.Output → Core.SPComp Bool) (hswap : Crypto.AdvantageA (Crypto.SecurityDefs.INDCPA_Game C.toEncScheme m₀ m₁ true) (ctrIdealGame C) A ≤ Crypto.SecurityDefs.PRF_Adv F x Ared) : Crypto.SecurityDefs.INDCPA_Adv C.toEncScheme m₀ m₁ A ≤ H.ε

Single-block CTR mode: the computational IND-CPA bound.

The IND-CPA advantage of single-block CTR is at most the block cipher's PRF advantage H.ε. The proof is the advantage triangle inequality over the two hops:

• the PRF-swap hop AdvantageA (challenge true) (ctrIdealGame) A is the reduction's soundness (hswap): an IND-CPA distinguisher here is a PRF distinguisher Ared on input x, so the hop is bounded by PRF_Adv F x Ared, which PRFAssumption H caps at H.ε;
• the perfect hop AdvantageA (ctrIdealGame) (challenge false) A is 0, because ctr_game_eq_ideal identifies ctrIdealGame with the false challenge world.

Because CTRBlockScheme is the ideal-cipher (bijection-family) model, the PRF-swap hop is itself 0 here (see ctr_perfect_indcpa); the theorem states the reduction in the general form a real PRF instantiation uses.