law michael_mic_length

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

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

394# Michael (IEEE 802.11i): the tag of every message under every key has 8 bytes
395law michael_mic_length:
396  for +k: Hs.HsW2
397  for +m: B.Octets
398  {B.Octets.len(MI.HsMichael.mic(k, m)) == 8n : Nat}