Encrypt-then-MAC Authenticated Encryption and PRF-Based Instantiation

This module formalizes the generic Encrypt-then-MAC composition (encryptThenMAC) and its security reductions (Boneh and Shoup, A Graduate Course in Applied Cryptography, Version 0.6, Section 9.4.1 and Theorem 9.2, printed pp. 367–368), together with a concrete randomized PRF-based symmetric cipher (prfCipher, [BS23], Section 5.4.1, Example 5.2 and Theorem 5.2, printed pp. 183–189) that witnesses joint non-vacuity of all hypotheses:

1. Generic Encrypt-then-MAC composition (encryptThenMAC, etmToMACForger, etmToCPAAdversary, succProbability_ciGame_encryptThenMAC_eq, advantage_cpaGame_encryptThenMAC_eq, ciphertextIntegrity_encryptThenMAC, indcpa_encryptThenMAC, authenticatedEncryption_encryptThenMAC, indcca_encryptThenMAC) ([BS23], Section 9.4.1, Theorem 9.2, printed pp. 367–368): given a symmetric cipher E : SymmetricCipher whose ciphertexts on n-bit plaintexts under supported keys at security parameter n have length M.msgLen n, and a message authentication code M : MACScheme authenticating M.msgLen n-bit messages:
   • keyGen n samples independent keys ke ← E.keyGen n and km ← M.keyGen n and encodes the pair as encPair encBits encBits (ke, km).
   • encrypt n k msg encrypts c ← E.encrypt n (unframe k) msg, signs tag ← M.sign (dropFrame k) c, and returns encPair encBits encBits (c, tag).
   • decrypt n k ct checks canonical pair framing encPair encBits encBits (unframe ct, dropFrame ct) == ct, checks (unframe ct).length == M.msgLen n, and verifies M.verify (dropFrame k) (unframe ct) (dropFrame ct); if all three hold, it returns E.decrypt n (unframe k) (unframe ct), and otherwise none. Because encPair encBits encBits is injective, ciphertext freshness in ciGame coincides with message-tag pair freshness in M.sufCmaGame, yielding exact per-parameter equalities for both ciphertext integrity (succProbability_ciGame_encryptThenMAC_eq) and CPA advantage (advantage_cpaGame_encryptThenMAC_eq). Combining Theorem 9.2 with Theorem 9.1 (AuthenticatedEncryption.indcca) yields indcca_encryptThenMAC, and combining with MACScheme.reindex on prfMAC yields authenticatedEncryption_encryptThenMAC_prfMAC and indcca_encryptThenMAC_prfMAC.
2. Concrete non-vacuous PRF-based symmetric cipher and end-to-end Encrypt-then-MAC instance (prfCipher, cpaToPrfDistinguisher, advantage_cpaGame_prfCipher_le, PseudorandomFunction.indcpa_prfCipher, prfEncryptThenMAC, PseudorandomFunction.authenticatedEncryption_prfEncryptThenMAC, PseudorandomFunction.indcca_prfEncryptThenMAC) ([BS23], Section 5.4.1, Example 5.2 and Theorem 5.2, printed pp. 183–189): for any PseudorandomFunction family, prfCipher encrypts an n-bit message msg under an n-bit key k by sampling a random nonce r ← BitString.sampleList n and outputting the 2 * n-bit ciphertext r ++ List.zipWith xor (family k r) msg. Using OracleComp.IdenticalUntilBad.advantage_le between the lazy random-function game (Boneh–Shoup Game 2, "faithful gnome") and the fresh one-time-pad game (Boneh–Shoup Game 3, "forgetful gnome"), we prove the quantitative CPA bound of Theorem 5.2 and derive PseudorandomFunction.indcpa_prfCipher. Combining prfCipher with (prfMAC family hprf.polyTime).reindex (fun n => 2 * n) _ produces prfEncryptThenMAC, which satisfies AuthenticatedEncryption and INDCCA assuming only PseudorandomFunction family.

Specializations and omissions relative to Boneh–Shoup Section 9.4.1 and Section 5.4.1

• Ciphertext-length compatibility (c.length = M.msgLen n): in Section 9.4.1 (printed p. 367), E is defined over (Ke, M, C) and I over (Km, C, T). Here plaintexts at security parameter n have length n and ciphertexts under supported keys have length M.msgLen n. Because (M.reindex ctLen hctLen).msgLen n = M.msgLen (ctLen n), reindexing M by ctLen supplies message length ctLen n when the base MAC has M.msgLen = id (as holds for prfMAC), while transferring M.SUFCMA to (M.reindex ctLen hctLen).SUFCMA via MACScheme.SUFCMA.reindex additionally requires StrictMono ctLen (both hold for prfEncryptThenMAC with ctLen := fun n => 2 * n).
• Omitted 1AE half and query-count preservation in Theorem 9.2: Theorem 9.2 in [BS23] (printed p. 367) also states that "Also, EEtM is 1AE-secure assuming E is semantically secure and I is a one-time secure MAC system." and that Bmac (resp. Bcpa) "makes no more signing queries than Aci makes encryption queries" (resp. "makes no more encryption queries than does Acpa"). This module formalizes the multi-query adaptive AuthenticatedEncryption and INDCCA statements; the one-time 1AE half and separate query-count preservation theorems are omitted.
• Specialization of Theorem 5.2 to the Example 5.2 one-time-pad instantiation (prfCipher) and two-world CPA bound with a factor-2 collision term: Theorem 5.2 in [BS23] (printed p. 184; proof on printed pp. 184–189) is stated for the general hybrid cipher E' combining a PRF F with a semantically secure cipher E, with bound CPAadv[A, E'] <= Q^2 / N + 2 * PRFadv[B_F, F] + Q * SSadv[B_E, E] in the bit-guessing CPA game (where Q^2 / N arises from the birthday bound Pr[Z] <= Q^2 / (2 * N) in equation (5.11) on printed p. 187). Here prfCipher formalizes the Example 5.2 instantiation (printed pp. 183–184) where E is the one-time pad k xor m on {0, 1}^n (SSadv = 0, N = 2^n), and advantage_cpaGame_prfCipher_le bounds two-world cpaGame distinguishing advantage by PRFadv[cpaToPrfDistinguisher adversary false, F] + PRFadv[cpaToPrfDistinguisher adversary true, F] + 2 * Q^2 / 2^n: it uses two fixed-bit PRF distinguishers instead of one coin-flipping distinguisher B_F with factor 2, and its collision term 2 * Q^2 / 2^n is 2× the source's Q^2 / N = Q^2 / 2^n because bad_prfCipherForgetfulWithBadOracle_le uses a per-step union bound Q * Q / 2^n per challenge bit rather than the birthday sum sum_{i < Q} i / 2^n <= Q^2 / 2^(n + 1).

Main definitions

• Cslib.Crypto.encryptThenMAC: generic Encrypt-then-MAC symmetric cipher (Section 9.4.1).
• Cslib.Crypto.etmToMACHandler, Cslib.Crypto.etmToMACForger: ciphertext-integrity to SUF-CMA forger reduction (Theorem 9.2, Part 1).
• Cslib.Crypto.etmToCPAHandler, Cslib.Crypto.etmToCPAAdversary: IND-CPA reduction for encryptThenMAC (Theorem 9.2, Part 2).
• Cslib.Crypto.prfCipher: concrete randomized PRF-based symmetric cipher with 2 * n-bit ciphertexts (Example 5.2).
• Cslib.Crypto.cpaToPrfHandler, Cslib.Crypto.cpaToPrfDistinguisher: CPA-to-PRF distinguisher reduction for prfCipher (Theorem 5.2, Figure 5.1).
• Cslib.Crypto.prfEncryptThenMAC: concrete Encrypt-then-MAC cipher combining prfCipher with reindexed prfMAC on 2 * n-bit ciphertexts.

Main results

• Cslib.Crypto.isOraclePPT_etmToMACForger, Cslib.Crypto.eval_sufCmaGame_etmToMACForger, Cslib.Crypto.succProbability_ciGame_encryptThenMAC_eq: exact CI-to-MAC reduction (CIadv = MACadv).
• Cslib.Crypto.isOraclePPT_etmToCPAAdversary, Cslib.Crypto.eval_cpaGame_etmToCPAAdversary, Cslib.Crypto.advantage_cpaGame_encryptThenMAC_eq: exact CPA reduction (CPAadv = CPAadv).
• Cslib.Crypto.ciphertextIntegrity_encryptThenMAC, Cslib.Crypto.indcpa_encryptThenMAC, Cslib.Crypto.authenticatedEncryption_encryptThenMAC, Cslib.Crypto.indcca_encryptThenMAC, Cslib.Crypto.authenticatedEncryption_encryptThenMAC_prfMAC, Cslib.Crypto.indcca_encryptThenMAC_prfMAC: asymptotic AE and IND-CCA security of Encrypt-then-MAC (Theorem 9.2 and Theorem 9.1).
• Cslib.Crypto.prfCipher_ciphertext_length, Cslib.Crypto.isOraclePPT_cpaToPrfDistinguisher, Cslib.Crypto.eval_prfRealGame_cpaToPrfDistinguisher, Cslib.Crypto.advantage_cpaGame_prfCipher_le, Cslib.Crypto.PseudorandomFunction.indcpa_prfCipher: quantitative and asymptotic IND-CPA security of prfCipher (Theorem 5.2).
• Cslib.Crypto.PseudorandomFunction.authenticatedEncryption_prfEncryptThenMAC, Cslib.Crypto.PseudorandomFunction.indcca_prfEncryptThenMAC: non-vacuous end-to-end AE and IND-CCA security of prfEncryptThenMAC from PseudorandomFunction family.

References

• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Version 0.6, Section 5.4.1 (Example 5.2, Theorem 5.2, printed pp. 183–189) and Section 9.4.1 (Theorem 9.2, printed pp. 367–368).

Generic Encrypt-then-MAC Construction and Security (Boneh–Shoup Section 9.4.1)

noncomputable def Cslib.Crypto.encryptThenMAC (E : SymmetricCipher) (M : MACScheme) (hctLen : ∀ (n : ℕ), ∀ ke ∈ (E.keyGen n).eval.support, ∀ (msg : List Bool), msg.length = n → ∀ c ∈ (E.encrypt n ke msg).eval.support, c.length = M.msgLen n) : SymmetricCipher

Encrypt-then-MAC symmetric cipher ([BS23], Section 9.4.1, printed p. 367): given a symmetric cipher E : SymmetricCipher whose ciphertexts on n-bit messages under supported keys at security parameter n have length M.msgLen n, and a message authentication code M : MACScheme on M.msgLen n-bit messages:

• keyGen n samples independent keys ke ← E.keyGen n and km ← M.keyGen n and returns encPair encBits encBits (ke, km).
• encrypt n k msg encrypts c ← E.encrypt n (unframe k) msg, computes a tag tag ← M.sign (dropFrame k) c, and returns encPair encBits encBits (c, tag).
• decrypt n k ct checks canonical pair framing encPair encBits encBits (unframe ct, dropFrame ct) == ct, checks (unframe ct).length == M.msgLen n, and verifies M.verify (dropFrame k) (unframe ct) (dropFrame ct); if all three hold, it returns E.decrypt n (unframe k) (unframe ct), and otherwise none.

Canonical pair framing encPair encBits encBits (c, tag) establishes a bijection between valid encoded ciphertexts ct and pairs (c, tag) with c.length = M.msgLen n, so ciphertext freshness in ciGame coincides with pair freshness in M.sufCmaGame.

Ciphertext-Integrity to SUF-CMA Reduction for Theorem 9.2

noncomputable def Cslib.Crypto.etmToMACHandler (E : SymmetricCipher) (n tagBound : ℕ) (ke : List Bool) (request : Unit × List Bool) : StateT Unit (Probability.WordOracleComp Unit) (List Bool)

Open stateful handler that simulates the ciEncryptionOracle of encryptThenMAC E M inside M.sufCmaGame ([BS23], Section 9.4.1, Theorem 9.2, Part 1): on an n-bit message query request.2, it encrypts c ← E.encrypt n ke request.2, queries the external MAC signing oracle on ((), c) (truncating the returned tag to tagBound bits), and returns encPair encBits encBits (c, tag).

noncomputable def Cslib.Crypto.etmToMACForger (E : SymmetricCipher) (M : MACScheme) (tagBound : ℕ → ℕ) (adversary : CIAdversary) : Forger

Ciphertext-integrity to SUF-CMA reduction etmToMACForger ([BS23], Section 9.4.1, Theorem 9.2, Part 1, printed pp. 367–368): samples ke ← E.keyGen n, runs adversary n [] against etmToMACHandler E n (tagBound n) ke, and when the candidate ciphertext out.1 has canonical pair framing and E.decrypt n ke (unframe out.1) succeeds, outputs the candidate forgery pair (unframe out.1, dropFrame out.1); otherwise outputs a dummy pair of first-component length ≠ M.msgLen n that is rejected by M.sufCmaGame.

theorem Cslib.Crypto.isOraclePPT_etmToMACForger (E : SymmetricCipher) (M : MACScheme) {tagBound : ℕ → ℕ} {adversary : CIAdversary} (htagBound : Turing.MultiTapeTM.ComputableInPolyTime tagBound Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hadversary : Probability.IsOraclePPT Turing.MultiTapeTM.encBits adversary) : Probability.IsOraclePPT (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (etmToMACForger E M tagBound adversary)

etmToMACForger preserves strict oracle-PPT admissibility (IsOraclePPT).

theorem Cslib.Crypto.eval_sufCmaGame_etmToMACForger (E : SymmetricCipher) (M : MACScheme) (hctLen : ∀ (n : ℕ), ∀ ke ∈ (E.keyGen n).eval.support, ∀ (msg : List Bool), msg.length = n → ∀ c ∈ (E.encrypt n ke msg).eval.support, c.length = M.msgLen n) (tagBound : ℕ → ℕ) (adversary : CIAdversary) (n : ℕ) (htagBound : ∀ km ∈ (M.keyGen n).eval.support, ∀ (c : List Bool), c.length = M.msgLen n → ∀ tag ∈ (M.sign km c).eval.support, tag.length ≤ tagBound n) : (M.sufCmaGame (etmToMACForger E M tagBound adversary) n).eval = ((encryptThenMAC E M hctLen).ciGame adversary n).eval

Running etmToMACForger E M tagBound adversary in M.sufCmaGame produces the exact same winning distribution as running adversary in (encryptThenMAC E M hctLen).ciGame whenever tagBound n bounds all MAC tag lengths on M.msgLen n-bit ciphertexts under supported keys at security parameter n.

theorem Cslib.Crypto.succProbability_ciGame_encryptThenMAC_eq (E : SymmetricCipher) (M : MACScheme) (hctLen : ∀ (n : ℕ), ∀ ke ∈ (E.keyGen n).eval.support, ∀ (msg : List Bool), msg.length = n → ∀ c ∈ (E.encrypt n ke msg).eval.support, c.length = M.msgLen n) (tagBound : ℕ → ℕ) (adversary : CIAdversary) (n : ℕ) (htagBound : ∀ km ∈ (M.keyGen n).eval.support, ∀ (c : List Bool), c.length = M.msgLen n → ∀ tag ∈ (M.sign km c).eval.support, tag.length ≤ tagBound n) : Game.succProbability ((encryptThenMAC E M hctLen).ciGame adversary n).eval = Game.succProbability (M.sufCmaGame (etmToMACForger E M tagBound adversary) n).eval

Quantitative Ciphertext-Integrity to SUF-CMA equality ([BS23], Section 9.4.1, Theorem 9.2, Part 1, printed pp. 367–368): when tagBound n bounds all MAC tag lengths on M.msgLen n-bit ciphertexts under supported keys at security parameter n, the ciphertext-integrity winning probability of adversary against encryptThenMAC E M hctLen equals the SUF-CMA winning probability of etmToMACForger E M tagBound adversary against M (CIadv[Aci, EEtM] = MACadv[Bmac, I]).

IND-CPA Reduction for Theorem 9.2

noncomputable def Cslib.Crypto.etmToCPAHandler (M : MACScheme) (n : ℕ) (km : List Bool) (request : Unit × List Bool) : StateT Unit (Probability.WordOracleComp Unit) (List Bool)

Open stateful handler that simulates the cpaEncryptionOracle of encryptThenMAC E M inside E.cpaGame ([BS23], Section 9.4.1, Theorem 9.2, Part 2): on a valid pair of n-bit messages request.2, it forwards request to the external CPA encryption oracle of E (truncating the returned ciphertext c to M.msgLen n bits), computes tag ← M.sign km c, and returns encPair encBits encBits (c, tag).

noncomputable def Cslib.Crypto.etmToCPAAdversary (M : MACScheme) (adversary : OracleDistinguisher) : OracleDistinguisher

IND-CPA reduction etmToCPAAdversary for encryptThenMAC E M ([BS23], Section 9.4.1, Theorem 9.2, Part 2, printed pp. 367–368): samples a secret MAC key km ← M.keyGen n privately and runs adversary n [] against etmToCPAHandler M n km.

theorem Cslib.Crypto.isOraclePPT_etmToCPAAdversary (M : MACScheme) {adversary : OracleDistinguisher} (hadversary : Probability.IsOraclePPT Turing.MultiTapeTM.encBool adversary) : Probability.IsOraclePPT Turing.MultiTapeTM.encBool (etmToCPAAdversary M adversary)

etmToCPAAdversary preserves strict oracle-PPT admissibility (IsOraclePPT).

theorem Cslib.Crypto.eval_cpaGame_etmToCPAAdversary (E : SymmetricCipher) (M : MACScheme) (hctLen : ∀ (n : ℕ), ∀ ke ∈ (E.keyGen n).eval.support, ∀ (msg : List Bool), msg.length = n → ∀ c ∈ (E.encrypt n ke msg).eval.support, c.length = M.msgLen n) (adversary : OracleDistinguisher) (bit : Bool) (n : ℕ) : (E.cpaGame (etmToCPAAdversary M adversary) bit n).eval = ((encryptThenMAC E M hctLen).cpaGame adversary bit n).eval

Running etmToCPAAdversary M adversary in E.cpaGame at challenge bit bit produces the exact same output distribution as running adversary in (encryptThenMAC E M hctLen).cpaGame at challenge bit bit.

theorem Cslib.Crypto.advantage_cpaGame_encryptThenMAC_eq (E : SymmetricCipher) (M : MACScheme) (hctLen : ∀ (n : ℕ), ∀ ke ∈ (E.keyGen n).eval.support, ∀ (msg : List Bool), msg.length = n → ∀ c ∈ (E.encrypt n ke msg).eval.support, c.length = M.msgLen n) (adversary : OracleDistinguisher) (n : ℕ) : Game.advantage ((encryptThenMAC E M hctLen).cpaGame adversary false n).eval ((encryptThenMAC E M hctLen).cpaGame adversary true n).eval = Game.advantage (E.cpaGame (etmToCPAAdversary M adversary) false n).eval (E.cpaGame (etmToCPAAdversary M adversary) true n).eval

Quantitative IND-CPA equality for Encrypt-then-MAC ([BS23], Section 9.4.1, Theorem 9.2, Part 2, printed pp. 367–368): the CPA distinguishing advantage of adversary against encryptThenMAC E M hctLen equals the CPA distinguishing advantage of etmToCPAAdversary M adversary against E (CPAadv[Acpa, EEtM] = CPAadv[Bcpa, E]).

Asymptotic Security of Encrypt-then-MAC (Boneh–Shoup Theorem 9.2)

theorem Cslib.Crypto.ciphertextIntegrity_encryptThenMAC (E : SymmetricCipher) (M : MACScheme) (hctLen : ∀ (n : ℕ), ∀ ke ∈ (E.keyGen n).eval.support, ∀ (msg : List Bool), msg.length = n → ∀ c ∈ (E.encrypt n ke msg).eval.support, c.length = M.msgLen n) (hmac : M.SUFCMA) : (encryptThenMAC E M hctLen).CiphertextIntegrity

SUF-CMA security implies Ciphertext Integrity for Encrypt-then-MAC ([BS23], Section 9.4.1, Theorem 9.2, Part 1, printed pp. 367–368): if M is strongly unforgeable (M.SUFCMA), then encryptThenMAC E M hctLen satisfies CiphertextIntegrity.

theorem Cslib.Crypto.indcpa_encryptThenMAC (E : SymmetricCipher) (M : MACScheme) (hctLen : ∀ (n : ℕ), ∀ ke ∈ (E.keyGen n).eval.support, ∀ (msg : List Bool), msg.length = n → ∀ c ∈ (E.encrypt n ke msg).eval.support, c.length = M.msgLen n) (hcpa : E.INDCPA) : (encryptThenMAC E M hctLen).INDCPA

IND-CPA security transfers to Encrypt-then-MAC ([BS23], Section 9.4.1, Theorem 9.2, Part 2, printed pp. 367–368): if E satisfies INDCPA, then encryptThenMAC E M hctLen also satisfies INDCPA.

theorem Cslib.Crypto.authenticatedEncryption_encryptThenMAC (E : SymmetricCipher) (M : MACScheme) (hctLen : ∀ (n : ℕ), ∀ ke ∈ (E.keyGen n).eval.support, ∀ (msg : List Bool), msg.length = n → ∀ c ∈ (E.encrypt n ke msg).eval.support, c.length = M.msgLen n) (hcpa : E.INDCPA) (hmac : M.SUFCMA) : (encryptThenMAC E M hctLen).AuthenticatedEncryption

Encrypt-then-MAC Authenticated Encryption Theorem ([BS23], Section 9.4.1, Theorem 9.2, printed pp. 367–368): if E is INDCPA-secure and M is SUFCMA-secure, then encryptThenMAC E M hctLen is an AuthenticatedEncryption cipher (INDCPA ∧ CiphertextIntegrity).

theorem Cslib.Crypto.indcca_encryptThenMAC (E : SymmetricCipher) (M : MACScheme) (hctLen : ∀ (n : ℕ), ∀ ke ∈ (E.keyGen n).eval.support, ∀ (msg : List Bool), msg.length = n → ∀ c ∈ (E.encrypt n ke msg).eval.support, c.length = M.msgLen n) (hcpa : E.INDCPA) (hmac : M.SUFCMA) : (encryptThenMAC E M hctLen).INDCCA

Encrypt-then-MAC Adaptive Chosen-Ciphertext Security ([BS23], combining Theorem 9.2 and Theorem 9.1): if E is INDCPA-secure and M is SUFCMA-secure, then encryptThenMAC E M hctLen is INDCCA-secure.

theorem Cslib.Crypto.authenticatedEncryption_encryptThenMAC_prfMAC (E : SymmetricCipher) {family : List Bool → List Bool → List Bool} (hprf : PseudorandomFunction family) {ctLen : ℕ → ℕ} (hctPoly : Turing.MultiTapeTM.ComputableInPolyTime ctLen Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hctMono : StrictMono ctLen) (hctLen : ∀ (n : ℕ), ∀ ke ∈ (E.keyGen n).eval.support, ∀ (msg : List Bool), msg.length = n → ∀ c ∈ (E.encrypt n ke msg).eval.support, c.length = ctLen n) (hcpa : E.INDCPA) : (encryptThenMAC E ((prfMAC family ⋯).reindex ctLen hctPoly) hctLen).AuthenticatedEncryption

Encrypt-then-MAC with a reindexed PRF-based MAC is Authenticated Encryption ([BS23], combining Theorem 6.2 and Theorem 9.2): if E is INDCPA-secure with ciphertext-length schedule ctLen (strictly monotone and computable in plain polynomial time) and family is a uniform PseudorandomFunction, then encryptThenMAC E ((prfMAC family hprf.polyTime).reindex ctLen hctPoly) hctLen satisfies AuthenticatedEncryption.

theorem Cslib.Crypto.indcca_encryptThenMAC_prfMAC (E : SymmetricCipher) {family : List Bool → List Bool → List Bool} (hprf : PseudorandomFunction family) {ctLen : ℕ → ℕ} (hctPoly : Turing.MultiTapeTM.ComputableInPolyTime ctLen Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hctMono : StrictMono ctLen) (hctLen : ∀ (n : ℕ), ∀ ke ∈ (E.keyGen n).eval.support, ∀ (msg : List Bool), msg.length = n → ∀ c ∈ (E.encrypt n ke msg).eval.support, c.length = ctLen n) (hcpa : E.INDCPA) : (encryptThenMAC E ((prfMAC family ⋯).reindex ctLen hctPoly) hctLen).INDCCA

Encrypt-then-MAC with a reindexed PRF-based MAC is IND-CCA secure ([BS23], combining Theorem 6.2, Theorem 9.2, and Theorem 9.1): if E is INDCPA-secure with ciphertext-length schedule ctLen (strictly monotone and computable in plain polynomial time) and family is a uniform PseudorandomFunction, then encryptThenMAC E ((prfMAC family hprf.polyTime).reindex ctLen hctPoly) hctLen satisfies INDCCA.

Concrete Non-Vacuous PRF-Based Cipher (Boneh–Shoup Example 5.2 & Theorem 5.2)

noncomputable def Cslib.Crypto.prfCipher (family : List Bool → List Bool → List Bool) (hpoly : Turing.MultiTapeTM.ComputableInPolyTime (fun (pair : List Bool × List Bool) => family pair.1 pair.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hlen : ∀ (key query : List Bool), query.length = key.length → (family key query).length = key.length) : SymmetricCipher

Randomized PRF-based symmetric cipher ([BS23], Section 5.4.1, Example 5.2 and Theorem 5.2, printed pp. 183–189): given a keyed function family family : List Bool → List Bool → List Bool computable in plain polynomial time that maps n-bit keys and n-bit inputs to n-bit outputs:

• keyGen n samples a uniform n-bit key k ← BitString.sampleList n.
• encrypt n k msg samples a uniform n-bit nonce r ← BitString.sampleList n and outputs the 2 * n-bit ciphertext r ++ List.zipWith xor (family k r) msg.
• decrypt n k ct checks ct.length == 2 * n; if so, splits r := ct.take n and c := ct.drop n and outputs some (List.zipWith xor (family k r) c), and otherwise outputs none.

theorem Cslib.Crypto.prfCipher_ciphertext_length (family : List Bool → List Bool → List Bool) (hpoly : Turing.MultiTapeTM.ComputableInPolyTime (fun (pair : List Bool × List Bool) => family pair.1 pair.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hlen : ∀ (key query : List Bool), query.length = key.length → (family key query).length = key.length) (n : ℕ) (k : List Bool) (hk : k ∈ ((prfCipher family hpoly hlen).keyGen n).eval.support) (msg : List Bool) (hmsg : msg.length = n) (ct : List Bool) (hct : ct ∈ ((prfCipher family hpoly hlen).encrypt n k msg).eval.support) : ct.length = 2 * n

Every supported ciphertext of prfCipher family hpoly hlen on an n-bit plaintext under a supported key at security parameter n has length 2 * n.

CPA-to-PRF Reduction and Game Hops for Theorem 5.2

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

Open stateful handler that simulates the cpaEncryptionOracle of prfCipher inside the PRF distinguishing experiment ([BS23], Section 5.4.1, Theorem 5.2, Figure 5.1, printed pp. 185–186): on a pair of n-bit messages (m0, m1), it samples a random nonce r ← BitString.sampleList n, queries the external PRF/random-function oracle at ((), r) (truncating the returned pad to n bits), and returns r ++ List.zipWith xor pad msg where msg := if bit then m1 else m0.

noncomputable def Cslib.Crypto.cpaToPrfDistinguisher (adversary : OracleDistinguisher) (bit : Bool) : OracleDistinguisher

CPA-to-PRF reduction cpaToPrfDistinguisher ([BS23], Section 5.4.1, Theorem 5.2, Figure 5.1, printed pp. 185–186): runs adversary n [] against cpaToPrfHandler n bit.

theorem Cslib.Crypto.isOraclePPT_cpaToPrfDistinguisher {adversary : OracleDistinguisher} (hadversary : Probability.IsOraclePPT Turing.MultiTapeTM.encBool adversary) (bit : Bool) : Probability.IsOraclePPT Turing.MultiTapeTM.encBool (cpaToPrfDistinguisher adversary bit)

cpaToPrfDistinguisher preserves strict oracle-PPT admissibility (IsOraclePPT).

theorem Cslib.Crypto.eval_prfRealGame_cpaToPrfDistinguisher (family : List Bool → List Bool → List Bool) (hpoly : Turing.MultiTapeTM.ComputableInPolyTime (fun (pair : List Bool × List Bool) => family pair.1 pair.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hlen : ∀ (key query : List Bool), query.length = key.length → (family key query).length = key.length) (adversary : OracleDistinguisher) (bit : Bool) (n : ℕ) : (prfRealGame family (cpaToPrfDistinguisher adversary bit) n).eval = ((prfCipher family hpoly hlen).cpaGame adversary bit n).eval

Running cpaToPrfDistinguisher adversary bit in prfRealGame family produces the exact same output distribution as running adversary in (prfCipher family hpoly hlen).cpaGame at challenge bit bit ([BS23], Section 5.4.1, Theorem 5.2, Game 0, printed pp. 184–185).

theorem Cslib.Crypto.advantage_cpaGame_prfCipher_le (family : List Bool → List Bool → List Bool) (hpoly : Turing.MultiTapeTM.ComputableInPolyTime (fun (pair : List Bool × List Bool) => family pair.1 pair.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hlen : ∀ (key query : List Bool), query.length = key.length → (family key query).length = key.length) (adversary : OracleDistinguisher) (n Q : ℕ) (hq : ProbOracleComp.IsQueryBounded (adversary n []) Q) : ↑(Game.advantage ((prfCipher family hpoly hlen).cpaGame adversary false n).eval ((prfCipher family hpoly hlen).cpaGame adversary true n).eval) ≤ ↑(Game.advantage (prfRealGame family (cpaToPrfDistinguisher adversary false) n).eval (prfIdealGame (cpaToPrfDistinguisher adversary false) n).eval) + ↑(Game.advantage (prfRealGame family (cpaToPrfDistinguisher adversary true) n).eval (prfIdealGame (cpaToPrfDistinguisher adversary true) n).eval) + 2 * ↑Q ^ 2 / 2 ^ n

Quantitative IND-CPA security bound for prfCipher ([BS23], Section 5.4.1, Theorem 5.2, equation (5.5), printed pp. 184–189): for any OracleDistinguisher making at most Q encryption queries at security parameter n, the CPA distinguishing advantage against prfCipher is bounded by the sum of the PRF distinguishing advantages of cpaToPrfDistinguisher adversary false and cpaToPrfDistinguisher adversary true plus 2 * Q^2 / 2^n (where 2 * Q^2 / 2^n is a factor-2 loosening of the source's Q^2 / N = Q^2 / 2^n collision term from equation (5.11) on printed p. 187, arising from the Q * Q / 2^n union bound per challenge bit in bad_prfCipherForgetfulWithBadOracle_le).

theorem Cslib.Crypto.PseudorandomFunction.indcpa_prfCipher {family : List Bool → List Bool → List Bool} (hprf : PseudorandomFunction family) : (prfCipher family ⋯ ⋯).INDCPA

Any secure PseudorandomFunction yields an INDCPA-secure symmetric cipher prfCipher ([BS23], Section 5.4.1, Example 5.2 and Theorem 5.2, printed pp. 183–189).

End-to-End Non-Vacuous PRF Encrypt-then-MAC Instance

noncomputable def Cslib.Crypto.prfEncryptThenMAC (family : List Bool → List Bool → List Bool) (hpoly : Turing.MultiTapeTM.ComputableInPolyTime (fun (pair : List Bool × List Bool) => family pair.1 pair.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hlen : ∀ (key query : List Bool), query.length = key.length → (family key query).length = key.length) : SymmetricCipher

Concrete PRF-based Encrypt-then-MAC cipher combining prfCipher (2 * n-bit ciphertexts on n-bit plaintexts) with (prfMAC family hpoly).reindex (fun n => 2 * n) ((by polytime)) (authenticating 2 * n-bit ciphertexts at security parameter n).

theorem Cslib.Crypto.PseudorandomFunction.authenticatedEncryption_prfEncryptThenMAC {family : List Bool → List Bool → List Bool} (hprf : PseudorandomFunction family) : (prfEncryptThenMAC family ⋯ ⋯).AuthenticatedEncryption

End-to-end non-vacuity of authenticatedEncryption_encryptThenMAC: for any secure PseudorandomFunction family, prfEncryptThenMAC satisfies AuthenticatedEncryption, with all hypotheses (hctLen, INDCPA, and SUFCMA) discharged simultaneously from hprf.

theorem Cslib.Crypto.PseudorandomFunction.indcca_prfEncryptThenMAC {family : List Bool → List Bool → List Bool} (hprf : PseudorandomFunction family) : (prfEncryptThenMAC family ⋯ ⋯).INDCCA

End-to-end non-vacuity of indcca_encryptThenMAC and AuthenticatedEncryption.indcca: for any secure PseudorandomFunction family, prfEncryptThenMAC satisfies adaptive chosen-ciphertext security (INDCCA), with all hypotheses discharged simultaneously from hprf.