|
|
|---|
|
|
|
|---|
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-listp for the password and salt arguments, posp for 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-listp of length equal to the length argument.
- Fix its inputs to byte-listp and posp as 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.