Module Hacl_star.EverCrypt

This module exposes the EverCrypt cryptographic provider, which offers agile and multiplexing interfaces for HACL* primitives.

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

Multiplexing interface for Chacha20-Poly1305

ECDH and EdDSA

Algorithms for digital signatures and key agreement

Curve25519

Multiplexing interface for ECDH using Curve25519

Ed25519

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), 4 variants of SHA-3 (SHA3-224, SHA3-256, SHA3-384, SHA3-512), BLAKE2 (both BLAKE2b and BLAKE2s), and 2 legacy algorithms (SHA-1, MD5). It offers both direct hashing and a streaming interface.

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.

module HMAC : sig ... end

Agile, multiplexing interface for HMAC

Poly1305

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.

module HKDF : sig ... end

Agile, multiplexing interface for HKDF

DRBG

Deterministic random bit generator

HMAC-DRBG

module DRBG : sig ... end

Agile, multiplexing interface for HMAC-DRBG