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