Kdf
A library for Key Derivation Functions
The KDF library includes a formal specification for PBKDF2,
Password-Based Key Derivation Function 2, specialized to use the pseudorandom function HMAC-SHA-512. This key derivation function is defined in IETF RFC 8018
The following include-book command may be helpful to bring in the library:
(include-book "kestrel/crypto/kdf/pbkdf2-hmac-sha-512" :dir :system)
Interface Functions
pbkdf2-hmac-sha-512
(pbkdf2-hmac-sha-512 p s c dklen)
Arguments:
- P -- the password, an octet string represented as a list of 8-bit bytes
- S -- the salt, an octet string represented as a list of 8-bit bytes
- c -- the iteraction count. Note that BIP 39 uses an iteraction count of 2048.
- dkLen -- the intended length in octets of the derived key. Note that BIP 39 uses a length of 64.
Returns a list of dkLen bytes.
pbkdf2-hmac-sha-512-strings
(pbkdf2-hmac-sha-512-from-strings p-string s-string c dklen)
Arguments:
- P-string -- the password, an octet string represented as an ACL2 string
- S-string -- the salt, an octet string represented as a an ACL2 string
- c -- the iteraction count. Note that BIP 39 uses an iteraction count of 2048.
- dkLen -- the intended length in octets of the derived key. Note that BIP 39 uses a length of 64.
Returns a list of dkLen bytes.
