tea.bend

bend-osdev-legacy-ciphers@0.1.0.0 · 176 lines · 19 definitions

1# TEA (D. Wheeler, R. Needham, "TEA, a Tiny Encryption Algorithm", Fast
2# Software Encryption 1994): a 64-bit block cipher with a 128-bit key. This
3# file also holds the steps TEA and XTEA (xtea.bend) share.
4#
5# The block is two 32-bit words y, z and the key four words k0 .. k3. Each
6# cycle adds delta (0x9E3779B9) to sum, then
7#   y += ((z << 4) + k0) xor (z + sum) xor ((z >> 5) + k1)
8#   z += ((y << 4) + k2) xor (y + sum) xor ((y >> 5) + k3)
9# The key schedule turns the key into a list of such steps (each adds a
10# function of one half to the other); decryption undoes them last to first,
11# each by subtracting what it added: the same function as the paper's decode
12# routine, and decrypt(encrypt(b)) == b is provable for every key and block
13# (an addition is undone by a subtraction, for every word).
14#
15# The paper fixes 32-bit words and leaves their byte order open ("same
16# endian coding or decoding"). The order is a parameter: little-endian words
17# (the Linux kernel's "tea") are LcTea.key, big-endian ones LcTea.key_be; the
18# number of cycles (32 recommended) is a parameter of LcTea.key_with. A
19# little-endian key reverses the bytes of each block word on the way in and
20# out (a step undone by itself).
21import Base
22import bend-osdev-bytes@0.1.0.0/bytes.bend as B
23import bend-osdev-legacy-ciphers@0.1.0.0/legacy_ciphers.bend as L
24
25# The steps (internal), on the block as LcBlock64{y, z}
26type LcTeaOp is Data:
27  LcTeaY{s: U32, a: U32, b: U32}
28  LcTeaZ{s: U32, a: U32, b: U32}
29  LcXteaY{c: U32}
30  LcXteaZ{c: U32}
31  LcTeaBswap{}
32
33# TEA's function of one half: ((x << 4) + a) xor (x + s) xor ((x >> 5) + b)
34def tea.g(+x: U32, s: U32, a: U32, b: U32) -> U32:
35  U32.xor(U32.xor(U32.add(U32.shln(x, 4n), a), U32.add(x, s)), U32.add(U32.shrn(x, 5n), b))
36
37# XTEA's: (((x << 4) xor (x >> 5)) + x) xor c
38def xtea.g(+x: U32, c: U32) -> U32:
39  U32.xor(U32.add(U32.xor(U32.shln(x, 4n), U32.shrn(x, 5n)), x), c)
40
41def tea.op(o: LcTeaOp, b: L.LcBlock64) -> L.LcBlock64:
42  match o:
43    case LcTeaY{s, ka, kb}:
44      match b:
45        case L.LcBlock64{y, +z}:
46          L.LcBlock64{U32.add(y, tea.g(z, s, ka, kb)), z}
47    case LcTeaZ{s, ka, kb}:
48      match b:
49        case L.LcBlock64{+y, z}:
50          L.LcBlock64{y, U32.add(z, tea.g(y, s, ka, kb))}
51    case LcXteaY{c}:
52      match b:
53        case L.LcBlock64{y, +z}:
54          L.LcBlock64{U32.add(y, xtea.g(z, c)), z}
55    case LcXteaZ{c}:
56      match b:
57        case L.LcBlock64{+y, z}:
58          L.LcBlock64{y, U32.add(z, xtea.g(y, c))}
59    case LcTeaBswap{}:
60      match b:
61        case L.LcBlock64{y, z}:
62          L.LcBlock64{L.lc.bswap.bits(y), L.lc.bswap.bits(z)}
63
64# the step undone
65def tea.unop(o: LcTeaOp, b: L.LcBlock64) -> L.LcBlock64:
66  match o:
67    case LcTeaY{s, ka, kb}:
68      match b:
69        case L.LcBlock64{y, +z}:
70          L.LcBlock64{U32.sub(y, tea.g(z, s, ka, kb)), z}
71    case LcTeaZ{s, ka, kb}:
72      match b:
73        case L.LcBlock64{+y, z}:
74          L.LcBlock64{y, U32.sub(z, tea.g(y, s, ka, kb))}
75    case LcXteaY{c}:
76      match b:
77        case L.LcBlock64{y, +z}:
78          L.LcBlock64{U32.sub(y, xtea.g(z, c)), z}
79    case LcXteaZ{c}:
80      match b:
81        case L.LcBlock64{+y, z}:
82          L.LcBlock64{y, U32.sub(z, xtea.g(y, c))}
83    case LcTeaBswap{}:
84      match b:
85        case L.LcBlock64{y, z}:
86          L.LcBlock64{L.lc.bswap.bits(y), L.lc.bswap.bits(z)}
87
88def tea.run(os: List<&2, LcTeaOp>, b: L.LcBlock64) -> L.LcBlock64:
89  match os:
90    case Nil{}:
91      b
92    case Con{o, t}:
93      tea.run(t, tea.op(o, b))
94
95def tea.unrun(os: List<&2, LcTeaOp>, b: L.LcBlock64) -> L.LcBlock64:
96  match os:
97    case Nil{}:
98      b
99    case Con{o, t}:
100      tea.unop(o, tea.unrun(t, b))
101
102# The key and its byte order (shared with XTEA)
103
104def tea.delta() -> U32:
105  2654435769
106
107# the four key words, little-endian (le True) or big-endian
108def tea.word(le: Bool, +xs: List<&2, U32>, +i: Nat) -> U32:
109  match le:
110    case True{}:
111      L.lc.le(L.lc.at(xs, i), L.lc.at(xs, Nat.add(i, 1n)), L.lc.at(xs, Nat.add(i, 2n)), L.lc.at(xs, Nat.add(i, 3n)))
112    case False{}:
113      L.lc.be(L.lc.at(xs, i), L.lc.at(xs, Nat.add(i, 1n)), L.lc.at(xs, Nat.add(i, 2n)), L.lc.at(xs, Nat.add(i, 3n)))
114
115def tea.append(xs: List<&2, LcTeaOp>, ys: List<&2, LcTeaOp>) -> List<&2, LcTeaOp>:
116  match xs:
117    case Nil{}:
118      ys
119    case Con{h, t}:
120      Con{h, tea.append(t, ys)}
121
122# the steps in the chosen byte order: little-endian words are byte-swapped
123# on the way in and out
124def tea.order(le: Bool, os: List<&2, LcTeaOp>) -> List<&2, LcTeaOp>:
125  match le:
126    case True{}:
127      Con{LcTeaBswap{}, tea.append(os, [LcTeaBswap{}])}
128    case False{}:
129      os
130
131# TEA's steps for n more cycles, sum the value before the next
132def tea.cycles(n: Nat, +s: U32, +k0: U32, +k1: U32, +k2: U32, +k3: U32) -> List<&2, LcTeaOp>:
133  match n:
134    case 0n:
135      Nil{}
136    case 1n+p:
137      +s1 = U32.add(s, tea.delta())
138      Con{LcTeaY{s1, k0, k1}, Con{LcTeaZ{s1, k2, k3}, tea.cycles(p, s1, k0, k1, k2, k3)}}
139
140# A TEA key: the steps of the cipher (opaque; built by LcTea.key)
141type LcTeaKey is Data:
142  LcTeaKey{ops: List<&2, LcTeaOp>}
143
144def tea.key.pick(ok: Bool, +le: Bool, n: Nat, +xs: List<&2, U32>) -> Result<&2, &2, L.LcError, LcTeaKey>:
145  match ok:
146    case True{}:
147      Done{LcTeaKey{tea.order(le, tea.cycles(n, 0, tea.word(le, xs, 0n), tea.word(le, xs, 4n), tea.word(le, xs, 8n), tea.word(le, xs, 12n)))}}
148    case False{}:
149      Fail{L.LcBadKeyLength{B.len(xs)}}
150
151# The cipher
152
153# a 16-byte key, words in the order le picks (True: little-endian), and n
154# cycles (32 recommended)
155def LcTea.key_with(le: Bool, n: Nat, o: B.Octets) -> Result<&2, &2, L.LcError, LcTeaKey>:
156  +xs = B.Octets.to_list(o)
157  tea.key.pick(Nat.is_eq(B.len(xs), 16n), le, n, xs)
158
159# the named default: little-endian words (the Linux kernel's "tea"), 32
160# cycles
161def LcTea.key(o: B.Octets) -> Result<&2, &2, L.LcError, LcTeaKey>:
162  LcTea.key_with(True{}, 32n, o)
163
164# big-endian words, 32 cycles
165def LcTea.key_be(o: B.Octets) -> Result<&2, &2, L.LcError, LcTeaKey>:
166  LcTea.key_with(False{}, 32n, o)
167
168def LcTea.encrypt(k: LcTeaKey, b: L.LcBlock64) -> L.LcBlock64:
169  match k:
170    case LcTeaKey{ops}:
171      tea.run(ops, b)
172
173def LcTea.decrypt(k: LcTeaKey, b: L.LcBlock64) -> L.LcBlock64:
174  match k:
175    case LcTeaKey{ops}:
176      tea.unrun(ops, b)