Authenticated Encryption and Adaptive Chosen-Ciphertext Security

This module formalizes symmetric authenticated encryption (AuthenticatedEncryption) and adaptive chosen-ciphertext security (INDCCA) following Boneh and Shoup, A Graduate Course in Applied Cryptography, Version 0.6, Chapter 5 (Sections 5.3 and 5.10) and Chapter 9 (Sections 9.1 and 9.2.2–9.2.3):

1. Symmetric ciphers and adaptive CPA security (SymmetricCipher, cpaGame, INDCPA, not_indcpa_of_ciphertext_length_eq) ([BS23], Section 5.3, Attack Game 5.2, Definition 5.2, and Example 5.1, printed pp. 181–182; Exercise 5.10(a), printed p. 211): a uniform symmetric cipher on n-bit messages at security parameter n consists of strict PPT key generation keyGen, strict PPT encryption encrypt, and deterministic polynomial-time decryption decrypt returning Option (List Bool) (encoded via encOption encBits). In cpaGame, an adaptive OracleDistinguisher submits left-or-right pairs (m0, m1) of n-bit messages and receives encrypt n k (if bit then m1 else m0). We also formalize Example 5.1 and Exercise 5.10(a) (not_indcpa_of_ciphertext_length_eq): if every supported ciphertext of an n-bit message has length n, decryption completeness forces encrypt to be a deterministic permutation on n-bit strings, which a 2-query CPA adversary (detCPAAdversary) breaks with advantage 1.
2. Ciphertext integrity and authenticated encryption (ciGame, CiphertextIntegrity, AuthenticatedEncryption) ([BS23], Section 9.1, Attack Game 9.1 and Definitions 9.1–9.2, printed pp. 358–359): in ciGame, an adaptive CIAdversary queries an encryption oracle on n-bit messages (logging returned ciphertexts in queriedCiphertexts) and wins by outputting a candidate ciphertext ct such that !queriedCiphertexts.contains ct and (decrypt n k ct).isSome. A cipher provides AuthenticatedEncryption when it satisfies both INDCPA and CiphertextIntegrity.
3. Adaptive chosen-ciphertext security and AE $\Rightarrow$ CCA (ccaGame, INDCCA, ccaToCPAAdversary, ccaToCIAdversary, ccaToCIHiddenBitAdversary, advantage_ccaGame_le, advantage_ccaGame_le_two_mul, AuthenticatedEncryption.indcca) ([BS23], Sections 9.2.2–9.2.3, Attack Game 9.2, Definition 9.5, and Theorem 9.1, printed pp. 362–365): in ccaGame, a two-channel CCAAdversary (Operation = Bool) may interleave left-or-right encryption queries (false, recording challenge ciphertexts) with decryption queries (true, rejecting recorded challenge ciphertexts and returning encOption encBits (decrypt n k ct) on all other ciphertexts). Using the difference lemma (OracleComp.IdenticalUntilBad.advantage_le, [BS23], Theorem 4.7) between ccaGame and ccaRejectGame (where all decryption queries are rejected), we prove that every AuthenticatedEncryption cipher is INDCCA-secure.

The generic Encrypt-then-MAC composition ([BS23], Section 9.4.1, Theorem 9.2, printed pp. 367–368) and its concrete non-vacuous PRF-based cipher instance ([BS23], Section 5.4.1, Example 5.2 and Theorem 5.2, printed pp. 183–187) are planned for PR 3 of #1000.

Specializations and losses relative to Boneh–Shoup Chapter 9

• Fixed n-bit plaintext domain at security parameter n: encryption queries take n-bit messages (msg.length = n in ciGame, m0.length = n ∧ m1.length = n in cpaGame and ccaGame). Malformed encryption queries return [] without invoking encrypt or recording a challenge ciphertext.
• Challenge-ciphertext decryption queries in ccaOracle: in Section 9.2.2 (printed p. 362), the text stipulates that "The restriction we impose is that the adversary may not ask for the decryptions of any of these ciphertexts." In ccaOracle, decryption queries on previously returned challenge ciphertexts (queriedCiphertexts) are instead answered with [] = encOption encBits none (rejection), which is equivalent for adversaries respecting the restriction and makes ccaOracle a total function on all queries.
• Omitted 1AE $\Rightarrow$ 1CCA half and query-count preservation in Theorem 9.1: Theorem 9.1 in [BS23] (printed p. 363) also states that "If E is 1AE-secure, then it is 1CCA-secure." (using Definition 9.6 on p. 363) and that "Moreover, Bcpa and Bci both make at most Qe encryption queries." This module formalizes the multi-query adaptive AuthenticatedEncryption (Definition 9.2) and INDCCA (Definition 9.5) notions and the AE ⇒ CCA implication; the one-time notions (1AE, 1CCA) and a separate encryption-query count preservation theorem are omitted.
• Total-query budget in Theorem 9.1: in equation (9.3) of [BS23] (printed p. 363), the CI term has coefficient 2 * Qd (where Qd bounds decryption queries). Here ccaToCIAdversary samples a query index uniformly from {0, ..., dyadicSize (Q n) - 1} via ProbComp.sampleDyadicIndex (Q n) (where Q n < dyadicSize (Q n) ≤ 2 * Q n + 2) and decrements the countdown on every external oracle call (Sum.inr) of (adversary n []).IsQueryBounded (Q n), where Q n bounds total queries Qe + Qd. This yields factor dyadicSize (Q n) in advantage_ccaGame_le and 2 * dyadicSize (Q n) ≤ 4 * Q n + 4 in advantage_ccaGame_le_two_mul, which remains polynomial in n for AuthenticatedEncryption.indcca.

Main definitions

• Cslib.Crypto.CIAdversary, Cslib.Crypto.CCAAdversary: adaptive ciphertext-integrity and chosen-ciphertext adversaries.
• Cslib.Crypto.SymmetricCipher: uniform symmetric cipher on n-bit messages.
• Cslib.Crypto.SymmetricCipher.cpaGame, INDCPA, detCPAAdversary: adaptive symmetric CPA game, security predicate, and 2-query determinism distinguisher ([BS23], Attack Game 5.2 / Definition 5.2 / Example 5.1).
• Cslib.Crypto.SymmetricCipher.ciGame, CiphertextIntegrity, AuthenticatedEncryption: ciphertext-integrity game, CI predicate, and AE predicate ([BS23], Attack Game 9.1 / Definitions 9.1–9.2).
• Cslib.Crypto.SymmetricCipher.ccaGame, ccaRejectGame, INDCCA: adaptive CCA game, all-reject hybrid game, and CCA security predicate ([BS23], Attack Game 9.2 / Definition 9.5).
• Cslib.Crypto.SymmetricCipher.ccaToCPAAdversary, ccaToCIAdversary, ccaToCIHiddenBitAdversary: Theorem 9.1 reductions from CCA to CPA and CI.

Main results

• Cslib.Crypto.SymmetricCipher.isPPTOn_cpaGame, isPPT_cpaGame, isPPTOn_ciGame, isPPT_ciGame, isPPTOn_ccaGame, isPPT_ccaGame: strict PPT certificates for the CPA, CI, and CCA experiments.
• Cslib.Crypto.SymmetricCipher.encrypt_eq_of_ciphertext_length_eq, Cslib.Crypto.SymmetricCipher.advantage_cpaGame_detCPAAdversary, Cslib.Crypto.SymmetricCipher.not_indcpa_of_ciphertext_length_eq: any cipher whose ciphertexts on n-bit messages have length n is forced by decryption completeness to be deterministic and hence cannot satisfy INDCPA ([BS23], Example 5.1 and Exercise 5.10(a)).
• Cslib.Crypto.SymmetricCipher.isOraclePPT_ccaToCPAAdversary, Cslib.Crypto.SymmetricCipher.isOraclePPT_ccaToCIAdversary, Cslib.Crypto.SymmetricCipher.isOraclePPT_ccaToCIHiddenBitAdversary: IsOraclePPT certificates for the Theorem 9.1 reductions.
• Cslib.Crypto.SymmetricCipher.advantage_ccaGame_le, Cslib.Crypto.SymmetricCipher.advantage_ccaGame_le_two_mul, Cslib.Crypto.SymmetricCipher.AuthenticatedEncryption.indcca: quantitative and asymptotic AE $\Rightarrow$ CCA security ([BS23], Theorem 9.1).

References

• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Version 0.6, Section 5.3 (pp. 181–182), Exercise 5.10(a) (p. 211), and Chapter 9, Sections 9.1 and 9.2.2–9.2.3 (pp. 357–365).

@[reducible, inline]

abbrev Cslib.Crypto.CIAdversary : Type

An adaptive ciphertext-integrity adversary receives the unary security parameter and an auxiliary word, queries an encryption oracle on chosen messages, and outputs a candidate ciphertext.

@[reducible, inline]

abbrev Cslib.Crypto.CCAAdversary : Type

An adaptive chosen-ciphertext distinguisher receives the unary security parameter and an auxiliary word, queries a left-or-right encryption oracle (false) and a decryption oracle (true), and outputs a distinguishing bit.

structure Cslib.Crypto.SymmetricCipher : Type

A uniform symmetric cipher on n-bit messages at security parameter n, with strict probabilistic polynomial-time key generation and encryption, deterministic polynomial-time decryption (returning Option (List Bool)), and perfect decryption completeness on supported keys, n-bit messages, and ciphertexts ([BS23], Sections 5.3 and 9.1).

• keyGen : ℕ → ProbComp (List Bool)

  Sample a symmetric secret key k at unary security parameter n.

• encrypt : ℕ → List Bool → List Bool → ProbComp (List Bool)

  Probabilistically encrypt a message msg under secret key k at security parameter n.

• decrypt : ℕ → List Bool → List Bool → Option (List Bool)

  Deterministically decrypt a candidate ciphertext ct under secret key k at parameter n, returning none on rejection and some msg on acceptance.

• keyGen_ppt : Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits self.keyGen

  Key generation is uniformly strict PPT in the unary security parameter.

• encrypt_ppt : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits fun (p : ℕ × List Bool × List Bool) => self.encrypt p.1 p.2.1 p.2.2

  Encryption is uniformly strict PPT in (n, k, msg).

• decrypt_polyTime : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool × List Bool) => self.decrypt p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) (Turing.MultiTapeTM.encOption Turing.MultiTapeTM.encBits)

  Decryption is computable in plain polynomial time on (n, k, ct).

• decrypt_encrypt (n : ℕ) (k : List Bool) : k ∈ (self.keyGen n).eval.support → ∀ (msg : List Bool), msg.length = n → ∀ ct ∈ (self.encrypt n k msg).eval.support, self.decrypt n k ct = some msg

  Every ciphertext produced by encrypt on an n-bit message under a supported secret key at security parameter n decrypts to some msg.

theorem Cslib.Crypto.SymmetricCipher.isPPTOn_keyGen_comp (E : SymmetricCipher) {γ : Type} {encIn : γ ↪ List Bool} {n : γ → ℕ} (hn : Turing.MultiTapeTM.ComputableInPolyTime n encIn Turing.MultiTapeTM.encUnary) : Probability.IsPPTOn encIn Turing.MultiTapeTM.encBits fun (a : γ) => E.keyGen (n a)

E.keyGen composed with a plain polynomial-time parameter selector is uniformly strict PPT.

theorem Cslib.Crypto.SymmetricCipher.isPPTOn_encrypt_comp (E : SymmetricCipher) {γ : Type} {encIn : γ ↪ List Bool} {n : γ → ℕ} {k msg : γ → List Bool} (hn : Turing.MultiTapeTM.ComputableInPolyTime n encIn Turing.MultiTapeTM.encUnary) (hk : Turing.MultiTapeTM.ComputableInPolyTime k encIn Turing.MultiTapeTM.encBits) (hmsg : Turing.MultiTapeTM.ComputableInPolyTime msg encIn Turing.MultiTapeTM.encBits) : Probability.IsPPTOn encIn Turing.MultiTapeTM.encBits fun (a : γ) => E.encrypt (n a) (k a) (msg a)

E.encrypt composed with plain polynomial-time parameter, key, and message selectors is uniformly strict PPT.

theorem Cslib.Crypto.SymmetricCipher.computableInPolyTime_decrypt_comp (E : SymmetricCipher) {γ : Type} {encIn : γ ↪ List Bool} {n : γ → ℕ} {k ct : γ → List Bool} (hn : Turing.MultiTapeTM.ComputableInPolyTime n encIn Turing.MultiTapeTM.encUnary) (hk : Turing.MultiTapeTM.ComputableInPolyTime k encIn Turing.MultiTapeTM.encBits) (hct : Turing.MultiTapeTM.ComputableInPolyTime ct encIn Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ) => E.decrypt (n a) (k a) (ct a)) encIn (Turing.MultiTapeTM.encOption Turing.MultiTapeTM.encBits)

E.decrypt composed with plain polynomial-time parameter, key, and ciphertext selectors is computable in plain polynomial time.

Adaptive Chosen-Plaintext Security (cpaGame, INDCPA)

noncomputable def Cslib.Crypto.SymmetricCipher.cpaEncryptionOracle (E : SymmetricCipher) (n : ℕ) (k : List Bool) (bit : Bool) (request : Unit × List Bool) : StateT Unit ProbComp (List Bool)

Stateful left-or-right CPA encryption oracle ([BS23], Section 5.3, Attack Game 5.2): decode the request into m0 = unframe request.2 and m1 = dropFrame request.2; if both have length n, encrypt if bit then m1 else m0 under k, and otherwise return [].

noncomputable def Cslib.Crypto.SymmetricCipher.cpaGame (E : SymmetricCipher) (adversary : OracleDistinguisher) (bit : Bool) (n : ℕ) : ProbComp Bool

The adaptive symmetric IND-CPA experiment ([BS23], Section 5.3, Attack Game 5.2): sample k ← E.keyGen n and run adversary n [] against E.cpaEncryptionOracle n k bit.

theorem Cslib.Crypto.SymmetricCipher.isPPTOn_run_cpaEncryptionOracle (E : SymmetricCipher) {adversary : OracleDistinguisher} (hadversary : Probability.IsOraclePPT Turing.MultiTapeTM.encBool adversary) (bit : Bool) : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBool (Turing.MultiTapeTM.encFinEnum Unit)) fun (caller : ℕ × List Bool) => (OracleComp.interpret (ProbOracleComp.handler (fun (m : ℕ) => StateT.lift (ProbComp.unifFin m)) (E.cpaEncryptionOracle caller.1 caller.2 bit)) (adversary caller.1 [])).run ()

Running an oracle-PPT distinguisher against cpaEncryptionOracle is uniformly strict PPT in (n, k) for each challenge bit bit.

theorem Cslib.Crypto.SymmetricCipher.isPPTOn_cpaGame (E : SymmetricCipher) {adversary : OracleDistinguisher} (hadversary : Probability.IsOraclePPT Turing.MultiTapeTM.encBool adversary) (bit : Bool) : Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool (E.cpaGame adversary bit)

The symmetric CPA experiment is uniformly strict PPT in the unary security parameter.

theorem Cslib.Crypto.SymmetricCipher.isPPT_cpaGame (E : SymmetricCipher) {adversary : OracleDistinguisher} (hadversary : Probability.IsOraclePPT Turing.MultiTapeTM.encBool adversary) (bit : Bool) : Probability.IsPPT Turing.MultiTapeTM.encBool fun (n : ℕ) (x : List Bool) => E.cpaGame adversary bit n

The symmetric CPA experiment is uniformly strict PPT, independently of unused auxiliary input.

def Cslib.Crypto.SymmetricCipher.INDCPA (E : SymmetricCipher) : Prop

Adaptive chosen-plaintext security (INDCPA) for a symmetric cipher ([BS23], Section 5.3, Attack Game 5.2 and Definition 5.2): every uniform strict IsOraclePPT encBool distinguisher has negligible advantage between E.cpaGame adversary false and E.cpaGame adversary true.

Impossibility of Zero-Expansion CPA Security (Boneh–Shoup Example 5.1 & Exercise 5.10(a))

theorem Cslib.Crypto.SymmetricCipher.encrypt_eq_of_ciphertext_length_eq (E : SymmetricCipher) {n : ℕ} {ke : List Bool} (hke : ke ∈ (E.keyGen n).eval.support) (hctLen : ∀ (msg : List Bool), msg.length = n → ∀ c ∈ (E.encrypt n ke msg).eval.support, c.length = n) {msg : List Bool} (hmsg : msg.length = n) {c₁ c₂ : List Bool} (hc₁ : c₁ ∈ (E.encrypt n ke msg).eval.support) (hc₂ : c₂ ∈ (E.encrypt n ke msg).eval.support) : c₁ = c₂

Zero ciphertext expansion forces deterministic encryption ([BS23], Exercise 5.10(a), printed p. 211): if every supported ciphertext of an n-bit message under a supported key ke at parameter n has length n, then decryption completeness (E.decrypt_encrypt) gives an injection from the 2^n plaintexts BitString n into BitString n by choosing one supported ciphertext per plaintext; by finiteness of BitString n, this map is surjective, forcing all supported ciphertexts of any n-bit plaintext msg under ke to coincide.

def Cslib.Crypto.SymmetricCipher.detCPAAdversary : OracleDistinguisher

Two-query CPA distinguisher against any deterministic symmetric cipher ([BS23], Example 5.1, printed p. 182): queries (0^n, 1^n) followed by (0^n, 0^n) and outputs true iff the two returned ciphertexts are equal (c₁ == c₂).

theorem Cslib.Crypto.SymmetricCipher.isOraclePPT_detCPAAdversary : Probability.IsOraclePPT Turing.MultiTapeTM.encBool detCPAAdversary

detCPAAdversary is uniformly strict oracle-PPT (IsOraclePPT encBool).

theorem Cslib.Crypto.SymmetricCipher.eval_cpaGame_detCPAAdversary_false (E : SymmetricCipher) (n : ℕ) (hctLen : ∀ ke ∈ (E.keyGen n).eval.support, ∀ (msg : List Bool), msg.length = n → ∀ c ∈ (E.encrypt n ke msg).eval.support, c.length = n) : (E.cpaGame detCPAAdversary false n).eval = PMF.pure true

In Experiment false, detCPAAdversary receives two encryptions of 0^n; when all supported ciphertexts of n-bit plaintexts have length n, both encryptions return the same ciphertext and detCPAAdversary outputs true with probability 1.

theorem Cslib.Crypto.SymmetricCipher.eval_cpaGame_detCPAAdversary_true (E : SymmetricCipher) {n : ℕ} (hn : 1 ≤ n) (hctLen : ∀ ke ∈ (E.keyGen n).eval.support, ∀ (msg : List Bool), msg.length = n → ∀ c ∈ (E.encrypt n ke msg).eval.support, c.length = n) : (E.cpaGame detCPAAdversary true n).eval = PMF.pure false

In Experiment true for n ≥ 1, detCPAAdversary receives an encryption of 1^n followed by an encryption of 0^n; by decryption completeness the two ciphertexts are distinct, so detCPAAdversary outputs false with probability 1.

theorem Cslib.Crypto.SymmetricCipher.advantage_cpaGame_detCPAAdversary (E : SymmetricCipher) {n : ℕ} (hn : 1 ≤ n) (hctLen : ∀ ke ∈ (E.keyGen n).eval.support, ∀ (msg : List Bool), msg.length = n → ∀ c ∈ (E.encrypt n ke msg).eval.support, c.length = n) : Game.advantage (E.cpaGame detCPAAdversary false n).eval (E.cpaGame detCPAAdversary true n).eval = 1

At every security parameter n ≥ 1 where supported ciphertexts of n-bit plaintexts have length n, detCPAAdversary achieves CPA advantage 1 ([BS23], Example 5.1).

theorem Cslib.Crypto.SymmetricCipher.not_indcpa_of_ciphertext_length_eq (E : SymmetricCipher) (hctLen : ∀ (n : ℕ), ∀ ke ∈ (E.keyGen n).eval.support, ∀ (msg : List Bool), msg.length = n → ∀ c ∈ (E.encrypt n ke msg).eval.support, c.length = n) : ¬E.INDCPA

No zero-expansion symmetric cipher is CPA-secure ([BS23], Example 5.1 and Exercise 5.10(a), printed pp. 182, 211): if for every security parameter n, every supported key ke, and every n-bit message msg, every supported ciphertext of msg has length n, then E cannot satisfy INDCPA.

Ciphertext Integrity and Authenticated Encryption (ciGame, CiphertextIntegrity,

AuthenticatedEncryption)

noncomputable def Cslib.Crypto.SymmetricCipher.ciEncryptionOracle (E : SymmetricCipher) (n : ℕ) (k : List Bool) (request : Unit × List Bool) : StateT (List (List Bool)) ProbComp (List Bool)

Stateful encryption oracle for the ciphertext-integrity game ([BS23], Section 9.1, Attack Game 9.1): if request.2.length == n, encrypt request.2 under k, prepend the resulting ciphertext to queriedCiphertexts, and return it; otherwise return [] without modifying the ciphertext log.

noncomputable def Cslib.Crypto.SymmetricCipher.ciGame (E : SymmetricCipher) (adversary : CIAdversary) (n : ℕ) : ProbComp Bool

The ciphertext-integrity experiment ([BS23], Section 9.1, Attack Game 9.1): sample k ← E.keyGen n, run adversary n [] with oracle access to E.ciEncryptionOracle n k, and accept when the adversary outputs a candidate ciphertext ct that was never returned by the encryption oracle (!out.2.contains out.1) and decrypts without rejection ((E.decrypt n k out.1).isSome).

theorem Cslib.Crypto.SymmetricCipher.isPPTOn_run_ciEncryptionOracle (E : SymmetricCipher) {adversary : CIAdversary} (hadversary : Probability.IsOraclePPT Turing.MultiTapeTM.encBits adversary) : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) fun (caller : ℕ × List Bool) => (OracleComp.interpret (ProbOracleComp.handler (fun (m : ℕ) => StateT.lift (ProbComp.unifFin m)) (E.ciEncryptionOracle caller.1 caller.2)) (adversary caller.1 [])).run []

Running an oracle-PPT CI adversary against ciEncryptionOracle is uniformly strict PPT in (n, k).

theorem Cslib.Crypto.SymmetricCipher.isPPTOn_ciGame (E : SymmetricCipher) {adversary : CIAdversary} (hadversary : Probability.IsOraclePPT Turing.MultiTapeTM.encBits adversary) : Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool (E.ciGame adversary)

The ciphertext-integrity experiment is uniformly strict PPT in the unary security parameter.

theorem Cslib.Crypto.SymmetricCipher.isPPT_ciGame (E : SymmetricCipher) {adversary : CIAdversary} (hadversary : Probability.IsOraclePPT Turing.MultiTapeTM.encBits adversary) : Probability.IsPPT Turing.MultiTapeTM.encBool fun (n : ℕ) (x : List Bool) => E.ciGame adversary n

The ciphertext-integrity experiment is uniformly strict PPT, independently of unused auxiliary input.

def Cslib.Crypto.SymmetricCipher.CiphertextIntegrity (E : SymmetricCipher) : Prop

Ciphertext integrity (CiphertextIntegrity, or CI) for a symmetric cipher ([BS23], Section 9.1, Attack Game 9.1 and Definition 9.1): every uniform strict IsOraclePPT encBits adversary has negligible probability of outputting a fresh valid ciphertext.

theorem Cslib.Crypto.SymmetricCipher.CiphertextIntegrity.negligible {E : SymmetricCipher} (h : E.CiphertextIntegrity) (adversary : CIAdversary) (hadversary : Probability.IsOraclePPT Turing.MultiTapeTM.encBits adversary) : Negligible fun (n : ℕ) => Game.succProbability (E.ciGame adversary n).eval

Ciphertext integrity gives negligible winning probability in ciGame for every oracle-PPT CI adversary.

theorem Cslib.Crypto.SymmetricCipher.CiphertextIntegrity.of_negligible {E : SymmetricCipher} (h : ∀ (adversary : ℕ → List Bool → Probability.WordOracleComp Unit (List Bool)), Probability.IsOraclePPT Turing.MultiTapeTM.encBits adversary → Negligible fun (n : ℕ) => Game.succProbability (E.ciGame adversary n).eval) : E.CiphertextIntegrity

Establish CiphertextIntegrity by bounding every oracle-PPT CI adversary's winning probability.

def Cslib.Crypto.SymmetricCipher.AuthenticatedEncryption (E : SymmetricCipher) : Prop

Authenticated encryption (AuthenticatedEncryption, or AE-security) for a symmetric cipher ([BS23], Section 9.1, Definition 9.2): the cipher satisfies both INDCPA and CiphertextIntegrity.

Adaptive Chosen-Ciphertext Security (ccaGame, ccaRejectGame, INDCCA)

noncomputable def Cslib.Crypto.SymmetricCipher.ccaOracle (E : SymmetricCipher) (n : ℕ) (k : List Bool) (bit : Bool) (request : Bool × List Bool) : StateT (List (List Bool)) ProbComp (List Bool)

Stateful two-channel oracle for the adaptive chosen-ciphertext experiment ([BS23], Section 9.2.2, Attack Game 9.2):

• On an encryption query (false, req): decode m0 = unframe req and m1 = dropFrame req; if both have length n, encrypt if bit then m1 else m0 under k, prepend the resulting ciphertext ct to queriedCiphertexts, and return ct; otherwise return [].
• On a decryption query (true, ct): if queriedCiphertexts.contains ct is true, return [] (prohibited challenge ciphertext); otherwise return encOption encBits (E.decrypt n k ct).

noncomputable def Cslib.Crypto.SymmetricCipher.ccaGame (E : SymmetricCipher) (adversary : CCAAdversary) (bit : Bool) (n : ℕ) : ProbComp Bool

The adaptive chosen-ciphertext experiment ([BS23], Section 9.2.2, Attack Game 9.2): sample k ← E.keyGen n and run adversary n [] against E.ccaOracle n k bit.

theorem Cslib.Crypto.SymmetricCipher.isPPTOn_run_ccaOracle (E : SymmetricCipher) {adversary : CCAAdversary} (hadversary : Probability.IsOraclePPT Turing.MultiTapeTM.encBool adversary) (bit : Bool) : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBool (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) fun (caller : ℕ × List Bool) => (OracleComp.interpret (ProbOracleComp.handler (fun (m : ℕ) => StateT.lift (ProbComp.unifFin m)) (E.ccaOracle caller.1 caller.2 bit)) (adversary caller.1 [])).run []

Running an oracle-PPT CCA adversary against ccaOracle is uniformly strict PPT in (n, k) for each challenge bit bit.

theorem Cslib.Crypto.SymmetricCipher.isPPTOn_ccaGame (E : SymmetricCipher) {adversary : CCAAdversary} (hadversary : Probability.IsOraclePPT Turing.MultiTapeTM.encBool adversary) (bit : Bool) : Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool (E.ccaGame adversary bit)

The adaptive CCA experiment is uniformly strict PPT in the unary security parameter.

theorem Cslib.Crypto.SymmetricCipher.isPPT_ccaGame (E : SymmetricCipher) {adversary : CCAAdversary} (hadversary : Probability.IsOraclePPT Turing.MultiTapeTM.encBool adversary) (bit : Bool) : Probability.IsPPT Turing.MultiTapeTM.encBool fun (n : ℕ) (x : List Bool) => E.ccaGame adversary bit n

The adaptive CCA experiment is uniformly strict PPT, independently of unused auxiliary input.

def Cslib.Crypto.SymmetricCipher.INDCCA (E : SymmetricCipher) : Prop

Adaptive chosen-ciphertext security (INDCCA, or CCA-security) for a symmetric cipher ([BS23], Section 9.2.2, Attack Game 9.2 and Definition 9.5, printed p. 362): every uniform strict IsOraclePPT encBool CCA adversary has negligible advantage between E.ccaGame adversary false and E.ccaGame adversary true.

In [BS23], Section 9.2.2, Definition 9.5 defines adaptive multi-query CCA security, whereas one-time CCA security (1CCA) is defined separately in Definition 9.6 (printed p. 363).

Authenticated Encryption Implies Adaptive CCA Security (Boneh–Shoup Theorem 9.1)

noncomputable def Cslib.Crypto.SymmetricCipher.ccaRejectOracle (E : SymmetricCipher) (n : ℕ) (k : List Bool) (bit : Bool) (request : Bool × List Bool) : StateT (List (List Bool)) ProbComp (List Bool)

Hybrid two-channel oracle for Game 1 in the proof of [BS23], Theorem 9.1 (Section 9.2.3, printed pp. 363–364): encryption queries (false, req) behave identically to ccaOracle, whereas every decryption query (true, _) immediately returns [] (rejection) without invoking decrypt.

noncomputable def Cslib.Crypto.SymmetricCipher.ccaRejectGame (E : SymmetricCipher) (adversary : CCAAdversary) (bit : Bool) (n : ℕ) : ProbComp Bool

The all-reject hybrid CCA experiment (Game 1 in [BS23], Section 9.2.3, Theorem 9.1): sample k ← E.keyGen n and run adversary n [] against E.ccaRejectOracle n k bit.

noncomputable def Cslib.Crypto.SymmetricCipher.ccaToCPAHandler (n ctBound : ℕ) (request : Bool × List Bool) : StateT Unit (Probability.WordOracleComp Unit) (List Bool)

Stateful handler for ccaToCPAAdversary ([BS23], Section 9.2.3, Theorem 9.1): reject all decryption queries (true, _) with [], and forward valid left-or-right encryption queries (false, req) to the external CPA encryption oracle (truncating replies to ctBound).

noncomputable def Cslib.Crypto.SymmetricCipher.ccaToCPAAdversary (ctBound : ℕ → ℕ) (adversary : CCAAdversary) : OracleDistinguisher

Reduction from the all-reject hybrid ccaRejectGame to the adaptive CPA experiment cpaGame ([BS23], Section 9.2.3, adversary $B_{\mathrm{cpa}}$ in Theorem 9.1): run adversary n [] against ccaToCPAHandler n (ctBound n).

theorem Cslib.Crypto.SymmetricCipher.isOraclePPT_ccaToCPAAdversary {ctBound : ℕ → ℕ} (hctBound : Turing.MultiTapeTM.ComputableInPolyTime ctBound Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) {adversary : CCAAdversary} (hadversary : Probability.IsOraclePPT Turing.MultiTapeTM.encBool adversary) : Probability.IsOraclePPT Turing.MultiTapeTM.encBool (ccaToCPAAdversary ctBound adversary)

ccaToCPAAdversary preserves strict oracle-PPT admissibility (IsOraclePPT).

theorem Cslib.Crypto.SymmetricCipher.eval_cpaGame_ccaToCPAAdversary (E : SymmetricCipher) (ctBound : ℕ → ℕ) (adversary : CCAAdversary) (bit : Bool) (n : ℕ) (hctBound : ∀ k ∈ (E.keyGen n).eval.support, ∀ (msg : List Bool), msg.length = n → ∀ ct ∈ (E.encrypt n k msg).eval.support, ct.length ≤ ctBound n) : (E.cpaGame (ccaToCPAAdversary ctBound adversary) bit n).eval = (E.ccaRejectGame adversary bit n).eval

When ctBound n bounds all ciphertext lengths produced by E.encrypt n k on n-bit messages, running ccaToCPAAdversary ctBound adversary in cpaGame has the exact same output distribution as ccaRejectGame adversary ([BS23], Section 9.2.3, equation (9.7) in the proof of Theorem 9.1, printed p. 365).

noncomputable def Cslib.Crypto.SymmetricCipher.ccaToCIHandler (n ctBound : ℕ) (bit : Bool) (request : Bool × List Bool) : StateT (ℕ × Bool × List Bool) (Probability.WordOracleComp Unit) (List Bool)

Stateful handler for ccaToCIAtIndexAdversary and ccaToCIAdversary ([BS23], Section 9.2.3, adversary $B_{\mathrm{ci}}$ in Theorem 9.1): maintains (rem, (hasCaptured, capturedCt)) : ℕ × (Bool × List Bool).

• Once hasCaptured = true, all subsequent queries return [] without calling the external CI encryption oracle.
• While hasCaptured = false:
  • if rem == 0, a decryption query (true, ct) captures (0, (true, ct)) and an encryption query (false, _) captures (0, (true, [])), both returning [] without calling the external CI oracle;
  • if rem != 0, a decryption query (true, _) returns ([], (rem - 1, (false, []))), and an encryption query (false, req) with (unframe req).length == n && (dropFrame req).length == n queries the external CI encryption oracle on if bit then dropFrame req else unframe req (truncating the reply to ctBound) and transitions to (rem - 1, (false, [])).

noncomputable def Cslib.Crypto.SymmetricCipher.ccaToCIAtIndexAdversary (ctBound : ℕ → ℕ) (j : ℕ) (bit : Bool) (adversary : CCAAdversary) : CIAdversary

Deterministic-index ciphertext-integrity reduction at query countdown j ([BS23], Section 9.2.3, Theorem 9.1): run adversary n [] against ccaToCIHandler n (ctBound n) bit starting from (j, (false, [])) and output the captured ciphertext candidate out.2.2.2.

noncomputable def Cslib.Crypto.SymmetricCipher.ccaToCIAdversary (ctBound Q : ℕ → ℕ) (bit : Bool) (adversary : CCAAdversary) : CIAdversary

Reduction from decryption-oracle forgery in ccaRejectGame to the ciphertext-integrity game ciGame for fixed challenge bit bit ([BS23], Section 9.2.3, adversary $B_{\mathrm{ci}}$ in Theorem 9.1): sample a uniform dyadic query countdown j ← ProbOracleComp.sample (ProbComp.sampleDyadicIndex (Q n)) and run ccaToCIAtIndexAdversary ctBound j bit adversary.

noncomputable def Cslib.Crypto.SymmetricCipher.ccaToCIHiddenBitAdversary (ctBound Q : ℕ → ℕ) (adversary : CCAAdversary) : CIAdversary

Single-adversary ciphertext-integrity reduction that samples a hidden challenge bit uniformly via BitString.sampleList 1 and invokes ccaToCIAdversary ([BS23], Section 9.2.3, proof of Theorem 9.1, printed p. 364).

theorem Cslib.Crypto.SymmetricCipher.isOraclePPT_ccaToCIAdversary {ctBound Q : ℕ → ℕ} (hctBound : Turing.MultiTapeTM.ComputableInPolyTime ctBound Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hQ : Turing.MultiTapeTM.ComputableInPolyTime Q Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (bit : Bool) {adversary : CCAAdversary} (hadversary : Probability.IsOraclePPT Turing.MultiTapeTM.encBool adversary) : Probability.IsOraclePPT Turing.MultiTapeTM.encBits (ccaToCIAdversary ctBound Q bit adversary)

ccaToCIAdversary preserves strict oracle-PPT admissibility (IsOraclePPT).

theorem Cslib.Crypto.SymmetricCipher.isOraclePPT_ccaToCIHiddenBitAdversary {ctBound Q : ℕ → ℕ} (hctBound : Turing.MultiTapeTM.ComputableInPolyTime ctBound Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hQ : Turing.MultiTapeTM.ComputableInPolyTime Q Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) {adversary : CCAAdversary} (hadversary : Probability.IsOraclePPT Turing.MultiTapeTM.encBool adversary) : Probability.IsOraclePPT Turing.MultiTapeTM.encBits (ccaToCIHiddenBitAdversary ctBound Q adversary)

ccaToCIHiddenBitAdversary preserves strict oracle-PPT admissibility (IsOraclePPT).

Difference-Lemma Hop and Query-Budget Induction for Theorem 9.1

theorem Cslib.Crypto.SymmetricCipher.eval_ciGame_ccaToCIAdversary (E : SymmetricCipher) (ctBound Q : ℕ → ℕ) (bit : Bool) (adversary : CCAAdversary) (n : ℕ) : (E.ciGame (ccaToCIAdversary ctBound Q bit adversary) n).eval = (Probability.PMF.uniformOfFintype (Fin (Probability.dyadicSize (Q n)))).bind fun (i : Fin (Probability.dyadicSize (Q n))) => (E.ciGame (ccaToCIAtIndexAdversary ctBound (↑i) bit adversary) n).eval

Running ccaToCIAdversary in ciGame averages ccaToCIAtIndexAdversary uniformly over Fin (dyadicSize (Q n)).

theorem Cslib.Crypto.SymmetricCipher.advantage_ccaGame_le (E : SymmetricCipher) (ctBound Q : ℕ → ℕ) (adversary : CCAAdversary) (n : ℕ) (hq : ProbOracleComp.IsQueryBounded (adversary n []) (Q n)) (hctBound : ∀ k ∈ (E.keyGen n).eval.support, ∀ (msg : List Bool), msg.length = n → ∀ ct ∈ (E.encrypt n k msg).eval.support, ct.length ≤ ctBound n) : ↑(Game.advantage (E.ccaGame adversary false n).eval (E.ccaGame adversary true n).eval) ≤ ↑(Probability.dyadicSize (Q n)) * ↑(Game.succProbability (E.ciGame (ccaToCIAdversary ctBound Q false adversary) n).eval) + ↑(Game.advantage (E.cpaGame (ccaToCPAAdversary ctBound adversary) false n).eval (E.cpaGame (ccaToCPAAdversary ctBound adversary) true n).eval) + ↑(Probability.dyadicSize (Q n)) * ↑(Game.succProbability (E.ciGame (ccaToCIAdversary ctBound Q true adversary) n).eval)

Quantitative AE $\Rightarrow$ CCA bound ([BS23], Section 9.2.3, Theorem 9.1, printed pp. 363–365): for any CCAAdversary making at most Q n total oracle queries at security parameter n, the adaptive CCA distinguishing advantage is bounded by the CPA advantage of ccaToCPAAdversary plus dyadicSize (Q n) times the ciphertext-integrity winning probabilities of ccaToCIAdversary for bit = false and bit = true.

Relative to equation (9.3) in [BS23] (CCAadv[A, E] ≤ CPAadv[Bcpa, E] + 2 Qd · CIadv[Bci, E]), ccaToCIAdversary samples a query index uniformly from {0, ..., dyadicSize (Q n) - 1} over the total query budget Q n ≥ Qe + Qd, giving coefficient dyadicSize (Q n) ≤ 2 * Q n + 2 per bit.

theorem Cslib.Crypto.SymmetricCipher.eval_ciGame_ccaToCIHiddenBitAdversary (E : SymmetricCipher) (ctBound Q : ℕ → ℕ) (adversary : CCAAdversary) (n : ℕ) : (E.ciGame (ccaToCIHiddenBitAdversary ctBound Q adversary) n).eval = (Probability.PMF.uniformOfFintype Bool).bind fun (bit : Bool) => (E.ciGame (ccaToCIAdversary ctBound Q bit adversary) n).eval

Running ccaToCIHiddenBitAdversary in ciGame averages ccaToCIAdversary uniformly over bit : Bool.

theorem Cslib.Crypto.SymmetricCipher.advantage_ccaGame_le_two_mul (E : SymmetricCipher) (ctBound Q : ℕ → ℕ) (adversary : CCAAdversary) (n : ℕ) (hq : ProbOracleComp.IsQueryBounded (adversary n []) (Q n)) (hctBound : ∀ k ∈ (E.keyGen n).eval.support, ∀ (msg : List Bool), msg.length = n → ∀ ct ∈ (E.encrypt n k msg).eval.support, ct.length ≤ ctBound n) : ↑(Game.advantage (E.ccaGame adversary false n).eval (E.ccaGame adversary true n).eval) ≤ 2 * ↑(Probability.dyadicSize (Q n)) * ↑(Game.succProbability (E.ciGame (ccaToCIHiddenBitAdversary ctBound Q adversary) n).eval) + ↑(Game.advantage (E.cpaGame (ccaToCPAAdversary ctBound adversary) false n).eval (E.cpaGame (ccaToCPAAdversary ctBound adversary) true n).eval)

Single-adversary quantitative AE $\Rightarrow$ CCA bound ([BS23], Section 9.2.3, Theorem 9.1, equation (9.3) and proof on printed pp. 363–364): using ccaToCIHiddenBitAdversary to sample the hidden challenge bit uniformly yields factor 2 * dyadicSize (Q n) ≤ 4 * Q n + 4 (over the total query budget Q n, vs. 2 * Qd over decryption queries in (9.3)) on the single CI adversary.

theorem Cslib.Crypto.SymmetricCipher.AuthenticatedEncryption.indcca {E : SymmetricCipher} (hAE : E.AuthenticatedEncryption) : E.INDCCA

Authenticated encryption implies adaptive CCA security ([BS23], Section 9.2.3, Theorem 9.1, printed pp. 363–365): every symmetric cipher satisfying AuthenticatedEncryption (INDCPA ∧ CiphertextIntegrity) also satisfies INDCCA (the multi-query AE ⇒ CCA half of Theorem 9.1; the one-time 1AE ⇒ 1CCA half over Definition 9.6 is omitted).