1(*---------------------------------------------------------------------------*) 2(* Operations performed in a round: *) 3(* *) 4(* - applying Sboxes *) 5(* - shifting rows *) 6(* - mixing columns *) 7(* - adding round keys *) 8(* *) 9(* We prove "inversion" theorems for each of these *) 10(* *) 11(*---------------------------------------------------------------------------*) 12 13(* For interactive work 14 quietdec := true; 15 app load ["MultTheory", "tablesTheory", "wordsLib"]; 16 quietdec := false; 17*) 18 19open HolKernel Parse boolLib bossLib; 20open pairTheory wordsTheory MultTheory wordsLib; 21 22(*---------------------------------------------------------------------------*) 23(* Make bindings to pre-existing stuff *) 24(*---------------------------------------------------------------------------*) 25 26val RESTR_EVAL_TAC = computeLib.RESTR_EVAL_TAC; 27 28val Sbox_Inversion = tablesTheory.Sbox_Inversion; 29 30(*---------------------------------------------------------------------------*) 31(* Create the theory. *) 32(*---------------------------------------------------------------------------*) 33 34val _ = new_theory "RoundOp"; 35 36(*---------------------------------------------------------------------------*) 37(* A block is 16 bytes. A state also has that type, although states have *) 38(* a special format. *) 39(*---------------------------------------------------------------------------*) 40 41val _ = type_abbrev("block", 42 Type`:word8 # word8 # word8 # word8 # 43 word8 # word8 # word8 # word8 # 44 word8 # word8 # word8 # word8 # 45 word8 # word8 # word8 # word8`); 46 47val _ = type_abbrev("state", Type`:block`); 48val _ = type_abbrev("key", Type`:state`); 49val _ = type_abbrev("w8x4", Type`:word8 # word8 # word8 # word8`); 50 51 52val ZERO_BLOCK_def = 53 Define 54 `ZERO_BLOCK = (0w,0w,0w,0w, 55 0w,0w,0w,0w, 56 0w,0w,0w,0w, 57 0w,0w,0w,0w) : block`; 58 59(*---------------------------------------------------------------------------*) 60(* Case analysis on a block. *) 61(*---------------------------------------------------------------------------*) 62 63val FORALL_BLOCK = Q.store_thm 64("FORALL_BLOCK", 65 `(!b:block. P b) = 66 !w1 w2 w3 w4 w5 w6 w7 w8 w9 w10 w11 w12 w13 w14 w15 w16. 67 P (w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,w16)`, 68 SIMP_TAC std_ss [FORALL_PROD]); 69 70(*---------------------------------------------------------------------------*) 71(* XOR on blocks. Definition and algebraic properties. *) 72(*---------------------------------------------------------------------------*) 73 74val XOR_BLOCK_def = Define 75 `XOR_BLOCK ((a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15):block) 76 ((b0,b1,b2,b3,b4,b5,b6,b7,b8,b9,b10,b11,b12,b13,b14,b15):block) 77 = 78 (a0 ?? b0, a1 ?? b1, a2 ?? b2, a3 ?? b3, 79 a4 ?? b4, a5 ?? b5, a6 ?? b6, a7 ?? b7, 80 a8 ?? b8, a9 ?? b9, a10 ?? b10, a11 ?? b11, 81 a12 ?? b12, a13 ?? b13, a14 ?? b14, a15 ?? b15)`; 82 83val XOR_BLOCK_ZERO = Q.store_thm 84("XOR_BLOCK_ZERO", 85 `!x:block. XOR_BLOCK x ZERO_BLOCK = x`, 86 SIMP_TAC std_ss 87 [FORALL_BLOCK,XOR_BLOCK_def, ZERO_BLOCK_def, WORD_XOR_CLAUSES]); 88 89val XOR_BLOCK_INV = Q.store_thm 90("XOR_BLOCK_INV", 91 `!x:block. XOR_BLOCK x x = ZERO_BLOCK`, 92 SIMP_TAC std_ss 93 [FORALL_BLOCK,XOR_BLOCK_def, ZERO_BLOCK_def, WORD_XOR_CLAUSES]); 94 95val XOR_BLOCK_AC = Q.store_thm 96("XOR_BLOCK_AC", 97 `(!x y z:block. XOR_BLOCK (XOR_BLOCK x y) z = XOR_BLOCK x (XOR_BLOCK y z)) /\ 98 (!x y:block. XOR_BLOCK x y = XOR_BLOCK y x)`, 99 SIMP_TAC (srw_ss()) [FORALL_BLOCK,XOR_BLOCK_def]); 100 101val XOR_BLOCK_IDEM = Q.store_thm 102("XOR_BLOCK_IDEM", 103 `(!v u. XOR_BLOCK (XOR_BLOCK v u) u = v) /\ 104 (!v u. XOR_BLOCK v (XOR_BLOCK v u) = u)`, 105 METIS_TAC [XOR_BLOCK_INV,XOR_BLOCK_AC,XOR_BLOCK_ZERO]); 106 107(*---------------------------------------------------------------------------*) 108(* Moving data into and out of a state *) 109(*---------------------------------------------------------------------------*) 110 111val to_state_def = Define 112 `to_state ((b0,b1,b2,b3,b4,b5,b6,b7,b8,b9,b10,b11,b12,b13,b14,b15) :block) 113 = 114 (b0,b4,b8,b12, 115 b1,b5,b9,b13, 116 b2,b6,b10,b14, 117 b3,b7,b11,b15) : state`; 118 119val from_state_def = Define 120 `from_state((b0,b4,b8,b12, 121 b1,b5,b9,b13, 122 b2,b6,b10,b14, 123 b3,b7,b11,b15) :state) 124 = (b0,b1,b2,b3,b4,b5,b6,b7,b8,b9,b10,b11,b12,b13,b14,b15) : block`; 125 126 127val to_state_Inversion = Q.store_thm 128 ("to_state_Inversion", 129 `!s:state. from_state(to_state s) = s`, 130 SIMP_TAC std_ss [FORALL_BLOCK, from_state_def, to_state_def]); 131 132 133val from_state_Inversion = Q.store_thm 134 ("from_state_Inversion", 135 `!s:state. to_state(from_state s) = s`, 136 SIMP_TAC std_ss [FORALL_BLOCK, from_state_def, to_state_def]); 137 138 139(*---------------------------------------------------------------------------*) 140(* Apply an Sbox to the state *) 141(*---------------------------------------------------------------------------*) 142 143val _ = Parse.hide "S"; (* to make parameter S a variable *) 144 145val genSubBytes_def = try Define 146 `genSubBytes S ((b00,b01,b02,b03, 147 b10,b11,b12,b13, 148 b20,b21,b22,b23, 149 b30,b31,b32,b33) :state) 150 = 151 (S b00, S b01, S b02, S b03, 152 S b10, S b11, S b12, S b13, 153 S b20, S b21, S b22, S b23, 154 S b30, S b31, S b32, S b33) :state`; 155 156val _ = Parse.reveal "S"; 157 158val SubBytes_def = Define `SubBytes = genSubBytes Sbox`; 159val InvSubBytes_def = Define `InvSubBytes = genSubBytes InvSbox`; 160 161val SubBytes_Inversion = Q.store_thm 162("SubBytes_Inversion", 163 `!s:state. genSubBytes InvSbox (genSubBytes Sbox s) = s`, 164 SIMP_TAC std_ss [FORALL_BLOCK,genSubBytes_def,Sbox_Inversion]); 165 166 167(*--------------------------------------------------------------------------- 168 Left-shift the first row not at all, the second row by 1, the 169 third row by 2, and the last row by 3. And the inverse operation. 170 ---------------------------------------------------------------------------*) 171 172val ShiftRows_def = Define 173 `ShiftRows ((b00,b01,b02,b03, 174 b10,b11,b12,b13, 175 b20,b21,b22,b23, 176 b30,b31,b32,b33) :state) 177 = 178 (b00,b01,b02,b03, 179 b11,b12,b13,b10, 180 b22,b23,b20,b21, 181 b33,b30,b31,b32) :state`; 182 183val InvShiftRows_def = Define 184 `InvShiftRows ((b00,b01,b02,b03, 185 b11,b12,b13,b10, 186 b22,b23,b20,b21, 187 b33,b30,b31,b32) :state) 188 = 189 (b00,b01,b02,b03, 190 b10,b11,b12,b13, 191 b20,b21,b22,b23, 192 b30,b31,b32,b33) :state`; 193 194(*--------------------------------------------------------------------------- 195 InvShiftRows inverts ShiftRows 196 ---------------------------------------------------------------------------*) 197 198val ShiftRows_Inversion = Q.store_thm 199("ShiftRows_Inversion", 200 `!s:state. InvShiftRows (ShiftRows s) = s`, 201 SIMP_TAC std_ss [FORALL_BLOCK] THEN REPEAT STRIP_TAC THEN EVAL_TAC); 202 203(*---------------------------------------------------------------------------*) 204(* For alternative decryption scheme *) 205(*---------------------------------------------------------------------------*) 206 207val ShiftRows_SubBytes_Commute = Q.store_thm 208 ("ShiftRows_SubBytes_Commute", 209 `!s. ShiftRows (SubBytes s) = SubBytes (ShiftRows s)`, 210 SIMP_TAC std_ss [FORALL_BLOCK] THEN REPEAT STRIP_TAC THEN EVAL_TAC); 211 212 213val InvShiftRows_InvSubBytes_Commute = Q.store_thm 214 ("InvShiftRows_InvSubBytes_Commute", 215 `!s. InvShiftRows (InvSubBytes s) = InvSubBytes (InvShiftRows s)`, 216 SIMP_TAC std_ss [FORALL_BLOCK] THEN REPEAT STRIP_TAC THEN EVAL_TAC); 217 218 219(*--------------------------------------------------------------------------- 220 Column multiplication and its inverse 221 ---------------------------------------------------------------------------*) 222 223val MultCol_def = Define 224 `MultCol (a,b,c,d) = 225 ((2w ** a) ?? (3w ** b) ?? c ?? d, 226 a ?? (2w ** b) ?? (3w ** c) ?? d, 227 a ?? b ?? (2w ** c) ?? (3w ** d), 228 (3w ** a) ?? b ?? c ?? (2w ** d))`; 229 230val InvMultCol_def = Define 231 `InvMultCol (a,b,c,d) = 232 ((0xEw ** a) ?? (0xBw ** b) ?? (0xDw ** c) ?? (9w ** d), 233 (9w ** a) ?? (0xEw ** b) ?? (0xBw ** c) ?? (0xDw ** d), 234 (0xDw ** a) ?? (9w ** b) ?? (0xEw ** c) ?? (0xBw ** d), 235 (0xBw ** a) ?? (0xDw ** b) ?? (9w ** c) ?? (0xEw ** d))`; 236 237(*---------------------------------------------------------------------------*) 238(* Inversion lemmas for column multiplication. Proved with an ad-hoc tactic *) 239(*---------------------------------------------------------------------------*) 240 241val BYTE_CASES_TAC = 242 Cases_word_value 243 THEN RW_TAC std_ss [fetch "Mult" "mult_tables"] 244 THEN REWRITE_TAC [fetch "Mult" "mult_tables"] 245 THEN WORD_EVAL_TAC; 246 247 248val lemma_a1 = Count.apply Q.prove 249(`!a. 0xEw ** (2w ** a) ?? 0xBw ** a ?? 0xDw ** a ?? 9w ** (3w ** a) = a`, 250 BYTE_CASES_TAC); 251 252val lemma_a2 = Count.apply Q.prove 253(`!b. 0xEw ** (3w ** b) ?? 0xBw ** (2w ** b) ?? 0xDw ** b ?? 9w ** b = 0w`, 254 BYTE_CASES_TAC); 255 256val lemma_a3 = Count.apply Q.prove 257(`!c. 0xEw ** c ?? 0xBw ** (3w ** c) ?? 0xDw ** (2w ** c) ?? 9w ** c = 0w`, 258 BYTE_CASES_TAC); 259 260val lemma_a4 = Count.apply Q.prove 261(`!d. 0xEw ** d ?? 0xBw ** d ?? 0xDw ** (3w ** d) ?? 9w ** (2w ** d) = 0w`, 262 BYTE_CASES_TAC); 263 264val lemma_b1 = Count.apply Q.prove 265(`!a. 9w ** (2w ** a) ?? 0xEw ** a ?? 0xBw ** a ?? 0xDw ** (3w ** a) = 0w`, 266 BYTE_CASES_TAC); 267 268val lemma_b2 = Count.apply Q.prove 269(`!b. 9w ** (3w ** b) ?? 0xEw ** (2w ** b) ?? 0xBw ** b ?? 0xDw ** b = b`, 270 BYTE_CASES_TAC); 271 272val lemma_b3 = Count.apply Q.prove 273(`!c. 9w ** c ?? 0xEw ** (3w ** c) ?? 0xBw ** (2w ** c) ?? 0xDw ** c = 0w`, 274 BYTE_CASES_TAC); 275 276val lemma_b4 = Count.apply Q.prove 277(`!d. 9w ** d ?? 0xEw ** d ?? 0xBw ** (3w ** d) ?? 0xDw ** (2w ** d) = 0w`, 278 BYTE_CASES_TAC); 279 280val lemma_c1 = Count.apply Q.prove 281(`!a. 0xDw ** (2w ** a) ?? 9w ** a ?? 0xEw ** a ?? 0xBw ** (3w ** a) = 0w`, 282 BYTE_CASES_TAC THEN EVAL_TAC); 283 284val lemma_c2 = Count.apply Q.prove 285(`!b. 0xDw ** (3w ** b) ?? 9w ** (2w ** b) ?? 0xEw ** b ?? 0xBw ** b = 0w`, 286 BYTE_CASES_TAC); 287 288val lemma_c3 = Count.apply Q.prove 289(`!c. 0xDw ** c ?? 9w ** (3w ** c) ?? 0xEw ** (2w ** c) ?? 0xBw ** c = c`, 290 BYTE_CASES_TAC); 291 292val lemma_c4 = Count.apply Q.prove 293(`!d. 0xDw ** d ?? 9w ** d ?? 0xEw ** (3w ** d) ?? 0xBw ** (2w ** d) = 0w`, 294 BYTE_CASES_TAC); 295 296val lemma_d1 = Count.apply Q.prove 297(`!a. 0xBw ** (2w ** a) ?? 0xDw ** a ?? 9w ** a ?? 0xEw ** (3w ** a) = 0w`, 298 BYTE_CASES_TAC); 299 300val lemma_d2 = Count.apply Q.prove 301(`!b. 0xBw ** (3w ** b) ?? 0xDw ** (2w ** b) ?? 9w ** b ?? 0xEw ** b = 0w`, 302 BYTE_CASES_TAC); 303 304val lemma_d3 = Count.apply Q.prove 305(`!c. 0xBw ** c ?? 0xDw ** (3w ** c) ?? 9w ** (2w ** c) ?? 0xEw ** c = 0w`, 306 BYTE_CASES_TAC THEN EVAL_TAC); 307 308val lemma_d4 = Count.apply Q.prove 309(`!d. 0xBw ** d ?? 0xDw ** d ?? 9w ** (3w ** d) ?? 0xEw ** (2w ** d) = d`, 310 BYTE_CASES_TAC); 311 312(*---------------------------------------------------------------------------*) 313(* The following lemma is hideous to prove without permutative rewriting *) 314(*---------------------------------------------------------------------------*) 315 316val rearrange_xors = Q.prove 317(`(a1 ?? b1 ?? c1 ?? d1) ?? 318 (a2 ?? b2 ?? c2 ?? d2) ?? 319 (a3 ?? b3 ?? c3 ?? d3) ?? 320 (a4 ?? b4 ?? c4 ?? d4) 321 = 322 (a1 ?? a2 ?? a3 ?? a4) ?? 323 (b1 ?? b2 ?? b3 ?? b4) ?? 324 (c1 ?? c2 ?? c3 ?? c4) ?? 325 (d1 ?? d2 ?? d3 ?? d4)`, 326 SRW_TAC [] []); 327 328val mix_lemma1 = Q.prove 329(`!a b c d. 330 (0xEw ** ((2w ** a) ?? (3w ** b) ?? c ?? d)) ?? 331 (0xBw ** (a ?? (2w ** b) ?? (3w ** c) ?? d)) ?? 332 (0xDw ** (a ?? b ?? (2w ** c) ?? (3w ** d))) ?? 333 (9w ** ((3w ** a) ?? b ?? c ?? (2w ** d))) 334 = a`, 335 RW_TAC std_ss [ConstMultDistrib] 336 THEN ONCE_REWRITE_TAC [rearrange_xors] 337 THEN RW_TAC std_ss [lemma_a1,lemma_a2,lemma_a3,lemma_a4,WORD_XOR_CLAUSES]); 338 339val mix_lemma2 = Q.prove 340(`!a b c d. 341 (9w ** ((2w ** a) ?? (3w ** b) ?? c ?? d)) ?? 342 (0xEw ** (a ?? (2w ** b) ?? (3w ** c) ?? d)) ?? 343 (0xBw ** (a ?? b ?? (2w ** c) ?? (3w ** d))) ?? 344 (0xDw ** ((3w ** a) ?? b ?? c ?? (2w ** d))) 345 = b`, 346 RW_TAC std_ss [ConstMultDistrib] 347 THEN ONCE_REWRITE_TAC [rearrange_xors] 348 THEN RW_TAC std_ss [lemma_b1,lemma_b2,lemma_b3,lemma_b4,WORD_XOR_CLAUSES]); 349 350val mix_lemma3 = Q.prove 351(`!a b c d. 352 (0xDw ** ((2w ** a) ?? (3w ** b) ?? c ?? d)) ?? 353 (9w ** (a ?? (2w ** b) ?? (3w ** c) ?? d)) ?? 354 (0xEw ** (a ?? b ?? (2w ** c) ?? (3w ** d))) ?? 355 (0xBw ** ((3w ** a) ?? b ?? c ?? (2w ** d))) 356 = c`, 357 RW_TAC std_ss [ConstMultDistrib] 358 THEN ONCE_REWRITE_TAC [rearrange_xors] 359 THEN RW_TAC std_ss [lemma_c1,lemma_c2,lemma_c3,lemma_c4,WORD_XOR_CLAUSES]); 360 361val mix_lemma4 = Q.prove 362(`!a b c d. 363 (0xBw ** ((2w ** a) ?? (3w ** b) ?? c ?? d)) ?? 364 (0xDw ** (a ?? (2w ** b) ?? (3w ** c) ?? d)) ?? 365 (9w ** (a ?? b ?? (2w ** c) ?? (3w ** d))) ?? 366 (0xEw ** ((3w ** a) ?? b ?? c ?? (2w ** d))) 367 = d`, 368 RW_TAC std_ss [ConstMultDistrib] 369 THEN ONCE_REWRITE_TAC [rearrange_xors] 370 THEN RW_TAC std_ss [lemma_d1,lemma_d2,lemma_d3,lemma_d4,WORD_XOR_CLAUSES]); 371 372(*---------------------------------------------------------------------------*) 373(* Get the constants of various definitions *) 374(*---------------------------------------------------------------------------*) 375 376val mult = Term `Mult$**`; 377val n2w = Term `n2w`; 378 379(*---------------------------------------------------------------------------*) 380(* Mixing columns *) 381(*---------------------------------------------------------------------------*) 382 383val genMixColumns_def = Define 384 `genMixColumns MC ((b00,b01,b02,b03, 385 b10,b11,b12,b13, 386 b20,b21,b22,b23, 387 b30,b31,b32,b33) :state) 388 = let (b00', b10', b20', b30') = MC (b00,b10,b20,b30) in 389 let (b01', b11', b21', b31') = MC (b01,b11,b21,b31) in 390 let (b02', b12', b22', b32') = MC (b02,b12,b22,b32) in 391 let (b03', b13', b23', b33') = MC (b03,b13,b23,b33) 392 in 393 (b00', b01', b02', b03', 394 b10', b11', b12', b13', 395 b20', b21', b22', b23', 396 b30', b31', b32', b33') : state`; 397 398 399val MixColumns_def = Define `MixColumns = genMixColumns MultCol`; 400val InvMixColumns_def = Define `InvMixColumns = genMixColumns InvMultCol`; 401 402val MixColumns_Inversion = Q.store_thm 403("MixColumns_Inversion", 404 `!s. genMixColumns InvMultCol (genMixColumns MultCol s) = s`, 405 SIMP_TAC std_ss [FORALL_BLOCK] 406 THEN RESTR_EVAL_TAC [mult,n2w] 407 THEN RW_TAC std_ss [mix_lemma1,mix_lemma2,mix_lemma3,mix_lemma4]); 408 409 410(*--------------------------------------------------------------------------- 411 Pairwise XOR the state with the round key 412 ---------------------------------------------------------------------------*) 413 414val AddRoundKey_def = Define `AddRoundKey = XOR_BLOCK`; 415 416(*---------------------------------------------------------------------------*) 417(* For alternative decryption scheme *) 418(*---------------------------------------------------------------------------*) 419 420val InvMixColumns_Distrib = Q.store_thm 421("InvMixColumns_Distrib", 422 `!s k. InvMixColumns (AddRoundKey s k) 423 = 424 AddRoundKey (InvMixColumns s) (InvMixColumns k)`, 425 SIMP_TAC std_ss [FORALL_BLOCK] THEN 426 SRW_TAC [] [XOR_BLOCK_def, AddRoundKey_def, InvMixColumns_def, LET_THM, 427 genMixColumns_def, InvMultCol_def, ConstMultDistrib]); 428 429 430val _ = export_theory(); 431