Expand description

Authenticated Encryption (AEAD)

💡 This is a hacspec representation of the HPKE RFC. The text is mostly verbatim from the RFC with changes where required. It demonstrates the possibilities of hacspec for specifications.

  • Seal(key, nonce, aad, pt): Encrypt and authenticate plaintext pt with associated data aad using symmetric key key and nonce nonce, yielding ciphertext and tag ct. This function can raise a MessageLimitReachedError upon failure.
  • Open(key, nonce, aad, ct): Decrypt ciphertext and tag ct using associated data aad with symmetric key key and nonce nonce, returning plaintext message pt. This function can raise an OpenError or MessageLimitReachedError upon failure.
  • Nk: The length in bytes of a key for this algorithm.
  • Nn: The length in bytes of a nonce for this algorithm.
  • Nt: The length in bytes of the authentication tag for this algorithm.

Security Requirements on an AEAD

All AEADs MUST be IND-CCA2-secure, as is currently true for all AEADs listed in AEAD.

Enums

Authenticated Encryption with Associated Data (AEAD) Functions

Functions

Decrypt ciphertext and tag ct using associated data aad with symmetric key key and nonce nonce, returning plaintext message pt. This function can raise an OpenError or MessageLimitReachedError upon failure.

Encrypt and authenticate plaintext pt with associated data aad using symmetric key key and nonce nonce, yielding ciphertext and tag ct. This function can raise a MessageLimitReachedError upon failure.

The length in bytes of a key for this algorithm.

The length in bytes of a nonce for this algorithm.

The length in bytes of the authentication tag for this algorithm.

Type Definitions

An AEAD key is a sequence of bytes.

An AEAD nonce is a sequence of bytes.