legacy_ciphers.bend

bend-osdev-legacy-ciphers@0.1.0.0 · 391 lines · 59 definitions

1# bend-osdev-legacy-ciphers: the older block and stream ciphers a kernel's
2# crypto layer still carries (DES, 3DES, SM4, Camellia, Serpent, Twofish,
3# ARIA, CAST-256, Blowfish, CAST-128, TEA, XTEA, FCrypt, RC4), one file per
4# cipher. This file holds what they share: the package's error type, the
5# 64-bit block, word helpers, tables, and Feistel rounds over any round
6# function.
7#
8# The 128-bit block ciphers (sm4.bend, camellia.bend, serpent.bend,
9# twofish.bend, aria.bend, cast6.bend) work on cipher-modes' CmBlock, so they
10# plug into every mode there as the template arguments ~K, ~enc, ~dec. The
11# 64-bit ones (des.bend, tdes.bend, blowfish.bend, cast5.bend, tea.bend,
12# xtea.bend, fcrypt.bend) work on LcBlock64 below, and the 64-bit modes in
13# modes64.bend.
14import Base
15import bend-osdev-bytes@0.1.0.0/bytes.bend as B
16import bend-osdev-word64@0.1.0.0/word64.bend as W
17
18# Every failure the package reports
19type LcError is Data:
20  LcBadKeyLength{got: Nat}
21  LcBadIvLength{got: Nat}
22  LcNotBlockMultiple{len: Nat}
23
24# A 64-bit block: two 32-bit words, big-endian (hi holds bytes 0 to 3, byte 0
25# in its top 8 bits). Every value of the type is a block, so "decryption
26# inverts encryption" can be stated for every block. The type is open: a
27# cipher may build and match blocks directly.
28type LcBlock64 is Data:
29  LcBlock64{hi: U32, lo: U32}
30
31def LcBlock64.zero() -> LcBlock64:
32  LcBlock64{0, 0}
33
34def LcBlock64.xor(a: LcBlock64, b: LcBlock64) -> LcBlock64:
35  match a b:
36    case LcBlock64{a0, a1} LcBlock64{b0, b1}:
37      LcBlock64{U32.xor(a0, b0), U32.xor(a1, b1)}
38
39# Words, natively: fast, for the parts of a cipher no proof inverts (round
40# functions and key schedules). n is 1 to 31.
41
42def lc.rotl(+x: U32, +n: Nat) -> U32:
43  U32.or(U32.shln(x, n), U32.shrn(x, Nat.sub(32n, n)))
44
45# byte n of x, counting from the least significant (n = 0 to 3)
46def lc.byte(x: U32, n: Nat) -> U32:
47  U32.and(255, U32.shrn(x, Nat.mul(8n, n)))
48
49# the word with bytes a (most significant), b, c, d
50def lc.be(a: U32, b: U32, c: U32, d: U32) -> U32:
51  U32.or(U32.or(U32.shln(U32.and(255, a), 24n), U32.shln(U32.and(255, b), 16n)), U32.or(U32.shln(U32.and(255, c), 8n), U32.and(255, d)))
52
53# the word with bytes a (least significant), b, c, d
54def lc.le(a: U32, b: U32, c: U32, d: U32) -> U32:
55  lc.be(d, c, b, a)
56
57# bit i of x (0 the least significant), as 0 or 1
58def lc.bit(x: U32, i: Nat) -> U32:
59  U32.and(1, U32.shrn(x, i))
60
61# element n of a list of words (0 past the end)
62def lc.at(xs: List<&2, U32>, n: Nat) -> U32:
63  match xs:
64    case Nil{}:
65      0
66    case Con{h, t}:
67      match n:
68        case 0n:
69          h
70        case 1n+p:
71          lc.at(t, p)
72
73# Words as bits: for the steps a proof must undo (rotations, byte swaps, bit
74# permutations). They are built by slicing a word's bits (bend-osdev-word64's
75# W64.bits), so a proof about a symbolic word computes through them; they are
76# slower than the native forms above.
77
78# the (m + n)-bit word w rotated left by n
79def lc.wrotl(+m: Nat, +n: Nat, +w: Word(Nat.add(m, n))) -> Word(Nat.add(n, m)):
80  W.W64.bits.cat(n, m, W.W64.bits.hi(m, n, w), W.W64.bits.lo(m, n, w))
81
82def lc.rotl1.bits(x: U32) -> U32:
83  match x:
84    case U32{+w}:
85      U32{lc.wrotl(31n, 1n, w)}
86
87def lc.rotl3.bits(x: U32) -> U32:
88  match x:
89    case U32{+w}:
90      U32{lc.wrotl(29n, 3n, w)}
91
92def lc.rotl5.bits(x: U32) -> U32:
93  match x:
94    case U32{+w}:
95      U32{lc.wrotl(27n, 5n, w)}
96
97def lc.rotl7.bits(x: U32) -> U32:
98  match x:
99    case U32{+w}:
100      U32{lc.wrotl(25n, 7n, w)}
101
102def lc.rotl10.bits(x: U32) -> U32:
103  match x:
104    case U32{+w}:
105      U32{lc.wrotl(22n, 10n, w)}
106
107def lc.rotl13.bits(x: U32) -> U32:
108  match x:
109    case U32{+w}:
110      U32{lc.wrotl(19n, 13n, w)}
111
112def lc.rotl19.bits(x: U32) -> U32:
113  match x:
114    case U32{+w}:
115      U32{lc.wrotl(13n, 19n, w)}
116
117def lc.rotl22.bits(x: U32) -> U32:
118  match x:
119    case U32{+w}:
120      U32{lc.wrotl(10n, 22n, w)}
121
122def lc.rotl25.bits(x: U32) -> U32:
123  match x:
124    case U32{+w}:
125      U32{lc.wrotl(7n, 25n, w)}
126
127def lc.rotl27.bits(x: U32) -> U32:
128  match x:
129    case U32{+w}:
130      U32{lc.wrotl(5n, 27n, w)}
131
132def lc.rotl29.bits(x: U32) -> U32:
133  match x:
134    case U32{+w}:
135      U32{lc.wrotl(3n, 29n, w)}
136
137def lc.rotl31.bits(x: U32) -> U32:
138  match x:
139    case U32{+w}:
140      U32{lc.wrotl(1n, 31n, w)}
141
142# the low 8 bits of a word, as bits, and the byte with these bits
143def lc.bits8(b: U32) -> Word(8n):
144  match b:
145    case U32{w}:
146      W.W64.bits.lo(8n, 24n, w)
147
148def lc.of8(s: Word(8n)) -> U32:
149  U32{W.W64.bits.cat(8n, 24n, s, Word.zero(24n))}
150
151# the word with bytes a (most significant), b, c, d, by bits
152def lc.be.bits(a: U32, b: U32, c: U32, d: U32) -> U32:
153  U32{W.W64.bits.cat(8n, 24n, lc.bits8(d), W.W64.bits.cat(8n, 16n, lc.bits8(c), W.W64.bits.cat(8n, 8n, lc.bits8(b), lc.bits8(a))))}
154
155# the bytes of w, by bits: b0 the most significant
156def lc.b0.bits(w: U32) -> U32:
157  match w:
158    case U32{x}:
159      lc.of8(W.W64.bits.hi(8n, 8n, W.W64.bits.hi(8n, 16n, W.W64.bits.hi(8n, 24n, x))))
160
161def lc.b1.bits(w: U32) -> U32:
162  match w:
163    case U32{x}:
164      lc.of8(W.W64.bits.lo(8n, 8n, W.W64.bits.hi(8n, 16n, W.W64.bits.hi(8n, 24n, x))))
165
166def lc.b2.bits(w: U32) -> U32:
167  match w:
168    case U32{x}:
169      lc.of8(W.W64.bits.lo(8n, 16n, W.W64.bits.hi(8n, 24n, x)))
170
171def lc.b3.bits(w: U32) -> U32:
172  match w:
173    case U32{x}:
174      lc.of8(W.W64.bits.lo(8n, 24n, x))
175
176# the word with its bytes in reverse order (big-endian to little-endian)
177def lc.bswap.bits(+w: U32) -> U32:
178  lc.be.bits(lc.b3.bits(w), lc.b2.bits(w), lc.b1.bits(w), lc.b0.bits(w))
179
180# the bits of a word, most significant first, in front of acc
181def lc.msb.go(n: Nat, w: Word(n), acc: List<&2, Bool>) -> List<&2, Bool>:
182  match n:
183    case 0n:
184      acc
185    case 1n+p:
186      match w:
187        case WCon{h, t}:
188          lc.msb.go(p, t, Con{h, acc})
189
190def lc.msb(x: U32, acc: List<&2, Bool>) -> List<&2, Bool>:
191  match x:
192    case U32{w}:
193      lc.msb.go(32n, w, acc)
194
195# bs reversed, in front of acc
196def lc.rev_bits(bs: List<&2, Bool>, acc: List<&2, Bool>) -> List<&2, Bool>:
197  match bs:
198    case Nil{}:
199      acc
200    case Con{h, t}:
201      lc.rev_bits(t, Con{h, acc})
202
203# all but the first n of bs
204def lc.drop_bits(n: Nat, bs: List<&2, Bool>) -> List<&2, Bool>:
205  match n:
206    case 0n:
207      bs
208    case 1n+p:
209      match bs:
210        case Nil{}:
211          Nil{}
212        case Con{h, t}:
213          lc.drop_bits(p, t)
214
215# the n-bit word whose bits, least significant first, are the first n of bs
216# (False past the end)
217def lc.word_lsb(n: Nat, bs: List<&2, Bool>) -> Word(n):
218  match n:
219    case 0n:
220      WNil{}
221    case 1n+p:
222      match bs:
223        case Nil{}:
224          WCon{False{}, lc.word_lsb(p, Nil{})}
225        case Con{h, t}:
226          WCon{h, lc.word_lsb(p, t)}
227
228# the element i of bs (False past the end)
229def lc.nth(bs: List<&2, Bool>, i: Nat) -> Bool:
230  match bs:
231    case Nil{}:
232      False{}
233    case Con{h, t}:
234      match i:
235        case 0n:
236          h
237        case 1n+p:
238          lc.nth(t, p)
239
240# Tables: a complete binary tree of words, read by the bits of an index. Bend
241# 2.0.37 recomputes a table def at every call, so a cipher builds its tables
242# once, when its key is made, and keeps them in the key.
243
244type LcTab is Data:
245  LcLeaf{v: U32}
246  LcNode{l: LcTab, r: LcTab}
247
248def lc.tab.leaves(xs: List<&2, U32>) -> List<&2, LcTab>:
249  match xs:
250    case Nil{}:
251      Nil{}
252    case Con{h, t}:
253      Con{LcLeaf{h}, lc.tab.leaves(t)}
254
255def lc.tab.pairs(ts: List<&2, LcTab>) -> List<&2, LcTab>:
256  match ts:
257    case Con{a, Con{b, t}}:
258      Con{LcNode{a, b}, lc.tab.pairs(t)}
259    case _:
260      Nil{}
261
262def lc.tab.up(n: Nat, ts: List<&2, LcTab>) -> List<&2, LcTab>:
263  match n:
264    case 0n:
265      ts
266    case 1n+p:
267      lc.tab.up(p, lc.tab.pairs(ts))
268
269def lc.tab.root(ts: List<&2, LcTab>) -> LcTab:
270  match ts:
271    case Nil{}:
272      LcLeaf{0}
273    case Con{h, t}:
274      h
275
276# the table of the 2^d words xs (entry i is element i)
277def lc.tab(d: Nat, xs: List<&2, U32>) -> LcTab:
278  lc.tab.root(lc.tab.up(d, lc.tab.leaves(xs)))
279
280def lc.tab.pick(one: Bool, l: LcTab, r: LcTab) -> LcTab:
281  match one:
282    case True{}:
283      r
284    case False{}:
285      l
286
287# entry i of a table of depth d (i below 2^d)
288def lc.tab.get(d: Nat, t: LcTab, +i: U32) -> U32:
289  match d:
290    case 0n:
291      match t:
292        case LcLeaf{v}:
293          v
294        case LcNode{l, r}:
295          0
296    case 1n+(+p):
297      match t:
298        case LcLeaf{v}:
299          v
300        case LcNode{l, r}:
301          lc.tab.get(p, lc.tab.pick(U32.is_eq(lc.bit(i, p), 1), l, r), i)
302
303# the bits of i (below 2^d) that pick its entry, most significant first
304def lc.tab.path(d: Nat, +i: U32) -> List<&2, Bool>:
305  match d:
306    case 0n:
307      Nil{}
308    case 1n+(+p):
309      Con{U32.is_eq(lc.bit(i, p), 1), lc.tab.path(p, i)}
310
311def lc.tab.set.go(t: LcTab, path: List<&2, Bool>, v: U32) -> LcTab:
312  match t:
313    case LcLeaf{w}:
314      LcLeaf{v}
315    case LcNode{l, r}:
316      match path:
317        case Nil{}:
318          LcNode{l, r}
319        case Con{b, rest}:
320          match b:
321            case True{}:
322              LcNode{l, lc.tab.set.go(r, rest, v)}
323            case False{}:
324              LcNode{lc.tab.set.go(l, rest, v), r}
325
326# entry i of a table of depth d set to v (i below 2^d)
327def lc.tab.set(d: Nat, t: LcTab, +i: U32, v: U32) -> LcTab:
328  lc.tab.set.go(t, lc.tab.path(d, i), v)
329
330# Feistel rounds over any round function f (CAST-128, FCrypt): the round with
331# round key k is (L, R) -> (R, L xor f(k, R)), and it is undone by
332# (L', R') -> (R' xor f(k, L'), L') whatever f is, so a list of rounds is
333# undone by its rounds undone in reverse order (PROOF.bend: fe_*)
334
335def lc.fe.step(~RK: Data, ~f: RK -> U32 -> U32, k: RK, b: LcBlock64) -> LcBlock64:
336  match b:
337    case LcBlock64{l, +r}:
338      LcBlock64{r, U32.xor(l, f(k, r))}
339
340def lc.fe.unstep(~RK: Data, ~f: RK -> U32 -> U32, k: RK, b: LcBlock64) -> LcBlock64:
341  match b:
342    case LcBlock64{+l, r}:
343      LcBlock64{U32.xor(r, f(k, l)), l}
344
345def lc.fe.run(~RK: Data, ~f: RK -> U32 -> U32, ks: List<&2, RK>, b: LcBlock64) -> LcBlock64:
346  match ks:
347    case Nil{}:
348      b
349    case Con{k, t}:
350      lc.fe.run(~RK, ~f, t, lc.fe.step(~RK, ~f, k, b))
351
352def lc.fe.unrun(~RK: Data, ~f: RK -> U32 -> U32, ks: List<&2, RK>, b: LcBlock64) -> LcBlock64:
353  match ks:
354    case Nil{}:
355      b
356    case Con{k, t}:
357      lc.fe.unstep(~RK, ~f, k, lc.fe.unrun(~RK, ~f, t, b))
358
359# the two halves exchanged
360def lc.swap(b: LcBlock64) -> LcBlock64:
361  match b:
362    case LcBlock64{h, l}:
363      LcBlock64{l, h}
364
365# Blocks as byte strings (built on bits, so the round trip is provable)
366
367# the 8 bytes of a block in front of rest
368def lc.block_bytes(b: LcBlock64, rest: List<&2, U32>) -> List<&2, U32>:
369  match b:
370    case LcBlock64{+hi, +lo}:
371      Con{lc.b0.bits(hi), Con{lc.b1.bits(hi), Con{lc.b2.bits(hi), Con{lc.b3.bits(hi), Con{lc.b0.bits(lo), Con{lc.b1.bits(lo), Con{lc.b2.bits(lo), Con{lc.b3.bits(lo), rest}}}}}}}}
372
373def lc.block8(a0: U32, a1: U32, a2: U32, a3: U32, a4: U32, a5: U32, a6: U32, a7: U32) -> LcBlock64:
374  LcBlock64{lc.be.bits(a0, a1, a2, a3), lc.be.bits(a4, a5, a6, a7)}
375
376def LcBlock64.to_octets(b: LcBlock64) -> B.Octets:
377  B.Octets.of_list(lc.block_bytes(b, Nil{}))
378
379def lc.block_of(xs: List<&2, U32>) -> Maybe<&2, LcBlock64>:
380  match xs:
381    case Con{a0, Con{a1, Con{a2, Con{a3, Con{a4, Con{a5, Con{a6, Con{a7, Nil{}}}}}}}}}:
382      Some{lc.block8(a0, a1, a2, a3, a4, a5, a6, a7)}
383    case _:
384      None{}
385
386# an 8-byte string as a block (big-endian words); None for any other length
387def LcBlock64.of_octets(o: B.Octets) -> Maybe<&2, LcBlock64>:
388  lc.block_of(B.Octets.to_list(o))
389
390def LcBlock64.hex(b: LcBlock64) -> String:
391  B.hex(lc.block_bytes(b, Nil{}))