cipher_core.bend

bend-osdev-cipher-core@0.1.0.0 · 388 lines · 59 definitions

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