1	# XTS (IEEE Std 1619-2007, XTS-AES; NIST SP 800-38E), the tweakable mode for
2	# storage, over any 128-bit block cipher (see cipher-modes.bend for the
3	# template arguments). A data unit (a sector) is encrypted under two keys: k1
4	# for the data and k2 for the tweak. With i the data unit's 128-bit sequence
5	# number, as 16 little-endian bytes:
6	#   T_0 = E(k2, i),  T_(j+1) = T_j * alpha  (in GF(2^128), below)
7	#   C_j = E(k1, P_j xor T_j) xor T_j
8	# A data unit of at least 16 bytes whose length is not a multiple of 16 ends
9	# with ciphertext stealing (IEEE 1619, 5.3.2): the last full block's
10	# ciphertext lends its tail to pad the partial block.
11	import Base
12	import bend-osdev-bytes@0.1.0.0/bytes.bend as B
13	import bend-osdev-word64@0.1.0.0/word64.bend as W
14	import ./cipher_modes.bend as M
15	
16	# Multiplication by alpha (the polynomial x) in GF(2^128) modulo
17	# x^128 + x^7 + x^2 + x + 1, with the block read as a little-endian number
18	# (IEEE 1619, 5.2): every byte shifts left one bit, taking the top bit of the
19	# byte before it; the top bit of byte 15 wraps round as 135 (0x87) into byte 0.
20	
21	# each byte of w shifted left, with the carries between w's own bytes
22	def xts.shift(+w: U32) -> U32:
23	  U32.or(U32.and(4278124286, U32.shl(w)), U32.and(65793, U32.shrn(w, 15n)))
24	
25	# the carry out of w's last byte, into the first byte of the next word
26	def xts.carry(w: U32) -> U32:
27	  U32.shln(U32.and(128, w), 17n)
28	
29	def Xts.mul_alpha(t: M.CmBlock) -> M.CmBlock:
30	  match t:
31	    case M.CmBlock{+w0, +w1, +w2, +w3}:
32	      M.CmBlock{U32.xor(xts.shift(w0), U32.and(2264924160, M.cm.mask(U32.shrn(w3, 7n)))), U32.or(xts.shift(w1), xts.carry(w0)), U32.or(xts.shift(w2), xts.carry(w1)), U32.or(xts.shift(w3), xts.carry(w2))}
33	
34	# One block under tweak t
35	
36	def xts.benc(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, p: M.CmBlock, +t: M.CmBlock) -> M.CmBlock:
37	  M.CmBlock.xor(enc(k, M.CmBlock.xor(p, t)), t)
38	
39	def xts.bdec(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, c: M.CmBlock, +t: M.CmBlock) -> M.CmBlock:
40	  M.CmBlock.xor(dec(k, M.CmBlock.xor(c, t)), t)
41	
42	# The block layer: whole blocks from tweak t (t = T_j for the first of them)
43	
44	def xts.enc(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, bs: List<&2, M.CmBlock>, +t: M.CmBlock) -> List<&2, M.CmBlock>:
45	  match bs:
46	    case Nil{}:
47	      Nil{}
48	    case Con{p, rest}:
49	      Con{xts.benc(~K, ~enc, k, p, t), xts.enc(~K, ~enc, k, rest, Xts.mul_alpha(t))}
50	
51	def xts.dec(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, bs: List<&2, M.CmBlock>, +t: M.CmBlock) -> List<&2, M.CmBlock>:
52	  match bs:
53	    case Nil{}:
54	      Nil{}
55	    case Con{c, rest}:
56	      Con{xts.bdec(~K, ~dec, k, c, t), xts.dec(~K, ~dec, k, rest, Xts.mul_alpha(t))}
57	
58	# The same, tail-recursive (the blocks so far kept reversed in acc), so a
59	# data unit can be of any length: PROOF.bend proves each equal to its
60	# structural form above for every input
61	
62	def xts.enc.go(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, bs: List<&2, M.CmBlock>, +t: M.CmBlock, acc: List<&2, M.CmBlock>) -> List<&2, M.CmBlock>:
63	  match bs:
64	    case Nil{}:
65	      M.cm.blocks.rev_onto(acc, Nil{})
66	    case Con{p, rest}:
67	      xts.enc.go(~K, ~enc, k, rest, Xts.mul_alpha(t), Con{xts.benc(~K, ~enc, k, p, t), acc})
68	
69	def xts.enc.fast(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, bs: List<&2, M.CmBlock>, +t: M.CmBlock) -> List<&2, M.CmBlock>:
70	  xts.enc.go(~K, ~enc, k, bs, t, Nil{})
71	
72	def xts.dec.go(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, bs: List<&2, M.CmBlock>, +t: M.CmBlock, acc: List<&2, M.CmBlock>) -> List<&2, M.CmBlock>:
73	  match bs:
74	    case Nil{}:
75	      M.cm.blocks.rev_onto(acc, Nil{})
76	    case Con{c, rest}:
77	      xts.dec.go(~K, ~dec, k, rest, Xts.mul_alpha(t), Con{xts.bdec(~K, ~dec, k, c, t), acc})
78	
79	def xts.dec.fast(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, bs: List<&2, M.CmBlock>, +t: M.CmBlock) -> List<&2, M.CmBlock>:
80	  xts.dec.go(~K, ~dec, k, bs, t, Nil{})
81	
82	def Xts.encrypt_blocks(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k1: K, t: M.CmBlock, bs: List<&2, M.CmBlock>) -> List<&2, M.CmBlock>:
83	  xts.enc.fast(~K, ~enc, k1, bs, t)
84	
85	def Xts.decrypt_blocks(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k1: K, t: M.CmBlock, bs: List<&2, M.CmBlock>) -> List<&2, M.CmBlock>:
86	  xts.dec.fast(~K, ~dec, k1, bs, t)
87	
88	# T_0: the encrypted sequence number
89	def Xts.tweak(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k2: K, i: M.CmBlock) -> M.CmBlock:
90	  enc(k2, i)
91	
92	# the 16-byte sequence number of data unit n (a sector number): n in
93	# little-endian order, then zeros
94	def Xts.sector(n: W.W64) -> B.Octets:
95	  B.Octets.append(B.Octets.le64(n), B.Octets.zeros(8n))
96	
97	# The byte layer, with ciphertext stealing (IEEE 1619, 5.3.2). A data unit
98	# is its whole blocks and a tail of 0 to 15 bytes. All whole blocks but the
99	# last go through the block layer; the last one and the tail are encrypted
100	# together, by steal_c (the last full ciphertext block) and steal_t (the
101	# final partial one), from the tweak t = T_(n-1).
102	
103	# T_0 * alpha^n
104	def xts.alpha_n(n: Nat, +t: M.CmBlock) -> M.CmBlock:
105	  match n:
106	    case 0n:
107	      t
108	    case 1n+q:
109	      xts.alpha_n(q, Xts.mul_alpha(t))
110	
111	def xts.steal_c.go(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, partial: Bool, +k: K, p: M.CmBlock, +tail: List<&2, U32>, +t: M.CmBlock) -> M.CmBlock:
112	  match partial:
113	    case False{}:
114	      xts.benc(~K, ~enc, k, p, t)
115	    case True{}:
116	      +cc = M.cm.bytes_of(xts.benc(~K, ~enc, k, p, t))
117	      xts.benc(~K, ~enc, k, M.cm.block_of(B.append(tail, B.drop(B.len(tail), cc))), Xts.mul_alpha(t))
118	
119	def xts.steal_t.go(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, partial: Bool, +k: K, p: M.CmBlock, +tail: List<&2, U32>, +t: M.CmBlock) -> List<&2, U32>:
120	  match partial:
121	    case False{}:
122	      Nil{}
123	    case True{}:
124	      B.take(B.len(tail), M.cm.bytes_of(xts.benc(~K, ~enc, k, p, t)))
125	
126	# the ciphertext of the last whole block p and the tail, under tweak t
127	def xts.steal_c(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, p: M.CmBlock, +tail: List<&2, U32>, +t: M.CmBlock) -> M.CmBlock:
128	  xts.steal_c.go(~K, ~enc, Nat.is_lt(0n, B.len(tail)), k, p, tail, t)
129	
130	def xts.steal_t(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, p: M.CmBlock, +tail: List<&2, U32>, +t: M.CmBlock) -> List<&2, U32>:
131	  xts.steal_t.go(~K, ~enc, Nat.is_lt(0n, B.len(tail)), k, p, tail, t)
132	
133	# the plaintext of the last whole ciphertext block c and the tail
134	def xts.dsteal.go(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, partial: Bool, +k: K, c: M.CmBlock, +tail: List<&2, U32>, +t: M.CmBlock) -> List<&2, U32>:
135	  match partial:
136	    case False{}:
137	      M.cm.bytes_of(xts.bdec(~K, ~dec, k, c, t))
138	    case True{}:
139	      +pp = M.cm.bytes_of(xts.bdec(~K, ~dec, k, c, Xts.mul_alpha(t)))
140	      M.cm.bytes_onto(xts.bdec(~K, ~dec, k, M.cm.block_of(B.append(tail, B.drop(B.len(tail), pp))), t), B.take(B.len(tail), pp))
141	
142	def xts.dsteal(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, c: M.CmBlock, +tail: List<&2, U32>, +t: M.CmBlock) -> List<&2, U32>:
143	  xts.dsteal.go(~K, ~dec, Nat.is_lt(0n, B.len(tail)), k, c, tail, t)
144	
145	# all but the last of p then rest; and the last
146	def xts.init(rest: List<&2, M.CmBlock>, p: M.CmBlock) -> List<&2, M.CmBlock>:
147	  match rest:
148	    case Nil{}:
149	      Nil{}
150	    case Con{q, r}:
151	      Con{p, xts.init(r, q)}
152	
153	def xts.last(rest: List<&2, M.CmBlock>, p: M.CmBlock) -> M.CmBlock:
154	  match rest:
155	    case Nil{}:
156	      p
157	    case Con{q, r}:
158	      xts.last(r, q)
159	
160	def xts.eout(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, +t: M.CmBlock, +init: List<&2, M.CmBlock>, +last: M.CmBlock, +tail: List<&2, U32>) -> List<&2, U32>:
161	  +tl = xts.alpha_n(List.length(&2, M.CmBlock, init), t)
162	  M.cm.join_onto(List.append(&2, M.CmBlock, xts.enc(~K, ~enc, k, init, t), Con{xts.steal_c(~K, ~enc, k, last, tail, tl), Nil{}}), xts.steal_t(~K, ~enc, k, last, tail, tl))
163	
164	def xts.dout(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, +t: M.CmBlock, +init: List<&2, M.CmBlock>, +last: M.CmBlock, +tail: List<&2, U32>) -> List<&2, U32>:
165	  M.cm.join_onto(xts.dec(~K, ~dec, k, init, t), xts.dsteal(~K, ~dec, k, last, tail, xts.alpha_n(List.length(&2, M.CmBlock, init), t)))
166	
167	def xts.e2(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, +t: M.CmBlock, s: M.CmSplit, +n: Nat) -> Result<&2, &2, M.CmError, B.Octets>:
168	  match s:
169	    case M.CmSplit{bs, tail}:
170	      match bs:
171	        case Nil{}:
172	          Fail{M.CmTooShort{n}}
173	        case Con{+p, +rest}:
174	          Done{B.Octets.of_list(xts.eout(~K, ~enc, k, t, xts.init(rest, p), xts.last(rest, p), tail))}
175	
176	def xts.d2(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, +t: M.CmBlock, s: M.CmSplit, +n: Nat) -> Result<&2, &2, M.CmError, B.Octets>:
177	  match s:
178	    case M.CmSplit{bs, tail}:
179	      match bs:
180	        case Nil{}:
181	          Fail{M.CmTooShort{n}}
182	        case Con{+c, +rest}:
183	          Done{B.Octets.of_list(xts.dout(~K, ~dec, k, t, xts.init(rest, c), xts.last(rest, c), tail))}
184	
185	def xts.e1(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, r: Result<&2, &2, M.CmError, M.CmBlock>, +xs: List<&2, U32>) -> Result<&2, &2, M.CmError, B.Octets>:
186	  match r:
187	    case Fail{e}:
188	      Fail{e}
189	    case Done{t}:
190	      xts.e2(~K, ~enc, k, t, M.cm.split(xs), B.len(xs))
191	
192	def xts.d1(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, r: Result<&2, &2, M.CmError, M.CmBlock>, +xs: List<&2, U32>) -> Result<&2, &2, M.CmError, B.Octets>:
193	  match r:
194	    case Fail{e}:
195	      Fail{e}
196	    case Done{t}:
197	      xts.d2(~K, ~dec, k, t, M.cm.split(xs), B.len(xs))
198	
199	def xts.tweak.go(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k2: K, r: Result<&2, &2, M.CmError, M.CmBlock>) -> Result<&2, &2, M.CmError, M.CmBlock>:
200	  match r:
201	    case Fail{e}:
202	      Fail{e}
203	    case Done{v}:
204	      Done{enc(k2, v)}
205	
206	# T_0, from the 16-byte sequence number i
207	def xts.tweak(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k2: K, i: B.Octets) -> Result<&2, &2, M.CmError, M.CmBlock>:
208	  +xs = B.Octets.to_list(i)
209	  xts.tweak.go(~K, ~enc, k2, M.cm.need_block(xs, M.CmBadTweakLength{B.len(xs)}))
210	
211	# The byte layer, tail-recursive: what Xts.encrypt and Xts.decrypt run
212	# (xts.init .. xts.d1 are the structural forms; PROOF.bend: xtsp.e1_eq,
213	# d1_eq)
214	
215	def xts.init.go(rest: List<&2, M.CmBlock>, p: M.CmBlock, acc: List<&2, M.CmBlock>) -> List<&2, M.CmBlock>:
216	  match rest:
217	    case Nil{}:
218	      M.cm.blocks.rev_onto(acc, Nil{})
219	    case Con{q, r}:
220	      xts.init.go(r, q, Con{p, acc})
221	
222	def xts.init.fast(rest: List<&2, M.CmBlock>, p: M.CmBlock) -> List<&2, M.CmBlock>:
223	  xts.init.go(rest, p, Nil{})
224	
225	def xts.eout.fast(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, +t: M.CmBlock, +init: List<&2, M.CmBlock>, +last: M.CmBlock, +tail: List<&2, U32>) -> List<&2, U32>:
226	  +tl = xts.alpha_n(M.cm.blocks.len(init), t)
227	  M.cm.join_onto.fast(M.cm.blocks.append(xts.enc.fast(~K, ~enc, k, init, t), Con{xts.steal_c(~K, ~enc, k, last, tail, tl), Nil{}}), xts.steal_t(~K, ~enc, k, last, tail, tl))
228	
229	def xts.dout.fast(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, +t: M.CmBlock, +init: List<&2, M.CmBlock>, +last: M.CmBlock, +tail: List<&2, U32>) -> List<&2, U32>:
230	  M.cm.join_onto.fast(xts.dec.fast(~K, ~dec, k, init, t), xts.dsteal(~K, ~dec, k, last, tail, xts.alpha_n(M.cm.blocks.len(init), t)))
231	
232	def xts.e2.fast(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, +t: M.CmBlock, s: M.CmSplit, +n: Nat) -> Result<&2, &2, M.CmError, B.Octets>:
233	  match s:
234	    case M.CmSplit{bs, tail}:
235	      match bs:
236	        case Nil{}:
237	          Fail{M.CmTooShort{n}}
238	        case Con{+p, +rest}:
239	          Done{B.Octets.of_list(xts.eout.fast(~K, ~enc, k, t, xts.init.fast(rest, p), xts.last(rest, p), tail))}
240	
241	def xts.d2.fast(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, +t: M.CmBlock, s: M.CmSplit, +n: Nat) -> Result<&2, &2, M.CmError, B.Octets>:
242	  match s:
243	    case M.CmSplit{bs, tail}:
244	      match bs:
245	        case Nil{}:
246	          Fail{M.CmTooShort{n}}
247	        case Con{+c, +rest}:
248	          Done{B.Octets.of_list(xts.dout.fast(~K, ~dec, k, t, xts.init.fast(rest, c), xts.last(rest, c), tail))}
249	
250	def xts.e1.fast(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, r: Result<&2, &2, M.CmError, M.CmBlock>, +xs: List<&2, U32>) -> Result<&2, &2, M.CmError, B.Octets>:
251	  match r:
252	    case Fail{e}:
253	      Fail{e}
254	    case Done{t}:
255	      xts.e2.fast(~K, ~enc, k, t, M.cm.split.fast(xs), B.len.fast(xs))
256	
257	def xts.d1.fast(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, r: Result<&2, &2, M.CmError, M.CmBlock>, +xs: List<&2, U32>) -> Result<&2, &2, M.CmError, B.Octets>:
258	  match r:
259	    case Fail{e}:
260	      Fail{e}
261	    case Done{t}:
262	      xts.d2.fast(~K, ~dec, k, t, M.cm.split.fast(xs), B.len.fast(xs))
263	
264	# Xts.encrypt and Xts.decrypt through the structural forms (the laws' proofs
265	# reason about these; PROOF.bend proves them equal to the public defs)
266	def Xts.encrypt.ref(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k1: K, +k2: K, i: B.Octets, p: B.Octets) -> Result<&2, &2, M.CmError, B.Octets>:
267	  xts.e1(~K, ~enc, k1, xts.tweak(~K, ~enc, k2, i), B.Octets.to_list(p))
268	
269	def Xts.decrypt.ref(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, ~dec: K -> M.CmBlock -> M.CmBlock, +k1: K, +k2: K, i: B.Octets, c: B.Octets) -> Result<&2, &2, M.CmError, B.Octets>:
270	  xts.d1(~K, ~dec, k1, xts.tweak(~K, ~enc, k2, i), B.Octets.to_list(c))
271	
272	# the data unit p (at least 16 bytes) with sequence number i (16 bytes)
273	def Xts.encrypt(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k1: K, +k2: K, i: B.Octets, p: B.Octets) -> Result<&2, &2, M.CmError, B.Octets>:
274	  xts.e1.fast(~K, ~enc, k1, xts.tweak(~K, ~enc, k2, i), B.Octets.to_list(p))
275	
276	# decryption needs enc too: the tweak is always encrypted
277	def Xts.decrypt(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, ~dec: K -> M.CmBlock -> M.CmBlock, +k1: K, +k2: K, i: B.Octets, c: B.Octets) -> Result<&2, &2, M.CmError, B.Octets>:
278	  xts.d1.fast(~K, ~dec, k1, xts.tweak(~K, ~enc, k2, i), B.Octets.to_list(c))