def block_mask

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/mac/hmac.bend:71

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/mac.bend as MAC
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/hmac.bend as Spec

71# The masked key block of the implementation is (K0 XOR pad) of FIPS 198-1.
72def block_mask(+key: List<&2, U32>, +pad: U32, +hp: {U32.xor(0, pad) == pad : U32}) -> {MAC.mask(MAC.block_key(key), 64n, pad) == Spec.xor_pad(Spec.k0(key), pad) : List<&2, U32>}:
73  %Equal.sym(Bool, MAC.fits(key, 64n), Nat.is_le(List.length(&2, U32, key), 64n), fits_len(key, 64n)) : {MAC.mask(MAC.block_key_if(key, _), 64n, pad) == Spec.xor_pad(Spec.zero_pad(Spec.shorten_if(key, Nat.is_le(List.length(&2, U32, key), 64n))), pad) : List<&2, U32>}
74  block_mask_if(key, pad, hp, Nat.is_le(List.length(&2, U32, key), 64n), {==})