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