This repository contains a wide range of cryptographic algorithms specified in the Cryptol language. Our long-term goal is for these specifications to be literate files that share as much common code as possible, and to allow implementation correctness proofs to depend on one shared, canonical description of the algorithms they target. As a starting point, however, we plan to collect as many specifications as we can find, as-is, and incrementally improve their presentation and inter-dependency.
All Cryptol files in this repository are covered by the BSDv3 license.
This repo has executable specifications for many cryptographic algorithms.
This repo includes all the general purpose, quantum-resistant algorithms approved in the Commercial National Security Algorithm Suite 2.0 (CNSA 2.0) and one of the application-specific algorithms. The repo includes most of the approved parameter sets for each of the above algorithms; this table only links to the parameters specifically included in CNSA 2.0.
| Primitive | Specification | Parameters |
|---|---|---|
| Block cipher | AES | AES256 1 |
| Key establishment | ML-KEM | ML-KEM-1024 |
| Signature | ML-DSA | ML-DSA-87 |
| Hashing | SHA2 | SHA-384, SHA-512 |
| Hashing | SHA3 (Keccak) | SHA3-384, SHA3-512 |
This repo includes several quantum-resistant schemes drawn from the finalists of the NIST Post-Quantum Cryptography competition. Some of these have been updated to the final approved version; others are from earlier rounds of the competition.
| Primitive | NIST Name (Original Name) | Type | Versions Available |
|---|---|---|---|
| PKE / KEM | ML-KEM (CRYSTALS-Kyber) | Lattice-based | Final spec (FIPS-203) |
| Signature | ML-DSA (CRYSTALS-Dilithium) | Lattice-based | Final spec (FIPS-204) |
| Signature | FN-DSA (FALCON) | Lattice-based | Round 1.2 |
| Signature | SLH-DSA (SPHINCS+) | Hash-based | Round 3.1 |
We appreciate the generous help of the authors who were willing to share their work with us, while developing early versions of these executable specifications. We are truly grateful for their support. In particular, we'd like to thank:
- Vadim Lyubashevsky (CRYSTALS Kyber and CRYSTALS Dilithium)
- Andreas Hülsing (SPHINCS+)
- Pierre-Alain Fouque and Thomas Pornin (FALCON)
This repo includes the set of cryptographic algorithms specified in NSA's Suite B Cryptography.
| Primitive | Specification | Parameters |
|---|---|---|
| Block cipher | AES | AES128-CTR, AES128-GCM, AES256-CTR, AES256-GCM |
| Key agreement | ECDH | ECDH-P256, ECDH-P384 |
| Signature | ECDSA | ECDSA-P256-SHA256, ECDSA-P384-SHA384 |
| Hashing | SHA2 | SHA-256, SHA-384 |
There are some ciphers for authenticated encryption that are commonly used but not formally NIST-approved, like ChaCha20-Poly1305 and AES-GCM-SIV. There are also many block ciphers, including some of historical interest (e.g. Triple DES), and a smaller collection of stream ciphers
There is an implementation of HMAC that is used to instantiate a hash-based key derivation function (HKDF).
There are two members of the BLAKE family of hash functions, as well as several historical hash functions, like MD5 and SHA1, that are not suitable for general use. There's also a version of the standardized deterministic random bit generator (DRBG).
There's a family of RSA-based schemes, including the basic RSA cipher, RSA with various encoding schemes, and some RSA-based signature schemes.
The Cryptol specs presented here are written with the objective of being as close as possible to the specs as presented in the official papers so that even someone without cryptographic experience can verify that the Cryptol code meets the spec by reading it "line by line". As a result, the Cryptol code may not be as efficient as other implementations (for example it may implement DFT instead of FFT), yet it is closer to the paper definitions and aims to be functionally equivalent to them.
In addition to "correctness by visual inspection," the executable specs in this repo define provable properties. Some of these are "internal" properties of the specs (e.g. two functions must be each others' inverses). Others define top-level properties of schemes (e.g. in a signature scheme, a signature generated on a message with a valid key will verify). High-level properties are not always provable — some schemes, like ML-KEM and ML-DSA, have correctness properties that hold with overwhelming probability (but not for every possible input) — but can be checked.
Finally, NIST provides known-answer tests (KATs) via the CAVP program that can be used to check that a scheme aligns with the standardized version. We have properties that prove that we satisfy the KATs on the majority of schemes for which they are available (although we typically only include a subset of the available KATs).
You can contribute to this project by submitting issues or bug reports.
