tdes.bend

bend-osdev-legacy-ciphers@0.1.0.0 · 62 lines · 11 definitions

1# Triple DES, TDEA (NIST SP 800-67 Rev. 2, 2017): three DES keys, encryption
2# E_K3(D_K2(E_K1(b))) and decryption D_K1(E_K2(D_K3(c))), with DES from
3# des.bend. SP 800-67 Rev. 2 allows keying option 1 only (three distinct
4# keys, 24 bytes); keying option 2 (K3 = K1, 16 bytes) is here for reading
5# old data, as the kernel's des3_ede accepts it too. SP 800-67 also requires
6# the keys to differ; that is not checked here.
7import Base
8import bend-osdev-bytes@0.1.0.0/bytes.bend as B
9import bend-osdev-legacy-ciphers@0.1.0.0/legacy_ciphers.bend as L
10import bend-osdev-legacy-ciphers@0.1.0.0/des.bend as D
11
12# A TDEA key bundle: three DES keys (opaque)
13type LcTdesKey is Data:
14  LcTdesKey{k1: D.LcDesKey, k2: D.LcDesKey, k3: D.LcDesKey}
15
16# the bundle of three DES keys, in the order K1, K2, K3
17def LcTdes.of_des(k1: D.LcDesKey, k2: D.LcDesKey, k3: D.LcDesKey) -> LcTdesKey:
18  LcTdesKey{k1, k2, k3}
19
20def tdes.des_key(+xs: List<&2, U32>) -> D.LcDesKey:
21  D.des.key_of(L.lc.be(L.lc.at(xs, 0n), L.lc.at(xs, 1n), L.lc.at(xs, 2n), L.lc.at(xs, 3n)), L.lc.be(L.lc.at(xs, 4n), L.lc.at(xs, 5n), L.lc.at(xs, 6n), L.lc.at(xs, 7n)))
22
23def tdes.key3(+xs: List<&2, U32>) -> LcTdesKey:
24  LcTdesKey{tdes.des_key(xs), tdes.des_key(B.drop(8n, xs)), tdes.des_key(B.drop(16n, xs))}
25
26def tdes.key2(+xs: List<&2, U32>) -> LcTdesKey:
27  LcTdesKey{tdes.des_key(xs), tdes.des_key(B.drop(8n, xs)), tdes.des_key(xs)}
28
29def tdes.key.pick(three: Bool, two: Bool, +xs: List<&2, U32>) -> Result<&2, &2, L.LcError, LcTdesKey>:
30  match three two:
31    case True{} _:
32      Done{tdes.key3(xs)}
33    case False{} True{}:
34      Done{tdes.key2(xs)}
35    case False{} False{}:
36      Fail{L.LcBadKeyLength{B.len(xs)}}
37
38# keying option 1: K1, K2, K3 as 24 bytes
39def LcTdes.key3(o: B.Octets) -> Result<&2, &2, L.LcError, LcTdesKey>:
40  +xs = B.Octets.to_list(o)
41  tdes.key.pick(Nat.is_eq(B.len(xs), 24n), False{}, xs)
42
43# keying option 2: K1, K2 as 16 bytes, and K3 = K1
44def LcTdes.key2(o: B.Octets) -> Result<&2, &2, L.LcError, LcTdesKey>:
45  +xs = B.Octets.to_list(o)
46  tdes.key.pick(False{}, Nat.is_eq(B.len(xs), 16n), xs)
47
48# option 1 for 24 bytes, option 2 for 16
49def LcTdes.key(o: B.Octets) -> Result<&2, &2, L.LcError, LcTdesKey>:
50  +xs = B.Octets.to_list(o)
51  +n = B.len(xs)
52  tdes.key.pick(Nat.is_eq(n, 24n), Nat.is_eq(n, 16n), xs)
53
54def LcTdes.encrypt(k: LcTdesKey, b: L.LcBlock64) -> L.LcBlock64:
55  match k:
56    case LcTdesKey{k1, k2, k3}:
57      D.LcDes.encrypt(k3, D.LcDes.decrypt(k2, D.LcDes.encrypt(k1, b)))
58
59def LcTdes.decrypt(k: LcTdesKey, b: L.LcBlock64) -> L.LcBlock64:
60  match k:
61    case LcTdesKey{k1, k2, k3}:
62      D.LcDes.decrypt(k1, D.LcDes.encrypt(k2, D.LcDes.decrypt(k3, b)))