law kbkdf_hmac_sha256_vector

bend-osdev-crypto@0.1.0.0 · LAWS.bend:621

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-crypto@0.1.0.0/hmac.bend as Hm
import bend-osdev-crypto@0.1.0.0/inst_sha2.bend as SH
import bend-osdev-crypto@0.1.0.0/kbkdf.bend as Kb

621# KBKDF in counter mode over HMAC-SHA-256 (32-bit counter and [L]_2), the
622# key "secret key bytes", Label "label", Context "context", 32 bytes:
623# Python's cryptography's KBKDFHMAC gives this value. Stated on the stream
624# (what CrKbkdf.counter_kdf returns once its length checks pass): those
625# checks compare with 2^32, which --verdict's kernel cannot compute in time;
626# check.bend runs the checked derivation
627law kbkdf_hmac_sha256_vector:
628  {Kb.CrKbkdf.counter_stream(~Hm.CrHmacKey, ~Hm.CrHmac.mac(~SH.CrSha2.sha256), ~4n, Hm.CrHmac.key(~64n, ~SH.CrSha2.sha256, B.Octets.of_string("secret key bytes")), Kb.CrKbkdf.fixed(~4n, B.Octets.of_string("label"), B.Octets.of_string("context"), 32n), 32n) == B.Octets.of_list([36, 187, 186, 187, 150, 131, 248, 143, 109, 68, 1, 79, 191, 147, 235, 99, 232, 125, 99, 110, 60, 243, 238, 232, 217, 114, 189, 30, 217, 156, 9, 202]) : B.Octets}