IND-CPA Security Games

The IND-CPA (Indistinguishability under Chosen Plaintext Attack) security games for symmetric encryption schemes.

The IND-CPA game proceeds as:

1. The challenger generates a random key k.
2. The adversary chooses two messages m₀, m₁.
3. The challenger encrypts mᵦ for a random bit b.
4. The adversary tries to guess b.

An encryption scheme is IND-CPA secure if no efficient adversary can guess b with probability significantly better than 1/2.

Main definitions

• indCPA_real — encrypt the first message (b = 0).
• indCPA_ideal — encrypt the second message (b = 1).
• INDCPA_Advantage — the distinguishing advantage.

References

• [Bellare & Rogaway, Introduction to Modern Cryptography]
• [Katz & Lindell, Introduction to Modern Cryptography, Chapter 3]

IND-CPA Security Games

noncomputable def CatCryptCore.Examples.INDCPA.indCPA_real (E : CatCrypt.Crypto.EncScheme) (m₀ _m₁ : E.Plaintext) : CatCrypt.Core.SPComp E.Ciphertext

Real IND-CPA game: encrypt the first message m₀.

This corresponds to the game where the challenger bit b = 0, so the adversary receives Enc(k, m₀).

Equations

• CatCryptCore.Examples.INDCPA.indCPA_real E m₀ _m₁ = do let k ← E.keyGen E.encrypt k m₀

noncomputable def CatCryptCore.Examples.INDCPA.indCPA_ideal (E : CatCrypt.Crypto.EncScheme) (_m₀ m₁ : E.Plaintext) : CatCrypt.Core.SPComp E.Ciphertext

Ideal IND-CPA game: encrypt the second message m₁.

This corresponds to the game where the challenger bit b = 1, so the adversary receives Enc(k, m₁).

Equations

• CatCryptCore.Examples.INDCPA.indCPA_ideal E _m₀ m₁ = do let k ← E.keyGen E.encrypt k m₁

noncomputable def CatCryptCore.Examples.INDCPA.INDCPA_Advantage (E : CatCrypt.Crypto.EncScheme) (m₀ m₁ : E.Plaintext) (A : E.Ciphertext → CatCrypt.Core.SPComp Bool) : ENNReal

IND-CPA advantage: the distinguishing advantage between real and ideal games.

An encryption scheme is IND-CPA secure if for all efficient adversaries A and all message pairs (m₀, m₁), the advantage is negligible.

Equations

• CatCryptCore.Examples.INDCPA.INDCPA_Advantage E m₀ m₁ A = CatCrypt.Crypto.AdvantageA (CatCryptCore.Examples.INDCPA.indCPA_real E m₀ m₁) (CatCryptCore.Examples.INDCPA.indCPA_ideal E m₀ m₁) A

Perfect IND-CPA Security

Perfect IND-CPA security means the advantage is exactly 0 for all adversaries. This is achievable by one-time-pad style encryption.

def CatCryptCore.Examples.INDCPA.PerfectINDCPA (E : CatCrypt.Crypto.EncScheme) : Prop

An encryption scheme has perfect IND-CPA security if for all message pairs the real and ideal games satisfy the pRHL judgment with eqPost.

The precondition eqPre (heap equality) holds when starting from empty heaps.

Equations

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

theorem CatCryptCore.Examples.INDCPA.perfect_indcpa_zero_advantage (E : CatCrypt.Crypto.EncScheme) (hPerf : PerfectINDCPA E) (m₀ m₁ : E.Plaintext) (A : E.Ciphertext → CatCrypt.Core.SPComp Bool) : INDCPA_Advantage E m₀ m₁ A = 0

Perfect IND-CPA security implies zero advantage for all adversaries.