law mac_verify_tag_agrees

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

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-crypto@0.1.0.0/mac.bend as Mc

174law mac_verify_tag_agrees:
175  for ~K: Data
176  for ~compute: K -> B.Octets -> B.Octets
177  for +k: K
178  for +m: B.Octets
179  for t: B.Octets
180  {Mc.CrMac.verify_tag(~K, ~compute, k, m, t) == B.Octets.is_eq(compute(k, m), t) : Bool}