This repository contains a wide range of cryptographic algorithms specified in the Cryptol language. Our long-term goal is to 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.
Some of the widely adopted cryptographic algorithms contained in this repository are listed below.
| Primitive | Synthesis | Verification | |
|---|---|---|---|
| Block Cipher | AES | ||
| Triple DES | |||
| Stream Cipher | ChaCha20-Poly1305 | ||
| Message Authentication | HMAC | ||
| Digital Signature | ECDSA | ||
| SPHINCS+ | |||
| Hash | SHA1 | ||
| SHA256 | |||
| SHA2, SHA3 |