		Search-engine friendly clone of the ACL2 documentation.

Cryptography

Hmac

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:

(hmac-sha-256 k text) applies HMAC-SHA-256 to key k (a list of bytes) and data text (a list of bits). Returns a list of 32 bytes.
(hmac-sha-512 k text) applies HMAC-SHA-512 to key k (a list of bytes) and data text (a list of bits). Returns a list of 64 bytes.

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.