Module `Hacl_star.EverCrypt`

type bytes = SharedDefs.CBytes.t: bytes is ultimately an alias for Stdlib.Bytes.t, the type of buffers currently used throughout the library

module Error : sig ... end: Return type used for AEAD functions

AEAD

Algorithms for AEAD (authenticated encryption with additional data)

Agile interface

module AEAD : sig ... end: Agile, multiplexing AEAD interface exposing AES128-GCM, AES256-GCM, and Chacha20-Poly1305

Chacha20-Poly1305

module Chacha20_Poly1305 : SharedDefs.Chacha20_Poly1305: Multiplexing interface for Chacha20-Poly1305

ECDH and EdDSA

Algorithms for digital signatures and key agreement

Curve25519

module Curve25519 : SharedDefs.Curve25519: Multiplexing interface for ECDH using Curve25519

Ed25519

module Ed25519 : SharedDefs.EdDSA: This interface does not yet support multiplexing and is identical to the one in Hacl.Ed25519

Hashing

Agile interface

module Hash : sig ... end: Agile, multiplexing hashing interface, exposing 4 variants of SHA-2 (SHA-224, SHA-256, SHA-384, SHA-512), BLAKE2, and 2 legacy algorithms (SHA-1, MD5). It offers both direct hashing and a streaming interface.

SHA-2

Multiplexing interfaces for SHA-224 and SHA-256 which use Intel SHA extensions when available.

module SHA2_224 : SharedDefs.HashFunction: Direct hashing with SHA-224

module SHA2_256 : SharedDefs.HashFunction: Direct hashing with SHA-256

MACs

Message authentication codes

HMAC

Portable HMAC implementations. They can use optimised assembly implementations for the underlying hash function, if such an implementation exists and Intel SHA extensions are available (see SHA-2).

module HMAC : sig ... end: Agile, multiplexing interface for HMAC

module HMAC_SHA2_256 : SharedDefs.MAC: Multiplexing interface for HMAC-SHA-256

module HMAC_SHA2_384 : SharedDefs.MAC: Multiplexing interface for HMAC-SHA-384

module HMAC_SHA2_512 : SharedDefs.MAC: Multiplexing interface for HMAC-SHA-512

Poly1305

module Poly1305 : SharedDefs.MAC: Multiplexing interface for Poly1305

Key derivation

HKDF

HMAC-based key derivation function

Portable HKDF implementations. They can use optimised assembly implementations for the underlying hash function, if such an implementation exists and Intel SHA extensions are available (see SHA-2).

module HKDF : sig ... end: Agile, multiplexing interface for HKDF

module HKDF_SHA2_256 : SharedDefs.HKDF: Multiplexing interface for HKDF using SHA2-256

module HKDF_SHA2_384 : SharedDefs.HKDF: Multiplexing interface for HKDF using SHA2-384

module HKDF_SHA2_512 : SharedDefs.HKDF: Multiplexing interface for HKDF using SHA2-512

DRBG

Deterministic random bit generator

HMAC-DRBG

module DRBG : sig ... end: Agile, multiplexing interface for HMAC-DRBG