1	# XCBC-MAC over any block cipher (the block-cipher interface, block.bend), as
2	# RFC 3566 (The AES-XCBC-MAC-96 Algorithm and Its Use With IPsec, 2003)
3	# defines it for AES-128, after J. Black and P. Rogaway's three-key
4	# construction:
5	#   K1 = E(K, 0x01..01), K2 = E(K, 0x02..02), K3 = E(K, 0x03..03)
6	#   E[0] = 0; E[i] = E(K1, M[i] xor E[i-1]) for every block but the last;
7	#   the last block whole:  E[n] = E(K1, M[n] xor E[n-1] xor K2)
8	#   the last block short (or an empty message): padded with one 1 bit and
9	#   zeros to a block, E[n] = E(K1, pad(M[n]) xor E[n-1] xor K3)
10	# and the tag is E[n] (RFC 3566 truncates it to 96 bits for IPsec:
11	# CrXcbc.mac96). Over another cipher the constants are blocks of 0x01, 0x02,
12	# 0x03 bytes of its block size, and K1 must be a key the cipher takes (its
13	# key size equal to its block size, as for AES-128).
14	#
15	# As a MAC (mac.bend): ~CrXcbcKey<K>, ~CrXcbc.key(..), ~CrXcbc.mac(..),
16	# ~CrXcbc.verify(..), verify the interface's named default, so the MAC laws
17	# hold for XCBC over every cipher (LAWS.bend: xcbc_accepts).
18	import Base
19	import bend-osdev-bytes@0.1.0.0/bytes.bend as B
20	import ./crypto.bend as Cr
21	import ./mac.bend as Mc
22	import ./octets.bend as O
23	
24	# one block of bytes encrypted (a string the format refuses stays as it is)
25	def cr.xcbc.encb(~K: Data, ~Blk: Data, ~enc: K -> Blk -> Blk, ~blk_to: Blk -> B.Octets, +k: K, x: Maybe<&2, Blk>, +o: B.Octets) -> B.Octets:
26	  match x:
27	    case None{}:
28	      o
29	    case Some{b}:
30	      blk_to(enc(k, b))
31	
32	def cr.xcbc.e(~K: Data, ~Blk: Data, ~enc: K -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, +k: K, +o: B.Octets) -> B.Octets:
33	  cr.xcbc.encb(~K, ~Blk, ~enc, ~blk_to, k, blk_of(o), o)
34	
35	# An XCBC key: the cipher's key schedule of K1, and K2 and K3 as bytes
36	type CrXcbcKey<-K: Data> is Data:
37	  CrXcbcKey{k1: K, k2: B.Octets, k3: B.Octets}
38	
39	def cr.xcbc.key.of(~K: Data, ~Blk: Data, ~bsize: Nat, ~key: B.Octets -> Result<&2, &2, Cr.CrError, K>, ~enc: K -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, +k: K) -> Result<&2, &2, Cr.CrError, CrXcbcKey<K>>:
40	  +k2 = cr.xcbc.e(~K, ~Blk, ~enc, ~blk_of, ~blk_to, k, O.CrOct.rep(bsize, 2))
41	  +k3 = cr.xcbc.e(~K, ~Blk, ~enc, ~blk_of, ~blk_to, k, O.CrOct.rep(bsize, 3))
42	  Result.map(&2, &2, Cr.CrError, K, CrXcbcKey<K>, k1 => CrXcbcKey{k1, k2, k3}, key(cr.xcbc.e(~K, ~Blk, ~enc, ~blk_of, ~blk_to, k, O.CrOct.rep(bsize, 1))))
43	
44	# The key from a raw key K (refused when the cipher refuses K or K1)
45	def CrXcbc.key(~K: Data, ~Blk: Data, ~bsize: Nat, ~key: B.Octets -> Result<&2, &2, Cr.CrError, K>, ~enc: K -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, o: B.Octets) -> Result<&2, &2, Cr.CrError, CrXcbcKey<K>>:
46	  Result.bind(&2, &2, Cr.CrError, K, CrXcbcKey<K>, key(o), k => cr.xcbc.key.of(~K, ~Blk, ~bsize, ~key, ~enc, ~blk_of, ~blk_to, k))
47	
48	def cr.xcbc.full(full: Bool, +bsize: Nat, +k2: B.Octets, +k3: B.Octets, +p: B.Octets) -> B.Octets:
49	  match full:
50	    case True{}:
51	      O.CrOct.xor(p, k2)
52	    case False{}:
53	      O.CrOct.xor(B.Octets.append(p, B.Octets.cons(128, B.Octets.zeros(Nat.sub(bsize, Nat.add(B.Octets.len(p), 1n))))), k3)
54	
55	# the CBC-MAC over the pieces from E = e; the last piece is whole or short
56	def cr.xcbc.go(~K: Data, ~Blk: Data, ~bsize: Nat, ~enc: K -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, +k1: K, +k2: B.Octets, +k3: B.Octets, ps: List<&2, List<&2, U32>>, +e: B.Octets) -> B.Octets:
57	  match ps:
58	    case Nil{}:
59	      cr.xcbc.e(~K, ~Blk, ~enc, ~blk_of, ~blk_to, k1, O.CrOct.xor(cr.xcbc.full(False{}, bsize, k2, k3, B.Octets.empty()), e))
60	    case Con{p, t}:
61	      match t:
62	        case Nil{}:
63	          +po = B.Octets.of_list(p)
64	          cr.xcbc.e(~K, ~Blk, ~enc, ~blk_of, ~blk_to, k1, O.CrOct.xor(cr.xcbc.full(Nat.is_eq(B.Octets.len(po), bsize), bsize, k2, k3, po), e))
65	        case Con{q, u}:
66	          cr.xcbc.go(~K, ~Blk, ~bsize, ~enc, ~blk_of, ~blk_to, k1, k2, k3, Con{q, u}, cr.xcbc.e(~K, ~Blk, ~enc, ~blk_of, ~blk_to, k1, O.CrOct.xor(B.Octets.of_list(p), e)))
67	
68	# The tag of m (one block)
69	def CrXcbc.mac(~K: Data, ~Blk: Data, ~bsize: Nat, ~enc: K -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, kk: CrXcbcKey<K>, m: B.Octets) -> B.Octets:
70	  match kk:
71	    case CrXcbcKey{+k1, +k2, +k3}:
72	      cr.xcbc.go(~K, ~Blk, ~bsize, ~enc, ~blk_of, ~blk_to, k1, k2, k3, O.CrOct.pieces(bsize, B.Octets.to_list(m)), B.Octets.zeros(bsize))
73	
74	# RFC 3566's AES-XCBC-MAC-96: the tag's first 12 bytes
75	def CrXcbc.mac96(~K: Data, ~Blk: Data, ~bsize: Nat, ~enc: K -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, kk: CrXcbcKey<K>, m: B.Octets) -> B.Octets:
76	  B.Octets.take(12n, CrXcbc.mac(~K, ~Blk, ~bsize, ~enc, ~blk_of, ~blk_to, kk, m))
77	
78	# whether t is m's tag (every byte compared; the MAC interface's default)
79	def CrXcbc.verify(~K: Data, ~Blk: Data, ~bsize: Nat, ~enc: K -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, kk: CrXcbcKey<K>, m: B.Octets, t: B.Octets) -> Bool:
80	  Mc.CrMac.verify_tag(~CrXcbcKey<K>, ~CrXcbc.mac(~K, ~Blk, ~bsize, ~enc, ~blk_of, ~blk_to), kk, m, t)