From 0a8c3001e52361d5f5dd1bf73ec83ca9e27199bc Mon Sep 17 00:00:00 2001 From: Joe Hendrix Date: Fri, 12 Aug 2022 17:10:02 -0700 Subject: [PATCH] Update README --- README.md | 32 +++++++++++++++++++++++++++++--- 1 file changed, 29 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 8c69406..4288c2e 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,32 @@ # Cryptography in Lean 4 -This repo contains some experiments that are progressing to specifications of AES, SHA3 and Classic McEliece -in Lean. +This repo is intended to provide a comprehensive collection of specifications +of cryptographic algorithms in Lean 4. Each algorithm will have a complete, +executable specification along with test vectors for some validation that the +algorithm is correctly specified. -Please contact me if you are interested in working on cryptographic specifications in Lean. \ No newline at end of file +The repositiory currently contains a complete specification of the +[Classic McEliece](https://classic.mceliece.org/) algorithm on the +``kem/mceliece348864`` parameter set. It has been +derived from the [Nist Round 3](https://classic.mceliece.org/nist.html) +submission files. Our [continuous integration](https://github.com/joehendrix/lean-crypto/actions) +validates that the Lean specification produces the same known-answer tests +as the C reference implementation. + +The cryptographic library also links in [OpenSSL](https://www.openssl.org/) +and [libkeccak](https://codeberg.org/maandree/libkeccak) so +that we can invoke fast C implementations of AES and SHAKE respectively. + +This repository also includes experiments aimed at mapping the cryptographic +specifications into SMT so that we can take advantage of automated constraint +solving to reason about cryptographic specificiations including equivalence +checking and checking correctness properties of specifications. + +Plans for the Future +==================== + +This repository is still in its early stages. Our next plans are to: + +* Write reference specifications of AES and SHAKE that can be validated + against known answer tests. +* Complete specifications of other Classic Mceliece parameter sets.