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