michael.bend

bend-osdev-hashes@0.1.0.0 · 78 lines · 10 definitions

1# Michael, the message integrity code of TKIP (IEEE Std 802.11i-2004; the
2# algorithm as A. Wool, IEEE Trans. Wireless Commun. 3(5), 2004, Fig. 1,
3# and Huang, Seberry, Susilo and Bunder, LNCS 3823, 2005, Algorithms 2.1
4# and 2.2, describe it; README.md): a 64-bit tag under a 64-bit key, over
5# 32-bit words, little-endian (the byte order those sources do not state;
6# IEEE 802.11-2012 M.6.3's TKIP vector confirms it, while the six recalled
7# test vectors are unverified: README.md). With the key (K0, K1) as two
8# little-endian words, (L, R) = (K0, K1); the message is padded with the
9# byte 0x5a and four to seven zero bytes to a multiple of four bytes; each
10# word M_i is taken in by L = L xor M_i, (L, R) = b(L, R), where b is
11#   R ^= L <<< 17; L += R; R ^= XSWAP(L); L += R;
12#   R ^= L <<< 3;  L += R; R ^= L >>> 2;   L += R
13# (XSWAP swaps the two bytes of each 16-bit half); the tag is L and R,
14# little-endian. Michael was designed for the old hardware TKIP runs on,
15# for a security level of only about 20 bits: it is here for TKIP.
16#
17# It streams through the engine with four-byte blocks (~last = 3). As a MAC
18# the crypto package adapts it (crypto/inst_michael.bend).
19import Base
20import bend-osdev-bytes@0.1.0.0/bytes.bend as B
21import bend-osdev-hashes@0.1.0.0/hashes.bend as Hs
22
23# the block function b
24def hs.michael.b(lr: Hs.HsW2) -> Hs.HsW2:
25  match lr:
26    case Hs.HsW2{+l0, r0}:
27      +r1 = U32.xor(r0, Hs.hs.rotl(l0, 17n))
28      +l1 = U32.add(l0, r1)
29      +r2 = U32.xor(r1, U32.or(U32.shrn(U32.and(4278255360, l1), 8n), U32.shln(U32.and(16711935, l1), 8n)))
30      +l2 = U32.add(l1, r2)
31      +r3 = U32.xor(r2, Hs.hs.rotl(l2, 3n))
32      +l3 = U32.add(l2, r3)
33      +r4 = U32.xor(r3, Hs.hs.rotl(l3, 30n))
34      Hs.HsW2{U32.add(l3, r4), r4}
35
36def hs.michael.word(lr: Hs.HsW2, w: U32) -> Hs.HsW2:
37  match lr:
38    case Hs.HsW2{l, r}:
39      hs.michael.b(Hs.HsW2{U32.xor(l, w), r})
40
41# One four-byte word (any other length leaves the value unchanged)
42def HsMichael.compress(lr: Hs.HsW2, blk: List<&2, U32>) -> Hs.HsW2:
43  match blk:
44    case [b0, b1, b2, b3]:
45      hs.michael.word(lr, Hs.hs.le(b0, b1, b2, b3))
46    case _:
47      lr
48
49# The key: eight bytes, as (K0, K1) (HsBadKeyLength otherwise)
50def hs.michael.key(xs: List<&2, U32>) -> Result<&2, &2, Hs.HsError, Hs.HsW2>:
51  match xs:
52    case [a0, a1, a2, a3, b0, b1, b2, b3]:
53      Done{Hs.HsW2{Hs.hs.le(a0, a1, a2, a3), Hs.hs.le(b0, b1, b2, b3)}}
54    case _:
55      Fail{Hs.HsBadKeyLength{B.len(xs)}}
56
57def HsMichael.key(o: B.Octets) -> Result<&2, &2, Hs.HsError, Hs.HsW2>:
58  hs.michael.key(B.Octets.to_list(o))
59
60# the state before any byte, under a key
61def HsMichael.init(k: Hs.HsW2) -> Hs.HsMdState<Hs.HsW2>:
62  Hs.HsMd.start(~Hs.HsW2, k)
63
64def HsMichael.update(s: Hs.HsMdState<Hs.HsW2>, o: B.Octets) -> Hs.HsMdState<Hs.HsW2>:
65  Hs.HsMd.update(~Hs.HsW2, ~HsMichael.compress, ~3, s, o)
66
67# the padding after cnt bytes of an unfinished word: 0x5a, then four to
68# seven zeros, to a whole number of words
69def hs.michael.pad(cnt: U32) -> List<&2, U32>:
70  Con{90, B.zeros(U32.to_nat(U32.add(4, U32.and(U32.sub(3, cnt), 3))))}
71
72# the tag of the bytes so far
73def HsMichael.final(+s: Hs.HsMdState<Hs.HsW2>) -> B.Octets:
74  Hs.HsW2.le(Hs.HsMd.cv(~Hs.HsW2, Hs.HsMd.update_list(~Hs.HsW2, ~HsMichael.compress, ~3, s, hs.michael.pad(Hs.HsMd.count(~Hs.HsW2, s)))))
75
76# The tag in one call
77def HsMichael.mic(k: Hs.HsW2, o: B.Octets) -> B.Octets:
78  HsMichael.final(HsMichael.update(HsMichael.init(k), o))