A library for the HMAC keyed-hash message authentication code
The HMAC library includes formal specifications for HMAC-SHA-256 and HMAC-SHA-512, i.e., for the HMAC keyed-hash message authentication code, using either SHA-256 or SHA-512 as the underlying hash function. HMAC is defined in RFC 2104.
The following include-book commands may be helpful to bring in the library:
(include-book "kestrel/crypto/hmac/hmac-sha-256" :dir :system) (include-book "kestrel/crypto/hmac/hmac-sha-512" :dir :system)
Or one can do:
(include-book "kestrel/crypto/hmac/top" :dir :system)
The interface functions are:
See RFC 2104 for guidance on the length of the keys used.
See the comments in the source files for more information on the HMAC library.
The library also includes tests of the specifications.