106ohm/cryptol-specs

A central repository for specifications of cryptographic algorithms in Cryptol

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