serpent.bend

bend-osdev-legacy-ciphers@0.1.0.0 · 404 lines · 53 definitions

1# Serpent (R. Anderson, E. Biham, L. Knudsen, "Serpent: A Proposal for the
2# Advanced Encryption Standard", AES submission, 1998), in its bitslice
3# description: a 128-bit block cipher with keys of up to 256 bits, as a
4# cipher for cipher-modes' modes (~LcSerpentKey, ~LcSerpent.encrypt,
5# ~LcSerpent.decrypt).
6#
7# Serpent reads the block as four little-endian words X0..X3 (byte 0 is the
8# low byte of X0, as in the NESSIE vectors and the kernel); a CmBlock holds
9# big-endian words, so the cipher swaps each word's bytes on the way in and
10# out. The key schedule turns the key into a list of steps, each one
11# invertible: the byte swap, the 33 round-key XORs, the 32 S-box layers and
12# the 31 linear transformations. Encryption runs the steps first to last;
13# decryption undoes them last to first (the inverse S-boxes and the inverse
14# linear transformation), as the paper's decryption does, and
15# decrypt(encrypt(b)) == b is provable for every key and block.
16#
17# The S-box layer works on bits: bit j of X0..X3 is a 4-bit value (X0 its low
18# bit) that the S-box maps, so a proof can undo it one bit position at a time.
19# The rotations of the linear transformation are computed on bits too; the
20# key schedule's arithmetic is native.
21import Base
22import bend-osdev-bytes@0.1.0.0/bytes.bend as B
23import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M
24import bend-osdev-legacy-ciphers@0.1.0.0/legacy_ciphers.bend as L
25
26# The eight S-boxes (section 2, "the S-boxes"): entry v is S_i(v)
27
28type LcSpBox is Data:
29  LcSp0{}
30  LcSp1{}
31  LcSp2{}
32  LcSp3{}
33  LcSp4{}
34  LcSp5{}
35  LcSp6{}
36  LcSp7{}
37
38def sp.table(b: LcSpBox) -> List<&2, U32>:
39  match b:
40    case LcSp0{}:
41      [3, 8, 15, 1, 10, 6, 5, 11, 14, 13, 4, 2, 7, 0, 9, 12]
42    case LcSp1{}:
43      [15, 12, 2, 7, 9, 0, 5, 10, 1, 11, 14, 8, 6, 13, 3, 4]
44    case LcSp2{}:
45      [8, 6, 7, 9, 3, 12, 10, 15, 13, 1, 14, 4, 0, 11, 5, 2]
46    case LcSp3{}:
47      [0, 15, 11, 8, 12, 9, 6, 3, 13, 1, 2, 4, 10, 7, 5, 14]
48    case LcSp4{}:
49      [1, 15, 8, 3, 12, 0, 11, 6, 2, 5, 4, 10, 9, 14, 7, 13]
50    case LcSp5{}:
51      [15, 5, 2, 11, 4, 10, 9, 12, 0, 3, 14, 8, 13, 6, 7, 1]
52    case LcSp6{}:
53      [7, 2, 12, 5, 8, 4, 6, 11, 14, 9, 1, 15, 13, 3, 10, 0]
54    case LcSp7{}:
55      [1, 13, 15, 0, 14, 8, 2, 11, 7, 4, 12, 10, 9, 3, 5, 6]
56
57# the inverse S-boxes
58def sp.itable(b: LcSpBox) -> List<&2, U32>:
59  match b:
60    case LcSp0{}:
61      [13, 3, 11, 0, 10, 6, 5, 12, 1, 14, 4, 7, 15, 9, 8, 2]
62    case LcSp1{}:
63      [5, 8, 2, 14, 15, 6, 12, 3, 11, 4, 7, 9, 1, 13, 10, 0]
64    case LcSp2{}:
65      [12, 9, 15, 4, 11, 14, 1, 2, 0, 3, 6, 13, 5, 8, 10, 7]
66    case LcSp3{}:
67      [0, 9, 10, 7, 11, 14, 6, 13, 3, 5, 12, 2, 4, 8, 15, 1]
68    case LcSp4{}:
69      [5, 0, 8, 3, 10, 9, 7, 14, 2, 12, 11, 6, 4, 15, 13, 1]
70    case LcSp5{}:
71      [8, 15, 2, 9, 4, 1, 13, 14, 11, 6, 5, 3, 7, 12, 10, 0]
72    case LcSp6{}:
73      [15, 10, 1, 13, 5, 3, 6, 0, 4, 9, 14, 7, 2, 12, 8, 11]
74    case LcSp7{}:
75      [3, 0, 6, 13, 9, 14, 15, 8, 5, 12, 11, 7, 10, 1, 4, 2]
76
77def sp.pick(inv: Bool, b: LcSpBox) -> List<&2, U32>:
78  match inv:
79    case True{}:
80      sp.itable(b)
81    case False{}:
82      sp.table(b)
83
84# the S-box (inv False) or its inverse (inv True) at v
85def sp.sbox(b: LcSpBox, inv: Bool, v: U32) -> U32:
86  L.lc.at(sp.pick(inv, b), U32.to_nat(v))
87
88# Four bits: bit j of X0, X1, X2, X3 (X0's is the low bit of the S-box input)
89type LcSpNib is Data:
90  LcSpNib{a: Bool, b: Bool, c: Bool, d: Bool}
91
92def sp.na(n: LcSpNib) -> Bool:
93  match n:
94    case LcSpNib{a, b, c, d}:
95      a
96
97def sp.nb(n: LcSpNib) -> Bool:
98  match n:
99    case LcSpNib{a, b, c, d}:
100      b
101
102def sp.nc(n: LcSpNib) -> Bool:
103  match n:
104    case LcSpNib{a, b, c, d}:
105      c
106
107def sp.nd(n: LcSpNib) -> Bool:
108  match n:
109    case LcSpNib{a, b, c, d}:
110      d
111
112def sp.bit(+v: U32, i: Nat) -> Bool:
113  U32.is_eq(L.lc.bit(v, i), 1)
114
115def sp.nib(b: LcSpBox, inv: Bool, n: LcSpNib) -> LcSpNib:
116  match n:
117    case LcSpNib{x0, x1, x2, x3}:
118      +v = U32.or(U32.or(Bool.to_u32(x0), U32.shl(Bool.to_u32(x1))), U32.or(U32.shln(Bool.to_u32(x2), 2n), U32.shln(Bool.to_u32(x3), 3n)))
119      +w = sp.sbox(b, inv, v)
120      LcSpNib{sp.bit(w, 0n), sp.bit(w, 1n), sp.bit(w, 2n), sp.bit(w, 3n)}
121
122# Four m-bit words
123type LcSpQ<-m: Nat> is Data:
124  LcSpQ{a: Word(m), b: Word(m), c: Word(m), d: Word(m)}
125
126def sp.qa(-m: Nat, q: LcSpQ<m>) -> Word(m):
127  match q:
128    case LcSpQ{a, b, c, d}:
129      a
130
131def sp.qb(-m: Nat, q: LcSpQ<m>) -> Word(m):
132  match q:
133    case LcSpQ{a, b, c, d}:
134      b
135
136def sp.qc(-m: Nat, q: LcSpQ<m>) -> Word(m):
137  match q:
138    case LcSpQ{a, b, c, d}:
139      c
140
141def sp.qd(-m: Nat, q: LcSpQ<m>) -> Word(m):
142  match q:
143    case LcSpQ{a, b, c, d}:
144      d
145
146# the S-box (or its inverse) at every bit position of four m-bit words
147def sp.layer(+b: LcSpBox, +inv: Bool, m: Nat, q: LcSpQ<m>) -> LcSpQ<m>:
148  match m:
149    case 0n:
150      q
151    case 1n+p:
152      match q:
153        case LcSpQ{WCon{x0, t0}, WCon{x1, t1}, WCon{x2, t2}, WCon{x3, t3}}:
154          +o = sp.nib(b, inv, LcSpNib{x0, x1, x2, x3})
155          +r = sp.layer(b, inv, p, LcSpQ{t0, t1, t2, t3})
156          LcSpQ{WCon{sp.na(o), sp.qa(p, r)}, WCon{sp.nb(o), sp.qb(p, r)}, WCon{sp.nc(o), sp.qc(p, r)}, WCon{sp.nd(o), sp.qd(p, r)}}
157
158# the S-box layer (or its inverse) on the state X0..X3
159def sp.sop(+b: LcSpBox, +inv: Bool, s: M.CmBlock) -> M.CmBlock:
160  match s:
161    case M.CmBlock{U32{w0}, U32{w1}, U32{w2}, U32{w3}}:
162      +r = sp.layer(b, inv, 32n, LcSpQ{w0, w1, w2, w3})
163      M.CmBlock{U32{sp.qa(32n, r)}, U32{sp.qb(32n, r)}, U32{sp.qc(32n, r)}, U32{sp.qd(32n, r)}}
164
165# The linear transformation (section 2), step by step, and each step undone
166
167def sp.lt1(s: M.CmBlock) -> M.CmBlock:
168  match s:
169    case M.CmBlock{x0, x1, x2, x3}:
170      M.CmBlock{L.lc.rotl13.bits(x0), x1, x2, x3}
171
172def sp.lt2(s: M.CmBlock) -> M.CmBlock:
173  match s:
174    case M.CmBlock{x0, x1, x2, x3}:
175      M.CmBlock{x0, x1, L.lc.rotl3.bits(x2), x3}
176
177# X1 = X1 xor X0 xor X2 (its own inverse)
178def sp.lt3(s: M.CmBlock) -> M.CmBlock:
179  match s:
180    case M.CmBlock{+x0, x1, +x2, x3}:
181      M.CmBlock{x0, U32.xor(x1, U32.xor(x0, x2)), x2, x3}
182
183# X3 = X3 xor X2 xor (X0 << 3) (its own inverse)
184def sp.lt4(s: M.CmBlock) -> M.CmBlock:
185  match s:
186    case M.CmBlock{+x0, x1, +x2, x3}:
187      M.CmBlock{x0, x1, x2, U32.xor(x3, U32.xor(x2, U32.shln(x0, 3n)))}
188
189def sp.lt5(s: M.CmBlock) -> M.CmBlock:
190  match s:
191    case M.CmBlock{x0, x1, x2, x3}:
192      M.CmBlock{x0, L.lc.rotl1.bits(x1), x2, L.lc.rotl7.bits(x3)}
193
194# X0 = X0 xor X1 xor X3 (its own inverse)
195def sp.lt6(s: M.CmBlock) -> M.CmBlock:
196  match s:
197    case M.CmBlock{x0, +x1, x2, +x3}:
198      M.CmBlock{U32.xor(x0, U32.xor(x1, x3)), x1, x2, x3}
199
200# X2 = X2 xor X3 xor (X1 << 7) (its own inverse)
201def sp.lt7(s: M.CmBlock) -> M.CmBlock:
202  match s:
203    case M.CmBlock{x0, +x1, x2, +x3}:
204      M.CmBlock{x0, x1, U32.xor(x2, U32.xor(x3, U32.shln(x1, 7n))), x3}
205
206def sp.lt8(s: M.CmBlock) -> M.CmBlock:
207  match s:
208    case M.CmBlock{x0, x1, x2, x3}:
209      M.CmBlock{L.lc.rotl5.bits(x0), x1, L.lc.rotl22.bits(x2), x3}
210
211def sp.ilt1(s: M.CmBlock) -> M.CmBlock:
212  match s:
213    case M.CmBlock{x0, x1, x2, x3}:
214      M.CmBlock{L.lc.rotl19.bits(x0), x1, x2, x3}
215
216def sp.ilt2(s: M.CmBlock) -> M.CmBlock:
217  match s:
218    case M.CmBlock{x0, x1, x2, x3}:
219      M.CmBlock{x0, x1, L.lc.rotl29.bits(x2), x3}
220
221def sp.ilt5(s: M.CmBlock) -> M.CmBlock:
222  match s:
223    case M.CmBlock{x0, x1, x2, x3}:
224      M.CmBlock{x0, L.lc.rotl31.bits(x1), x2, L.lc.rotl25.bits(x3)}
225
226def sp.ilt8(s: M.CmBlock) -> M.CmBlock:
227  match s:
228    case M.CmBlock{x0, x1, x2, x3}:
229      M.CmBlock{L.lc.rotl27.bits(x0), x1, L.lc.rotl10.bits(x2), x3}
230
231def sp.lt(s: M.CmBlock) -> M.CmBlock:
232  sp.lt8(sp.lt7(sp.lt6(sp.lt5(sp.lt4(sp.lt3(sp.lt2(sp.lt1(s))))))))
233
234def sp.ilt(s: M.CmBlock) -> M.CmBlock:
235  sp.ilt1(sp.ilt2(sp.lt3(sp.lt4(sp.ilt5(sp.lt6(sp.lt7(sp.ilt8(s))))))))
236
237# The steps of the cipher (internal)
238type LcSpOp is Data:
239  LcSpBswap{}
240  LcSpKey{k: M.CmBlock}
241  LcSpS{b: LcSpBox}
242  LcSpLt{}
243
244def sp.op(o: LcSpOp, s: M.CmBlock) -> M.CmBlock:
245  match o:
246    case LcSpBswap{}:
247      match s:
248        case M.CmBlock{a, b, c, d}:
249          M.CmBlock{L.lc.bswap.bits(a), L.lc.bswap.bits(b), L.lc.bswap.bits(c), L.lc.bswap.bits(d)}
250    case LcSpKey{k}:
251      M.CmBlock.xor(s, k)
252    case LcSpS{b}:
253      sp.sop(b, False{}, s)
254    case LcSpLt{}:
255      sp.lt(s)
256
257# the step undone
258def sp.unop(o: LcSpOp, s: M.CmBlock) -> M.CmBlock:
259  match o:
260    case LcSpBswap{}:
261      match s:
262        case M.CmBlock{a, b, c, d}:
263          M.CmBlock{L.lc.bswap.bits(a), L.lc.bswap.bits(b), L.lc.bswap.bits(c), L.lc.bswap.bits(d)}
264    case LcSpKey{k}:
265      M.CmBlock.xor(s, k)
266    case LcSpS{b}:
267      sp.sop(b, True{}, s)
268    case LcSpLt{}:
269      sp.ilt(s)
270
271def sp.run(os: List<&2, LcSpOp>, s: M.CmBlock) -> M.CmBlock:
272  match os:
273    case Nil{}:
274      s
275    case Con{o, t}:
276      sp.run(t, sp.op(o, s))
277
278def sp.unrun(os: List<&2, LcSpOp>, s: M.CmBlock) -> M.CmBlock:
279  match os:
280    case Nil{}:
281      s
282    case Con{o, t}:
283      sp.unop(o, sp.unrun(t, s))
284
285# The key schedule (section 2, "the key schedule")
286
287
288# S-box n (n = 0 to 7)
289def sp.box.go(n: Nat) -> LcSpBox:
290  match n:
291    case 0n:
292      LcSp0{}
293    case 1n:
294      LcSp1{}
295    case 2n:
296      LcSp2{}
297    case 3n:
298      LcSp3{}
299    case 4n:
300      LcSp4{}
301    case 5n:
302      LcSp5{}
303    case 6n:
304      LcSp6{}
305    case _:
306      LcSp7{}
307
308# the prekeys w_i = (w_(i-8) xor w_(i-5) xor w_(i-3) xor w_(i-1) xor phi xor
309# i) <<< 11, for n more words from i; win holds w_(i-8) .. w_(i-1)
310# S-box n mod 8
311def sp.box(n: Nat) -> LcSpBox:
312  sp.box.go(Nat.mod(n, 8n))
313
314def sp.prekeys(n: Nat, +i: U32, win: List<&2, U32>) -> List<&2, U32>:
315  match n:
316    case 0n:
317      Nil{}
318    case 1n+p:
319      match win:
320        case Con{a, Con{b, Con{c, Con{+d, Con{e, Con{+f, Con{g, Con{+h, t}}}}}}}}:
321          +w = L.lc.rotl(U32.xor(U32.xor(U32.xor(a, d), U32.xor(f, h)), U32.xor(2654435769, i)), 11n)
322          Con{w, sp.prekeys(p, U32.add(i, 1), [b, c, d, e, f, g, h, w])}
323        case _:
324          Nil{}
325
326# round key K_i = S_((3 - i) mod 8)(w_(4i) .. w_(4i+3)), as an XOR step, for
327# n more round keys from i
328def sp.round_keys(n: Nat, +i: Nat, ws: List<&2, U32>) -> List<&2, M.CmBlock>:
329  match n:
330    case 0n:
331      Nil{}
332    case 1n+p:
333      match ws:
334        case Con{a, Con{b, Con{c, Con{d, t}}}}:
335          Con{sp.sop(sp.box(Nat.sub(35n, i)), False{}, M.CmBlock{a, b, c, d}), sp.round_keys(p, Nat.add(i, 1n), t)}
336        case _:
337          Nil{}
338
339# the steps of the 32 rounds from round i: K_i, S_(i mod 8), then LT (rounds
340# 0 to 30) or K_32 (round 31)
341def sp.rounds(ks: List<&2, M.CmBlock>, +i: Nat) -> List<&2, LcSpOp>:
342  match ks:
343    case Con{k, Con{k32, Nil{}}}:
344      [LcSpKey{k}, LcSpS{sp.box(i)}, LcSpKey{k32}]
345    case Con{k, t}:
346      Con{LcSpKey{k}, Con{LcSpS{sp.box(i)}, Con{LcSpLt{}, sp.rounds(t, Nat.add(i, 1n))}}}
347    case Nil{}:
348      Nil{}
349
350def sp.append(xs: List<&2, LcSpOp>, ys: List<&2, LcSpOp>) -> List<&2, LcSpOp>:
351  match xs:
352    case Nil{}:
353      ys
354    case Con{h, t}:
355      Con{h, sp.append(t, ys)}
356
357# A Serpent key: the steps of the cipher (opaque; built by LcSerpent.key)
358type LcSerpentKey is Data:
359  LcSerpentKey{ops: List<&2, LcSpOp>}
360
361def sp.pad.pick(short: Bool, +xs: List<&2, U32>, +n: Nat) -> List<&2, U32>:
362  match short:
363    case True{}:
364      B.append(xs, Con{1, B.zeros(Nat.sub(31n, n))})
365    case False{}:
366      xs
367
368# the key bytes padded to 256 bits: a 1 bit after the key, then zeros
369def sp.pad(+xs: List<&2, U32>, +n: Nat) -> List<&2, U32>:
370  sp.pad.pick(Nat.is_lt(n, 32n), xs, n)
371
372def sp.le(+xs: List<&2, U32>, +i: Nat) -> U32:
373  +j = Nat.mul(4n, i)
374  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)))
375
376def sp.key(+xs: List<&2, U32>) -> LcSerpentKey:
377  +k = sp.pad(xs, B.len(xs))
378  +win = {[sp.le(k, 0n), sp.le(k, 1n), sp.le(k, 2n), sp.le(k, 3n), sp.le(k, 4n), sp.le(k, 5n), sp.le(k, 6n), sp.le(k, 7n)] : List<&2, U32>}
379  LcSerpentKey{Con{LcSpBswap{}, sp.append(sp.rounds(sp.round_keys(33n, 0n, sp.prekeys(132n, 0, win)), 0n), [LcSpBswap{}])}}
380
381def sp.key.pick(ok: Bool, +xs: List<&2, U32>) -> Result<&2, &2, L.LcError, LcSerpentKey>:
382  match ok:
383    case True{}:
384      Done{sp.key(xs)}
385    case False{}:
386      Fail{L.LcBadKeyLength{B.len(xs)}}
387
388# The cipher
389
390# a key of 0 to 32 bytes (16, 24 and 32 are the usual sizes; a shorter key is
391# padded as the specification says)
392def LcSerpent.key(o: B.Octets) -> Result<&2, &2, L.LcError, LcSerpentKey>:
393  +xs = B.Octets.to_list(o)
394  sp.key.pick(Nat.is_le(B.len(xs), 32n), xs)
395
396def LcSerpent.encrypt(k: LcSerpentKey, b: M.CmBlock) -> M.CmBlock:
397  match k:
398    case LcSerpentKey{ops}:
399      sp.run(ops, b)
400
401def LcSerpent.decrypt(k: LcSerpentKey, b: M.CmBlock) -> M.CmBlock:
402  match k:
403    case LcSerpentKey{ops}:
404      sp.unrun(ops, b)