camellia.bend
bend-osdev-camellia@0.1.0.0 · 358 lines · 0 definitions
1# Camellia (RFC 3713, A Description of the Camellia Encryption Algorithm,
2# 2004): a 128-bit block cipher with 128-, 192- or 256-bit keys, as a cipher
3# for the 128-bit modes (~LcCamelliaKey, ~LcCamellia.encrypt,
4# ~LcCamellia.decrypt).
5#
6# The state is the block as a CmBlock: D1 is its first two words, D2 its last
7# two. The key schedule turns the key into a list of steps, each one
8# invertible: the whitening XORs, the Feistel rounds (D2 ^= F(D1, k), then
9# D1 ^= F(D2, k)), the FL / FL^-1 layers, and the final swap of D1 and D2.
10# Encryption runs the steps first to last; decryption undoes them last to
11# first. That is the same function as RFC 3713's decryption with the
12# subkeys reversed, and it makes decrypt(encrypt(b)) == b provable for every
13# key and block: each step is undone whatever F is.
14import Base
15import bend-osdev-bytes@0.1.1.0/bytes.bend as B
16import bend-osdev-mode-core@0.1.0.0/mode_core.bend as M
17import bend-osdev-cipher-core@0.1.0.0/cipher_core.bend as L
18
19# SBOX1 (RFC 3713, 2.4.4); SBOX2, SBOX3 and SBOX4 are derived from it
20def cam.sbox1.list() -> List<&2, U32>:
21 [112, 130, 44, 236, 179, 39, 192, 229, 228, 133, 87, 53, 234, 12, 174, 65,
22 35, 239, 107, 147, 69, 25, 165, 33, 237, 14, 79, 78, 29, 101, 146, 189,
23 134, 184, 175, 143, 124, 235, 31, 206, 62, 48, 220, 95, 94, 197, 11, 26,
24 166, 225, 57, 202, 213, 71, 93, 61, 217, 1, 90, 214, 81, 86, 108, 77,
25 139, 13, 154, 102, 251, 204, 176, 45, 116, 18, 43, 32, 240, 177, 132, 153,
26 223, 76, 203, 194, 52, 126, 118, 5, 109, 183, 169, 49, 209, 23, 4, 215,
27 20, 88, 58, 97, 222, 27, 17, 28, 50, 15, 156, 22, 83, 24, 242, 34,
28 254, 68, 207, 178, 195, 181, 122, 145, 36, 8, 232, 168, 96, 252, 105, 80,
29 170, 208, 160, 125, 161, 137, 98, 151, 84, 91, 30, 149, 224, 255, 100, 210,
30 16, 196, 0, 72, 163, 247, 117, 219, 138, 3, 230, 218, 9, 63, 221, 148,
31 135, 92, 131, 2, 205, 74, 144, 51, 115, 103, 246, 243, 157, 127, 191, 226,
32 82, 155, 216, 38, 200, 55, 198, 59, 129, 150, 111, 75, 19, 190, 99, 46,
33 233, 121, 167, 140, 159, 110, 188, 142, 41, 245, 249, 182, 47, 253, 180, 89,
34 120, 152, 6, 106, 231, 70, 113, 186, 212, 37, 171, 66, 136, 162, 141, 250,
35 114, 7, 185, 85, 248, 238, 172, 10, 54, 73, 42, 104, 60, 56, 241, 164,
36 64, 40, 211, 123, 187, 201, 67, 193, 21, 227, 173, 244, 119, 199, 128, 158]
37
38# a byte rotated left by n
39def cam.rotl8(+x: U32, +n: Nat) -> U32:
40 U32.and(255, U32.or(U32.shln(x, n), U32.shrn(x, Nat.sub(8n, n))))
41
42# the entries of a table for x = i, i + 1, .., i + n - 1
43def cam.gen(~f: U32 -> U32, n: Nat, +i: U32) -> List<&2, U32>:
44 match n:
45 case 0n:
46 Nil{}
47 case 1n+p:
48 Con{f(i), cam.gen(~f, p, U32.add(i, 1))}
49
50def cam.s1.raw(+x: U32) -> U32:
51 L.lc.at(cam.sbox1.list(), U32.to_nat(x))
52
53def cam.s1() -> L.LcTab:
54 L.lc.tab(8n, cam.sbox1.list())
55
56# SBOX2[x] = SBOX1[x] <<< 1, SBOX3[x] = SBOX1[x] <<< 7, SBOX4[x] = SBOX1[x <<< 1]
57def cam.s2() -> L.LcTab:
58 L.lc.tab(8n, cam.gen(~(x => cam.rotl8(cam.s1.raw(x), 1n)), 256n, 0))
59
60def cam.s3() -> L.LcTab:
61 L.lc.tab(8n, cam.gen(~(x => cam.rotl8(cam.s1.raw(x), 7n)), 256n, 0))
62
63def cam.s4() -> L.LcTab:
64 L.lc.tab(8n, cam.gen(~(x => cam.s1.raw(cam.rotl8(x, 1n))), 256n, 0))
65
66# The four S-boxes as tables, built once per key (internal)
67type LcCamTabs is Data:
68 LcCamTabs{s1: L.LcTab, s2: L.LcTab, s3: L.LcTab, s4: L.LcTab}
69
70def cam.tables() -> LcCamTabs:
71 LcCamTabs{cam.s1(), cam.s2(), cam.s3(), cam.s4()}
72
73# The F-function (RFC 3713, 2.4.1), on 64-bit values as LcBlock64
74
75def cam.hi(x: L.LcBlock64) -> U32:
76 match x:
77 case L.LcBlock64{h, l}:
78 h
79
80def cam.lo(x: L.LcBlock64) -> U32:
81 match x:
82 case L.LcBlock64{h, l}:
83 l
84
85def cam.p(+t1: U32, +t2: U32, +t3: U32, +t4: U32, +t5: U32, +t6: U32, +t7: U32, +t8: U32) -> L.LcBlock64:
86 +y1 = U32.xor(U32.xor(U32.xor(t1, t3), U32.xor(t4, t6)), U32.xor(t7, t8))
87 +y2 = U32.xor(U32.xor(U32.xor(t1, t2), U32.xor(t4, t5)), U32.xor(t7, t8))
88 +y3 = U32.xor(U32.xor(U32.xor(t1, t2), U32.xor(t3, t5)), U32.xor(t6, t8))
89 +y4 = U32.xor(U32.xor(U32.xor(t2, t3), U32.xor(t4, t5)), U32.xor(t6, t7))
90 +y5 = U32.xor(U32.xor(U32.xor(t1, t2), t6), U32.xor(t7, t8))
91 +y6 = U32.xor(U32.xor(U32.xor(t2, t3), t5), U32.xor(t7, t8))
92 +y7 = U32.xor(U32.xor(U32.xor(t3, t4), t5), U32.xor(t6, t8))
93 +y8 = U32.xor(U32.xor(U32.xor(t1, t4), t5), U32.xor(t6, t7))
94 L.LcBlock64{L.lc.be(y1, y2, y3, y4), L.lc.be(y5, y6, y7, y8)}
95
96def cam.f(t: LcCamTabs, x: L.LcBlock64, k: L.LcBlock64) -> L.LcBlock64:
97 match t x k:
98 case LcCamTabs{+s1, +s2, +s3, +s4} L.LcBlock64{xh, xl} L.LcBlock64{kh, kl}:
99 +a = U32.xor(xh, kh)
100 +b = U32.xor(xl, kl)
101 cam.p(L.lc.tab.get(8n, s1, L.lc.byte(a, 3n)), L.lc.tab.get(8n, s2, L.lc.byte(a, 2n)), L.lc.tab.get(8n, s3, L.lc.byte(a, 1n)), L.lc.tab.get(8n, s4, L.lc.byte(a, 0n)), L.lc.tab.get(8n, s2, L.lc.byte(b, 3n)), L.lc.tab.get(8n, s3, L.lc.byte(b, 2n)), L.lc.tab.get(8n, s4, L.lc.byte(b, 1n)), L.lc.tab.get(8n, s1, L.lc.byte(b, 0n)))
102
103# FL and FL^-1 (RFC 3713, 2.4.2)
104def cam.fl(x: L.LcBlock64, k: L.LcBlock64) -> L.LcBlock64:
105 match x k:
106 case L.LcBlock64{+x1, x2} L.LcBlock64{k1, k2}:
107 +y2 = U32.xor(x2, L.lc.rotl(U32.and(x1, k1), 1n))
108 L.LcBlock64{U32.xor(x1, U32.or(y2, k2)), y2}
109
110def cam.flinv(y: L.LcBlock64, k: L.LcBlock64) -> L.LcBlock64:
111 match y k:
112 case L.LcBlock64{y1, +y2} L.LcBlock64{k1, k2}:
113 +x1 = U32.xor(y1, U32.or(y2, k2))
114 L.LcBlock64{x1, U32.xor(y2, L.lc.rotl(U32.and(x1, k1), 1n))}
115
116# D1 ^= a, D2 ^= b
117def cam.white(a: L.LcBlock64, b: L.LcBlock64, s: M.CmBlock) -> M.CmBlock:
118 match a b:
119 case L.LcBlock64{a0, a1} L.LcBlock64{b0, b1}:
120 M.CmBlock.xor(s, M.CmBlock{a0, a1, b0, b1})
121
122# The steps of the cipher (internal)
123type LcCamOp is Data:
124 LcCamWhite{a: L.LcBlock64, b: L.LcBlock64}
125 LcCamF1{t: LcCamTabs, k: L.LcBlock64}
126 LcCamF2{t: LcCamTabs, k: L.LcBlock64}
127 LcCamFl{a: L.LcBlock64, b: L.LcBlock64}
128 LcCamSwap{}
129
130def cam.op(o: LcCamOp, s: M.CmBlock) -> M.CmBlock:
131 match o:
132 case LcCamWhite{a, b}:
133 cam.white(a, b, s)
134 case LcCamF1{t, k}:
135 match s:
136 case M.CmBlock{+s0, +s1, s2, s3}:
137 +f = cam.f(t, L.LcBlock64{s0, s1}, k)
138 M.CmBlock{s0, s1, U32.xor(s2, cam.hi(f)), U32.xor(s3, cam.lo(f))}
139 case LcCamF2{t, k}:
140 match s:
141 case M.CmBlock{s0, s1, +s2, +s3}:
142 +f = cam.f(t, L.LcBlock64{s2, s3}, k)
143 M.CmBlock{U32.xor(s0, cam.hi(f)), U32.xor(s1, cam.lo(f)), s2, s3}
144 case LcCamFl{a, b}:
145 match s:
146 case M.CmBlock{s0, s1, s2, s3}:
147 +d1 = cam.fl(L.LcBlock64{s0, s1}, a)
148 +d2 = cam.flinv(L.LcBlock64{s2, s3}, b)
149 M.CmBlock{cam.hi(d1), cam.lo(d1), cam.hi(d2), cam.lo(d2)}
150 case LcCamSwap{}:
151 match s:
152 case M.CmBlock{s0, s1, s2, s3}:
153 M.CmBlock{s2, s3, s0, s1}
154
155# the step undone
156def cam.unop(o: LcCamOp, s: M.CmBlock) -> M.CmBlock:
157 match o:
158 case LcCamWhite{a, b}:
159 cam.white(a, b, s)
160 case LcCamF1{t, k}:
161 match s:
162 case M.CmBlock{+s0, +s1, s2, s3}:
163 +f = cam.f(t, L.LcBlock64{s0, s1}, k)
164 M.CmBlock{s0, s1, U32.xor(s2, cam.hi(f)), U32.xor(s3, cam.lo(f))}
165 case LcCamF2{t, k}:
166 match s:
167 case M.CmBlock{s0, s1, +s2, +s3}:
168 +f = cam.f(t, L.LcBlock64{s2, s3}, k)
169 M.CmBlock{U32.xor(s0, cam.hi(f)), U32.xor(s1, cam.lo(f)), s2, s3}
170 case LcCamFl{a, b}:
171 match s:
172 case M.CmBlock{s0, s1, s2, s3}:
173 +d1 = cam.flinv(L.LcBlock64{s0, s1}, a)
174 +d2 = cam.fl(L.LcBlock64{s2, s3}, b)
175 M.CmBlock{cam.hi(d1), cam.lo(d1), cam.hi(d2), cam.lo(d2)}
176 case LcCamSwap{}:
177 match s:
178 case M.CmBlock{s0, s1, s2, s3}:
179 M.CmBlock{s2, s3, s0, s1}
180
181def cam.run(os: List<&2, LcCamOp>, s: M.CmBlock) -> M.CmBlock:
182 match os:
183 case Nil{}:
184 s
185 case Con{o, t}:
186 cam.run(t, cam.op(o, s))
187
188def cam.unrun(os: List<&2, LcCamOp>, s: M.CmBlock) -> M.CmBlock:
189 match os:
190 case Nil{}:
191 s
192 case Con{o, t}:
193 cam.unop(o, cam.unrun(t, s))
194
195# The key schedule (RFC 3713, 2.2), on 128-bit values as CmBlocks
196
197def cam.xor128(a: M.CmBlock, b: M.CmBlock) -> M.CmBlock:
198 M.CmBlock.xor(a, b)
199
200# q rotated left by 32 bits, and by r bits (r = 0 to 31)
201def cam.rotw(q: M.CmBlock) -> M.CmBlock:
202 match q:
203 case M.CmBlock{a, b, c, d}:
204 M.CmBlock{b, c, d, a}
205
206def cam.rotb(q: M.CmBlock, +r: Nat) -> M.CmBlock:
207 match q:
208 case M.CmBlock{+a, +b, +c, +d}:
209 +s = Nat.sub(32n, r)
210 M.CmBlock{U32.or(U32.shln(a, r), U32.shrn(b, s)), U32.or(U32.shln(b, r), U32.shrn(c, s)), U32.or(U32.shln(c, r), U32.shrn(d, s)), U32.or(U32.shln(d, r), U32.shrn(a, s))}
211
212def cam.rotws(n: Nat, q: M.CmBlock) -> M.CmBlock:
213 match n:
214 case 0n:
215 q
216 case 1n+p:
217 cam.rotws(p, cam.rotw(q))
218
219# q <<< n
220def cam.rol(q: M.CmBlock, +n: Nat) -> M.CmBlock:
221 cam.rotb(cam.rotws(Nat.div(n, 32n), q), Nat.mod(n, 32n))
222
223def cam.top(q: M.CmBlock) -> L.LcBlock64:
224 match q:
225 case M.CmBlock{a, b, c, d}:
226 L.LcBlock64{a, b}
227
228def cam.bot(q: M.CmBlock) -> L.LcBlock64:
229 match q:
230 case M.CmBlock{a, b, c, d}:
231 L.LcBlock64{c, d}
232
233# the high and the low 64 bits of q <<< n
234def cam.h(q: M.CmBlock, +n: Nat) -> L.LcBlock64:
235 cam.top(cam.rol(q, n))
236
237def cam.l(q: M.CmBlock, +n: Nat) -> L.LcBlock64:
238 cam.bot(cam.rol(q, n))
239
240def cam.sigma(n: Nat) -> L.LcBlock64:
241 match n:
242 case 0n:
243 L.LcBlock64{2694735487, 1003262091}
244 case 1n:
245 L.LcBlock64{3061508184, 1286239154}
246 case 2n:
247 L.LcBlock64{3337565999, 3914302142}
248 case 3n:
249 L.LcBlock64{1426019237, 4057165596}
250 case 4n:
251 L.LcBlock64{283453434, 3731369245}
252 case _:
253 L.LcBlock64{2958461122, 3018244605}
254
255# D2 ^= F(D1, Sigma_i); D1 ^= F(D2, Sigma_(i+1)), on the 128-bit value D1:D2
256def cam.mix(+t: LcCamTabs, q: M.CmBlock, +i: Nat) -> M.CmBlock:
257 cam.op(LcCamF2{t, cam.sigma(Nat.add(i, 1n))}, cam.op(LcCamF1{t, cam.sigma(i)}, q))
258
259# KA from KL and KR
260def cam.ka(+t: LcCamTabs, +kl: M.CmBlock, kr: M.CmBlock) -> M.CmBlock:
261 cam.mix(t, cam.xor128(kl, cam.mix(t, cam.xor128(kl, kr), 0n)), 2n)
262
263# KB from KA and KR
264def cam.kb(t: LcCamTabs, ka: M.CmBlock, kr: M.CmBlock) -> M.CmBlock:
265 cam.mix(t, cam.xor128(ka, kr), 4n)
266
267# the steps for a 128-bit key
268def cam.ops128(+t: LcCamTabs, +kl: M.CmBlock, +ka: M.CmBlock) -> List<&2, LcCamOp>:
269 [LcCamWhite{cam.h(kl, 0n), cam.l(kl, 0n)},
270 LcCamF1{t, cam.h(ka, 0n)}, LcCamF2{t, cam.l(ka, 0n)}, LcCamF1{t, cam.h(kl, 15n)}, LcCamF2{t, cam.l(kl, 15n)}, LcCamF1{t, cam.h(ka, 15n)}, LcCamF2{t, cam.l(ka, 15n)},
271 LcCamFl{cam.h(ka, 30n), cam.l(ka, 30n)},
272 LcCamF1{t, cam.h(kl, 45n)}, LcCamF2{t, cam.l(kl, 45n)}, LcCamF1{t, cam.h(ka, 45n)}, LcCamF2{t, cam.l(kl, 60n)}, LcCamF1{t, cam.h(ka, 60n)}, LcCamF2{t, cam.l(ka, 60n)},
273 LcCamFl{cam.h(kl, 77n), cam.l(kl, 77n)},
274 LcCamF1{t, cam.h(kl, 94n)}, LcCamF2{t, cam.l(kl, 94n)}, LcCamF1{t, cam.h(ka, 94n)}, LcCamF2{t, cam.l(ka, 94n)}, LcCamF1{t, cam.h(kl, 111n)}, LcCamF2{t, cam.l(kl, 111n)},
275 LcCamSwap{}, LcCamWhite{cam.h(ka, 111n), cam.l(ka, 111n)}]
276
277# the steps for a 192- or 256-bit key
278def cam.ops256(+t: LcCamTabs, +kl: M.CmBlock, +kr: M.CmBlock, +ka: M.CmBlock, +kb: M.CmBlock) -> List<&2, LcCamOp>:
279 [LcCamWhite{cam.h(kl, 0n), cam.l(kl, 0n)},
280 LcCamF1{t, cam.h(kb, 0n)}, LcCamF2{t, cam.l(kb, 0n)}, LcCamF1{t, cam.h(kr, 15n)}, LcCamF2{t, cam.l(kr, 15n)}, LcCamF1{t, cam.h(ka, 15n)}, LcCamF2{t, cam.l(ka, 15n)},
281 LcCamFl{cam.h(kr, 30n), cam.l(kr, 30n)},
282 LcCamF1{t, cam.h(kb, 30n)}, LcCamF2{t, cam.l(kb, 30n)}, LcCamF1{t, cam.h(kl, 45n)}, LcCamF2{t, cam.l(kl, 45n)}, LcCamF1{t, cam.h(ka, 45n)}, LcCamF2{t, cam.l(ka, 45n)},
283 LcCamFl{cam.h(kl, 60n), cam.l(kl, 60n)},
284 LcCamF1{t, cam.h(kr, 60n)}, LcCamF2{t, cam.l(kr, 60n)}, LcCamF1{t, cam.h(kb, 60n)}, LcCamF2{t, cam.l(kb, 60n)}, LcCamF1{t, cam.h(kl, 77n)}, LcCamF2{t, cam.l(kl, 77n)},
285 LcCamFl{cam.h(ka, 77n), cam.l(ka, 77n)},
286 LcCamF1{t, cam.h(kr, 94n)}, LcCamF2{t, cam.l(kr, 94n)}, LcCamF1{t, cam.h(ka, 94n)}, LcCamF2{t, cam.l(ka, 94n)}, LcCamF1{t, cam.h(kl, 111n)}, LcCamF2{t, cam.l(kl, 111n)},
287 LcCamSwap{}, LcCamWhite{cam.h(kb, 111n), cam.l(kb, 111n)}]
288
289# A Camellia key: the steps of the cipher (opaque; built by LcCamellia.key)
290type LcCamelliaKey is Data:
291 LcCamelliaKey{ops: List<&2, LcCamOp>}
292
293# word i (big-endian) of the key bytes xs
294def cam.w(+xs: List<&2, U32>, +i: Nat) -> U32:
295 +j = Nat.mul(4n, i)
296 L.lc.be(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)))
297
298def cam.key128(+xs: List<&2, U32>) -> LcCamelliaKey:
299 +kl = {M.CmBlock{cam.w(xs, 0n), cam.w(xs, 1n), cam.w(xs, 2n), cam.w(xs, 3n)} : M.CmBlock}
300 +t = cam.tables()
301 LcCamelliaKey{cam.ops128(t, kl, cam.ka(t, kl, M.CmBlock.zero()))}
302
303def cam.key256.go(+kl: M.CmBlock, +kr: M.CmBlock) -> LcCamelliaKey:
304 +t = cam.tables()
305 +ka = cam.ka(t, kl, kr)
306 LcCamelliaKey{cam.ops256(t, kl, kr, ka, cam.kb(t, ka, kr))}
307
308# a 192-bit key's KR is its last 64 bits, then their complement
309def cam.key192(+xs: List<&2, U32>) -> LcCamelliaKey:
310 +r0 = cam.w(xs, 4n)
311 +r1 = cam.w(xs, 5n)
312 cam.key256.go(M.CmBlock{cam.w(xs, 0n), cam.w(xs, 1n), cam.w(xs, 2n), cam.w(xs, 3n)}, M.CmBlock{r0, r1, U32.not(r0), U32.not(r1)})
313
314def cam.key256(+xs: List<&2, U32>) -> LcCamelliaKey:
315 cam.key256.go(M.CmBlock{cam.w(xs, 0n), cam.w(xs, 1n), cam.w(xs, 2n), cam.w(xs, 3n)}, M.CmBlock{cam.w(xs, 4n), cam.w(xs, 5n), cam.w(xs, 6n), cam.w(xs, 7n)})
316
317# the key for 16, 24 or 32 bytes, if n says so
318def cam.key.pick(n16: Bool, n24: Bool, n32: Bool, +xs: List<&2, U32>) -> Result<&2, &2, L.LcError, LcCamelliaKey>:
319 match n16 n24 n32:
320 case True{} _ _:
321 Done{cam.key128(xs)}
322 case False{} True{} _:
323 Done{cam.key192(xs)}
324 case False{} False{} True{}:
325 Done{cam.key256(xs)}
326 case False{} False{} False{}:
327 Fail{L.LcBadKeyLength{B.len(xs)}}
328
329# The cipher
330
331# a 16-, 24- or 32-byte key (Camellia-128, -192, -256, by its length)
332def LcCamellia.key(o: B.Octets) -> Result<&2, &2, L.LcError, LcCamelliaKey>:
333 +xs = B.Octets.to_list(o)
334 +n = B.len(xs)
335 cam.key.pick(Nat.is_eq(n, 16n), Nat.is_eq(n, 24n), Nat.is_eq(n, 32n), xs)
336
337# a key of exactly this size
338def LcCamellia.key128(o: B.Octets) -> Result<&2, &2, L.LcError, LcCamelliaKey>:
339 +xs = B.Octets.to_list(o)
340 cam.key.pick(Nat.is_eq(B.len(xs), 16n), False{}, False{}, xs)
341
342def LcCamellia.key192(o: B.Octets) -> Result<&2, &2, L.LcError, LcCamelliaKey>:
343 +xs = B.Octets.to_list(o)
344 cam.key.pick(False{}, Nat.is_eq(B.len(xs), 24n), False{}, xs)
345
346def LcCamellia.key256(o: B.Octets) -> Result<&2, &2, L.LcError, LcCamelliaKey>:
347 +xs = B.Octets.to_list(o)
348 cam.key.pick(False{}, False{}, Nat.is_eq(B.len(xs), 32n), xs)
349
350def LcCamellia.encrypt(k: LcCamelliaKey, b: M.CmBlock) -> M.CmBlock:
351 match k:
352 case LcCamelliaKey{ops}:
353 cam.run(ops, b)
354
355def LcCamellia.decrypt(k: LcCamelliaKey, b: M.CmBlock) -> M.CmBlock:
356 match k:
357 case LcCamelliaKey{ops}:
358 cam.unrun(ops, b)