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).
19	import Base
20	import bend-osdev-bytes@0.1.0.0/bytes.bend as B
21	import ./hashes.bend as Hs
22	
23	# the block function b
24	def 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	
36	def 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)
42	def 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)
50	def 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	
57	def 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
61	def HsMichael.init(k: Hs.HsW2) -> Hs.HsMdState<Hs.HsW2>:
62	  Hs.HsMd.start(~Hs.HsW2, k)
63	
64	def 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
69	def 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
73	def 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
77	def HsMichael.mic(k: Hs.HsW2, o: B.Octets) -> B.Octets:
78	  HsMichael.final(HsMichael.update(HsMichael.init(k), o))