law michael_short_key

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

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

400# Michael (IEEE 802.11i): a key of 7 bytes is refused
401law michael_short_key:
402  {Result.map(&2, &2, Hs.HsError, Hs.HsW2, Unit, k => Unit{}, MI.HsMichael.key(B.Octets.zeros(7n))) == Fail{Hs.HsBadKeyLength{7n}} : Result<&2, &2, Hs.HsError, Unit>}