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