cipher_modes.bend

bend-osdev-cipher-modes@0.1.0.0 · 299 lines · 50 definitions

1# bend-osdev-cipher-modes: block-cipher modes of operation over any 128-bit
2# block cipher. This file holds what every mode shares: the 128-bit block, the
3# package's error type, and the byte-level helpers the modes are built from.
4#
5# The block cipher is a parameter. Every mode takes it as template arguments:
6#   ~K: Data                          the cipher's key (an expanded key schedule)
7#   ~enc: K -> CmBlock -> CmBlock     encryption of one block
8#   ~dec: K -> CmBlock -> CmBlock     decryption of one block (CBC, XTS only)
9# and the key itself as +k: K. The modes never look inside K, so they run on
10# any cipher with 128-bit blocks; aes.bend supplies AES-128 and AES-256.
11#
12# A CmBlock is four 32-bit words, big-endian: w0 holds bytes 0 to 3 of the
13# block, byte 0 in its top 8 bits. Every value of the type is a block (there is
14# no out-of-range byte), so a cipher's "decryption inverts encryption" can be
15# stated for every block. The type is open: a cipher adapter may build and
16# match blocks directly.
17import Base
18import bend-osdev-bytes@0.1.0.0/bytes.bend as B
19import bend-osdev-word64@0.1.0.0/word64.bend as W
20
21type CmBlock is Data:
22  CmBlock{w0: U32, w1: U32, w2: U32, w3: U32}
23
24# Every failure a mode can report
25type CmError is Data:
26  CmBadKeyLength{got: Nat}
27  CmBadIvLength{got: Nat}
28  CmBadTweakLength{got: Nat}
29  CmBadNonceLength{got: Nat}
30  CmBadTagLength{got: Nat}
31  CmBadBlockSize{got: Nat}
32  CmNotBlockMultiple{len: Nat}
33  CmTooShort{len: Nat}
34  CmTooLong{len: Nat}
35  CmBadPadding{}
36  CmTagMismatch{}
37
38# Blocks
39
40def CmBlock.zero() -> CmBlock:
41  CmBlock{0, 0, 0, 0}
42
43def CmBlock.xor(a: CmBlock, b: CmBlock) -> CmBlock:
44  match a b:
45    case CmBlock{a0, a1, a2, a3} CmBlock{b0, b1, b2, b3}:
46      CmBlock{U32.xor(a0, b0), U32.xor(a1, b1), U32.xor(a2, b2), U32.xor(a3, b3)}
47
48# Bytes and words (internal). Words are split into bytes and joined back by
49# bit slicing (bend-osdev-word64's W64.bits), not by shifts and masks, so that
50# the round trips can be proved for every word.
51
52# a byte (the low 8 bits of x), as bend-osdev-bytes masks it
53def cm.byte(x: U32) -> U32:
54  B.byte(x)
55
56def cm.bits8(b: U32) -> Word(8n):
57  match b:
58    case U32{w}:
59      W.W64.bits.lo(8n, 24n, w)
60
61def cm.of8(s: Word(8n)) -> U32:
62  U32{W.W64.bits.cat(8n, 24n, s, Word.zero(24n))}
63
64# the word with bytes a, b, c, d, most significant first
65def cm.word(a: U32, b: U32, c: U32, d: U32) -> U32:
66  U32{W.W64.bits.cat(8n, 24n, cm.bits8(d), W.W64.bits.cat(8n, 16n, cm.bits8(c), W.W64.bits.cat(8n, 8n, cm.bits8(b), cm.bits8(a))))}
67
68# the bytes of w, most significant first
69def cm.b0(w: U32) -> U32:
70  match w:
71    case U32{x}:
72      cm.of8(W.W64.bits.hi(8n, 8n, W.W64.bits.hi(8n, 16n, W.W64.bits.hi(8n, 24n, x))))
73
74def cm.b1(w: U32) -> U32:
75  match w:
76    case U32{x}:
77      cm.of8(W.W64.bits.lo(8n, 8n, W.W64.bits.hi(8n, 16n, W.W64.bits.hi(8n, 24n, x))))
78
79def cm.b2(w: U32) -> U32:
80  match w:
81    case U32{x}:
82      cm.of8(W.W64.bits.lo(8n, 16n, W.W64.bits.hi(8n, 24n, x)))
83
84def cm.b3(w: U32) -> U32:
85  match w:
86    case U32{x}:
87      cm.of8(W.W64.bits.lo(8n, 24n, x))
88
89# the four bytes of w, most significant first, in front of rest
90def cm.unword(+w: U32, rest: List<&2, U32>) -> List<&2, U32>:
91  Con{cm.b0(w), Con{cm.b1(w), Con{cm.b2(w), Con{cm.b3(w), rest}}}}
92
93def cm.w0(b: CmBlock) -> U32:
94  match b:
95    case CmBlock{w0, w1, w2, w3}:
96      w0
97
98def cm.w1(b: CmBlock) -> U32:
99  match b:
100    case CmBlock{w0, w1, w2, w3}:
101      w1
102
103def cm.w2(b: CmBlock) -> U32:
104  match b:
105    case CmBlock{w0, w1, w2, w3}:
106      w2
107
108def cm.w3(b: CmBlock) -> U32:
109  match b:
110    case CmBlock{w0, w1, w2, w3}:
111      w3
112
113# the 16 bytes of a block in front of rest (always 16 cells, whatever b is)
114def cm.bytes_onto(+b: CmBlock, rest: List<&2, U32>) -> List<&2, U32>:
115  cm.unword(cm.w0(b), cm.unword(cm.w1(b), cm.unword(cm.w2(b), cm.unword(cm.w3(b), rest))))
116
117def cm.bytes_of(b: CmBlock) -> List<&2, U32>:
118  cm.bytes_onto(b, Nil{})
119
120def cm.block16(a0: U32, a1: U32, a2: U32, a3: U32, a4: U32, a5: U32, a6: U32, a7: U32, a8: U32, a9: U32, a10: U32, a11: U32, a12: U32, a13: U32, a14: U32, a15: U32) -> CmBlock:
121  CmBlock{cm.word(a0, a1, a2, a3), cm.word(a4, a5, a6, a7), cm.word(a8, a9, a10, a11), cm.word(a12, a13, a14, a15)}
122
123def cm.block_of.full(xs: List<&2, U32>) -> CmBlock:
124  match xs:
125    case Con{a0, Con{a1, Con{a2, Con{a3, Con{a4, Con{a5, Con{a6, Con{a7, Con{a8, Con{a9, Con{a10, Con{a11, Con{a12, Con{a13, Con{a14, Con{a15, t}}}}}}}}}}}}}}}}:
126      cm.block16(a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15)
127    case _:
128      CmBlock.zero()
129
130# the block of the first 16 bytes of xs, zero-filled if xs is shorter
131def cm.block_of(xs: List<&2, U32>) -> CmBlock:
132  cm.block_of.full(B.append(B.take(16n, xs), B.zeros(16n)))
133
134# A byte string as its whole blocks and the 0 to 15 bytes after them
135type CmSplit is Data:
136  CmSplit{blocks: List<&2, CmBlock>, tail: List<&2, U32>}
137
138def cm.split.cons(b: CmBlock, s: CmSplit) -> CmSplit:
139  match s:
140    case CmSplit{bs, t}:
141      CmSplit{Con{b, bs}, t}
142
143def cm.split(+xs: List<&2, U32>) -> CmSplit:
144  match xs:
145    case Con{a0, Con{a1, Con{a2, Con{a3, Con{a4, Con{a5, Con{a6, Con{a7, Con{a8, Con{a9, Con{a10, Con{a11, Con{a12, Con{a13, Con{a14, Con{a15, t}}}}}}}}}}}}}}}}:
146      cm.split.cons(cm.block16(a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15), cm.split(t))
147    case _:
148      CmSplit{Nil{}, xs}
149
150def cm.split.blocks(s: CmSplit) -> List<&2, CmBlock>:
151  match s:
152    case CmSplit{bs, t}:
153      bs
154
155def cm.split.tail(s: CmSplit) -> List<&2, U32>:
156  match s:
157    case CmSplit{bs, t}:
158      t
159
160# the bytes of the blocks bs, in front of rest
161def cm.join_onto(bs: List<&2, CmBlock>, rest: List<&2, U32>) -> List<&2, U32>:
162  match bs:
163    case Nil{}:
164      rest
165    case Con{b, t}:
166      cm.bytes_onto(b, cm.join_onto(t, rest))
167
168def cm.join(bs: List<&2, CmBlock>) -> List<&2, U32>:
169  cm.join_onto(bs, Nil{})
170
171# byte-wise XOR, as long as the shorter list
172def cm.xor_bytes(xs: List<&2, U32>, ys: List<&2, U32>) -> List<&2, U32>:
173  match xs ys:
174    case Con{a, s} Con{b, t}:
175      Con{cm.byte(U32.xor(a, b)), cm.xor_bytes(s, t)}
176    case _ _:
177      Nil{}
178
179# the OR of the byte-wise XORs: 0 exactly when the lists agree, computed
180# without stopping at the first difference
181# The same, tail-recursive. Bend 2.0.37's runtime overflows its stack at some
182# tens of thousands of nested non-tail calls, so the structural forms above,
183# which the proofs reason about, cannot run on long messages; the modes run
184# these instead, and PROOF.bend proves each equal to its structural form for
185# every input.
186
187# the blocks of bs in reverse order, in front of acc
188def cm.blocks.rev_onto(bs: List<&2, CmBlock>, acc: List<&2, CmBlock>) -> List<&2, CmBlock>:
189  match bs:
190    case Nil{}:
191      acc
192    case Con{b, t}:
193      cm.blocks.rev_onto(t, Con{b, acc})
194
195def cm.blocks.len.go(bs: List<&2, CmBlock>, n: Nat) -> Nat:
196  match bs:
197    case Nil{}:
198      n
199    case Con{b, t}:
200      cm.blocks.len.go(t, 1n+n)
201
202# the number of blocks (List.length)
203def cm.blocks.len(bs: List<&2, CmBlock>) -> Nat:
204  cm.blocks.len.go(bs, 0n)
205
206# xs, then ys (List.append)
207def cm.blocks.append(xs: List<&2, CmBlock>, ys: List<&2, CmBlock>) -> List<&2, CmBlock>:
208  cm.blocks.rev_onto(cm.blocks.rev_onto(xs, Nil{}), ys)
209
210# the blocks split so far are kept reversed in acc (cm.split)
211def cm.split.go(+xs: List<&2, U32>, acc: List<&2, CmBlock>) -> CmSplit:
212  match xs:
213    case Con{a0, Con{a1, Con{a2, Con{a3, Con{a4, Con{a5, Con{a6, Con{a7, Con{a8, Con{a9, Con{a10, Con{a11, Con{a12, Con{a13, Con{a14, Con{a15, t}}}}}}}}}}}}}}}}:
214      cm.split.go(t, Con{cm.block16(a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15), acc})
215    case _:
216      CmSplit{cm.blocks.rev_onto(acc, Nil{}), xs}
217
218def cm.split.fast(+xs: List<&2, U32>) -> CmSplit:
219  cm.split.go(xs, Nil{})
220
221# the bytes of the blocks rs (last first) in front of acc
222def cm.join.go(rs: List<&2, CmBlock>, acc: List<&2, U32>) -> List<&2, U32>:
223  match rs:
224    case Nil{}:
225      acc
226    case Con{b, t}:
227      cm.join.go(t, cm.bytes_onto(b, acc))
228
229# cm.join_onto
230def cm.join_onto.fast(bs: List<&2, CmBlock>, rest: List<&2, U32>) -> List<&2, U32>:
231  cm.join.go(cm.blocks.rev_onto(bs, Nil{}), rest)
232
233def cm.xor_bytes.go(xs: List<&2, U32>, ys: List<&2, U32>, acc: List<&2, U32>) -> List<&2, U32>:
234  match xs ys:
235    case Con{a, s} Con{b, t}:
236      cm.xor_bytes.go(s, t, Con{cm.byte(U32.xor(a, b)), acc})
237    case _ _:
238      B.rev(acc)
239
240# cm.xor_bytes
241def cm.xor_bytes.fast(xs: List<&2, U32>, ys: List<&2, U32>) -> List<&2, U32>:
242  cm.xor_bytes.go(xs, ys, Nil{})
243
244def cm.diff(xs: List<&2, U32>, ys: List<&2, U32>, acc: U32) -> U32:
245  match xs ys:
246    case Con{a, s} Con{b, t}:
247      cm.diff(s, t, U32.or(acc, cm.byte(U32.xor(a, b))))
248    case Nil{} Nil{}:
249      acc
250    case _ _:
251      1
252
253# equality of two byte lists with no early exit of the same length (a tag check)
254def cm.ct_eq(xs: List<&2, U32>, ys: List<&2, U32>) -> Bool:
255  U32.is_eq(cm.diff(xs, ys, 0), 0)
256
257# 0 for a 0 bit, all ones for a 1 bit (the low bit of b)
258def cm.mask(b: U32) -> U32:
259  U32.sub(0, U32.and(1, b))
260
261# Checks, as steps of a Result block
262
263def cm.check(ok: Bool, e: CmError) -> Result<&2, &2, CmError, Unit>:
264  match ok:
265    case True{}:
266      Done{Unit{}}
267    case False{}:
268      Fail{e}
269
270# a 16-byte value as a block, or the error e
271def cm.need_block.pick(ok: Bool, xs: List<&2, U32>, e: CmError) -> Result<&2, &2, CmError, CmBlock>:
272  match ok:
273    case True{}:
274      Done{cm.block_of(xs)}
275    case False{}:
276      Fail{e}
277
278def cm.need_block(+xs: List<&2, U32>, e: CmError) -> Result<&2, &2, CmError, CmBlock>:
279  cm.need_block.pick(Nat.is_eq(B.len(xs), 16n), xs, e)
280
281# Blocks as byte strings
282
283def CmBlock.to_octets(b: CmBlock) -> B.Octets:
284  B.Octets.of_list(cm.bytes_of(b))
285
286def CmBlock.of_octets.pick(ok: Bool, xs: List<&2, U32>) -> Maybe<&2, CmBlock>:
287  match ok:
288    case True{}:
289      Some{cm.block_of(xs)}
290    case False{}:
291      None{}
292
293# a 16-byte string as a block; None for any other length
294def CmBlock.of_octets(o: B.Octets) -> Maybe<&2, CmBlock>:
295  +xs = B.Octets.to_list(o)
296  CmBlock.of_octets.pick(Nat.is_eq(B.len(xs), 16n), xs)
297
298def CmBlock.hex(b: CmBlock) -> String:
299  B.hex(cm.bytes_of(b))