xtea.bend

bend-osdev-legacy-ciphers@0.1.0.0 · 69 lines · 9 definitions

1# XTEA (R. Needham, D. Wheeler, "Tea extensions", 1997, the routine
2# "tean"): TEA with a different key schedule, a 64-bit block cipher with a
3# 128-bit key. Each cycle is
4#   y += (((z << 4) xor (z >> 5)) + z) xor (sum + k[sum & 3])
5#   sum += delta
6#   z += (((y << 4) xor (y >> 5)) + y) xor (sum + k[(sum >> 11) & 3])
7# The key schedule computes each step's sum + k[..] once, as a step of
8# tea.bend's (LcXteaY, LcXteaZ); decryption undoes the steps last to first,
9# the paper's decoding, so decrypt(encrypt(b)) == b is provable for every key
10# and block, as for TEA.
11#
12# The byte order of the words is a parameter, as for TEA: little-endian
13# (the Linux kernel's "xtea") is LcXtea.key, big-endian LcXtea.key_be, and
14# LcXtea.key_with takes the order and the number of cycles (32 recommended).
15import Base
16import bend-osdev-bytes@0.1.0.0/bytes.bend as B
17import bend-osdev-legacy-ciphers@0.1.0.0/legacy_ciphers.bend as L
18import bend-osdev-legacy-ciphers@0.1.0.0/tea.bend as T
19
20# key word i & 3 of k0 .. k3
21def xtea.kw(+i: U32, +k0: U32, +k1: U32, +k2: U32, +k3: U32) -> U32:
22  L.lc.at([k0, k1, k2, k3], U32.to_nat(U32.and(3, i)))
23
24# XTEA's steps for n more cycles from sum s
25def xtea.cycles(n: Nat, +s: U32, +k0: U32, +k1: U32, +k2: U32, +k3: U32) -> List<&2, T.LcTeaOp>:
26  match n:
27    case 0n:
28      Nil{}
29    case 1n+p:
30      +s1 = U32.add(s, T.tea.delta())
31      Con{T.LcXteaY{U32.add(s, xtea.kw(s, k0, k1, k2, k3))}, Con{T.LcXteaZ{U32.add(s1, xtea.kw(U32.shrn(s1, 11n), k0, k1, k2, k3))}, xtea.cycles(p, s1, k0, k1, k2, k3)}}
32
33# An XTEA key: the steps of the cipher (opaque; built by LcXtea.key)
34type LcXteaKey is Data:
35  LcXteaKey{ops: List<&2, T.LcTeaOp>}
36
37def xtea.key.pick(ok: Bool, +le: Bool, n: Nat, +xs: List<&2, U32>) -> Result<&2, &2, L.LcError, LcXteaKey>:
38  match ok:
39    case True{}:
40      Done{LcXteaKey{T.tea.order(le, xtea.cycles(n, 0, T.tea.word(le, xs, 0n), T.tea.word(le, xs, 4n), T.tea.word(le, xs, 8n), T.tea.word(le, xs, 12n)))}}
41    case False{}:
42      Fail{L.LcBadKeyLength{B.len(xs)}}
43
44# The cipher
45
46# a 16-byte key, words in the order le picks (True: little-endian), and n
47# cycles (32 recommended)
48def LcXtea.key_with(le: Bool, n: Nat, o: B.Octets) -> Result<&2, &2, L.LcError, LcXteaKey>:
49  +xs = B.Octets.to_list(o)
50  xtea.key.pick(Nat.is_eq(B.len(xs), 16n), le, n, xs)
51
52# the named default: little-endian words (the Linux kernel's "xtea"), 32
53# cycles
54def LcXtea.key(o: B.Octets) -> Result<&2, &2, L.LcError, LcXteaKey>:
55  LcXtea.key_with(True{}, 32n, o)
56
57# big-endian words, 32 cycles
58def LcXtea.key_be(o: B.Octets) -> Result<&2, &2, L.LcError, LcXteaKey>:
59  LcXtea.key_with(False{}, 32n, o)
60
61def LcXtea.encrypt(k: LcXteaKey, b: L.LcBlock64) -> L.LcBlock64:
62  match k:
63    case LcXteaKey{ops}:
64      T.tea.run(ops, b)
65
66def LcXtea.decrypt(k: LcXteaKey, b: L.LcBlock64) -> L.LcBlock64:
67  match k:
68    case LcXteaKey{ops}:
69      T.tea.unrun(ops, b)