package hacl-star

  1. Overview
  2. Docs
package hacl-star
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module EverCrypt.AEADSource

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
Sourcetype t

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.

Sourceval 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.

Sourceval 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.

Sourcemodule Noalloc : sig ... end

Versions of these functions which write their output in a buffer passed in as an argument