This directory contains the Cryptol specifications for the ML-DSA (Module-Lattice-Based Digital Signature Algorithm) as defined in the specification FIPS 204.
The Cryptol code in this executable specification was developed to closely resemble the standard; it prioritizes readability and obvious correctness over efficiency.
- Cryptol Version: 3.2.0.
- Environment variable CRYPTOLPATH should contain the path to the Cryptol specs repo.
The Cryptol specifications have been tested to ensure correctness. All properties related to correctness of the algorithms (such as decryption of encryption equaling identity and decoding of encoding equaling identity) pass successfully. Internal properties and other correctness checks can be run by loading any instantiation of ML-DSA and checking the docstrings (it will take some time to run, but should be less than an hour) in the Cryptol REPL:
:load Primitive/Asymmetric/Signature/ML_DSA/Instantiations/ML_DSA_44.cry
:check-docstrings
Each instantiation also has a small suite of known-answer tests (KATs) from a trusted source, including NIST's ACVP program and the post-quantum-crypto KATs. Individual KATs are annotated with the amount of time they are expected to take to run.
:load Primitive/Asymmetric/Signature/ML_DSA/Tests/ML_DSA_44.cry
:check-docstrings
This repo previously contained several implementations of CRYSTALS-Dilithium from the NIST Post-Quantum competition. This included versions and tests from Round 1, Round 2, and from the initial public draft of the eventual FIPS-204. They were removed in the commit with hash: