package mldsa
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page
Pure OCaml implementation of FIPS 204 ML-DSA
Install
dune-project
Dependency
Authors
Maintainers
Sources
v0.2.1.tar.gz
md5=cf10e50c23d778f822261222212229b8
sha512=3bd8ce7b420c82ddfaaaa173966be892ccfd7a50664c3db91c4e0b797942d2fdcabe6e240f400688ac19824290f9a0ee531db0e1e5782a6f04e745d1b6a2973c
doc/CHANGES.html
Changes
0.2.1 (2026-10-11)
The libraries are unchanged from 0.2.0; this release only changes what the source archive contains.
- Shrink release archives from about 21 MB to about 0.3 MB (#15). GitHub's tag archives, which opam downloads, now leave out the test vector corpora and
formal/. The package tests always check a known-answer subset intest/kat, about one case per parameter set and operation, and check the full corpora only from a git checkout. CI runs the package tests from the archive and keeps it under 512 KiB. - Document the opam-publish release flow that the releases use. dune-release builds its own archive, which would include the corpora.
0.2.0 (2026-09-27)
- Export TurboSHAKE128 and TurboSHAKE256 (RFC 9861) from
mlkemasMlkem.Rfc9861, for the HPKE KDFs ofdraft-ietf-hpke-pq. - Add Lean 4 proofs that every implementation matches its standard, and TLA+ models checked with TLC, in
formal/. No bug was found. - Extend the Lean proofs to TurboSHAKE:
turboshake128andturboshake256are proved to be RFC 9861 TurboSHAKE128 and TurboSHAKE256 for every input, output length and domain byte in0x01–0x7F, andMlkem.Rfc9861to reject every other domain and a negative length. - ML-DSA: follow FIPS 204 in
UseHintfor hints other than 0 or 1, reject nonces that do not fit in 16 bits, and refuse to encode more than omega hints. None is reachable through the public API. - ML-KEM: compare lengths before the constant-time equality check.
- SLH-DSA: reject tree-hash leaf indices outside the tree, and enforce the MGF1 mask length limit of RFC 8017.
- Test ML-DSA-65 key generation on seeds that make ExpandS read a longer SHAKE256 prefix.
0.1.1 (2026-09-20)
- Export SHAKE128 and SHAKE256 from
mlkemasMlkem.Fips202. A protocol that adopts ML-KEM often needs SHAKE itself, as HPKE does to derive an ML-KEM key pair, anddigestifprovides SHA-3 without the extendable-output functions. They are the functions ML-KEM already runs on. SHA3-256 and SHA3-512 stay internal, andmldsaandslhdsaare unchanged. - Hold the exported functions to OpenSSL's answers at the block boundaries of both sponges, and SHAKE256 to known answers under
js_of_ocaml, where the coverage was round trips alone.
0.1.0 (2026-09-20)
First release of the mlkem, mldsa, and slhdsa opam packages.
- Implement every FIPS 203 parameter set: ML-KEM-512, ML-KEM-768, and ML-KEM-1024.
- Implement every FIPS 204 parameter set: ML-DSA-44, ML-DSA-65, and ML-DSA-87, including typed keys/signatures, strict decoding, contexts, and explicit hedged and deterministic PureML-DSA signing.
- Implement all twelve FIPS 205 parameter sets: SHA2 and SHAKE 128s/f, 192s/f, and 256s/f, including WOTS+, FORS, XMSS, hypertree signing, contexts, and explicit hedged and deterministic PureSLH-DSA signing.
- Implement SHA-256, SHA-512, SHA3-256, SHA3-512, SHAKE128, SHAKE256, HMAC, and MGF1 entirely in OCaml, with no C stubs or runtime package dependencies.
- Use shared parameterized engines, fixed-bound NTT arithmetic for ML-KEM and ML-DSA, ML-KEM implicit rejection, and the final FIPS 205 address-clearing and big-endian FORS rules.
- Provide abstract per-algorithm key, ciphertext, shared-secret, and signature types; exact-length and canonical decoders; caller-provided randomness; and seed-based key generation and serialization.
- Isolate expanded ACVP and raw-message hooks in the explicitly testing-only
mlkem.for_testing,mldsa.for_testing, andslhdsa.for_testinglibraries. - Verify byte-for-byte NIST ACVP key generation and deterministic signatures for every parameter set; add all 2,863 applicable ML-KEM and ML-DSA cases from a pinned Wycheproof revision, pinned BoringSSL ML-KEM corpora, corruption and malformed-input tests, decoder fuzzing, and hash known answers.
- Check all 168 applicable NIST SLH-DSA signature-verification cases (24 valid and 144 invalid) and 36 signing known answers, covering hedged signing, 8192-byte messages, and 255-byte contexts for every parameter set.
- Redistribute the BoringSSL, Wycheproof, and NIST ACVP-Server test corpora with their upstream license notices; see
LICENSE.md. - Add native, bytecode, and
js_of_ocamlportability coverage. JavaScript CI exercises all ML-KEM and ML-DSA sets and representative SHA2/SHAKE SLH-DSA end-to-end operations. - Evaluate every ML-DSA signing rejection check before deciding to retry, document its remaining variable-time boundary, and inspect aggressively optimized ML-KEM/ML-DSA native control flow in CI.
- Split decoder fuzzing by family, isolate expensive exact-length SLH-DSA key imports, and run deterministic bounded fuzz cases in CI.
- Add release-ready opam metadata for three independent packages, Avrea-hosted CI across OCaml 4.13 through 5.4, a non-blocking lower-dependency-bounds job, and GitHub Actions pinned to the latest release SHAs.
- Document the unaudited security boundary and intentionally exclude all downstream protocol integrations from 0.1.0.
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page