Skip to content

A central repository for specifications of cryptographic algorithms in Cryptol

License

Notifications You must be signed in to change notification settings

GaloisInc/cryptol-specs

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 

Repository files navigation

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

About

A central repository for specifications of cryptographic algorithms in Cryptol

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages