|
|
|---|
|
|
|
|---|
A library for Keccak hash functions.
The following executable formal specifications follow the Keccak SHA-3 submission, Version 3, January 14, 2011, before SHA-3 was finalized. Here is a page that discusses the history.
There are two sets of functions described here: bit-oriented and byte-oriented. To call them, include the following book:
(include-book "kestrel/crypto/keccak/keccak" :dir :system)
Since Keccak is specified to accept bit strings of any length, the most general functions accept and return "bit strings", which we model by lists of bits. The input can be any number of bits and the output length is the number in the function name. There are four variants defined:
(keccak-224 bit-list) (keccak-256 bit-list) (keccak-384 bit-list) (keccak-512 bit-list)
More commonly, callers prefer to work with bytes. The following functions accept and return "hexadecimal strings with an even number of digits", which we model by lists of unsigned 8-bit bytes. The input can be any number of bytes and the output length in bytes is the number in the function name divided by 8. There are four variants defined:
(keccak-224-bytes byte-list) (keccak-256-bytes byte-list) (keccak-384-bytes byte-list) (keccak-512-bytes byte-list)
See the comments in the source file for more information.