Turn a mnemonic string into a seed.
(bip39-mnemonic-to-seed mnemonic passphrase) → seed
The mnemonic is also called a key since it is input to a key-stretching function, namely PBKDF2 HMAC-SHA-512. The mnemonic is the first input of PBKDF2 HMAC-SHA-512.
The second input of PBKDF2 HMAC-SHA-512 is the salt, which is a string.
It is composed of the string constant ``
PBKDF2 stretches the mnemonic and salt using 2,048 rounds of hashing with HMAC-SHA-512, producing a 512-bit (i.e. 64-byte) value. This is the seed, suitable as a BIP 32 seed.
Note that this function does not require the mnemonic string to be
a space-separated sequence of mnemonic words.
It accepts any string as mnemonic, as well as any string as passphrase.
More precisely, there are (large) limits on the lengths of these strings,
dictated by the limits on the password and salt inputs of
Function:
(defun bip39-mnemonic-to-seed (mnemonic passphrase) (declare (xargs :guard (and (stringp mnemonic) (stringp passphrase)))) (declare (xargs :guard (and (< (length mnemonic) (expt 2 125)) (< (length passphrase) (- (expt 2 125) (+ 128 4 8)))))) (b* ((password (string=>nats mnemonic)) (salt (string=>nats (string-append "mnemonic" (acl2::str-fix passphrase)))) (iterations 2048) (length 64)) (pbkdf2-hmac-sha-512 password salt iterations length)))
Theorem:
(defthm byte-listp-of-bip39-mnemonic-to-seed (b* ((seed (bip39-mnemonic-to-seed mnemonic passphrase))) (byte-listp seed)) :rule-classes :rewrite)
Theorem:
(defthm bip39-mnemonic-to-seed-of-str-fix-mnemonic (equal (bip39-mnemonic-to-seed (acl2::str-fix mnemonic) passphrase) (bip39-mnemonic-to-seed mnemonic passphrase)))
Theorem:
(defthm bip39-mnemonic-to-seed-streqv-congruence-on-mnemonic (implies (acl2::streqv mnemonic mnemonic-equiv) (equal (bip39-mnemonic-to-seed mnemonic passphrase) (bip39-mnemonic-to-seed mnemonic-equiv passphrase))) :rule-classes :congruence)
Theorem:
(defthm bip39-mnemonic-to-seed-of-str-fix-passphrase (equal (bip39-mnemonic-to-seed mnemonic (acl2::str-fix passphrase)) (bip39-mnemonic-to-seed mnemonic passphrase)))
Theorem:
(defthm bip39-mnemonic-to-seed-streqv-congruence-on-passphrase (implies (acl2::streqv passphrase passphrase-equiv) (equal (bip39-mnemonic-to-seed mnemonic passphrase) (bip39-mnemonic-to-seed mnemonic passphrase-equiv))) :rule-classes :congruence)
Theorem:
(defthm len-of-bip39-mnemonic-to-seed (equal (len (bip39-mnemonic-to-seed mnemonic passphrase)) 64))