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.
21	import Base
22	import bend-osdev-bytes@0.1.0.0/bytes.bend as B
23	import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M
24	import ./legacy_ciphers.bend as L
25	
26	# The eight S-boxes (section 2, "the S-boxes"): entry v is S_i(v)
27	
28	type LcSpBox is Data:
29	  LcSp0{}
30	  LcSp1{}
31	  LcSp2{}
32	  LcSp3{}
33	  LcSp4{}
34	  LcSp5{}
35	  LcSp6{}
36	  LcSp7{}
37	
38	def 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
58	def 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	
77	def 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
85	def 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)
89	type LcSpNib is Data:
90	  LcSpNib{a: Bool, b: Bool, c: Bool, d: Bool}
91	
92	def sp.na(n: LcSpNib) -> Bool:
93	  match n:
94	    case LcSpNib{a, b, c, d}:
95	      a
96	
97	def sp.nb(n: LcSpNib) -> Bool:
98	  match n:
99	    case LcSpNib{a, b, c, d}:
100	      b
101	
102	def sp.nc(n: LcSpNib) -> Bool:
103	  match n:
104	    case LcSpNib{a, b, c, d}:
105	      c
106	
107	def sp.nd(n: LcSpNib) -> Bool:
108	  match n:
109	    case LcSpNib{a, b, c, d}:
110	      d
111	
112	def sp.bit(+v: U32, i: Nat) -> Bool:
113	  U32.is_eq(L.lc.bit(v, i), 1)
114	
115	def 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
123	type LcSpQ<-m: Nat> is Data:
124	  LcSpQ{a: Word(m), b: Word(m), c: Word(m), d: Word(m)}
125	
126	def sp.qa(-m: Nat, q: LcSpQ<m>) -> Word(m):
127	  match q:
128	    case LcSpQ{a, b, c, d}:
129	      a
130	
131	def sp.qb(-m: Nat, q: LcSpQ<m>) -> Word(m):
132	  match q:
133	    case LcSpQ{a, b, c, d}:
134	      b
135	
136	def sp.qc(-m: Nat, q: LcSpQ<m>) -> Word(m):
137	  match q:
138	    case LcSpQ{a, b, c, d}:
139	      c
140	
141	def 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
147	def 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
159	def 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	
167	def 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	
172	def 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)
178	def 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)
184	def 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	
189	def 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)
195	def 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)
201	def 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	
206	def 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	
211	def 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	
216	def 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	
221	def 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	
226	def 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	
231	def 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	
234	def 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)
238	type LcSpOp is Data:
239	  LcSpBswap{}
240	  LcSpKey{k: M.CmBlock}
241	  LcSpS{b: LcSpBox}
242	  LcSpLt{}
243	
244	def 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
258	def 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	
271	def 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	
278	def 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)
289	def 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
311	def sp.box(n: Nat) -> LcSpBox:
312	  sp.box.go(Nat.mod(n, 8n))
313	
314	def 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
328	def 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)
341	def 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	
350	def 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)
358	type LcSerpentKey is Data:
359	  LcSerpentKey{ops: List<&2, LcSpOp>}
360	
361	def 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
369	def sp.pad(+xs: List<&2, U32>, +n: Nat) -> List<&2, U32>:
370	  sp.pad.pick(Nat.is_lt(n, 32n), xs, n)
371	
372	def 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	
376	def 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	
381	def 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)
392	def 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	
396	def LcSerpent.encrypt(k: LcSerpentKey, b: M.CmBlock) -> M.CmBlock:
397	  match k:
398	    case LcSerpentKey{ops}:
399	      sp.run(ops, b)
400	
401	def LcSerpent.decrypt(k: LcSerpentKey, b: M.CmBlock) -> M.CmBlock:
402	  match k:
403	    case LcSerpentKey{ops}:
404	      sp.unrun(ops, b)