Deterministic CPA Impossibility

This file formalizes the impossibility of CPA-secure deterministic encryption from Chapter 7.1 of "The Joy of Cryptography".

Overview

Any deterministic encryption scheme can be broken by a simple adversary that encrypts the same message twice and checks if the ciphertexts match. For the XOR-based scheme enc(k, m) = xor k m, we show that the distinguishing advantage is exactly 1.

No UC wrapper — this is an attack/insecurity result.

References

• [Rosulek, The Joy of Cryptography, Section 7.1]

Deterministic Encryption Scheme

structure CatCryptCore.Examples.DetCPA.DetEncScheme : Type

A deterministic encryption scheme: enc(key, msg) → ciphertext.

• enc : Bool → Bool → Bool

def CatCryptCore.Examples.DetCPA.xorDet : DetEncScheme

XOR-based deterministic encryption: enc(k, m) = xor k m.

Equations

• CatCryptCore.Examples.DetCPA.xorDet = { enc := xor }

Two-Encryption Game

noncomputable def CatCryptCore.Examples.DetCPA.det_enc_pair (E : DetEncScheme) (m₁ m₂ : Bool) : CatCrypt.Core.SPComp (Bool × Bool)

Game: encrypt two messages under the same random key, return ciphertext pair.

Equations

• CatCryptCore.Examples.DetCPA.det_enc_pair E m₁ m₂ = do let k ← CatCrypt.Core.SPComp.sample Bool CatCrypt.Core.SPComp.pure (E.enc k m₁, E.enc k m₂)

noncomputable def CatCryptCore.Examples.DetCPA.eq_adversary : Bool × Bool → CatCrypt.Core.SPComp Bool

Equality-checking adversary: returns true iff both ciphertexts are equal.

Equations

• CatCryptCore.Examples.DetCPA.eq_adversary (c₁, c₂) = CatCrypt.Core.SPComp.pure (c₁ == c₂)

Insecurity Proof

theorem CatCryptCore.Examples.DetCPA.same_msg_prTrue (m : Bool) : CatCrypt.Crypto.prTrue ((det_enc_pair xorDet m m).bind eq_adversary) CatCrypt.Core.Heap.empty = 1

For the XOR scheme encrypting the same message twice: the adversary always returns true (advantage 1 side).

theorem CatCryptCore.Examples.DetCPA.diff_msg_prTrue (m : Bool) : CatCrypt.Crypto.prTrue ((det_enc_pair xorDet m !m).bind eq_adversary) CatCrypt.Core.Heap.empty = 0

For the XOR scheme encrypting different messages: the adversary always returns false (advantage 0 side).

theorem CatCryptCore.Examples.DetCPA.det_enc_xor_insecure (m : Bool) : CatCrypt.Crypto.AdvantageA (det_enc_pair xorDet m m) (det_enc_pair xorDet m !m) eq_adversary = 1

Main theorem: XOR deterministic encryption is completely insecure.

The equality-checking adversary achieves advantage 1 when distinguishing same-message encryption from different-message encryption.