Module aead

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

AEAD

Authenticated Encryption with Associated Data (AEAD) Functions

Functions

AeadOpen

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.

AeadSeal

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.

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.

Type Aliases

Key

An AEAD key is a sequence of bytes.

Nonce

An AEAD nonce is a sequence of bytes.