1(*---------------------------------------------------------------------------*)
2(* TEA, a Tiny Encryption Algorithm                                          *)
3(* TEA routine is a Feistel type routine although addition and subtraction   *)
4(* are used as the reversible operators rather than XOR. The routine relies  *)
5(* on the alternate use of XOR and ADD to provide nonlinearity. A dual shift *)
6(* causes all bits of the key and data to be mixed repeatedly.The number of  *)
7(* rounds before a single bit change of the data or key has spread very      *)
8(* close to 32 is at most six, so that sixteen cycles may suffice and the    *)
9(* authors suggest 32. The key is set at 128 bits.                           *)
10(* See http://www.ftp.cl.cam.ac.uk/ftp/papers/djw-rmn/djw-rmn-tea.html       *)
11(* for more information.                                                     *)
12(*---------------------------------------------------------------------------*)
13
14Lib.with_flag (quietdec,true) use "prelim";
15
16quietdec := true;
17open wordsTheory wordsLib pairTheory pairLib;
18quietdec := false;
19
20val KMATCH_MP_TAC =
21  MATCH_MP_TAC o
22  Ho_Rewrite.REWRITE_RULE [AND_IMP_INTRO,
23           METIS_PROVE [] ``(a ==> !x. b x) = !x. a ==> b x``];
24
25val WORD_PRED_EXISTS = Q.prove
26(`!w:'a word. ~(w = 0w) ==> ?u. w = u + 1w`,
27  RW_TAC std_ss [] THEN
28  Q.EXISTS_TAC `w - 1w` THEN
29  RW_TAC std_ss [WORD_SUB_ADD,WORD_ADD_SUB,WORD_MULT_CLAUSES]);
30
31
32(*---------------------------------------------------------------------------*)
33(* Cipher types                                                              *)
34(*---------------------------------------------------------------------------*)
35
36val _ = type_abbrev("block", ``:word32 # word32``);
37val _ = type_abbrev("key",   ``:word32 # word32 # word32 # word32``);
38val _ = type_abbrev("state", ``:block # key # word32``);
39
40val DELTA_def = Define `DELTA = 0x9e3779b9w:word32`;
41
42val ShiftXor_def =
43 Define
44   `ShiftXor (x:word32,s,k0,k1) =
45          ((x << 4) + k0) ?? (x + s) ?? ((x >> 5) + k1)`;
46
47(* --------------------------------------------------------------------------*)
48(*      One round forward computation                                        *)
49(* --------------------------------------------------------------------------*)
50
51val Round_def =
52 Define
53   `Round ((y,z),(k0,k1,k2,k3),s):state =
54      let s' = s + DELTA in let
55          y' = y + ShiftXor(z, s', k0, k1)
56      in
57        ((y', z + ShiftXor(y', s', k2, k3)),
58         (k0,k1,k2,k3), s')`;
59
60(*---------------------------------------------------------------------------*)
61(* Arbitrary number of cipher rounds                                         *)
62(*---------------------------------------------------------------------------*)
63
64val Rounds_def =
65 Define
66   `Rounds (n:word32,s:state) =
67      if n=0w then s else Rounds (n-1w, Round s)`;
68
69val Rounds_ind = fetch "-" "Rounds_ind";
70
71(*---------------------------------------------------------------------------*)
72(* Encrypt  (32 rounds)                                                      *)
73(*---------------------------------------------------------------------------*)
74
75val TEAEncrypt_def =
76 Define
77   `TEAEncrypt (keys,txt) =
78      let (cipheredtxt,keys,sum) = Rounds(32w,(txt,keys,0w)) in
79      cipheredtxt`;
80
81(*===========================================================================*)
82(*      Decryption                                                           *)
83(*      Analogous to the encryption case                                     *)
84(*===========================================================================*)
85
86(*---------------------------------------------------------------------------*)
87(*     One round backward computation                                        *)
88(*---------------------------------------------------------------------------*)
89
90val InvRound_def =
91 Define
92   `InvRound((y,z),(k0,k1,k2,k3),sum)  =
93        ((y - ShiftXor(z - ShiftXor(y, sum, k2, k3), sum, k0, k1),
94          z - ShiftXor(y, sum, k2, k3)),
95         (k0,k1,k2,k3),
96         sum-DELTA)`;
97
98(*---------------------------------------------------------------------------*)
99(* Arbitrary number of decipher rounds                                       *)
100(*---------------------------------------------------------------------------*)
101
102val InvRounds_def =
103 Define
104   `InvRounds (n:word32,s:state) =
105     if n=0w then s else InvRounds (n-1w, InvRound s)`;
106
107(*---------------------------------------------------------------------------*)
108(* Decrypt (32 rounds)                                                       *)
109(*---------------------------------------------------------------------------*)
110
111val TEADecrypt_def =
112 Define
113   `TEADecrypt (keys,txt) =
114      let (plaintxt,keys,sum) = InvRounds(32w,(txt,keys,DELTA << 5))
115      in
116        plaintxt`;
117
118(*===========================================================================*)
119(* Correctness                                                               *)
120(*===========================================================================*)
121
122(*---------------------------------------------------------------------------*)
123(* Case analysis on a state                                                  *)
124(*---------------------------------------------------------------------------*)
125
126val FORALL_STATE = Q.prove
127 (`(!x:state. P x) = !v0 v1 k0 k1 k2 k3 sum. P((v0,v1),(k0,k1,k2,k3),sum)`,
128    METIS_TAC [PAIR]
129 );
130
131(*---------------------------------------------------------------------------*)
132(* Basic inversion lemma                                                     *)
133(*---------------------------------------------------------------------------*)
134
135val OneRound_Inversion = Q.store_thm("OneRound_Inversion",
136 `!s:state. InvRound (Round s) = s`,
137 SIMP_TAC std_ss [FORALL_STATE] THEN
138 RW_TAC list_ss [Round_def, InvRound_def,WORD_ADD_SUB, LET_THM]);
139
140(*---------------------------------------------------------------------------*)
141(* Tweaked version of Rounds induction.                                      *)
142(*---------------------------------------------------------------------------*)
143
144val Rounds_ind' = Q.prove
145(`!P.
146   (!(n:word32) b1 k1 s1.
147       (~(n = 0w) ==> P (n - 1w,Round(b1,k1,s1))) ==> P (n,(b1,k1,s1))) ==>
148     !i b k s:word32. P (i,b,k,s)`,
149 REPEAT STRIP_TAC THEN
150 MATCH_MP_TAC (DISCH_ALL(SPEC_ALL (UNDISCH (SPEC_ALL Rounds_ind)))) THEN
151 METIS_TAC [ABS_PAIR_THM]);
152
153(*---------------------------------------------------------------------------*)
154(* Main lemmas                                                               *)
155(*---------------------------------------------------------------------------*)
156
157val lemma1 = Q.prove
158(`!b k sum. ?b1. Round (b,k,sum) = (b1,k,sum+DELTA)`,
159 SIMP_TAC std_ss [FORALL_PROD,Round_def,LET_THM]);
160
161val lemma = Q.prove
162(`!i b k s. ?b1. Rounds (i,b,k,s) = (b1,k,s + DELTA * i)`,
163 recInduct Rounds_ind' THEN RW_TAC std_ss [] THEN
164  ONCE_REWRITE_TAC [Rounds_def] THEN
165  RW_TAC arith_ss [WORD_MULT_CLAUSES, WORD_ADD_0] THEN
166  RES_TAC THEN RW_TAC std_ss [] THENL
167  [METIS_TAC [lemma1,FST,SND],
168   `?b2. Round(b1,k1,s1) = (b2,k1,s1+DELTA)` by METIS_TAC [lemma1] THEN
169   RW_TAC arith_ss [WORD_EQ_ADD_LCANCEL,GSYM WORD_ADD_ASSOC] THEN
170   `?m. n = m + 1w` by METIS_TAC [WORD_PRED_EXISTS] THEN
171   RW_TAC std_ss [WORD_ADD_SUB,WORD_MULT_CLAUSES]]);
172
173val delta_shift = Q.prove
174(`DELTA << 5 = DELTA * 32w`,
175 REWRITE_TAC [DELTA_def] THEN WORDS_TAC);
176
177(*---------------------------------------------------------------------------*)
178(* Basic theorem about encryption/decryption                                 *)
179(*---------------------------------------------------------------------------*)
180
181val TEA_CORRECT = Q.store_thm
182("TEA_CORRECT",
183 `!plaintext keys.
184     TEADecrypt (keys,TEAEncrypt (keys,plaintext)) = plaintext`,
185 RW_TAC list_ss [TEAEncrypt_def, TEADecrypt_def, delta_shift]
186  THEN `(keys1 = keys) /\ (sum = DELTA * 32w)`
187        by METIS_TAC [lemma,WORD_ADD_0,PAIR_EQ]
188  THEN RW_TAC std_ss []
189  THEN Q.PAT_ASSUM `Rounds x = y` (SUBST_ALL_TAC o SYM)
190  THEN POP_ASSUM MP_TAC
191  THEN computeLib.RESTR_EVAL_TAC
192           (flatten(map decls ["Round", "InvRound", "DELTA"]))
193  THEN RW_TAC std_ss [OneRound_Inversion]);
194
195
196(*===========================================================================*)
197(*  Compilation                                                              *)
198(*===========================================================================*)
199
200val teaFns = [ShiftXor_def,Round_def,Rounds_def,TEAEncrypt_def];
201
202compile1 teaFns;
203
204(* TEAEncrypt unwound a bit, but leaves some simplifications still possible *)
205
206compile2 teaFns;
207
208(*---------------------------------------------------------------------------*)
209(* All previous, and closure conversion. Not needed for tea, but nevermind   *)
210(*---------------------------------------------------------------------------*)
211
212compile3 teaFns;
213
214(*---------------------------------------------------------------------------*)
215(* All previous, and register allocation.                                    *)
216(*---------------------------------------------------------------------------*)
217
218(* Fails on Rounds *)
219compile4 teaFns;
220
221(*---------------------------------------------------------------------------*)
222(* Different pass4, in which some intermediate steps are skipped.            *)
223(*---------------------------------------------------------------------------*)
224
225fun pass4a (env,def) =
226  let val def1 = pass1 def
227      val def2 = reg_alloc def1
228  in
229    def2
230  end;
231
232val compile4a = complist pass4a;
233
234compile4a teaFns;
235
236
237(* results:
238    |- ShiftXor =
239       (\(r0,r1,r2,r3).
240          (let r4 = r0 << 4 in
241           let r2 = r4 + r2 in
242           let r1 = r0 + r1 in
243           let r0 = r0 >> 5 in
244           let r0 = r0 + r3 in
245           let r0 = r1 ?? r0 in
246           let r0 = r2 ?? r0 in
247             r0)) : thm
248
249    |- Round =
250       (\((r0,r1),(r2,r3,r4,r5),r6).
251          (let r6 = r6 + DELTA in
252           let r7 = ShiftXor (r1,r6,r2,r3) in
253           let r0 = r0 + r7 in
254           let r7 = ShiftXor (r0,r6,r4,r5) in
255           let r1 = r1 + r7 in
256             ((r0,r1),(r2,r3,r4,r5),r6))) : thm
257
258    |- Rounds =
259       (\(r0,(r1,r2),(r3,r4,r5,r6),r7).
260          (let ((r0,r1),(r2,r3,r4,r5),r6) =
261                 (if r0 = 0w then
262                    ((r1,r2),(r3,r4,r5,r6),r7)
263                  else
264                    (let r0 = r0 - 1w in
265                     let ((r1,r2),(r3,r4,r5,r6),r7) =
266                           Round ((r1,r2),(r3,r4,r5,r6),r7)
267                     in
268                     let ((r0,r1),(r2,r3,r4,r5),r6) =
269                           Rounds (r0,(r1,r2),(r3,r4,r5,r6),r7)
270                     in
271                       ((r0,r1),(r2,r3,r4,r5),r6)))
272           in
273             ((r0,r1),(r2,r3,r4,r5),r6))) : thm
274
275 |- TEAEncrypt =
276       (\((r0,r1,r2,r3),r4,r5).
277          (let ((r0,r1),(r2,r3,r4,r5),r6) =
278                 Rounds (2w,(r4,r5),(r0,r1,r2,r3),0w)
279           in
280             (r0,r1))) : thm
281
282*)
283
284
285(* --------------------------------------------------------------------*)
286(* Another configuration:                                              *)
287(* Suppose we have only 4 registers available                          *)
288(* --------------------------------------------------------------------*)
289
290numRegs := 4;
291compile4a teaFns;
292
293(*
294Results:
295    PASS [|- ShiftXor =
296             (\(r0,r1,r2,r3).
297                (let m1 = r3 in
298                 let r3 = r0 << 4 in
299                 let r2 = r3 + r2 in
300                 let r1 = r0 + r1 in
301                 let r0 = r0 >> 5 in
302                 let r3 = m1 in
303                 let r0 = r0 + r3 in
304                 let r0 = r1 ?? r0 in
305                 let r0 = r2 ?? r0 in
306                   r0)),
307          |- Round =
308             (\((r0,r1),(r2,r3,m1,m2),m3).
309                (let m4 = r2 in
310                 let r2 = m3 in
311                 let r2 = r2 + DELTA in
312                 let m3 = r3 in
313                 let r3 = ShiftXor (r1,r2,m4,m3) in
314                 let r0 = r0 + r3 in
315                 let r3 = ShiftXor (r0,r2,m1,m2) in
316                 let r1 = r1 + r3 in
317                   ((r0,r1),(m4,m3,m1,m2),r2))),
318          |- Rounds =
319             (\(r0,(r1,r2),(r3,m1,m2,m3),m4).
320                (let ((r0,r1),(r2,r3,m1,m2),m3) =
321                       (if r0 = 0w then
322                          ((r1,r2),(r3,m1,m2,m3),m4)
323                        else
324                          (let r0 = r0 - 1w in
325                           let ((r1,r2),(r3,m4,m5,m6),m7) =
326                                 Round ((r1,r2),(r3,m1,m2,m3),m4)
327                           in
328                           let ((r0,r1),(r2,r3,m4,m5),m6) =
329                                 Rounds (r0,(r1,r2),(r3,m4,m5,m6),m7)
330                           in
331                             ((r0,r1),(r2,r3,m4,m5),m6)))
332                 in
333                   ((r0,r1),(r2,r3,m1,m2),m3))),
334          |- TEAEncrypt =
335             (\((r0,r1,r2,r3),m1,m2).
336                (let ((r0,r1),(r2,r3,m1,m1),m1) =
337                       Rounds (2w,(m1,m2),(r0,r1,r2,r3),0w)
338                 in
339                   (r0,r1)))] : (thm list, thm list * thm list) verdict
340*)
341
342(* --------------------------------------------------------------------*)
343(* An extreme configuration:                                           *)
344(* Suppose we have only 2 registers available                          *)
345(* We should have at least 2 registers when binary operations are      *)
346(* presented in the program (e.g. add * * * needs 2-3 registers).      *)
347(* --------------------------------------------------------------------*)
348
349numRegs := 2;
350compile4a teaFns;
351
352(*
353    PASS [|- ShiftXor =
354             (\(r0,r1,m1,m2).
355                (let m3 = r0 in
356                 let r0 = m3 in
357                 let r0 = r0 << 4 in
358                 let m4 = r1 in
359                 let r1 = m1 in
360                 let r0 = r0 + r1 in
361                 let r1 = m3 in
362                 let m1 = r0 in
363                 let r0 = m4 in
364                 let r0 = r1 + r0 in
365                 let r1 = m3 in
366                 let r1 = r1 >> 5 in
367                 let m3 = r0 in
368                 let r0 = m2 in
369                 let r0 = r1 + r0 in
370                 let r1 = m3 in
371                 let r0 = r1 ?? r0 in
372                 let r1 = m1 in
373                 let r0 = r1 ?? r0 in
374                   r0)),
375          |- Round =
376             (\((r0,r1),(m1,m2,m3,m4),m5).
377                (let m6 = r1 in
378                 let r1 = m5 in
379                 let r1 = r1 + DELTA in
380                 let m5 = r1 in
381                 let r1 = ShiftXor (m6,m5,m1,m2) in
382                 let r0 = r0 + r1 in
383                 let r1 = ShiftXor (r0,m5,m3,m4) in
384                 let m7 = r0 in
385                 let r0 = m6 in
386                 let r0 = r0 + r1 in
387                   ((m7,r0),(m1,m2,m3,m4),m5))),
388          |- Rounds =
389             (\(r0,(r1,m1),(m2,m3,m4,m5),m6).
390                (let ((r0,r1),(m1,m2,m3,m4),m5) =
391                       (if r0 = 0w then
392                          ((r1,m1),(m2,m3,m4,m5),m6)
393                        else
394                          (let r0 = r0 - 1w in
395                           let ((r1,m6),(m7,m8,m9,m10),m11) =
396                                 Round ((r1,m1),(m2,m3,m4,m5),m6)
397                           in
398                           let ((r0,r1),(m6,m7,m8,m9),m10) =
399                                 Rounds (r0,(r1,m6),(m7,m8,m9,m10),m11)
400                           in
401                             ((r0,r1),(m6,m7,m8,m9),m10)))
402                 in
403                   ((r0,r1),(m1,m2,m3,m4),m5))),
404          |- TEAEncrypt =
405             (\((r0,r1,m1,m2),m3,m4).
406                (let ((r0,r1),(m1,m1,m1,m1),m1) =
407                       Rounds (2w,(m3,m4),(r0,r1,m1,m2),0w)
408                 in
409                   (r0,r1)))] : (thm list, thm list * thm list) verdict
410
411*)
412