des.bend

bend-osdev-legacy-ciphers@0.1.0.0 · 358 lines · 60 definitions

1# DES (FIPS 46-3, Data Encryption Standard, 1999) as a 64-bit block cipher.
2#
3# The cipher is IP, sixteen Feistel rounds (L, R) -> (R, L xor f(K_i, R)),
4# the swap of the two halves, and IP^-1. Decryption here undoes each step in
5# reverse order: IP, the swap, the rounds undone last to first
6# ((L', R') -> (R' xor f(K_i, L'), L')), IP^-1. That is the same function as
7# FIPS 46-3's "the same algorithm with the key schedule reversed", written so
8# that decrypt(encrypt(b)) == b is provable for every key and every block
9# (LAWS.bend): a Feistel round is undone whatever its round function.
10#
11# IP and IP^-1 move bits as lists of Bools, so a proof computes through them.
12# The round function f and the key schedule use native word operations: f
13# looks up eight tables that combine each S-box with the permutation P (SP),
14# built from FIPS 46-3's S-boxes and P once per key (Bend 2.0.37 does not keep
15# a computed table between calls, so the key holds it).
16import Base
17import bend-osdev-bytes@0.1.0.0/bytes.bend as B
18import bend-osdev-legacy-ciphers@0.1.0.0/legacy_ciphers.bend as L
19
20# The tables of FIPS 46-3 (bit 1 is the most significant)
21
22# IP
23def des.ip.table() -> List<&2, Nat>:
24  [58n, 50n, 42n, 34n, 26n, 18n, 10n, 2n, 60n, 52n, 44n, 36n, 28n, 20n, 12n, 4n,
25    62n, 54n, 46n, 38n, 30n, 22n, 14n, 6n, 64n, 56n, 48n, 40n, 32n, 24n, 16n, 8n,
26    57n, 49n, 41n, 33n, 25n, 17n, 9n, 1n, 59n, 51n, 43n, 35n, 27n, 19n, 11n, 3n,
27    61n, 53n, 45n, 37n, 29n, 21n, 13n, 5n, 63n, 55n, 47n, 39n, 31n, 23n, 15n, 7n]
28
29# IP^-1
30def des.fp.table() -> List<&2, Nat>:
31  [40n, 8n, 48n, 16n, 56n, 24n, 64n, 32n, 39n, 7n, 47n, 15n, 55n, 23n, 63n, 31n,
32    38n, 6n, 46n, 14n, 54n, 22n, 62n, 30n, 37n, 5n, 45n, 13n, 53n, 21n, 61n, 29n,
33    36n, 4n, 44n, 12n, 52n, 20n, 60n, 28n, 35n, 3n, 43n, 11n, 51n, 19n, 59n, 27n,
34    34n, 2n, 42n, 10n, 50n, 18n, 58n, 26n, 33n, 1n, 41n, 9n, 49n, 17n, 57n, 25n]
35
36# P
37def des.p.table() -> List<&2, Nat>:
38  [16n, 7n, 20n, 21n, 29n, 12n, 28n, 17n, 1n, 15n, 23n, 26n, 5n, 18n, 31n, 10n,
39    2n, 8n, 24n, 14n, 32n, 27n, 3n, 9n, 19n, 13n, 30n, 6n, 22n, 11n, 4n, 25n]
40
41# PC-1, the bits of C_0
42def des.pc1c.table() -> List<&2, Nat>:
43  [57n, 49n, 41n, 33n, 25n, 17n, 9n, 1n, 58n, 50n, 42n, 34n, 26n, 18n, 10n, 2n,
44    59n, 51n, 43n, 35n, 27n, 19n, 11n, 3n, 60n, 52n, 44n, 36n]
45
46# PC-1, the bits of D_0
47def des.pc1d.table() -> List<&2, Nat>:
48  [63n, 55n, 47n, 39n, 31n, 23n, 15n, 7n, 62n, 54n, 46n, 38n, 30n, 22n, 14n, 6n,
49    61n, 53n, 45n, 37n, 29n, 21n, 13n, 5n, 28n, 20n, 12n, 4n]
50
51# PC-2, its first 24 entries
52def des.pc2a.table() -> List<&2, Nat>:
53  [14n, 17n, 11n, 24n, 1n, 5n, 3n, 28n, 15n, 6n, 21n, 10n, 23n, 19n, 12n, 4n,
54    26n, 8n, 16n, 7n, 27n, 20n, 13n, 2n]
55
56# PC-2, its last 24 entries
57def des.pc2b.table() -> List<&2, Nat>:
58  [41n, 52n, 31n, 37n, 47n, 55n, 30n, 40n, 51n, 45n, 33n, 48n, 44n, 49n, 39n, 56n,
59    34n, 53n, 46n, 42n, 50n, 36n, 29n, 32n]
60
61# the left shifts of the key schedule
62def des.shifts() -> List<&2, Nat>:
63  [1n, 1n, 2n, 2n, 2n, 2n, 2n, 2n, 1n, 2n, 2n, 2n, 2n, 2n, 2n, 1n]
64
65# S1: row r (0 to 3), column c (0 to 15) is entry 16r + c
66def des.s1() -> List<&2, U32>:
67  [14, 4, 13, 1, 2, 15, 11, 8, 3, 10, 6, 12, 5, 9, 0, 7,
68    0, 15, 7, 4, 14, 2, 13, 1, 10, 6, 12, 11, 9, 5, 3, 8,
69    4, 1, 14, 8, 13, 6, 2, 11, 15, 12, 9, 7, 3, 10, 5, 0,
70    15, 12, 8, 2, 4, 9, 1, 7, 5, 11, 3, 14, 10, 0, 6, 13]
71
72# S2: row r (0 to 3), column c (0 to 15) is entry 16r + c
73def des.s2() -> List<&2, U32>:
74  [15, 1, 8, 14, 6, 11, 3, 4, 9, 7, 2, 13, 12, 0, 5, 10,
75    3, 13, 4, 7, 15, 2, 8, 14, 12, 0, 1, 10, 6, 9, 11, 5,
76    0, 14, 7, 11, 10, 4, 13, 1, 5, 8, 12, 6, 9, 3, 2, 15,
77    13, 8, 10, 1, 3, 15, 4, 2, 11, 6, 7, 12, 0, 5, 14, 9]
78
79# S3: row r (0 to 3), column c (0 to 15) is entry 16r + c
80def des.s3() -> List<&2, U32>:
81  [10, 0, 9, 14, 6, 3, 15, 5, 1, 13, 12, 7, 11, 4, 2, 8,
82    13, 7, 0, 9, 3, 4, 6, 10, 2, 8, 5, 14, 12, 11, 15, 1,
83    13, 6, 4, 9, 8, 15, 3, 0, 11, 1, 2, 12, 5, 10, 14, 7,
84    1, 10, 13, 0, 6, 9, 8, 7, 4, 15, 14, 3, 11, 5, 2, 12]
85
86# S4: row r (0 to 3), column c (0 to 15) is entry 16r + c
87def des.s4() -> List<&2, U32>:
88  [7, 13, 14, 3, 0, 6, 9, 10, 1, 2, 8, 5, 11, 12, 4, 15,
89    13, 8, 11, 5, 6, 15, 0, 3, 4, 7, 2, 12, 1, 10, 14, 9,
90    10, 6, 9, 0, 12, 11, 7, 13, 15, 1, 3, 14, 5, 2, 8, 4,
91    3, 15, 0, 6, 10, 1, 13, 8, 9, 4, 5, 11, 12, 7, 2, 14]
92
93# S5: row r (0 to 3), column c (0 to 15) is entry 16r + c
94def des.s5() -> List<&2, U32>:
95  [2, 12, 4, 1, 7, 10, 11, 6, 8, 5, 3, 15, 13, 0, 14, 9,
96    14, 11, 2, 12, 4, 7, 13, 1, 5, 0, 15, 10, 3, 9, 8, 6,
97    4, 2, 1, 11, 10, 13, 7, 8, 15, 9, 12, 5, 6, 3, 0, 14,
98    11, 8, 12, 7, 1, 14, 2, 13, 6, 15, 0, 9, 10, 4, 5, 3]
99
100# S6: row r (0 to 3), column c (0 to 15) is entry 16r + c
101def des.s6() -> List<&2, U32>:
102  [12, 1, 10, 15, 9, 2, 6, 8, 0, 13, 3, 4, 14, 7, 5, 11,
103    10, 15, 4, 2, 7, 12, 9, 5, 6, 1, 13, 14, 0, 11, 3, 8,
104    9, 14, 15, 5, 2, 8, 12, 3, 7, 0, 4, 10, 1, 13, 11, 6,
105    4, 3, 2, 12, 9, 5, 15, 10, 11, 14, 1, 7, 6, 0, 8, 13]
106
107# S7: row r (0 to 3), column c (0 to 15) is entry 16r + c
108def des.s7() -> List<&2, U32>:
109  [4, 11, 2, 14, 15, 0, 8, 13, 3, 12, 9, 7, 5, 10, 6, 1,
110    13, 0, 11, 7, 4, 9, 1, 10, 14, 3, 5, 12, 2, 15, 8, 6,
111    1, 4, 11, 13, 12, 3, 7, 14, 10, 15, 6, 8, 0, 5, 9, 2,
112    6, 11, 13, 8, 1, 4, 10, 7, 9, 5, 0, 15, 14, 2, 3, 12]
113
114# S8: row r (0 to 3), column c (0 to 15) is entry 16r + c
115def des.s8() -> List<&2, U32>:
116  [13, 2, 8, 4, 6, 15, 11, 1, 10, 9, 3, 14, 5, 0, 12, 7,
117    1, 15, 13, 8, 10, 3, 7, 4, 12, 5, 6, 11, 0, 14, 9, 2,
118    7, 11, 4, 1, 9, 12, 14, 2, 0, 6, 10, 13, 15, 3, 5, 8,
119    2, 1, 14, 7, 4, 10, 8, 13, 15, 12, 9, 0, 3, 5, 6, 11]
120
121# IP and IP^-1, on bits
122
123# the bits of a block, bit 1 (the top bit of hi) first
124def des.bits(b: L.LcBlock64) -> List<&2, Bool>:
125  match b:
126    case L.LcBlock64{hi, lo}:
127      L.lc.msb(hi, L.lc.msb(lo, Nil{}))
128
129# the bits a table picks: entry t is bit t of bs
130def des.pick(tab: List<&2, Nat>, +bs: List<&2, Bool>) -> List<&2, Bool>:
131  match tab:
132    case Nil{}:
133      Nil{}
134    case Con{t, rest}:
135      Con{L.lc.nth(bs, Nat.sub(t, 1n)), des.pick(rest, bs)}
136
137# The two halves of the Feistel network (internal)
138type LcDesHalves is Data:
139  LcDesHalves{l: U32, r: U32}
140
141# 64 bits as halves: the first 32 (most significant first) are l
142def des.halves(bs: List<&2, Bool>) -> LcDesHalves:
143  +rv = L.lc.rev_bits(bs, Nil{})
144  LcDesHalves{U32{L.lc.word_lsb(32n, L.lc.drop_bits(32n, rv))}, U32{L.lc.word_lsb(32n, rv)}}
145
146def des.block(bs: List<&2, Bool>) -> L.LcBlock64:
147  +rv = L.lc.rev_bits(bs, Nil{})
148  L.LcBlock64{U32{L.lc.word_lsb(32n, L.lc.drop_bits(32n, rv))}, U32{L.lc.word_lsb(32n, rv)}}
149
150def des.hbits(h: LcDesHalves) -> List<&2, Bool>:
151  match h:
152    case LcDesHalves{l, r}:
153      L.lc.msb(l, L.lc.msb(r, Nil{}))
154
155def des.ip(b: L.LcBlock64) -> LcDesHalves:
156  des.halves(des.pick(des.ip.table(), des.bits(b)))
157
158def des.fp(h: LcDesHalves) -> L.LcBlock64:
159  des.block(des.pick(des.fp.table(), des.hbits(h)))
160
161def des.swap(h: LcDesHalves) -> LcDesHalves:
162  match h:
163    case LcDesHalves{l, r}:
164      LcDesHalves{r, l}
165
166# The round function f(K, R) = P(S(E(R) xor K))
167
168
169# a permutation of a 32-bit word (P): entry t is bit t of x
170def des.perm32(tab: List<&2, Nat>, +x: U32, acc: U32) -> U32:
171  match tab:
172    case Nil{}:
173      acc
174    case Con{t, rest}:
175      des.perm32(rest, x, U32.or(U32.shl(acc), L.lc.bit(x, Nat.sub(32n, t))))
176
177# the S-box entry for 6 bits b1 .. b6: row b1 b6, column b2 b3 b4 b5
178def des.sbox(s: List<&2, U32>, +x: U32) -> U32:
179  +row = U32.or(U32.and(2, U32.shrn(x, 4n)), U32.and(1, x))
180  +col = U32.and(15, U32.shr(x))
181  L.lc.at(s, U32.to_nat(U32.add(U32.mul(row, 16), col)))
182
183# the SP table of S-box s, its output placed sh bits up (28 for S1 .. 0 for
184# S8): entry x is P of S(x) in place
185def des.sp.go(n: Nat, +s: List<&2, U32>, +sh: Nat, +x: U32) -> List<&2, U32>:
186  match n:
187    case 0n:
188      Nil{}
189    case 1n+p:
190      Con{des.perm32(des.p.table(), U32.shln(des.sbox(s, x), sh), 0), des.sp.go(p, s, sh, U32.add(x, 1))}
191
192def des.sp(s: List<&2, U32>, sh: Nat) -> L.LcTab:
193  L.lc.tab(6n, des.sp.go(64n, s, sh, 0))
194
195def des.sp1() -> L.LcTab:
196  des.sp(des.s1(), 28n)
197
198def des.sp2() -> L.LcTab:
199  des.sp(des.s2(), 24n)
200
201def des.sp3() -> L.LcTab:
202  des.sp(des.s3(), 20n)
203
204def des.sp4() -> L.LcTab:
205  des.sp(des.s4(), 16n)
206
207def des.sp5() -> L.LcTab:
208  des.sp(des.s5(), 12n)
209
210def des.sp6() -> L.LcTab:
211  des.sp(des.s6(), 8n)
212
213def des.sp7() -> L.LcTab:
214  des.sp(des.s7(), 4n)
215
216def des.sp8() -> L.LcTab:
217  des.sp(des.s8(), 0n)
218
219# the eight SP tables, built once per key (internal)
220type LcDesSp is Data:
221  LcDesSp{t1: L.LcTab, t2: L.LcTab, t3: L.LcTab, t4: L.LcTab, t5: L.LcTab, t6: L.LcTab, t7: L.LcTab, t8: L.LcTab}
222
223def des.tables() -> LcDesSp:
224  LcDesSp{des.sp1(), des.sp2(), des.sp3(), des.sp4(), des.sp5(), des.sp6(), des.sp7(), des.sp8()}
225
226# a round key: a 48-bit subkey as its eight 6-bit groups, K's bits 1 to 6
227# first, and the SP tables (internal)
228type LcDesRk is Data:
229  LcDesRk{sp: LcDesSp, k0: U32, k1: U32, k2: U32, k3: U32, k4: U32, k5: U32, k6: U32, k7: U32}
230
231# group i of E(R): bits 4i .. 4i + 5 of R (bit 0 is bit 32), the top six bits
232# of R rotated left by n = 4i - 1 (mod 32)
233def des.e(+r: U32, +n: Nat) -> U32:
234  U32.and(63, U32.shrn(L.lc.rotl(r, n), 26n))
235
236def des.f(k: LcDesRk, +r: U32) -> U32:
237  match k:
238    case LcDesRk{LcDesSp{t1, t2, t3, t4, t5, t6, t7, t8}, k0, k1, k2, k3, k4, k5, k6, k7}:
239      +a = U32.xor(L.lc.tab.get(6n, t1, U32.xor(des.e(r, 31n), k0)), L.lc.tab.get(6n, t2, U32.xor(des.e(r, 3n), k1)))
240      +b = U32.xor(L.lc.tab.get(6n, t3, U32.xor(des.e(r, 7n), k2)), L.lc.tab.get(6n, t4, U32.xor(des.e(r, 11n), k3)))
241      +c = U32.xor(L.lc.tab.get(6n, t5, U32.xor(des.e(r, 15n), k4)), L.lc.tab.get(6n, t6, U32.xor(des.e(r, 19n), k5)))
242      +d = U32.xor(L.lc.tab.get(6n, t7, U32.xor(des.e(r, 23n), k6)), L.lc.tab.get(6n, t8, U32.xor(des.e(r, 27n), k7)))
243      U32.xor(U32.xor(a, b), U32.xor(c, d))
244
245# The Feistel network
246
247def des.step(k: LcDesRk, h: LcDesHalves) -> LcDesHalves:
248  match h:
249    case LcDesHalves{l, +r}:
250      LcDesHalves{r, U32.xor(l, des.f(k, r))}
251
252# the round undone
253def des.unstep(k: LcDesRk, h: LcDesHalves) -> LcDesHalves:
254  match h:
255    case LcDesHalves{+a, b}:
256      LcDesHalves{U32.xor(b, des.f(k, a)), a}
257
258# the rounds of ks, first to last
259def des.rounds(ks: List<&2, LcDesRk>, h: LcDesHalves) -> LcDesHalves:
260  match ks:
261    case Nil{}:
262      h
263    case Con{k, t}:
264      des.rounds(t, des.step(k, h))
265
266# the rounds of ks undone, last to first
267def des.unrounds(ks: List<&2, LcDesRk>, h: LcDesHalves) -> LcDesHalves:
268  match ks:
269    case Nil{}:
270      h
271    case Con{k, t}:
272      des.unstep(k, des.unrounds(t, h))
273
274# The key schedule
275
276def des.kbit.pick(low: Bool, +hi: U32, +lo: U32, +t: Nat) -> U32:
277  match low:
278    case True{}:
279      L.lc.bit(lo, Nat.sub(64n, t))
280    case False{}:
281      L.lc.bit(hi, Nat.sub(32n, t))
282
283# the bits that tab picks from the 64-bit key hi:lo, appended to acc
284def des.picks64(tab: List<&2, Nat>, +hi: U32, +lo: U32, acc: U32) -> U32:
285  match tab:
286    case Nil{}:
287      acc
288    case Con{+t, rest}:
289      des.picks64(rest, hi, lo, U32.or(U32.shl(acc), des.kbit.pick(Nat.is_lt(32n, t), hi, lo, t)))
290
291def des.cdbit.pick(low: Bool, +c: U32, +d: U32, +t: Nat) -> U32:
292  match low:
293    case True{}:
294      L.lc.bit(d, Nat.sub(56n, t))
295    case False{}:
296      L.lc.bit(c, Nat.sub(28n, t))
297
298# the bits that tab picks from the 56 bits C:D (28 each), appended to acc
299def des.picks56(tab: List<&2, Nat>, +c: U32, +d: U32, acc: U32) -> U32:
300  match tab:
301    case Nil{}:
302      acc
303    case Con{+t, rest}:
304      des.picks56(rest, c, d, U32.or(U32.shl(acc), des.cdbit.pick(Nat.is_lt(28n, t), c, d, t)))
305
306def des.rot28(+x: U32, +s: Nat) -> U32:
307  U32.and(268435455, U32.or(U32.shln(x, s), U32.shrn(x, Nat.sub(28n, s))))
308
309def des.group(+x: U32, n: Nat) -> U32:
310  U32.and(63, U32.shrn(x, n))
311
312# K_i = PC-2(C_i D_i), as its eight groups
313def des.subkey(sp: LcDesSp, +c: U32, +d: U32) -> LcDesRk:
314  +a = des.picks56(des.pc2a.table(), c, d, 0)
315  +b = des.picks56(des.pc2b.table(), c, d, 0)
316  LcDesRk{sp, des.group(a, 18n), des.group(a, 12n), des.group(a, 6n), des.group(a, 0n), des.group(b, 18n), des.group(b, 12n), des.group(b, 6n), des.group(b, 0n)}
317
318# K_1 .. K_16 from C_0, D_0
319def des.schedule(shifts: List<&2, Nat>, +sp: LcDesSp, +c: U32, +d: U32) -> List<&2, LcDesRk>:
320  match shifts:
321    case Nil{}:
322      Nil{}
323    case Con{+s, t}:
324      +c2 = des.rot28(c, s)
325      +d2 = des.rot28(d, s)
326      Con{des.subkey(sp, c2, d2), des.schedule(t, sp, c2, d2)}
327
328# A DES key: its sixteen round keys (opaque; built by LcDes.key)
329type LcDesKey is Data:
330  LcDesKey{ks: List<&2, LcDesRk>}
331
332# the key whose 64 bits (parity bits included, and ignored) are hi:lo
333def des.key_of(+hi: U32, +lo: U32) -> LcDesKey:
334  LcDesKey{des.schedule(des.shifts(), des.tables(), des.picks64(des.pc1c.table(), hi, lo, 0), des.picks64(des.pc1d.table(), hi, lo, 0))}
335
336def des.key.pick(ok: Bool, +xs: List<&2, U32>) -> Result<&2, &2, L.LcError, LcDesKey>:
337  match ok:
338    case True{}:
339      Done{des.key_of(L.lc.be(L.lc.at(xs, 0n), L.lc.at(xs, 1n), L.lc.at(xs, 2n), L.lc.at(xs, 3n)), L.lc.be(L.lc.at(xs, 4n), L.lc.at(xs, 5n), L.lc.at(xs, 6n), L.lc.at(xs, 7n)))}
340    case False{}:
341      Fail{L.LcBadKeyLength{B.len(xs)}}
342
343# The cipher
344
345# an 8-byte key (the parity bits, the low bit of each byte, are not checked)
346def LcDes.key(o: B.Octets) -> Result<&2, &2, L.LcError, LcDesKey>:
347  +xs = B.Octets.to_list(o)
348  des.key.pick(Nat.is_eq(B.len(xs), 8n), xs)
349
350def LcDes.encrypt(k: LcDesKey, b: L.LcBlock64) -> L.LcBlock64:
351  match k:
352    case LcDesKey{ks}:
353      des.fp(des.swap(des.rounds(ks, des.ip(b))))
354
355def LcDes.decrypt(k: LcDesKey, b: L.LcBlock64) -> L.LcBlock64:
356  match k:
357    case LcDesKey{ks}:
358      des.fp(des.unrounds(ks, des.swap(des.ip(b))))