twofish.bend

bend-osdev-legacy-ciphers@0.1.0.0 · 372 lines · 55 definitions

1# Twofish (B. Schneier, J. Kelsey, D. Whiting, D. Wagner, C. Hall, N.
2# Ferguson, "Twofish: A 128-Bit Block Cipher", AES submission, 1998): a
3# 128-bit block cipher with 128-, 192- or 256-bit keys, as a cipher for
4# cipher-modes' modes (~LcTwofishKey, ~LcTwofish.encrypt, ~LcTwofish.decrypt).
5#
6# Twofish reads the block as four little-endian words; a CmBlock holds
7# big-endian words, so the cipher swaps each word's bytes on the way in and
8# out. The key schedule turns the key into a list of steps, each one
9# invertible: the byte swap, the whitening XORs, the sixteen rounds
10#   (R0, R1, R2, R3) -> ((R2 xor F0) >>> 1, (R3 <<< 1) xor F1, R0, R1)
11# with (F0, F1) = F(R0, R1, r), and the swap that undoes the last round's
12# exchange of halves. Encryption runs the steps first to last; decryption
13# undoes them last to first, the same function as the paper's decryption, and
14# decrypt(encrypt(b)) == b is provable for every key and block: a round is
15# undone whatever F is. The byte swaps and the 1-bit rotations a round undoes
16# are computed on bits (legacy-ciphers.bend), so a proof computes through
17# them; F (the key-dependent S-boxes, the MDS matrix, the PHT) and the key
18# schedule use native word operations.
19import Base
20import bend-osdev-bytes@0.1.0.0/bytes.bend as B
21import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M
22import bend-osdev-legacy-ciphers@0.1.0.0/legacy_ciphers.bend as L
23
24# The permutations q0 and q1 (section 4.3.5): their 4-bit tables t0 .. t3
25
26def tf.q0.t() -> List<&2, U32>:
27  [8, 1, 7, 13, 6, 15, 3, 2, 0, 11, 5, 9, 14, 12, 10, 4,
28    14, 12, 11, 8, 1, 2, 3, 5, 15, 4, 10, 6, 7, 0, 9, 13,
29    11, 10, 5, 14, 6, 13, 9, 0, 12, 8, 15, 3, 2, 4, 7, 1,
30    13, 7, 15, 4, 1, 2, 6, 14, 9, 11, 3, 0, 8, 5, 12, 10]
31
32def tf.q1.t() -> List<&2, U32>:
33  [2, 8, 11, 13, 15, 7, 6, 14, 3, 1, 9, 4, 0, 10, 12, 5,
34    1, 14, 2, 11, 4, 12, 3, 7, 6, 13, 10, 5, 15, 9, 0, 8,
35    4, 12, 7, 5, 1, 6, 9, 10, 0, 14, 13, 8, 2, 11, 3, 15,
36    11, 9, 5, 1, 12, 3, 13, 14, 6, 4, 7, 15, 2, 0, 8, 10]
37
38# entry x of table i (0 to 3) of ts
39def tf.t(+ts: List<&2, U32>, i: Nat, +x: U32) -> U32:
40  L.lc.at(ts, Nat.add(Nat.mul(16n, i), U32.to_nat(x)))
41
42# a 4-bit value rotated right by one bit
43def tf.ror4(+x: U32) -> U32:
44  U32.and(15, U32.or(U32.shr(x), U32.shln(x, 3n)))
45
46def tf.q.half(+a: U32, +b: U32) -> U32:
47  U32.xor(U32.xor(a, tf.ror4(b)), U32.and(15, U32.shln(a, 3n)))
48
49def tf.q.go(+ts: List<&2, U32>, +a2: U32, +b2: U32) -> U32:
50  U32.add(U32.mul(16, tf.t(ts, 3n, tf.q.half(a2, b2))), tf.t(ts, 2n, U32.xor(a2, b2)))
51
52# q(x) from its tables
53def tf.q.raw(+ts: List<&2, U32>, +x: U32) -> U32:
54  +a0 = U32.shrn(x, 4n)
55  +b0 = U32.and(15, x)
56  tf.q.go(ts, tf.t(ts, 0n, U32.xor(a0, b0)), tf.t(ts, 1n, tf.q.half(a0, b0)))
57
58def tf.gen(~f: U32 -> U32, n: Nat, +i: U32) -> List<&2, U32>:
59  match n:
60    case 0n:
61      Nil{}
62    case 1n+p:
63      Con{f(i), tf.gen(~f, p, U32.add(i, 1))}
64
65def tf.q0() -> L.LcTab:
66  L.lc.tab(8n, tf.gen(~(x => tf.q.raw(tf.q0.t(), x)), 256n, 0))
67
68def tf.q1() -> L.LcTab:
69  L.lc.tab(8n, tf.gen(~(x => tf.q.raw(tf.q1.t(), x)), 256n, 0))
70
71# The tables, built once per key (internal): q0, q1 and the MDS columns
72type LcTfTabs is Data:
73  LcTfTabs{q0: L.LcTab, q1: L.LcTab, m0: L.LcTab, m1: L.LcTab, m2: L.LcTab, m3: L.LcTab}
74
75def tf.q(t: LcTfTabs, one: Bool, +x: U32) -> U32:
76  match t:
77    case LcTfTabs{q0, q1, m0, m1, m2, m3}:
78      match one:
79        case True{}:
80          L.lc.tab.get(8n, q1, x)
81        case False{}:
82          L.lc.tab.get(8n, q0, x)
83
84# GF(2^8) multiplication modulo the polynomial poly (with its x^8 term)
85
86def tf.xt(+a: U32, +poly: U32) -> U32:
87  U32.and(255, U32.xor(U32.shl(a), U32.and(poly, U32.sub(0, U32.and(1, U32.shrn(a, 7n))))))
88
89def tf.gmul.go(n: Nat, +a: U32, +b: U32, +poly: U32, p: U32) -> U32:
90  match n:
91    case 0n:
92      p
93    case 1n+q:
94      tf.gmul.go(q, tf.xt(a, poly), U32.shr(b), poly, U32.xor(p, U32.and(a, U32.sub(0, U32.and(1, b)))))
95
96def tf.gmul(+a: U32, +b: U32, +poly: U32) -> U32:
97  tf.gmul.go(8n, a, b, poly, 0)
98
99# The MDS matrix (section 4.2), over GF(2^8) modulo x^8 + x^6 + x^5 + x^3 + 1;
100# column j as a table: entry x is the word (MDS[0][j] x, .., MDS[3][j] x),
101# row 0 in the low byte
102
103def tf.mds.m() -> List<&2, U32>:
104  [1, 239, 91, 91,
105    91, 239, 239, 1,
106    239, 91, 1, 239,
107    239, 1, 239, 91]
108
109def tf.mds.col(+j: Nat, +x: U32) -> U32:
110  +m = tf.mds.m()
111  L.lc.le(tf.gmul(L.lc.at(m, j), x, 105), tf.gmul(L.lc.at(m, Nat.add(4n, j)), x, 105), tf.gmul(L.lc.at(m, Nat.add(8n, j)), x, 105), tf.gmul(L.lc.at(m, Nat.add(12n, j)), x, 105))
112
113def tf.mds0() -> L.LcTab:
114  L.lc.tab(8n, tf.gen(~(x => tf.mds.col(0n, x)), 256n, 0))
115
116def tf.mds1() -> L.LcTab:
117  L.lc.tab(8n, tf.gen(~(x => tf.mds.col(1n, x)), 256n, 0))
118
119def tf.mds2() -> L.LcTab:
120  L.lc.tab(8n, tf.gen(~(x => tf.mds.col(2n, x)), 256n, 0))
121
122def tf.mds3() -> L.LcTab:
123  L.lc.tab(8n, tf.gen(~(x => tf.mds.col(3n, x)), 256n, 0))
124
125def tf.tables() -> LcTfTabs:
126  LcTfTabs{tf.q0(), tf.q1(), tf.mds0(), tf.mds1(), tf.mds2(), tf.mds3()}
127
128def tf.mds(t: LcTfTabs, +y: U32) -> U32:
129  match t:
130    case LcTfTabs{q0, q1, m0, m1, m2, m3}:
131      U32.xor(U32.xor(L.lc.tab.get(8n, m0, L.lc.byte(y, 0n)), L.lc.tab.get(8n, m1, L.lc.byte(y, 1n))), U32.xor(L.lc.tab.get(8n, m2, L.lc.byte(y, 2n)), L.lc.tab.get(8n, m3, L.lc.byte(y, 3n))))
132
133# The function h (section 4.3.2)
134
135# byte i of x through q (q1 if p_i), then XOR byte i of l
136def tf.stage(+t: LcTfTabs, p0: Bool, p1: Bool, p2: Bool, p3: Bool, +x: U32, +l: U32) -> U32:
137  L.lc.le(U32.xor(tf.q(t, p0, L.lc.byte(x, 0n)), L.lc.byte(l, 0n)), U32.xor(tf.q(t, p1, L.lc.byte(x, 1n)), L.lc.byte(l, 1n)), U32.xor(tf.q(t, p2, L.lc.byte(x, 2n)), L.lc.byte(l, 2n)), U32.xor(tf.q(t, p3, L.lc.byte(x, 3n)), L.lc.byte(l, 3n)))
138
139# the stages every key length shares: with L_1, with L_0, then q alone
140def tf.h2(+t: LcTfTabs, +x: U32, +l0: U32, +l1: U32) -> U32:
141  tf.mds(t, tf.stage(t, True{}, False{}, True{}, False{}, tf.stage(t, False{}, False{}, True{}, True{}, tf.stage(t, False{}, True{}, False{}, True{}, x, l1), l0), 0))
142
143def tf.h3(+t: LcTfTabs, +x: U32, +l0: U32, +l1: U32, +l2: U32) -> U32:
144  tf.h2(t, tf.stage(t, True{}, True{}, False{}, False{}, x, l2), l0, l1)
145
146def tf.h4(+t: LcTfTabs, +x: U32, +l0: U32, +l1: U32, +l2: U32, +l3: U32) -> U32:
147  tf.h3(t, tf.stage(t, True{}, False{}, False{}, True{}, x, l3), l0, l1, l2)
148
149# h(X, L) for L = L_0 .. L_(k-1), k = 2, 3 or 4
150def tf.h(+t: LcTfTabs, +x: U32, l: List<&2, U32>) -> U32:
151  match l:
152    case Con{l0, Con{l1, Nil{}}}:
153      tf.h2(t, x, l0, l1)
154    case Con{l0, Con{l1, Con{l2, Nil{}}}}:
155      tf.h3(t, x, l0, l1, l2)
156    case Con{l0, Con{l1, Con{l2, Con{l3, more}}}}:
157      tf.h4(t, x, l0, l1, l2, l3)
158    case _:
159      0
160
161# The function F (section 4.3): g(X) = h(X, S), then the PHT and the round
162# subkeys K_(2r+8), K_(2r+9); F0 and F1 as an LcBlock64
163
164def tf.f(+t: LcTfTabs, +s: List<&2, U32>, r0: U32, r1: U32, ka: U32, kb: U32) -> L.LcBlock64:
165  +t0 = tf.h(t, r0, s)
166  +t1 = tf.h(t, L.lc.rotl(r1, 8n), s)
167  L.LcBlock64{U32.add(U32.add(t0, t1), ka), U32.add(U32.add(t0, U32.add(t1, t1)), kb)}
168
169def tf.f0(x: L.LcBlock64) -> U32:
170  match x:
171    case L.LcBlock64{a, b}:
172      a
173
174def tf.f1(x: L.LcBlock64) -> U32:
175  match x:
176    case L.LcBlock64{a, b}:
177      b
178
179# The steps of the cipher (internal)
180type LcTfOp is Data:
181  LcTfBswap{}
182  LcTfWhite{k: M.CmBlock}
183  LcTfRound{t: LcTfTabs, s: List<&2, U32>, ka: U32, kb: U32}
184  LcTfSwap{}
185
186def tf.op(o: LcTfOp, s: M.CmBlock) -> M.CmBlock:
187  match o:
188    case LcTfBswap{}:
189      match s:
190        case M.CmBlock{a, b, c, d}:
191          M.CmBlock{L.lc.bswap.bits(a), L.lc.bswap.bits(b), L.lc.bswap.bits(c), L.lc.bswap.bits(d)}
192    case LcTfWhite{k}:
193      M.CmBlock.xor(s, k)
194    case LcTfRound{tb, sk, ka, kb}:
195      match s:
196        case M.CmBlock{+r0, +r1, r2, r3}:
197          +f = tf.f(tb, sk, r0, r1, ka, kb)
198          M.CmBlock{L.lc.rotl31.bits(U32.xor(r2, tf.f0(f))), U32.xor(L.lc.rotl1.bits(r3), tf.f1(f)), r0, r1}
199    case LcTfSwap{}:
200      match s:
201        case M.CmBlock{a, b, c, d}:
202          M.CmBlock{c, d, a, b}
203
204# the step undone
205def tf.unop(o: LcTfOp, s: M.CmBlock) -> M.CmBlock:
206  match o:
207    case LcTfBswap{}:
208      match s:
209        case M.CmBlock{a, b, c, d}:
210          M.CmBlock{L.lc.bswap.bits(a), L.lc.bswap.bits(b), L.lc.bswap.bits(c), L.lc.bswap.bits(d)}
211    case LcTfWhite{k}:
212      M.CmBlock.xor(s, k)
213    case LcTfRound{tb, sk, ka, kb}:
214      match s:
215        case M.CmBlock{a, b, +c, +d}:
216          +f = tf.f(tb, sk, c, d, ka, kb)
217          M.CmBlock{c, d, U32.xor(L.lc.rotl1.bits(a), tf.f0(f)), L.lc.rotl31.bits(U32.xor(b, tf.f1(f)))}
218    case LcTfSwap{}:
219      match s:
220        case M.CmBlock{a, b, c, d}:
221          M.CmBlock{c, d, a, b}
222
223def tf.run(os: List<&2, LcTfOp>, s: M.CmBlock) -> M.CmBlock:
224  match os:
225    case Nil{}:
226      s
227    case Con{o, t}:
228      tf.run(t, tf.op(o, s))
229
230def tf.unrun(os: List<&2, LcTfOp>, s: M.CmBlock) -> M.CmBlock:
231  match os:
232    case Nil{}:
233      s
234    case Con{o, t}:
235      tf.unop(o, tf.unrun(t, s))
236
237# The key schedule (section 4.3)
238
239# the little-endian words of the key bytes xs, every other one from word i
240def tf.words(n: Nat, +xs: List<&2, U32>, +i: Nat) -> List<&2, U32>:
241  match n:
242    case 0n:
243      Nil{}
244    case 1n+p:
245      +j = Nat.mul(4n, i)
246      Con{L.lc.le(L.lc.at(xs, j), L.lc.at(xs, Nat.add(j, 1n)), L.lc.at(xs, Nat.add(j, 2n)), L.lc.at(xs, Nat.add(j, 3n))), tf.words(p, xs, Nat.add(i, 2n))}
247
248# The RS matrix (section 4.3), over GF(2^8) modulo x^8 + x^6 + x^3 + x^2 + 1
249def tf.rs() -> List<&2, U32>:
250  [1, 164, 85, 135, 90, 88, 219, 158,
251    164, 86, 130, 243, 30, 198, 104, 229,
252    2, 161, 252, 193, 71, 174, 61, 25,
253    164, 85, 135, 90, 88, 219, 158, 3]
254
255# row r of RS times the 8 key bytes from byte j
256def tf.rs.row(n: Nat, +xs: List<&2, U32>, +r: Nat, +j: Nat, +c: Nat, acc: U32) -> U32:
257  match n:
258    case 0n:
259      acc
260    case 1n+p:
261      tf.rs.row(p, xs, r, j, Nat.add(c, 1n), U32.xor(acc, tf.gmul(L.lc.at(tf.rs(), Nat.add(Nat.mul(8n, r), c)), L.lc.at(xs, Nat.add(j, c)), 77)))
262
263# S_i: RS times key bytes 8i .. 8i + 7
264def tf.s_word(+xs: List<&2, U32>, +i: Nat) -> U32:
265  +j = Nat.mul(8n, i)
266  L.lc.le(tf.rs.row(8n, xs, 0n, j, 0n, 0), tf.rs.row(8n, xs, 1n, j, 0n, 0), tf.rs.row(8n, xs, 2n, j, 0n, 0), tf.rs.row(8n, xs, 3n, j, 0n, 0))
267
268# S = (S_(k-1), .., S_0), the k words of the key-dependent S-boxes
269def tf.svec(n: Nat, +xs: List<&2, U32>, +i: Nat, acc: List<&2, U32>) -> List<&2, U32>:
270  match n:
271    case 0n:
272      acc
273    case 1n+p:
274      tf.svec(p, xs, Nat.add(i, 1n), Con{tf.s_word(xs, i), acc})
275
276# K_(2i) and K_(2i+1) as an LcBlock64
277def tf.kpair(+t: LcTfTabs, +me: List<&2, U32>, +mo: List<&2, U32>, +i: U32) -> L.LcBlock64:
278  +a = tf.h(t, U32.mul(U32.mul(2, i), 16843009), me)
279  +b = L.lc.rotl(tf.h(t, U32.mul(U32.add(U32.mul(2, i), 1), 16843009), mo), 8n)
280  L.LcBlock64{U32.add(a, b), L.lc.rotl(U32.add(a, U32.add(b, b)), 9n)}
281
282# the rounds' steps from round r, with the pairs K_(2r+8), K_(2r+9) in ks
283def tf.rounds(ks: List<&2, L.LcBlock64>, +t: LcTfTabs, +s: List<&2, U32>) -> List<&2, LcTfOp>:
284  match ks:
285    case Nil{}:
286      Nil{}
287    case Con{L.LcBlock64{a, b}, rest}:
288      Con{LcTfRound{t, s, a, b}, tf.rounds(rest, t, s)}
289
290def tf.kpairs(n: Nat, +t: LcTfTabs, +me: List<&2, U32>, +mo: List<&2, U32>, +i: U32) -> List<&2, L.LcBlock64>:
291  match n:
292    case 0n:
293      Nil{}
294    case 1n+p:
295      Con{tf.kpair(t, me, mo, i), tf.kpairs(p, t, me, mo, U32.add(i, 1))}
296
297def tf.white.le(a: L.LcBlock64, b: L.LcBlock64) -> LcTfOp:
298  match a b:
299    case L.LcBlock64{k0, k1} L.LcBlock64{k2, k3}:
300      LcTfWhite{M.CmBlock{k0, k1, k2, k3}}
301
302def tf.append(xs: List<&2, LcTfOp>, ys: List<&2, LcTfOp>) -> List<&2, LcTfOp>:
303  match xs:
304    case Nil{}:
305      ys
306    case Con{h, t}:
307      Con{h, tf.append(t, ys)}
308
309# the steps from the subkey pairs (K_0, K_1) .. (K_38, K_39)
310def tf.ops(ks: List<&2, L.LcBlock64>, +t: LcTfTabs, +s: List<&2, U32>) -> List<&2, LcTfOp>:
311  match ks:
312    case Con{p0, Con{p1, Con{p2, Con{p3, rest}}}}:
313      Con{LcTfBswap{}, Con{tf.white.le(p0, p1), tf.append(tf.rounds(rest, t, s), [LcTfSwap{}, tf.white.le(p2, p3), LcTfBswap{}])}}
314    case _:
315      Nil{}
316
317# A Twofish key: the steps of the cipher (opaque; built by LcTwofish.key)
318type LcTwofishKey is Data:
319  LcTwofishKey{ops: List<&2, LcTfOp>}
320
321# the key from k = 2, 3 or 4 64-bit words of key bytes xs
322def tf.key(+k: Nat, +xs: List<&2, U32>) -> LcTwofishKey:
323  +t = tf.tables()
324  LcTwofishKey{tf.ops(tf.kpairs(20n, t, tf.words(k, xs, 0n), tf.words(k, xs, 1n), 0), t, tf.svec(k, xs, 0n, Nil{}))}
325
326def tf.key.pick(n16: Bool, n24: Bool, n32: Bool, +xs: List<&2, U32>) -> Result<&2, &2, L.LcError, LcTwofishKey>:
327  match n16 n24 n32:
328    case True{} _ _:
329      Done{tf.key(2n, xs)}
330    case False{} True{} _:
331      Done{tf.key(3n, xs)}
332    case False{} False{} True{}:
333      Done{tf.key(4n, xs)}
334    case False{} False{} False{}:
335      Fail{L.LcBadKeyLength{B.len(xs)}}
336
337# The cipher
338
339# a 16-, 24- or 32-byte key (Twofish-128, -192, -256, by its length)
340def LcTwofish.key(o: B.Octets) -> Result<&2, &2, L.LcError, LcTwofishKey>:
341  +xs = B.Octets.to_list(o)
342  +n = B.len(xs)
343  tf.key.pick(Nat.is_eq(n, 16n), Nat.is_eq(n, 24n), Nat.is_eq(n, 32n), xs)
344
345# the key padded with zero bytes to 16, 24 or 32 bytes (section 4.3: keys
346# shorter than 256 bits are padded with zeros to the next defined length)
347def tf.pad.pick(n16: Bool, n24: Bool, n32: Bool, +n: Nat, +xs: List<&2, U32>) -> Result<&2, &2, L.LcError, LcTwofishKey>:
348  match n16 n24 n32:
349    case True{} _ _:
350      Done{tf.key(2n, B.append(xs, B.zeros(Nat.sub(16n, n))))}
351    case False{} True{} _:
352      Done{tf.key(3n, B.append(xs, B.zeros(Nat.sub(24n, n))))}
353    case False{} False{} True{}:
354      Done{tf.key(4n, B.append(xs, B.zeros(Nat.sub(32n, n))))}
355    case False{} False{} False{}:
356      Fail{L.LcBadKeyLength{n}}
357
358# a key of 1 to 32 bytes, zero-padded as the specification says
359def LcTwofish.key_padded(o: B.Octets) -> Result<&2, &2, L.LcError, LcTwofishKey>:
360  +xs = B.Octets.to_list(o)
361  +n = B.len(xs)
362  tf.pad.pick(Bool.and(Nat.is_lt(0n, n), Nat.is_le(n, 16n)), Nat.is_le(n, 24n), Nat.is_le(n, 32n), n, xs)
363
364def LcTwofish.encrypt(k: LcTwofishKey, b: M.CmBlock) -> M.CmBlock:
365  match k:
366    case LcTwofishKey{ops}:
367      tf.run(ops, b)
368
369def LcTwofish.decrypt(k: LcTwofishKey, b: M.CmBlock) -> M.CmBlock:
370  match k:
371    case LcTwofishKey{ops}:
372      tf.unrun(ops, b)