A formal specification of the SHA-2 hash functions
The SHA-2 library contains executable formal specifications of several hash functions: SHA-224, SHA-256, SHA-384, and SHA-512. These algorithms are described in NIST publication FIPS PUB 180-4.
The library also includes tests of the specifications.
The following include-book commands may be helpful to bring in the library:
(include-book "kestrel/crypto/sha-2/sha-224" :dir :system) (include-book "kestrel/crypto/sha-2/sha-256" :dir :system) (include-book "kestrel/crypto/sha-2/sha-384" :dir :system) (include-book "kestrel/crypto/sha-2/sha-512" :dir :system)
Or one can do:
(include-book "kestrel/crypto/sha-2/top" :dir :system)
The SHA-2 library contains two sets of interface functions: core functions that take lists of bits and additional convenience functions that take lists of bytes. All of the functions return the hash (or message digest) as a list of bytes. For both inputs and outputs, bytes are interpreted in a big-endian fashion. More precisely, a sequence of bytes can be converted to a sequence of bits by taking the bits from the first byte, starting with the most significant bit, then the bits of the next byte, and so on.
The interface functions are:
See the comments in the source files for more information.