AEAD (Authenticated Encryption with Associated Data) Security #
This file defines the IND-CCA2 security notion for AEAD schemes at the
abstract Word := Bool level.
AEAD Games #
The AEAD security game captures the difficulty of distinguishing:
- Real: encrypt returns real ciphertext
- Ideal: encrypt returns random ciphertext (of same length)
Main definitions #
AEADDef— an AEAD scheme (encrypt + decrypt)AEAD_Game_Real/AEAD_Game_Ideal— real/ideal AEAD gamesAEAD_Advantage— advantage of an adversary in breaking AEAD
Usage in EDHOC #
EDHOC uses AES-CCM-16-64-128 for:
- Encrypting message 3 (containing initiator's credential + MAC_3)
- Encrypting message 4 (optional, containing EAD_4)
- Message 2 uses XOR encryption (KEYSTREAM_2), not AEAD
Each AEAD operation contributes one ε_aead to the security bound.
Cross-Validation #
| Property | This file | Textbook |
|---|---|---|
| Game structure | AEAD_Game_Real/Ideal | Boneh-Shoup Def. 9.1 (IND-CPA for SKE) |
| Advantage | Advantage(Real, Ideal) | |Pr[W₀] - Pr[W₁]| |
| Formulation | Indistinguishability (real vs random) | Equiv. to IND-CCA2 for nonce-based AEAD |
Equivalent formalizations:
- EasyCrypt:
AEADtheory in various protocol formalizations - CryptoVerif:
IND-CPA/INT-CTXTmacros (split formulation)
Note: AEAD_Advantage uses an IND-CPA formulation (real ciphertext vs random,
no decryption oracle). AEAD_CCA_Advantage adds a decryption oracle for full
IND-CCA2 security. The standard AEAD security combines IND-CPA + INT-CTXT;
the IND-CCA2 formulation captures both. Use AEAD_CCA_Advantage for protocols
where the adversary can submit chosen ciphertexts (multi-message, interactive).
AEAD_CPA_le_CCA shows that IND-CCA2 implies IND-CPA.
References #
- Rogaway, Authenticated-Encryption with Associated-Data, CCS 2002
- Boneh & Shoup, A Graduate Course in Applied Cryptography, §9.5
- RFC 9528 — EDHOC, Section 5.3-5.4
AEAD Definition #
Abstract AEAD scheme definition, parametric over SampleableType W.
- encrypt : W → W → W → W
AEAD encryption: (key, plaintext, associated_data) → ciphertext. Models
aes_ccm_encrypt_tag_8in lakers'Cryptotrait. - decrypt : W → W → W → W
AEAD decryption: (key, ciphertext, associated_data) → plaintext. Models
aes_ccm_decrypt_tag_8in lakers'Cryptotrait. Returns the plaintext (abstract level doesn't model decryption failure).
Instances For
AEAD Games #
Type of AEAD adversary: receives a ciphertext and must distinguish real encryption from random.
Equations
Instances For
AEAD real game: sample random key, encrypt the adversary's chosen plaintext.
Equations
- CatCrypt.Crypto.Assumptions.AEAD_Game_Real D pt ad A = do let key ← CatCrypt.Core.SPComp.sample W have ct : W := D.encrypt key pt ad A ct
Instances For
AEAD ideal game: adversary receives a random ciphertext.
Equations
- CatCrypt.Crypto.Assumptions.AEAD_Game_Ideal A = do let ct ← CatCrypt.Core.SPComp.sample W A ct
Instances For
AEAD advantage: ability to distinguish real encryption from random.
Equations
Instances For
IsPure Proofs #
IND-CCA2 AEAD Games (with decryption oracle) #
Standard AEAD security requires both confidentiality (IND-CPA) and integrity (INT-CTXT). The IND-CCA2 formulation gives the adversary access to both encryption and decryption oracles, combining both properties into a single game.
References #
- Rogaway, Authenticated-Encryption with Associated-Data, CCS 2002
- Bellare & Namprempre, Authenticated Encryption: Relations among Notions and Analysis of the Generic Composition Paradigm, ASIACRYPT 2000
IND-CCA2 AEAD adversary: receives encryption and decryption oracles.
- run : (W → W → Core.SPComp W) → (W → W → Core.SPComp (Option W)) → Core.SPComp Bool
The adversary's computation, given:
- An encryption oracle: (plaintext, ad) → ciphertext
- A decryption oracle: (ciphertext, ad) → plaintext option Returns a distinguishing bit.
Instances For
IND-CCA2 real game: adversary gets real encryption and real decryption.
Equations
- One or more equations did not get rendered due to their size.
Instances For
IND-CCA2 ideal game: encryption returns random, decryption always rejects.
Equations
- One or more equations did not get rendered due to their size.
Instances For
IND-CCA2 AEAD advantage: ability to distinguish real enc+dec from random enc + reject-all dec.
Equations
Instances For
IND-CCA2 implies IND-CPA: any IND-CPA adversary can be lifted to an IND-CCA2 adversary that ignores the decryption oracle.
Equations
- One or more equations did not get rendered due to their size.
Instances For
IsPure Proofs (CCA) #
Keyed AEAD Games (KDM + Key Leakage) #
Non-Standard Assumption #
AEAD_Keyed_Advantage combines two non-standard properties:
- Key-dependent messages (KDM): plaintext and associated data depend on the key
via
pt ad : W → W, rather than being fixed constants. - Key leakage: the real game outputs
(ciphertext, key)as a pair, leaking the secret key alongside the ciphertext.
Standard AEAD_Advantage does NOT imply AEAD_Keyed_Advantage. In general,
KDM security requires additional assumptions (e.g., random oracle / ideal cipher).
Literature #
- KDM security: Black, Rogaway, Shrimpton, Encryption-Scheme Security in the Presence of Key-Dependent Messages, SAC 2003
- KDM for public-key: Applebaum et al., Key-Dependent Message Security, 2014
- Leakage resilience: Dodis et al., Public-Key Encryption Schemes with Auxiliary Inputs, TCC 2010; Dziembowski, Pietrzak, Leakage-Resilient Cryptography, 2008
Usage #
Used by EDHOC (genuinely needed: th_3 depends on prk_3e2m, creating a circular
key dependency). Also used by SSH, Kerberos, and HPKE multi-message (Phase B).
Not needed by HPKE single-shot modes (standard AEAD_Advantage suffices).
AEAD keyed real game: sample key, output (ciphertext, key) pair. The plaintext and associated data may depend on the key (key-dependent messages).
Equations
- CatCrypt.Crypto.Assumptions.aead_keyed_real D pt ad = (CatCrypt.Core.SPComp.sample W).bind fun (key : W) => CatCrypt.Core.SPComp.pure (D.encrypt key (pt key) (ad key), key)
Instances For
AEAD keyed ideal game: sample independent random pair.
Instances For
AEAD keyed advantage: distinguishing real encryption+key from random pair.