Standard Security Definitions

This file provides abstract security definitions for the most common cryptographic security notions. These serve as a reference catalog and provide reusable building blocks for security proofs.

Main definitions

Indistinguishability

• INDCPA_Game — IND-CPA (Indistinguishability under Chosen Plaintext Attack)
• INDCCA_Game — IND-CCA (Indistinguishability under Chosen Ciphertext Attack)

Pseudorandomness

• PRFScheme — Pseudorandom function family
• PRF_Game — PRF indistinguishability game

Authentication

• MACScheme — Message authentication code
• EUF_CMA_Game — Existential Unforgeability under Chosen Message Attack

Concrete instantiations

These abstract definitions are instantiated in the example files:

• CatCrypt.Examples.INDCPA — IND-CPA for EncScheme
• CatCrypt.Examples.INDCCA — IND-CCA for EncScheme
• CatCrypt.Examples.PRF — PRF security for Bool-based PRF
• CatCrypt.Examples.MAC — MAC security for Bool-based MAC
• CatCrypt.Examples.Schnorr — EUF-CMA for Schnorr signatures
• CatCrypt.Examples.ElGamal — IND-CPA for ElGamal PKE
• CatCrypt.Examples.PKE.Scheme — OT-CPA and MT-CPA for PKE

References

• [Bellare & Rogaway, Introduction to Modern Cryptography]
• [Katz & Lindell, Introduction to Modern Cryptography, 3rd ed.]
• [Rosulek, The Joy of Cryptography]

IND-CPA: Indistinguishability under Chosen Plaintext Attack

noncomputable def CatCrypt.Crypto.SecurityDefs.INDCPA_Game (E : EncScheme) (m₀ m₁ : E.Plaintext) (b : Bool) : Core.SPComp E.Ciphertext

IND-CPA game for a symmetric encryption scheme.

The adversary chooses two messages and receives an encryption of one. The game returns the ciphertext; the adversary tries to guess which message was encrypted.

• INDCPA_Game E m₀ m₁ true — encrypts m₀ (left/real)
• INDCPA_Game E m₀ m₁ false — encrypts m₁ (right/ideal)

Equations

• CatCrypt.Crypto.SecurityDefs.INDCPA_Game E m₀ m₁ b = do let k ← E.keyGen E.encrypt k (if b = true then m₀ else m₁)

noncomputable def CatCrypt.Crypto.SecurityDefs.INDCPA_Adv (E : EncScheme) (m₀ m₁ : E.Plaintext) (A : E.Ciphertext → Core.SPComp Bool) : ENNReal

IND-CPA advantage: distinguishing probability between left and right.

Equations

• CatCrypt.Crypto.SecurityDefs.INDCPA_Adv E m₀ m₁ A = CatCrypt.Crypto.AdvantageA (CatCrypt.Crypto.SecurityDefs.INDCPA_Game E m₀ m₁ true) (CatCrypt.Crypto.SecurityDefs.INDCPA_Game E m₀ m₁ false) A

IND-CCA: Indistinguishability under Chosen Ciphertext Attack

IND-CCA extends IND-CPA by handing the adversary a decryption oracle on ciphertexts other than the challenge. In this single-shot SPComp game framework a decryption oracle is faithfully modelled as an ordinary Lean function E.Ciphertext → SPComp (Option E.Plaintext) that closes over the game's secret key k; the CCA2 "may not query the challenge" restriction is enforced by the guard if c = cStar then none else E.decrypt k c. No oracle-state threading is needed because decryption is stateless — it only reads the key. The adversary takes the oracle as an explicit argument and may call it on any ciphertext, so the oracle is genuinely reachable (not a dead argument).

noncomputable def CatCrypt.Crypto.SecurityDefs.ccaDecOracle (E : EncScheme) (k : E.Key) (cStar : E.Ciphertext) : E.Ciphertext → Core.SPComp (Option E.Plaintext)

The restricted (off-challenge) decryption oracle used by the IND-CCA game: decrypt with the real key k, except reject (none) the challenge ciphertext cStar itself. This is the CCA2 restriction.

Equations

• CatCrypt.Crypto.SecurityDefs.ccaDecOracle E k cStar c = if c = cStar then CatCrypt.Core.SPComp.pure none else E.decrypt k c

noncomputable def CatCrypt.Crypto.SecurityDefs.rejectDecOracle (E : EncScheme) : E.Ciphertext → Core.SPComp (Option E.Plaintext)

The ideal always-reject decryption oracle: every ciphertext is rejected. This is the oracle of an ideal authenticated-encryption scheme, against which the real oracle is compared to measure ciphertext-integrity.

Equations

• CatCrypt.Crypto.SecurityDefs.rejectDecOracle E x✝ = CatCrypt.Core.SPComp.pure none

noncomputable def CatCrypt.Crypto.SecurityDefs.INDCCA_Game (E : EncScheme) (m₀ m₁ : E.Plaintext) (b : Bool) (A : (E.Ciphertext → Core.SPComp (Option E.Plaintext)) → E.Ciphertext → Core.SPComp Bool) : Core.SPComp Bool

IND-CCA game (CCA2, find-then-guess with a fixed message pair). The adversary A receives the challenge ciphertext together with the off-challenge decryption oracle ccaDecOracle E k cStar, and outputs a guess bit.

• INDCCA_Game E m₀ m₁ true A — encrypts m₀ (left/real)
• INDCCA_Game E m₀ m₁ false A — encrypts m₁ (right/ideal)

Equations

• CatCrypt.Crypto.SecurityDefs.INDCCA_Game E m₀ m₁ b A = do let k ← E.keyGen let cStar ← E.encrypt k (if b = true then m₀ else m₁) A (CatCrypt.Crypto.SecurityDefs.ccaDecOracle E k cStar) cStar

noncomputable def CatCrypt.Crypto.SecurityDefs.INDCCA_Adv (E : EncScheme) (m₀ m₁ : E.Plaintext) (A : (E.Ciphertext → Core.SPComp (Option E.Plaintext)) → E.Ciphertext → Core.SPComp Bool) : ENNReal

IND-CCA advantage: distinguishing probability between the m₀- and m₁-worlds when the adversary has decryption-oracle access.

Equations

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

noncomputable def CatCrypt.Crypto.SecurityDefs.INDCCA_rejectGame (E : EncScheme) (m₀ m₁ : E.Plaintext) (b : Bool) (A : (E.Ciphertext → Core.SPComp (Option E.Plaintext)) → E.Ciphertext → Core.SPComp Bool) : Core.SPComp Bool

The IND-CCA game with the real decryption oracle replaced by the ideal always-reject oracle. Since the reject oracle ignores the key, this game collapses to an IND-CPA game whose adversary ignores its (useless) oracle (see INDCCA_rejectGame_eq).

Equations

• CatCrypt.Crypto.SecurityDefs.INDCCA_rejectGame E m₀ m₁ b A = do let k ← E.keyGen let cStar ← E.encrypt k (if b = true then m₀ else m₁) A (CatCrypt.Crypto.SecurityDefs.rejectDecOracle E) cStar

theorem CatCrypt.Crypto.SecurityDefs.INDCCA_rejectGame_eq (E : EncScheme) (m₀ m₁ : E.Plaintext) (b : Bool) (A : (E.Ciphertext → Core.SPComp (Option E.Plaintext)) → E.Ciphertext → Core.SPComp Bool) : INDCCA_rejectGame E m₀ m₁ b A = (INDCPA_Game E m₀ m₁ b).bind fun (c : E.Ciphertext) => A (rejectDecOracle E) c

The always-reject IND-CCA game is exactly an IND-CPA game post-composed with the adversary reading its useless oracle: the reject oracle ignores the key, so the challenge production factors out by monad associativity.

PRF: Pseudorandom Function

structure CatCrypt.Crypto.SecurityDefs.PRFScheme : Type 1

A pseudorandom function family.

• Key : Type

  Key type

• Input : Type

  Input (domain) type

• Output : Type

  Output (range) type

• finKey : Fintype self.Key
• neKey : Nonempty self.Key
• finOutput : Fintype self.Output
• neOutput : Nonempty self.Output
• eval : self.Key → self.Input → self.Output

  The PRF evaluation function

noncomputable def CatCrypt.Crypto.SecurityDefs.PRF_Real (F : PRFScheme) (x : F.Input) : Core.SPComp F.Output

PRF real game: evaluate PRF with random key.

Equations

• CatCrypt.Crypto.SecurityDefs.PRF_Real F x = do let k ← CatCrypt.Core.SPComp.sample F.Key CatCrypt.Core.SPComp.pure (F.eval k x)

noncomputable def CatCrypt.Crypto.SecurityDefs.PRF_Ideal (F : PRFScheme) : Core.SPComp F.Output

PRF ideal game: return a uniformly random value.

Equations

• CatCrypt.Crypto.SecurityDefs.PRF_Ideal F = CatCrypt.Core.SPComp.sample F.Output

noncomputable def CatCrypt.Crypto.SecurityDefs.PRF_Adv (F : PRFScheme) (x : F.Input) (A : F.Output → Core.SPComp Bool) : ENNReal

PRF advantage: distinguishing PRF output from random.

Equations

• CatCrypt.Crypto.SecurityDefs.PRF_Adv F x A = CatCrypt.Crypto.AdvantageA (CatCrypt.Crypto.SecurityDefs.PRF_Real F x) (CatCrypt.Crypto.SecurityDefs.PRF_Ideal F) A

MAC: Message Authentication Code

structure CatCrypt.Crypto.SecurityDefs.MACScheme : Type 1

A message authentication code scheme.

• Key : Type

  Key type

• Message : Type

  Message type

• Tag : Type

  Tag type

• finKey : Fintype self.Key
• neKey : Nonempty self.Key
• finTag : Fintype self.Tag
• neTag : Nonempty self.Tag
• decTag : DecidableEq self.Tag
• mac : self.Key → self.Message → self.Tag

  Tag generation

• verify : self.Key → self.Message → self.Tag → Bool

  Verification (default: recompute and compare)

noncomputable def CatCrypt.Crypto.SecurityDefs.EUF_CMA_Real (M : MACScheme) (m m_star : M.Message) (t_star : M.Tag) : Core.SPComp Bool

EUF-CMA real game (simplified, single-query): adversary receives a tag on message m and tries to forge on m*.

Returns true if the adversary's forgery attempt verifies.

Equations

• CatCrypt.Crypto.SecurityDefs.EUF_CMA_Real M m m_star t_star = do let k ← CatCrypt.Core.SPComp.sample M.Key have _t : M.Tag := M.mac k m CatCrypt.Core.SPComp.pure (M.verify k m_star t_star)

noncomputable def CatCrypt.Crypto.SecurityDefs.EUF_CMA_Adv (M : MACScheme) (m m_star : M.Message) (t_star : M.Tag) (A : Bool → Core.SPComp Bool) : ENNReal

EUF-CMA advantage: probability of successful forgery.

Equations

• CatCrypt.Crypto.SecurityDefs.EUF_CMA_Adv M m m_star t_star A = CatCrypt.Crypto.prTrue (CatCrypt.Crypto.SecurityDefs.EUF_CMA_Real M m m_star t_star >>= A) CatCrypt.Core.Heap.empty

Advantage Bounds

theorem CatCrypt.Crypto.SecurityDefs.PRF_Adv_zero_of_rHoare (F : PRFScheme) (x : F.Input) (h : Relational.rHoare Relational.eqPre (PRF_Real F x) (PRF_Ideal F) Relational.eqPost) (A : F.Output → Core.SPComp Bool) : PRF_Adv F x A = 0

If a PRF is perfect (PRF output = random for all inputs), PRF advantage is 0.

theorem CatCrypt.Crypto.SecurityDefs.INDCPA_Adv_zero_of_rHoare (E : EncScheme) (m₀ m₁ : E.Plaintext) (h : Relational.rHoare Relational.eqPre (INDCPA_Game E m₀ m₁ true) (INDCPA_Game E m₀ m₁ false) Relational.eqPost) (A : E.Ciphertext → Core.SPComp Bool) : INDCPA_Adv E m₀ m₁ A = 0

If encryption is perfectly indistinguishable, IND-CPA advantage is 0.

theorem CatCrypt.Crypto.SecurityDefs.INDCCA_Adv_zero_of_rHoare (E : EncScheme) (m₀ m₁ : E.Plaintext) (A : (E.Ciphertext → Core.SPComp (Option E.Plaintext)) → E.Ciphertext → Core.SPComp Bool) (h : Relational.rHoare Relational.eqPre (INDCCA_Game E m₀ m₁ true A) (INDCCA_Game E m₀ m₁ false A) Relational.eqPost) : INDCCA_Adv E m₀ m₁ A = 0

If the two IND-CCA oracle-games are perfectly indistinguishable, the IND-CCA advantage is 0. Note the hypothesis quantifies over the whole oracle-game (adversary and decryption oracle included); for a genuinely confidential scheme with two distinct messages it is only met degenerately (e.g. m₀ = m₁), because the decryption oracle's answers depend on the secret key.

theorem CatCrypt.Crypto.SecurityDefs.INDCCA_reduces_to_INDCPA (E : EncScheme) (m₀ m₁ : E.Plaintext) (A : (E.Ciphertext → Core.SPComp (Option E.Plaintext)) → E.Ciphertext → Core.SPComp Bool) : INDCCA_Adv E m₀ m₁ A ≤ (Advantage (INDCCA_Game E m₀ m₁ true A) (INDCCA_rejectGame E m₀ m₁ true A) + INDCPA_Adv E m₀ m₁ fun (c : E.Ciphertext) => A (rejectDecOracle E) c) + Advantage (INDCCA_rejectGame E m₀ m₁ false A) (INDCCA_Game E m₀ m₁ false A)

IND-CCA reduces to IND-CPA plus decryption-oracle integrity. For any encryption scheme, the IND-CCA advantage is bounded by

• the two authenticity gaps — the advantage of distinguishing the real decryption oracle from the always-reject oracle, in each world — plus
• the IND-CPA advantage of the adversary that ignores its (reject) oracle.

This is the standard "authenticated encryption = confidentiality + integrity" decomposition, proved here purely from the triangle inequality for advantage: routing through the two always-reject games, whose difference is an IND-CPA game (INDCCA_rejectGame_eq). The two authenticity gaps are exactly the ciphertext-integrity (MAC-unforgeability) terms.