inst_michael.bend

bend-osdev-crypto@0.1.0.0 · 25 lines · 3 definitions

1# Michael (IEEE 802.11i's TKIP MIC; hashes/michael.bend) as a MAC: the
2# adapter for the hashes package's Michael, its key error mapped onto
3# CrError. The instance:
4#   ~Hs.HsW2, ~CrMichael.key, ~MI.HsMichael.mic, ~CrMichael.verify
5# (a key of 8 bytes; the tag is 8 bytes). Michael is weak by design (see
6# hashes/README.md): it is here for TKIP.
7import Base
8import bend-osdev-bytes@0.1.0.0/bytes.bend as B
9import bend-osdev-hashes@0.1.0.0/hashes.bend as Hs
10import bend-osdev-hashes@0.1.0.0/michael.bend as MI
11import bend-osdev-crypto@0.1.0.0/crypto.bend as Cr
12import bend-osdev-crypto@0.1.0.0/mac.bend as Mc
13
14def CrMichael.err(e: Hs.HsError) -> Cr.CrError:
15  match e:
16    case Hs.HsBadKeyLength{n}:
17      Cr.CrBadKeyLength{n}
18
19# the key of 8 raw bytes (CrBadKeyLength otherwise)
20def CrMichael.key(o: B.Octets) -> Result<&2, &2, Cr.CrError, Hs.HsW2>:
21  Cr.CrError.lift(~Hs.HsError, ~Hs.HsW2, ~CrMichael.err, MI.HsMichael.key(o))
22
23# whether t is m's tag (the named default verify: every byte compared)
24def CrMichael.verify(k: Hs.HsW2, m: B.Octets, t: B.Octets) -> Bool:
25  Mc.CrMac.verify_tag(~Hs.HsW2, ~MI.HsMichael.mic, k, m, t)