|
|
|---|
|
|
|
|---|
Introduce an interface for a cryptographic hash-based message authentication (HMAC) function.
HMAC is specified in the RFC 2104 standard. It is parameterized over a hash function, i.e. there is an HMAC variant for each choice of the hash function.
This macro introduces a weakly constrained ACL2 function for an HMAC function; the underlying hash function is specified via a reference to the name of an existing definterface-hash. The HMAC function takes two byte lists as arguments (the key and the text), and returns a byte list; the use of bytes (vs. bits) is consistent with RFC 2104. The guard of the function requires the arguments to be byte lists. The function is constrained to fix its arguments to byte lists, and to return a byte list whose size is the output size of the hash function.
If the referenced hash function has no limit on its input size,
the HMAC function has no limit on the sizes of its inputs either.
Otherwise, limits are derived as follows,
and included in the guard of the generated constrained function.
RFC 2104 says that the key size
must not exceed the hash function's block size
in order for the key to be used ``directly'',
otherwise the key is hashed and its hash used:
either way, the key or its hash is padded to the block size.
RFC 2104 says that an inner hash is taken
of the concatenation of
(i) the (xor'd) padded key or key hash and (ii) the text,
whose total size must therefore not exceed
the hash function's maximum input size:
it follows that the size of the text must not exceed
the hash function's maximum input size dimished by
the hash function's block size.
Note that definterface-hash has no information about
the hash function's block size,
which is therefore supplied directly to
This macro also introduces a few theorems that follow from the constraints. It also introduces an XDOC topic for the generated function, constraints, and theorems.
(definterface-hmac name :hash ... :block-size ... :topic ... :parents ... :short ... :long ... )
A symbol that names the HMAC function.
The name of an existing definterface-hash.
A constant expression whose value is a positive integer. This is the hash function's block size in bytes. This input must be present if the hash function has an input size limit; otherwise, this input must be absent.
A symbol that names the generated XDOC topic that surrounds the generated functions and theorems.
If not supplied, it defaults to
name followed by-interface .
These, if present, are added to the XDOC topic generated for the fixtype.
A constrained function that represents the HMAC function.
Its guard consists of byte-listp for both arguments and, if applicable, conditions on their lengths as explained above.
This function is constrained to:
- Return a byte-listp of length equal to the output size of the hash function.
- Fix its inputs to byte-listp.
The following additional theorems are also generated:
- A type prescription rules saying that the function returns a true-listp.
- A type prescription rule saying that the function returns a consp.