1	# CMAC (NIST SP 800-38B; RFC 4493 for AES-CMAC), a MAC over any 128-bit
2	# block cipher (only its encryption is used; see cipher-modes.bend for the
3	# template arguments).
4	#   L = E(0^128), K1 = dbl(L), K2 = dbl(K1)
5	#   dbl(X) = X << 1, xor 0x87 into the last byte when X's top bit was set
6	#   the message in 16-byte blocks M_1 .. M_n (n >= 1); the last is xored with
7	#   K1 if it is whole, else padded with 0x80 0x00 .. and xored with K2;
8	#   the MAC is the last block of their CBC encryption (IV 0).
9	# A message may arrive in pieces: start, update (any number of times) and
10	# finish give the MAC of the pieces joined.
11	import Base
12	import bend-osdev-bytes@0.1.0.0/bytes.bend as B
13	import ./cipher_modes.bend as M
14	
15	# Subkeys
16	
17	def Cmac.dbl(b: M.CmBlock) -> M.CmBlock:
18	  match b:
19	    case M.CmBlock{+w0, +w1, +w2, +w3}:
20	      M.CmBlock{U32.or(U32.shl(w0), U32.shrn(w1, 31n)), U32.or(U32.shl(w1), U32.shrn(w2, 31n)), U32.or(U32.shl(w2), U32.shrn(w3, 31n)), U32.xor(U32.shl(w3), U32.and(135, M.cm.mask(U32.shrn(w0, 31n))))}
21	
22	def cmac.k1(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K) -> M.CmBlock:
23	  Cmac.dbl(enc(k, M.CmBlock.zero()))
24	
25	def cmac.k2(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K) -> M.CmBlock:
26	  Cmac.dbl(cmac.k1(~K, ~enc, k))
27	
28	# the subkeys K1 and K2
29	def Cmac.subkey1(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K) -> M.CmBlock:
30	  cmac.k1(~K, ~enc, k)
31	
32	def Cmac.subkey2(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K) -> M.CmBlock:
33	  cmac.k2(~K, ~enc, k)
34	
35	# The state: the chaining value x, and the bytes not yet processed (at most
36	# 16, newest first) and their count. A full buffer is kept until the next byte
37	# arrives, since the last block is treated differently.
38	type CmacState is Data:
39	  CmacState{x: M.CmBlock, buf: List<&2, U32>, n: Nat}
40	
41	def Cmac.start() -> CmacState:
42	  CmacState{M.CmBlock.zero(), Nil{}, 0n}
43	
44	def cmac.push(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, full: Bool, +k: K, x: M.CmBlock, buf: List<&2, U32>, +n: Nat, b: U32) -> CmacState:
45	  match full:
46	    case True{}:
47	      CmacState{enc(k, M.CmBlock.xor(x, M.cm.block_of(List.reverse(&2, U32, buf)))), Con{b, Nil{}}, 1n}
48	    case False{}:
49	      CmacState{x, Con{b, buf}, 1n+n}
50	
51	def cmac.step(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, s: CmacState, b: U32) -> CmacState:
52	  match s:
53	    case CmacState{x, buf, +n}:
54	      cmac.push(~K, ~enc, Nat.is_eq(n, 16n), k, x, buf, n, b)
55	
56	def cmac.feed(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, xs: List<&2, U32>, s: CmacState) -> CmacState:
57	  match xs:
58	    case Nil{}:
59	      s
60	    case Con{h, t}:
61	      cmac.feed(~K, ~enc, k, t, cmac.step(~K, ~enc, k, s, h))
62	
63	# the state after the bytes of m
64	def Cmac.update(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, s: CmacState, m: B.Octets) -> CmacState:
65	  cmac.feed(~K, ~enc, k, B.Octets.to_list(m), s)
66	
67	# the last block: whole, xor K1; partial (or empty), padded, xor K2
68	def cmac.last(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, full: Bool, +k: K, x: M.CmBlock, last: List<&2, U32>) -> M.CmBlock:
69	  match full:
70	    case True{}:
71	      enc(k, M.CmBlock.xor(M.CmBlock.xor(x, M.cm.block_of(last)), cmac.k1(~K, ~enc, k)))
72	    case False{}:
73	      enc(k, M.CmBlock.xor(M.CmBlock.xor(x, M.cm.block_of(B.append(last, Con{128, Nil{}}))), cmac.k2(~K, ~enc, k)))
74	
75	# the 16-byte MAC
76	def Cmac.finish(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, s: CmacState) -> B.Octets:
77	  match s:
78	    case CmacState{x, buf, +n}:
79	      M.CmBlock.to_octets(cmac.last(~K, ~enc, Nat.is_eq(n, 16n), k, x, List.reverse(&2, U32, buf)))
80	
81	# The MAC of m in one call
82	def Cmac.mac(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, m: B.Octets) -> B.Octets:
83	  Cmac.finish(~K, ~enc, k, Cmac.update(~K, ~enc, k, Cmac.start(), m))
84	
85	# whether tag is m's 16-byte MAC, compared with no early exit
86	def Cmac.verify(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, m: B.Octets, tag: B.Octets) -> Bool:
87	  M.cm.ct_eq(B.Octets.to_list(Cmac.mac(~K, ~enc, k, m)), B.Octets.to_list(tag))