PQXDH in Lean

3. Authenticated Encryption with Associated Data🔗

An AEAD scheme provides both confidentiality and integrity for a plaintext message, while binding the ciphertext to unencrypted associated data (AD). In X3DH/PQXDH:

  • The session key SK (derived by the KDF) is the AEAD key.

  • Alice encrypts her first message using SK.

  • The associated data AD = IKₐᵖᵏ ‖ IKᵦᵖᵏ binds the ciphertext to both parties' identities, preventing key-mismatch attacks.

The concrete instantiation is AES-256 in CBC mode with HMAC (Encrypt-Then-MAC) (§2.5, p. 472, Bhargavan et al.). The paper assumes IND-CPA and INT-CTXT, which together imply IND-CCA2 for AEAD schemes (section 2.5, assumption 3).

  1. 3.1. Structure