Introduce an interface for a password-based key derivation function 2 (PBKDF2).

PBKDF2 is specified in the RFC 8018 standard. It is parameterized over a pseudorandom function, i.e. there is a PBKDF2 variant for each choice of the pseudorandom function. RFC 8018 assumes the pseudorandom function to be a binary function, since it is applied to two arguments (see Section 5.2 of RFC 8018).

This macro introduces a weakly constrained ACL2 function
for a PBKDF2 function;
the underlying pseudorandom function is specified via a reference to
the name of an existing `definterface-hmac`.
For now, only HMAC functions are supported
as choices for the PBKDF2's pseudorandom function.
The PBKDF2 function takes as arguments
two byte lists (the password and the salt)
and two positive integers (the iteration count and the key length);
the use of bytes (vs. bits, or strings) is consistent with RFC 8108.
The guard of the function requires the arguments
to be byte lists and positive integers.
The function is constrained to fix its arguments
to byte lists and positive integers,
and to return a byte list whose size is
the key length specified by the argument.

The password of the PBKDF2 function is used as the key of the underlying HMAC function according to RFC 8108. Thus, if the HMAC function has a limit (derived from the hash function) on the size of the keys it accepts, the same limit applies to the password of the PBKDF2 function and is added to the guard of the PBKDF2 function.

If the hash function has an input size limit,
the limit on the size of the HMAC function's text input
is as explained in `definterface-hmac`.
RFC 8108 says that the text passed to the HMAC function is
either (i) the salt concatenated with 4 bytes
or (ii) an output of the HMAC function:
while the latter is always well below the HMAC text size limit,
the former induces the constraint that the salt
must be below the limit for the HMAC text (see `definterface-hmac`)
diminished by 4.
The guard of the PBKDF2 function includes this constraint,
if applicable.

RFC 8108 says that the desired key length must not exceed

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-pbkdf2 name :hmac ... :topic ... :parents ... :short ... :long ... )

A symbol that names the PBKDF2 function.

The name of an existing

definterface-hmac.

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 PBKDF2 function.

Its guard consists of

byte-listpfor the password and salt arguments,pospfor the iteration and length arguments, and if applicable, conditions on the length of the password and salt derived as explained above.This function is constrained to:

- Return a
byte-listpof length equal to the length argument.- Fix its inputs to
byte-listpandpospas appropriate.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.

- Definterface-pbkdf2-implementation
- Implementation of
`definterface-pbkdf2`.