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).
21	import Base
22	import bend-osdev-bytes@0.1.0.0/bytes.bend as B
23	import ./legacy_ciphers.bend as L
24	
25	# The steps (internal), on the block as LcBlock64{y, z}
26	type 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)
34	def 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
38	def 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	
41	def 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
65	def 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	
88	def 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	
95	def 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	
104	def tea.delta() -> U32:
105	  2654435769
106	
107	# the four key words, little-endian (le True) or big-endian
108	def 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	
115	def 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
124	def 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
132	def 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)
141	type LcTeaKey is Data:
142	  LcTeaKey{ops: List<&2, LcTeaOp>}
143	
144	def 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)
155	def 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
161	def 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
165	def LcTea.key_be(o: B.Octets) -> Result<&2, &2, L.LcError, LcTeaKey>:
166	  LcTea.key_with(False{}, 32n, o)
167	
168	def LcTea.encrypt(k: LcTeaKey, b: L.LcBlock64) -> L.LcBlock64:
169	  match k:
170	    case LcTeaKey{ops}:
171	      tea.run(ops, b)
172	
173	def LcTea.decrypt(k: LcTeaKey, b: L.LcBlock64) -> L.LcBlock64:
174	  match k:
175	    case LcTeaKey{ops}:
176	      tea.unrun(ops, b)