		Search-engine friendly clone of the ACL2 documentation.

Interfaces

Hmac-sha-256-interface

HMAC-SHA-256 interface.

We instantiate HMAC with the SHA-256 hash, whose block size is 64 bytes according to FIPS 180-4.

Definitions and Theorems

Theorem: byte-list-of-hmac-sha-256

(defthm byte-list-of-hmac-sha-256
  (byte-listp (hmac-sha-256 key text)))

Theorem: len-of-hmac-sha-256

(defthm len-of-hmac-sha-256
  (equal (len (hmac-sha-256 key text))
         32))

Theorem: hmac-sha-256-of-byte-list-fix-key

(defthm hmac-sha-256-of-byte-list-fix-key
  (equal (hmac-sha-256 (byte-list-fix key) text)
         (hmac-sha-256 key text)))

Theorem: hmac-sha-256-byte-list-equiv-congruence-on-key

(defthm hmac-sha-256-byte-list-equiv-congruence-on-key
  (implies (byte-list-equiv key key-equiv)
           (equal (hmac-sha-256 key text)
                  (hmac-sha-256 key-equiv text)))
  :rule-classes :congruence)

Theorem: hmac-sha-256-of-byte-list-fix-text

(defthm hmac-sha-256-of-byte-list-fix-text
  (equal (hmac-sha-256 key (byte-list-fix text))
         (hmac-sha-256 key text)))

Theorem: hmac-sha-256-byte-list-equiv-congruence-on-text

(defthm hmac-sha-256-byte-list-equiv-congruence-on-text
  (implies (byte-list-equiv text text-equiv)
           (equal (hmac-sha-256 key text)
                  (hmac-sha-256 key text-equiv)))
  :rule-classes :congruence)

Theorem: true-listp-of-hmac-sha-256

(defthm true-listp-of-hmac-sha-256
  (true-listp (hmac-sha-256 key text))
  :rule-classes :type-prescription)

Theorem: consp-of-hmac-sha-256

(defthm consp-of-hmac-sha-256
  (consp (hmac-sha-256 key text))
  :rule-classes :type-prescription)

Theorem: byte-list32p-of-hmac-sha-256

(defthm byte-list32p-of-hmac-sha-256
  (byte-list32p (hmac-sha-256 key text)))