camellia.bend

bend-osdev-legacy-ciphers@0.1.0.0 · 358 lines · 50 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 cipher-modes' 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.0.0/bytes.bend as B
16import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M
17import bend-osdev-legacy-ciphers@0.1.0.0/legacy_ciphers.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)