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
14(*
15app load ["EmitML","wordsLib"];
16*)
17open HolKernel Parse boolLib bossLib;
18open wordsTheory wordsLib pairTheory pairLib basis_emitTheory;
19
20
21(*---------------------------------------------------------------------------*)
22(* Inititialize new theory for TEA                                           *)
23(*---------------------------------------------------------------------------*)
24
25val _ = new_theory "tea";
26
27(*---------------------------------------------------------------------------*)
28(* General stuff                                                             *)
29(*---------------------------------------------------------------------------*)
30
31val WORD_PRED_EXISTS = Q.prove
32(`!w:'a word. ~(w = 0w) ==> ?u. w = u + 1w`,
33  RW_TAC std_ss [] THEN
34  Q.EXISTS_TAC `w - 1w` THEN
35  RW_TAC std_ss [WORD_SUB_ADD,WORD_ADD_SUB,WORD_MULT_CLAUSES]);
36
37
38(*---------------------------------------------------------------------------*)
39(* Cipher types                                                              *)
40(*---------------------------------------------------------------------------*)
41
42val _ = type_abbrev("block", ``:word32 # word32``);
43val _ = type_abbrev("key",   ``:word32 # word32 # word32 # word32``);
44val _ = type_abbrev("state", ``:block # key # word32``);
45
46
47(*---------------------------------------------------------------------------*)
48(* Case analysis on a state                                                  *)
49(*---------------------------------------------------------------------------*)
50
51val FORALL_STATE = Q.store_thm
52("FORALL_STATE",
53 `(!x:state. P x) = !v0 v1 k0 k1 k2 k3 sum. P((v0,v1),(k0,k1,k2,k3),sum)`,
54    METIS_TAC [PAIR]);
55
56(*---------------------------------------------------------------------------*)
57(* Basic constants and operations.                                           *)
58(*---------------------------------------------------------------------------*)
59
60val DELTA_def = Define `DELTA = 0x9e3779b9w : word32`;
61
62(*---------------------------------------------------------------------------*)
63(* ?? = xor  (infix) and >>> is LSR                                          *)
64(*---------------------------------------------------------------------------*)
65
66val ShiftXor_def =
67 Define
68   `ShiftXor (x:word32,s,k0,k1) =
69          ((x << 4) + k0) ?? (x + s) ?? ((x >>> 5) + k1)`;
70
71(* --------------------------------------------------------------------------*)
72(*      One round forward computation                                        *)
73(* --------------------------------------------------------------------------*)
74
75val Round_def =
76 Define
77   `Round ((y,z),(k0,k1,k2,k3),s):state =
78      let s' = s + DELTA in let
79          y' = y + ShiftXor(z, s', k0, k1) in let
80          z' = z + ShiftXor(y', s', k2, k3)
81      in
82        ((y',z'), (k0,k1,k2,k3), s')`;
83
84(*---------------------------------------------------------------------------*)
85(* Arbitrary number of cipher rounds                                         *)
86(*---------------------------------------------------------------------------*)
87
88val Rounds_def =
89 Define
90   `Rounds (n:word32,s:state) =
91      if n=0w then s else Rounds (n-1w, Round s)`;
92
93val Rounds_ind = fetch "-" "Rounds_ind";   (* induction *)
94
95(*---------------------------------------------------------------------------*)
96(* Encrypt  (32 rounds)                                                      *)
97(*---------------------------------------------------------------------------*)
98
99val teaEncrypt_def =
100 Define
101   `teaEncrypt (keys,txt) =
102      let (cipheredtxt,keys,sum) = Rounds(32w,(txt,keys,0w)) in
103      cipheredtxt`;
104
105(*===========================================================================*)
106(*      Decryption                                                           *)
107(*      Analogous to the encryption case                                     *)
108(*===========================================================================*)
109
110(*---------------------------------------------------------------------------*)
111(*     One round backward computation                                        *)
112(*---------------------------------------------------------------------------*)
113
114val InvRound_def =
115 Define
116   `InvRound((y,z),(k0,k1,k2,k3),sum) =
117      let z' = z - ShiftXor(y, sum, k2, k3) in
118      let y' = y - ShiftXor(z',sum, k0, k1) in
119      let sum' = sum-DELTA
120      in
121         ((y',z'), (k0,k1,k2,k3), sum')`;
122
123(*---------------------------------------------------------------------------*)
124(* Arbitrary number of decipher rounds                                       *)
125(*---------------------------------------------------------------------------*)
126
127val InvRounds_def =
128 Define
129   `InvRounds (n:word32,s:state) =
130     if n=0w then s else InvRounds (n-1w, InvRound s)`;
131
132(*---------------------------------------------------------------------------*)
133(* Decrypt (32 rounds)                                                       *)
134(*---------------------------------------------------------------------------*)
135
136val teaDecrypt_def =
137 Define
138   `teaDecrypt (keys,txt) =
139      let (plaintxt,keys,sum) = InvRounds(32w,(txt,keys,DELTA << 5))
140      in
141        plaintxt`;
142
143(*===========================================================================*)
144(* Correctness                                                               *)
145(*===========================================================================*)
146
147(*---------------------------------------------------------------------------*)
148(* Basic inversion lemma                                                     *)
149(*---------------------------------------------------------------------------*)
150
151val OneRound_Inversion = Q.store_thm
152("OneRound_Inversion",
153 `!s:state. InvRound (Round s) = s`,
154 SIMP_TAC std_ss [FORALL_STATE] THEN
155 RW_TAC list_ss [Round_def, InvRound_def,WORD_ADD_SUB, LET_THM]);
156
157(*---------------------------------------------------------------------------*)
158(* Tweaked version of Rounds induction is more useful for this proof.        *)
159(*---------------------------------------------------------------------------*)
160
161val Rounds_ind' = Q.prove
162(`!P.
163   (!(n:word32) b1 k1 s1.
164       (~(n = 0w) ==> P (n - 1w,Round(b1,k1,s1))) ==> P (n,(b1,k1,s1))) ==>
165     !i b k s:word32. P (i,b,k,s)`,
166 REPEAT STRIP_TAC THEN
167 MATCH_MP_TAC (DISCH_ALL(SPEC_ALL (UNDISCH (SPEC_ALL Rounds_ind)))) THEN
168 METIS_TAC [ABS_PAIR_THM]);
169
170(*---------------------------------------------------------------------------*)
171(* Main lemmas                                                               *)
172(*---------------------------------------------------------------------------*)
173
174val lemma1 = Q.prove
175(`!b k sum. ?b1. Round (b,k,sum) = (b1,k,sum+DELTA)`,
176 SIMP_TAC std_ss [FORALL_PROD,Round_def,LET_THM]);
177
178val lemma2 = Q.prove
179(`!n b k s. ?b1. Rounds(n,b,k,s) = (b1,k,s + DELTA * n)`,
180 recInduct Rounds_ind' THEN RW_TAC std_ss [] THEN
181  ONCE_REWRITE_TAC [Rounds_def] THEN
182  RW_TAC arith_ss [WORD_MULT_CLAUSES, WORD_ADD_0] THEN
183  RES_TAC THEN RW_TAC std_ss [] THENL
184  [METIS_TAC [lemma1,FST,SND],
185   `?b2. Round(b1,k1,s1) = (b2,k1,s1+DELTA)` by METIS_TAC [lemma1] THEN
186   RW_TAC arith_ss [WORD_EQ_ADD_LCANCEL,GSYM WORD_ADD_ASSOC] THEN
187   `?m. n = m + 1w` by METIS_TAC [WORD_PRED_EXISTS] THEN
188   RW_TAC std_ss [WORD_ADD_SUB,WORD_MULT_CLAUSES]]);
189
190val DELTA_SHIFT = Q.store_thm
191("DELTA_SHIFT",
192 `DELTA << 5 = DELTA * 32w`,
193 REWRITE_TAC [DELTA_def] THEN WORD_EVAL_TAC);
194
195(*---------------------------------------------------------------------------*)
196(* Basic theorem about encryption/decryption                                 *)
197(*---------------------------------------------------------------------------*)
198
199val tea_correct = Q.store_thm
200("tea_correct",
201 `!plaintext keys.
202     teaDecrypt (keys,teaEncrypt (keys,plaintext)) = plaintext`,
203 RW_TAC list_ss [teaEncrypt_def, teaDecrypt_def, DELTA_SHIFT]
204  THEN rename [���Rounds(_,_,keys,_) = (_,keys_1,sum)���]
205  THEN `(keys_1 = keys) /\ (sum = DELTA * 32w)`
206        by METIS_TAC [lemma2,WORD_ADD_0,PAIR_EQ]
207  THEN RW_TAC std_ss []
208  THEN Q.PAT_ASSUM `Rounds x = y` (SUBST_ALL_TAC o SYM)
209  THEN POP_ASSUM MP_TAC
210  THEN computeLib.RESTR_EVAL_TAC
211           (flatten(map decls ["Round", "InvRound", "DELTA"]))
212  THEN RW_TAC std_ss [OneRound_Inversion]);
213
214(*---------------------------------------------------------------------------*)
215(* Generate ML code in current directory. The generated code depends on      *)
216(* ML code generated for the basic system. That code lives in                *)
217(*                                                                           *)
218(*   HOLDIR/src/emit/ML                                                      *)
219(*                                                                           *)
220(* and needs to be visible on the search path when using or loading teaML.   *)
221(*---------------------------------------------------------------------------*)
222
223(*
224val _ =
225 let open EmitML wordsTheory
226     val elems =
227     MLSIG "type num = numML.num"::
228     MLSIG "type word32 = wordsML.word32"::
229     MLSIG "type block = word32 * word32" ::
230     MLSIG "type key   = word32 * (word32 * (word32 * word32))" ::
231     MLSIG "type state = block * (key * word32)" ::
232     MLSIG "val DELTA : word32" ::
233     MLSIG "val ShiftXor : key -> word32" ::
234     MLSIG "val Round : state -> state" ::
235     MLSIG "val InvRound : state -> state" ::
236     MLSIG "val Rounds : word32 * state -> state" ::
237     MLSIG "val InvRounds : word32 * state -> state" ::
238     MLSIG "val teaEncrypt : key * block -> block" ::
239     MLSIG "val teaDecrypt : key * block -> block" ::
240     OPEN ["num","words","fcp"] ::
241     MLSTRUCT "type word32 = wordsML.word32" ::
242     MLSTRUCT "type block = word32 * word32" ::
243     MLSTRUCT "type key   = word32 * (word32 * (word32 * word32))" ::
244     MLSTRUCT "type state = block * (key * word32)" ::
245     map DEFN_NOSIG
246         [DELTA_def, ShiftXor_def, Round_def, InvRound_def,
247          Rounds_def, InvRounds_def, teaEncrypt_def, teaDecrypt_def]
248 in
249   emitML "" ("tea",elems)
250 end
251 handle _ => ();
252*)
253
254val _ = export_theory();
255