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
- Private keys, PSKs, and contexts are abstract types without printers or equality helpers.
- Sender and receiver contexts have separate types. Export-only contexts cannot encrypt.
- Contexts manage nonces and reject sequence exhaustion. Failed opens do not advance the sequence.
- Concurrent context operations are detected before cryptography. Applications still need to serialize calls.
- Operations that need randomness require an explicit generator.
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
- Key management: authenticate public keys and handle storage, distribution, rotation, and revocation.
- Framing: encode the encapsulated key and ciphertext, agree on the suite and mode, and bind protocol context with
infoandaad. - Message delivery: contexts require ordered messages. HPKE does not provide transport recovery or application-wide replay protection.
- Entropy: use a cryptographically secure RNG and high-entropy PSKs.
Psk.createchecks length, not entropy. - Secret retention: do not log key or PSK bytes. OCaml's garbage collector cannot guarantee secret erasure.
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.
- X448:
curve448has not been independently audited. Its constant-time design has been checked with tools, not proved. Read its security policy. - ML-KEM and SHAKE:
mlkemhas not been independently audited and does not guarantee constant-time execution. Read its security policy. - Pure ML-KEM: a failure of ML-KEM or its implementation has no elliptic-curve fallback. Hybrids combine both; their security relies on the combiner and at least one component remaining secure.
- Drafts: ML-KEM and hybrids follow
draft-ietf-hpke-pq-05; hybrids also follow the concrete hybrid KEM draft. Store derived private keys, not just derivation inputs, because draft changes can alter derivation. - Protocol version:
Hpke.Draft_hpke_04follows revision 04 of the HPKE successor draft. It does not changeHpke.Rfc9180's wire behavior. - Raw AEAD:
Aead.sealcannot prevent nonce reuse. Never encrypt twice with the same key and nonce. - Test helpers: never link
hpke.for_testingoutside tests. Reusing or disclosing its caller-chosen ephemeral key breaks confidentiality.
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.