law Sign.correct

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

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

9# sign is RFC 2104 / FIPS 198-1 HMAC over FIPS 180-4 SHA-256.
10law Sign.correct:
11  for +key: List<&2, U32>
12  for +msg: List<&2, U32>
13  {MAC.sign(key, msg) == Spec.hmac(key, msg) : List<&2, U32>}