law michael_split

bend-osdev-hashes@0.1.0.0 · LAWS.bend:382

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-hashes@0.1.0.0/hashes.bend as Hs
import bend-osdev-hashes@0.1.0.0/michael.bend as MI

382# Michael (IEEE 802.11i): the tag in two pieces is the one-call tag, for every key and split
383law michael_split:
384  for +k: Hs.HsW2
385  for +a: B.Octets
386  for +b: B.Octets
387  {MI.HsMichael.final(MI.HsMichael.update(MI.HsMichael.update(MI.HsMichael.init(k), a), b)) == MI.HsMichael.mic(k, B.Octets.append(a, b)) : B.Octets}