law kbkdf_counter_stream_length

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

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-crypto@0.1.0.0/kbkdf.bend as Kb

548# SP 800-108 KDFs over any MAC (kbkdf.bend), for every MAC, key, fixed
549# input data and length: each stream has the length asked for, a shorter
550# stream is a prefix of a longer one with the same fixed input (and IV), and
551# a derivation that succeeds has the length asked for. (The interface's
552# prefix law holds of the streams: a derivation binds its length L into
553# the fixed input, so derivations of two lengths differ.)
554law kbkdf_counter_stream_length:
555  for ~K: Data
556  for ~compute: K -> B.Octets -> B.Octets
557  for ~rlen: Nat
558  for +k: K
559  for +fixed: B.Octets
560  for +n: Nat
561  {B.Octets.len(Kb.CrKbkdf.counter_stream(~K, ~compute, ~rlen, k, fixed, n)) == n : Nat}