Module `EverCrypt.AEAD`

Agile, multiplexing AEAD interface exposing AES128-GCM, AES256-GCM, and Chacha20-Poly1305

To use the agile AEAD interface, users first need to initialise an internal state using init. This state will then need to be passed to every call to encrypt and decrypt. It can be reused as many times as needed. Users are not required to manually free the state.

The tag buffer must be 16 bytes long. For key and iv, each algorithm has different constraints:

AES128-GCM: key = 16 bytes , iv > 0 bytes
AES256-GCM: key = 32 bytes, iv > 0 bytes
Chacha20-Poly1305: key = 32 bytes, iv = 12 bytes

type t

val init : alg:SharedDefs.AEADDefs.alg -> key:bytes -> t Error.result: init alg key tries to allocate the internal state for algorithm alg with key and returns a t if successful or an Error.error_code otherwise.

val encrypt : st:t -> iv:bytes -> ad:bytes -> pt:bytes -> (bytes * bytes) Error.result: encrypt key iv ad pt takes a key, an initial value iv, additional data ad, and plaintext pt and, if successful, returns a tuple containing the encrypted pt and the authentication tag for the plaintext and the associated data.

val decrypt : st:t -> iv:bytes -> ad:bytes -> ct:bytes -> tag:bytes -> bytes Error.result: decrypt key iv ad ct tag takes a key, the initial value iv, additional data ad, ciphertext ct, and authentication tag tag, and, if successful, returns the decrypted ct.

module Noalloc : sig ... end: Versions of these functions which write their output in a buffer passed in as an argument