xts.bend

bend-osdev-cipher-modes@0.1.0.0 · 278 lines · 44 definitions

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.
11import Base
12import bend-osdev-bytes@0.1.0.0/bytes.bend as B
13import bend-osdev-word64@0.1.0.0/word64.bend as W
14import bend-osdev-cipher-modes@0.1.0.0/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
22def 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
26def xts.carry(w: U32) -> U32:
27  U32.shln(U32.and(128, w), 17n)
28
29def 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
36def 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
39def 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
44def 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
51def 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
62def 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
69def 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
72def 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
79def 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
82def 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
85def 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
89def 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
94def 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
104def 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
111def 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
119def 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
127def 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
130def 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
134def 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
142def 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
146def 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
153def 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
160def 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
164def 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
167def 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
176def 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
185def 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
192def 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
199def 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
207def 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
215def 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
222def xts.init.fast(rest: List<&2, M.CmBlock>, p: M.CmBlock) -> List<&2, M.CmBlock>:
223  xts.init.go(rest, p, Nil{})
224
225def 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
229def 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
232def 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
241def 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
250def 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
257def 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)
266def 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
269def 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)
273def 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
277def 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))