1(*---------------------------------------------------------------------------*)
2(*                                   RC6 Block Cipher                        *)
3(*                                        -- implemented in HOL              *)
4(*                                                                           *)
5(* This is a HOL implementation of the RC6 encryption algorithm due to       *)
6(* Ron Rivest and RSA Labs which was a candidate algorithm in the Advanced   *)
7(* Encryption Standard. For detailed information about RC6, please refer to  *)
8(*        http://www.rsasecurity.com/rsalabs/node.asp?id=2512                *)
9(* in which algorithm specification, Security and performance evaluation,    *)
10(* etc. can be found.                                                        *)
11(*---------------------------------------------------------------------------*)
12
13(* For interactive work
14  quietdec := true;
15  app load ["arithmeticTheory","wordsLib"];
16  open arithmeticTheory wordsTheory pairTheory listTheory wordsLib;
17  quietdec := false;
18*)
19
20open HolKernel Parse boolLib bossLib
21     arithmeticTheory pairTheory listTheory wordsLib;
22
23val _ = Globals.priming := SOME"_";
24
25(*---------------------------------------------------------------------------*)
26(* Make bindings to pre-existing stuff                                       *)
27(*---------------------------------------------------------------------------*)
28
29val RESTR_EVAL_TAC = computeLib.RESTR_EVAL_TAC;
30
31(*---------------------------------------------------------------------------*)
32(* Create the theory.                                                        *)
33(*---------------------------------------------------------------------------*)
34
35val _ = new_theory "RC6";
36
37(*---------------------------------------------------------------------------*)
38(* Type Definitions                                                          *)
39(*---------------------------------------------------------------------------*)
40
41val _ = type_abbrev("block", ``:word32 # word32 # word32 # word32``);
42
43val _ = type_abbrev("key",   ``:word32 # word32``);
44
45val _ = type_abbrev("keysched",
46        ``:word32 # word32 # word32 # word32 # word32 # word32 # word32 #
47           word32 # word32 # word32 # word32 # word32 # word32 # word32 #
48           word32 # word32 # word32 # word32 # word32 # word32 # word32 #
49           word32 # word32 # word32 # word32 # word32 # word32 # word32 #
50           word32 # word32 # word32 # word32 # word32 # word32 # word32 #
51           word32 # word32 # word32 # word32 # word32 # word32 # word32 #
52           word32 # word32``);
53
54val _ = type_abbrev("state", ``:word32#word32#word32#word32#word32#word32``);
55
56(*---------------------------------------------------------------------------*)
57(* Case analysis on blocks and keys.                                         *)
58(*---------------------------------------------------------------------------*)
59
60val FORALL_BLOCK = Q.store_thm
61  ("FORALL_BLOCK",
62    `(!b:block. P b) = !v0 v1 v2 v3. P (v0,v1,v2,v3)`,
63    SIMP_TAC std_ss [FORALL_PROD]);
64
65val FORALL_KEYS = Q.prove
66(`(!x:key. P x) = !k0 k1. P(k0,k1)`,
67  SIMP_TAC std_ss [FORALL_PROD]);
68
69(* --------------------------------------------------------------------------*)
70(*      Rotation operators                                                   *)
71(* --------------------------------------------------------------------------*)
72
73val LeftShift_def = Define
74   `LeftShift (x:word32) (n:word32) = x #<< (w2n n)`;
75
76val RightShift_def = Define
77   `RightShift (x:word32) (n:word32) = x #>> (w2n n)`;
78
79val _ = augment_srw_ss [rewrites [LeftShift_def, RightShift_def]];
80
81val _ = overload_on ("<<<",Term`$LeftShift`);
82val _ = overload_on (">>>",Term`$RightShift`);
83val _ = set_fixity "<<<" (Infixl 625);
84val _ = set_fixity ">>>" (Infixl 625);
85
86(*
87val EX_Shift_Lemma = Q.store_thm
88   ("EX_Shift_Lemma",
89   `!n. w2n n MOD WL < WL`,
90    ARW_TAC [WL_def, HB_def] THEN ARW_TAC [DIVISION]);
91
92val EX_Shift_Inversion = Q.store_thm
93  ("EX_Shift_Inversion",
94  `!s n. (s >>> n <<< n = s) /\ (s <<< n >>> n = s)`,
95  ASSUME_TAC EX_Shift_Lemma THEN
96  REWRITE_TAC [LeftShift_def, RightShift_def] THEN ARW_TAC [SHIFT_Inversion]);
97*)
98
99(* --------------------------------------------------------------------------*)
100(*      One round forward computation and one round backward computation     *)
101(* --------------------------------------------------------------------------*)
102
103(*---------------------------------------------------------------------------*)
104(*  r is the number of rounds                                                *)
105(*---------------------------------------------------------------------------*)
106
107val r_def = Define `r = 20`;
108
109val CompUT_def = Define
110   `CompUT (x:word32) = (x * (x + x + 1w)) #<< 5`;
111
112val FwdRound_def = Define
113  `FwdRound ((a,b,c,d):block) ((k0,k1):key)  =
114        (b,
115         ((c ?? CompUT d) <<< CompUT b) + k1,  (*c = (c xor u <<< t) + k1*)
116         d,
117         ((a ?? CompUT b) <<< CompUT d) + k0)`;
118
119val BwdRound_def = Define
120  `BwdRound ((a,b,c,d):block) ((k0,k1):key)  =  (* NB: (a,b,c,d) = (d,a,b,c) *)
121        (((d - k0) >>> CompUT c) ?? CompUT a,   (* a = ((a-k0) >>> u) xor t  *)
122         a,
123         ((b - k1) >>> CompUT a) ?? CompUT c,   (* c = ((c-k1) >>> t) xor u  *)
124         c)`;
125
126val OneRound_Inversion = Q.store_thm
127  ("OneRound_Inversion",
128  `!b:block k:key. BwdRound (FwdRound b k) k = b`,
129  SIMP_TAC std_ss [FORALL_BLOCK, FORALL_KEYS]
130    THEN SRW_TAC [] [FwdRound_def, BwdRound_def]);
131
132(*---------------------------------------------------------------------------*)
133(* Rotate keys and get a pair of keys from the head of the key schedule      *)
134(*---------------------------------------------------------------------------*)
135
136val ROTKEYS_def =
137 Define
138   `ROTKEYS (k0,k1,k2,k3,k4,k5,k6,k7,k8,k9,k10,k11,k12,
139      k13,k14,k15,k16,k17,k18,k19,k20,k21,k22,k23,k24,k25,k26,k27,
140      k28,k29,k30,k31,k32,k33,k34,k35,k36,k37,k38,k39,k40,k41,k42,k43)
141    =
142     (k2,k3,k4,k5,k6,k7,k8,k9,k10,k11,k12,k13,k14,k15,k16,k17,k18,
143      k19,k20,k21,k22,k23,k24,k25,k26,k27,k28,k29,k30,k31,k32,k33,
144      k34,k35,k36,k37,k38,k39,k40,k41,k42,k43,k0,k1) : keysched`;
145
146val GETKEYS_def =
147 Define
148   `GETKEYS (k0,k1,k2,k3,k4,k5,k6,k7,k8,k9,k10,k11,k12,k13,k14,k15,
149      k16,k17,k18,k19,k20,k21,k22,k23,k24,k25,k26,k27,k28,k29,k30,
150      k31,k32,k33,k34,k35,k36,k37,k38,k39,k40,k41,k42,k43)
151    = (k0,k1):key`;
152
153(*---------------------------------------------------------------------------*)
154(* Pre-Whitening and post-whitening in the encryption and the decryption     *)
155(* Note the difference of the key schedules between Round and InvRound. We   *)
156(* should make sure that corresponding Round and InvRound use the same keys  *)
157(*---------------------------------------------------------------------------*)
158
159val PreWhitening_def = Define
160 `PreWhitening (k:keysched) ((a,b,c,d):block)  =
161            (a, b + FST(GETKEYS(k)), c, d + SND(GETKEYS(k))) : block`;
162
163val PostWhitening_def = Define
164 `PostWhitening  (k:keysched) ((a,b,c,d):block)  =
165            (a + SND(GETKEYS(k)), b, c + SND(GETKEYS(k)), d) : block`;
166
167val InvPreWhitening_def = Define
168 `InvPreWhitening (k:keysched) ((a,b,c,d):block)  =
169            (a - SND(GETKEYS(k)), b, c - SND(GETKEYS(k)), d) : block`;
170
171val InvPostWhitening_def = Define
172 `InvPostWhitening (k:keysched) ((a,b,c,d):block)  =
173            (a, b - FST(GETKEYS(k)), c, d - SND(GETKEYS(k))) : block`;
174
175val Whitening_Inversion = Q.store_thm
176  ("Whitening_Inversion",
177  `!b k. (InvPostWhitening k (PreWhitening k b) = b) /\
178         (InvPreWhitening k (PostWhitening k b) = b)`,
179  SIMP_TAC std_ss [FORALL_BLOCK]
180    THEN SRW_TAC [] [InvPostWhitening_def, PreWhitening_def,
181                     InvPreWhitening_def, PostWhitening_def]);
182
183(*---------------------------------------------------------------------------*)
184(* Round operations in the encryption and the decryption. Slow to define.    *)
185(*---------------------------------------------------------------------------*)
186
187val Round_def =
188 tDefine
189   "Round"
190   `Round n (k:keysched) (b:block) =
191     if n=0
192      then PostWhitening k b
193      else Round (n-1) (ROTKEYS k) (FwdRound b (GETKEYS k))`
194  (WF_REL_TAC `measure FST` THEN RW_TAC arith_ss [ELIM_UNCURRY]);
195
196val Round_ind = fetch "-" "Round_ind";
197
198(*---------------------------------------------------------------------------*)
199(* Note the difference between Round and InvRound -- we should make sure     *)
200(* that PreWhitening and PostWhitening use the same key pair                 *)
201(*---------------------------------------------------------------------------*)
202
203val InvRound_def =
204 tDefine
205   "InvRound"
206   `InvRound n k b =
207      if n=0
208       then InvPreWhitening k b
209       else BwdRound (InvRound (n-1) (ROTKEYS k) b) (GETKEYS k)`
210  (WF_REL_TAC `measure FST` THEN RW_TAC arith_ss [ELIM_UNCURRY]);
211
212
213(*---------------------------------------------------------------------------*)
214(* Encrypt and Decrypt                                                       *)
215(* The number of rounds is 20. It is easy to change it into any value, but in*)
216(* in this case you should redefine the type keysched                        *)
217(*---------------------------------------------------------------------------*)
218
219val RC6_FWD_def =
220 Define
221   `RC6_FWD keys = Round r keys o PreWhitening keys`;
222
223val RC6_BWD_def =
224 Define
225   `RC6_BWD keys = InvPostWhitening keys o InvRound r keys`;
226
227(*---------------------------------------------------------------------------*)
228(* Main lemma                                                                *)
229(*---------------------------------------------------------------------------*)
230
231val [FwdRound] = decls "FwdRound";
232val [BwdRound] = decls "BwdRound";
233
234val RC6_LEMMA = Q.store_thm
235("RC6_LEMMA",
236 `!(plaintext:block) (keys:keysched).
237     RC6_BWD keys (RC6_FWD keys plaintext) = plaintext`,
238   RESTR_EVAL_TAC [FwdRound, BwdRound] THEN
239   RW_TAC std_ss [OneRound_Inversion, Whitening_Inversion]);
240
241(*---------------------------------------------------------------------------*)
242(* Build the keyschedule from a key. This definition is too specific, but    *)
243(* works fine for 128 bit blocks.                                            *)
244(*---------------------------------------------------------------------------*)
245
246val LIST_TO_KEYS_def =
247 Define
248  `(LIST_TO_KEYS [] acc = acc : keysched) /\
249   (LIST_TO_KEYS (h::t)
250      (k0,k1,k2,k3,k4,k5,k6,k7,k8,k9,k10,k11,k12,k13,k14,k15,k16,k17,k18,k19,
251       k20,k21,k22,k23,k24,k25,k26,k27,k28,k29,k30,k31,k32,k33,k34,k35,k36,k37,
252       k38,k39,k40,k41,k42,k43)
253     =
254      LIST_TO_KEYS t
255       (h,k1,k2,k3,k4,k5,k6,k7,k8,k9,k10,k11,k12,k13,k14,k15,k16,k17,k18,k19,
256        k20,k21,k22,k23,k24,k25,k26,k27,k28,k29,k30,k31,k32,k33,k34,k35,k36,
257        k37,k38,k39,k40,k41,k42,k43))`;
258
259val DUMMY_KEYS_def =
260 Define
261  `DUMMY_KEYS =
262     (0w,0w,0w,0w,0w,0w,0w,0w,0w,0w,
263      0w,0w,0w,0w,0w,0w,0w,0w,0w,0w,
264      0w,0w,0w,0w,0w,0w,0w,0w,0w,0w,
265      0w,0w,0w,0w,0w,0w,0w,0w,0w,0w,
266      0w,0w,0w,0w) : keysched`;
267
268val Pw_def = Define `
269    Pw = 0xB7E15163w:word32`;
270
271val Qw_def = Define `
272    Qw = 0x9E3779B9w:word32`;
273
274val init_S_def = Define `
275   (init_S 0 = [Pw]) /\
276   (init_S (SUC n) = (HD (init_S n) + Qw) :: (init_S n))`;
277
278val setKeys_def = Define `
279   (setKeys 0 S1 L a b = []) /\
280   (setKeys (SUC n) S1 L a b =
281     let a = (HD S1 + a + b) #<< 3 in
282     let b = (HD L + a + b) <<< (a+b) in
283         a::setKeys n (TL S1 ++ [a]) (TL L ++ [b]) a b)`;
284
285val mk_keysched_def = Define
286   `mk_keysched(L) = setKeys (r*2+4) (REVERSE(init_S (2*r-3))) L 0w 0w`;
287
288
289val setKeys_length = Q.prove
290 (`!i S1 L a b. i>0 ==>
291        (LENGTH (setKeys i S1 L a b) = SUC(LENGTH (setKeys (i-1) S1 L a b)))`,
292  Induct_on `i` THENL [
293    RW_TAC list_ss [],
294    RW_TAC list_ss [Ntimes setKeys_def 1] THEN
295    Cases_on `i=0` THENL [
296        RW_TAC list_ss [setKeys_def],
297        Q.SUBGOAL_THEN
298         `!i S1 L1 a1 b1 S2 L2 a2 b2.
299             LENGTH (setKeys i S1 L1 a1 b1) = LENGTH (setKeys i S2 L2 a2 b2)`
300        ASSUME_TAC THENL [
301            NTAC 4 (POP_ASSUM (K ALL_TAC)) THEN
302            Induct_on `i` THENL [
303                RW_TAC list_ss [setKeys_def],
304                RW_TAC list_ss [setKeys_def] THEN RW_TAC list_ss [LENGTH]],
305        RW_TAC list_ss []]]]
306  );
307
308(*---------------------------------------------------------------------------*)
309(* Sanity check                                                              *)
310(*---------------------------------------------------------------------------*)
311
312val keysched_length = Q.prove
313 (`!L. LENGTH (mk_keysched L) = r*2+4`,
314    RW_TAC list_ss [mk_keysched_def, r_def] THEN
315    RW_TAC list_ss [setKeys_length] THEN
316    RW_TAC arith_ss [setKeys_def, LENGTH]
317  );
318
319(*---------------------------------------------------------------------------*)
320(* Basic theorem about encryption/decryption                                 *)
321(*---------------------------------------------------------------------------*)
322
323val RC6_def = Define
324 `RC6 key =
325   let keys = LIST_TO_KEYS (mk_keysched key) DUMMY_KEYS
326   in (RC6_FWD keys, RC6_BWD keys)`;
327
328val RC6_CORRECT = Q.store_thm
329  ("RC6_CORRECT",
330   `!key plaintext.
331       ((encrypt,decrypt) = RC6 key)
332       ==>
333       (decrypt (encrypt plaintext) = plaintext)`,
334         RW_TAC std_ss [RC6_def,LET_THM,RC6_LEMMA]);
335
336val _ = export_theory();
337