Security

No released version is supported for production use. The library is for interoperability review and has not had an independent cryptographic audit. See the security policy for support and reporting terms.

API safeguards

Errors at protocol boundaries

Single-shot opens map peer-controlled decapsulation and authentication failures to Open_error. Key_mismatch and Unsupported_mode remain distinct configuration errors. Context setup exposes more specific errors; do not turn them into distinguishable responses to peers.

ML-KEM accepts a tampered encapsulation of the correct length and derives an unrelated secret (implicit rejection). Setup succeeds; the first open fails. Hybrids behave the same unless their curve element is invalid. Export-only protocols must confirm the exported secret with the peer before relying on it.

Application responsibilities

Base mode does not authenticate the sender. Auth and AuthPSK authenticate to the recipient, but are not signatures: a holder of the recipient's private key can impersonate any sender (and also needs the PSK for AuthPSK). A recipient cannot prove authorship to a third party. If your protocol needs signatures, use a signature scheme as well.

Primitives and draft support

Cryptographic primitives come from Mirage Crypto, curve448, mlkem, Digestif, and kdf. Their correctness and side-channel behavior are part of the library's security assumptions.

Evidence and limits

Tests cover published vectors, suite round trips, malformed inputs, error contracts, concurrency, and interruption. Vector sources and coverage are pinned in test-vector provenance; see development to run them.

Lean and TLA+ models check algorithm structure and context behavior. The models assume the cryptographic primitives and are checked against OCaml on concrete inputs. They are not a proof of the compiled library or a substitute for an audit.

Report a vulnerability

Use GitHub's private advisory form, not a public issue. Include the affected version or commit, suite and mode, a minimal reproduction, and the expected security impact. Maintainers aim to acknowledge reports within seven days and coordinate disclosure after a fix is available.