Encrypt-then-MAC: a composed authenticated-encryption scheme

Encrypt-then-MAC is the standard construction that turns a confidentiality-only encryption scheme into an authenticated one: encrypt the message, then MAC the resulting ciphertext, and transmit (ciphertext, tag). Decryption first checks the tag and only decrypts if it verifies. Following Rosulek, The Joy of Cryptography, §9-10 (MACs and authenticated encryption; Construction 10.9, Claim 10.10).

The construction is a combinator on core's EncScheme; its correctness is proved generically, and the XOR / one-time-pad instantiation achieves perfect IND-CPA security (advantage exactly 0).

The construction

Given an encryption scheme E and a MAC macF : MacKey → E.Ciphertext → Tag, EtM E … macF is the scheme with

• Key = E.Key × MacKey, Ciphertext = E.Ciphertext × Tag;
• keyGen samples an encryption key and a MAC key independently;
• encrypt (ke, km) m = let c ← E.encrypt ke m; (c, macF km c);
• decrypt (ke, km) (c, t) = if t = macF km c then E.decrypt ke c else ⊥.

Main results

• EtM — the Encrypt-then-MAC combinator on EncScheme.
• EtM_correct — the combinator preserves correctness: if E is correct, so is EtM E … macF. A ciphertext produced by encrypt carries a matching tag, so decryption clears the tag check and recovers the message.
• BoolEtM — the XOR instantiation: OTP encryption composed with the XOR MAC macF km c = km ⊕ c over Bool.
• boolEtM_correct — BoolEtM is correct (via EtM_correct and otp_correct).
• boolEtM_perfect_indcpa — BoolEtM has perfect IND-CPA security: every adversary has IND-CPA advantage exactly 0.

On the Adv_CCA ≤ Adv_MAC + Adv_CPA + Adv_MAC bound

The general Encrypt-then-MAC theorem bounds the authenticated (IND-CCA) advantage by the MAC's forging advantage plus the base scheme's IND-CPA advantage. Core currently exposes an IND-CPA game (INDCPA_Game) but no IND-CCA game, so the cleanest core-provable headline is the perfect IND-CPA security of the XOR instantiation, proved by the bijection-coupling technique of OneTimePad.lean.

References

• [Rosulek, The Joy of Cryptography, §9-10; Construction 10.9, Claim 10.10]
• [Bellare & Namprempre, Authenticated Encryption: Relations among Notions]

The Encrypt-then-MAC combinator

noncomputable def CatCrypt.Examples.EncryptThenMAC.EtM (E : Crypto.EncScheme) (MacKey Tag : Type) [Fintype MacKey] [Nonempty MacKey] [Fintype Tag] [Nonempty Tag] [DecidableEq Tag] (macF : MacKey → E.Ciphertext → Tag) : Crypto.EncScheme

Encrypt-then-MAC. Given an encryption scheme E and a deterministic MAC macF : MacKey → E.Ciphertext → Tag, produce the authenticated scheme that appends macF km c to each ciphertext c and refuses to decrypt a ciphertext whose tag does not verify.

Equations

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

Correctness of the combinator

theorem CatCrypt.Examples.EncryptThenMAC.EtM_correct (E : Crypto.EncScheme) (MacKey Tag : Type) [Fintype MacKey] [Nonempty MacKey] [Fintype Tag] [Nonempty Tag] [DecidableEq Tag] (macF : MacKey → E.Ciphertext → Tag) (hE : E.Correct) : (EtM E MacKey Tag macF).Correct

Encrypt-then-MAC preserves correctness. A ciphertext produced by encrypt, (c, macF km c) carries the matching tag, so decryption passes the tag check and falls through to E.decrypt, which recovers the message by hE.

The XOR / one-time-pad instantiation

def CatCrypt.Examples.EncryptThenMAC.boolXorMac (km c : Bool) : Bool

The XOR MAC over Bool: macF km c = km ⊕ c.

Equations

• CatCrypt.Examples.EncryptThenMAC.boolXorMac km c = (km ^^ c)

noncomputable def CatCrypt.Examples.EncryptThenMAC.BoolEtM : Crypto.EncScheme

Encrypt-then-MAC over Bool: OTP encryption composed with the XOR MAC.

Key = Bool × Bool (an encryption key and a MAC key), Plaintext = Bool, Ciphertext = Bool × Bool (the OTP ciphertext and its tag).

Equations

• CatCrypt.Examples.EncryptThenMAC.BoolEtM = CatCrypt.Examples.EncryptThenMAC.EtM CatCrypt.Examples.OTP.BoolOTP Bool Bool CatCrypt.Examples.EncryptThenMAC.boolXorMac

theorem CatCrypt.Examples.EncryptThenMAC.boolEtM_correct : BoolEtM.Correct

BoolEtM is correct, by EtM_correct and correctness of the one-time pad.

Perfect IND-CPA security of the XOR instantiation

def CatCrypt.Examples.EncryptThenMAC.encF (k : Bool × Bool) (m : Bool) : Bool × Bool

The BoolEtM ciphertext as a pure function of the (encryption, MAC) key pair and the message: k ↦ (k.1 ⊕ m, k.2 ⊕ (k.1 ⊕ m)).

Equations

• CatCrypt.Examples.EncryptThenMAC.encF k m = (k.1 ^^ m, k.2 ^^ (k.1 ^^ m))

theorem CatCrypt.Examples.EncryptThenMAC.boolEtM_indcpa_game_eq (m₀ m₁ b : Bool) : Crypto.SecurityDefs.INDCPA_Game BoolEtM m₀ m₁ b = do let k ← Core.SPComp.sample (Bool × Bool) Core.SPComp.pure (encF k (if b = true then m₀ else m₁))

The BoolEtM IND-CPA game, collapsed to a single Bool × Bool key sample followed by a pure ciphertext — the shape used by OneTimePad.lean. The two independent key samples fuse into one product sample (sample_prod_eq), and the OTP encryption's pure bind collapses (SPComp.pure_bind).

theorem CatCrypt.Examples.EncryptThenMAC.boolEtM_indcpa_coupling (m₀ m₁ : Bool) : Relational.rHoare Relational.eqPre (Crypto.SecurityDefs.INDCPA_Game BoolEtM m₀ m₁ true) (Crypto.SecurityDefs.INDCPA_Game BoolEtM m₀ m₁ false) Relational.eqPost

Coupling: the two IND-CPA games for BoolEtM are equidistributed.

The map (ke, km) ↦ (ke ⊕ (m₀ ⊕ m₁), km) is a bijection of the key space that carries the m₀-ciphertext onto the m₁-ciphertext: the OTP component becomes ke ⊕ (m₀ ⊕ m₁) ⊕ m₁ = ke ⊕ m₀, and the tag follows since it is a function of that component and the (unchanged) MAC key.

theorem CatCrypt.Examples.EncryptThenMAC.boolEtM_perfect_indcpa (m₀ m₁ : Bool) (A : BoolEtM.Ciphertext → Core.SPComp Bool) : Crypto.SecurityDefs.INDCPA_Adv BoolEtM m₀ m₁ A = 0

BoolEtM has perfect IND-CPA security: every adversary has IND-CPA advantage exactly 0.