1(* MARS Block Cipher 2 -- implemented in HOL 3 4 This is a HOL implementation of the encryption algorithm: 5 MARS by IBM 6 which is a candidate algorithm in the Advanced Encryption Standard 7 For detailed information about MARS, please refer to 8 http://www.research.ibm.com/security/mars.html 9 in which algorithm specification, Security and performance evaluation, 10 etc. could be found. 11*) 12 13 14(* For interactive work 15 quietdec := true; 16 app load ["wordsLib","MARS_SboxTheory","MARS_keyExpansionTheory"]; 17 open arithmeticTheory wordsLib pairTheory listTheory 18 MARS_SboxTheory MARS_keyExpansionTheory MARS_DataTheory; 19 quietdec := false; 20*) 21 22 open HolKernel Parse boolLib bossLib 23 arithmeticTheory wordsTheory wordsLib pairTheory listTheory 24 MARS_SboxTheory MARS_keyExpansionTheory MARS_DataTheory; 25 26(*---------------------------------------------------------------------------*) 27(* Make bindings to pre-existing stuff *) 28(*---------------------------------------------------------------------------*) 29 30val RESTR_EVAL_TAC = computeLib.RESTR_EVAL_TAC; 31val ARW_TAC = RW_TAC arith_ss; 32 33(*---------------------------------------------------------------------------*) 34(* Create the theory. *) 35(*---------------------------------------------------------------------------*) 36 37val _ = new_theory "MARS"; 38 39(*---------------------------------------------------------------------------*) 40(*-------------Forward round used by the encrypting function-----------------*) 41(*---------------------------------------------------------------------------*) 42 43val E_function_def = Define 44 `E_function(A, key1, key2) = 45 let R = ((A #<< 13) * key2) #<< 10 in 46 let M = (A + key1) #<< w2n ((R #>> 5) ?? 0x1fw) in 47 let L = (Sbox(l9b(A+key1)) ?? (R #>> 5) ?? R) #<< w2n (R ?? 0x1fw) 48 in (L,M,R)`; 49 50val en_f_rnd_def = Define 51 `en_f_rnd ((A,B,C,D),i) = 52 let B = (B ?? Sbox0(l8b(A))) + Sbox1(l8b(A #>> 8)) in 53 let C = C + Sbox0(l8b(A #>> 16)) in 54 let D = D ?? Sbox1(l8b(A #>> 24)) in 55 let A = (A #>> 24) + 56 ((if (i=5) \/ (i=1) then B else 0w) + 57 (if (i=4) \/ (i=0) then D else 0w)) 58 in (B,C,D,A) : block`; 59 60(*First add subkeys to data, then do eight rounds of forward mixing*) 61val (f_mix_def, f_mix_ind) = Defn.tprove ( 62 Hol_defn "f_mix" 63 `f_mix n (b:block) = 64 if n=0 then b 65 else f_mix (n-1) (en_f_rnd(b,n))`, 66 WF_REL_TAC `measure FST` THEN REPEAT PairRules.PGEN_TAC THEN DECIDE_TAC); 67 68val en_f_mix_def = Define ` 69 en_f_mix((A,B,C,D),k) = f_mix 8 ( 70 A+FST(GETKEYS(k)), B+SND(GETKEYS(k)), C+FST(GETKEYS(ROTKEYS(k))), 71 D+SND(GETKEYS(ROTKEYS(k))))`; 72 73val en_core_rnd_def = Define ` 74 en_core_rnd ((A,B,C,D):block, k:keysched, i) = 75 let (out1,out2,out3) = E_function(A,FST(GETKEYS(k)),SND(GETKEYS(k))) in 76 let A = A #<< 13 in 77 let C = C + out2 in 78 let B = if i<8 then B+out1 else B ?? out3 in 79 let D = if i<8 then D ?? out3 else D + out1 80 in (B, C, D, A):block`; 81 82val (core_def, core_ind) = Defn.tprove ( 83 Hol_defn "core" 84 `core i (b:block) (k:keysched) = 85 if i = 0 then b 86 else core (i-1) (en_core_rnd(b,k,i)) (ROTKEYS(k))`, 87 WF_REL_TAC `measure FST` THEN REPEAT PairRules.PGEN_TAC THEN DECIDE_TAC); 88 89val en_core_def = Define ` 90 en_core (b:block,k:keysched) = core 16 b k`; 91 92val en_b_rnd_def = Define ` 93 en_b_rnd ((A,B,C,D),i) = 94 let A = if (i=2) \/ (i=6) then A - D else A in 95 let A = if (i=3) \/ (i=7) then A - B else A in 96 let B = B ?? Sbox1(l8b(A)) in 97 let C = C - Sbox0(l8b(A #>> 24)) in 98 let D = (D - Sbox1(l8b(A #>> 16))) ?? Sbox0(l8b(A #>> 8)) in 99 let A = A #<< 24 100 in (B,C,D,A) : block`; 101 102(*Do eight rounds of backwards mixing*) 103val (b_mix_def, b_mix_ind) = Defn.tprove ( 104 Hol_defn "b_mix" 105 `b_mix i (b:block) (k:keysched) = 106 if i = 0 then b 107 else b_mix (i-1) (en_b_rnd(b,i)) k`, 108 WF_REL_TAC `measure FST` THEN REPEAT PairRules.PGEN_TAC THEN DECIDE_TAC); 109 110val PostWhitening_def = Define ` 111 PostWhitening ((A,B,C,D),k) = ( 112 A-FST(GETKEYS(k)), B-SND(GETKEYS(k)), C-FST(GETKEYS(ROTKEYS(k))), 113 D-SND(GETKEYS(ROTKEYS(k)))):block`; 114 115val en_b_mix_def = Define ` 116 en_b_mix(b:block,k:keysched) = PostWhitening(b_mix 8 b k,k)`; 117 118val _ = save_thm ("f_mix_def", f_mix_def); 119val _ = save_thm ("f_mix_ind", f_mix_ind); 120val _ = save_thm ("core_def", core_def); 121val _ = save_thm ("core_ind", core_ind); 122val _ = save_thm ("b_mix_def", b_mix_def); 123val _ = save_thm ("b_mix_ind", b_mix_ind); 124 125(*---------------------------------------------------------------------------*) 126(*-------------Backward round used by the decrypting function----------------*) 127(*---------------------------------------------------------------------------*) 128val de_f_rnd_def = Define 129 `de_f_rnd ((A,B,C,D),i) = 130 let (A,B,C,D) = (D #>> 24, A, B, C) in 131 let D = (D ?? Sbox0(l8b(A #>> 8))) + Sbox1(l8b(A #>> 16)) in 132 let C = C + Sbox0(l8b(A #>> 24)) in 133 let B = B ?? Sbox1(l8b(A)) in 134 let A = if (i=2) \/ (i=6) then A + D else A in 135 let A = if (i=3) \/ (i=7) then A + B else A in 136 (A, B, C, D) : block`; 137 138val (inv_f_mix_def, inv_f_mix_ind) = Defn.tprove ( 139 Hol_defn "inv_f_mix" 140 `inv_f_mix n (b:block) = 141 if n=0 then b 142 else de_f_rnd(inv_f_mix (n-1) b,n)`, 143 WF_REL_TAC `measure FST` THEN REPEAT PairRules.PGEN_TAC THEN DECIDE_TAC); 144 145val PreWhitening_def = Define ` 146 PreWhitening ((A,B,C,D),k) = ( 147 A+FST(GETKEYS(k)), B+SND(GETKEYS(k)), C+FST(GETKEYS(ROTKEYS(k))), 148 D+SND(GETKEYS(ROTKEYS(k)))):block`; 149 150val de_f_mix_def = Define ` 151 de_f_mix(b,k) = inv_f_mix 8 (PreWhitening(b,k))`; 152 153val de_core_rnd_def = Define ` 154 de_core_rnd ((A,B,C,D):block, k:keysched, i) = 155 let (A,B,C,D) = (D #>> 13,A,B,C) in 156 let (out1,out2,out3) = E_function(A,FST(GETKEYS(k)),SND(GETKEYS(k))) in 157 let C = C - out2 in 158 let B = if i<8 then B-out1 else B ?? out3 in 159 let D = if i<8 then D ?? out3 else D - out1 160 in (A, B, C, D)`; 161 162val (inv_core_def, inv_core_ind) = Defn.tprove ( 163 Hol_defn "inv_core" 164 `inv_core i (b:block) (k:keysched) = 165 if i = 0 then b 166 else de_core_rnd(inv_core (i-1) b (ROTKEYS(k)),k,i)`, 167 WF_REL_TAC `measure FST` THEN REPEAT PairRules.PGEN_TAC THEN DECIDE_TAC); 168 169val de_core_def = Define ` 170 de_core (b:block,k:keysched) = inv_core 16 b k`; 171 172val de_b_rnd_def = Define ` 173 de_b_rnd ((A,B,C,D),i) = 174 let (A,B,C,D) = (D,A,B,C) in 175 let A = A - ((if (i=5) \/ (i=1) then B else 0w) + 176 (if (i=4) \/ (i=0) then D else 0w)) in 177 let A = A #<< 24 in 178 let D = D ?? Sbox1(l8b(A #>> 24)) in 179 let C = C - Sbox0(l8b(A #>> 16)) in 180 let B = (B - Sbox1(l8b(A #>> 8))) ?? Sbox0(l8b(A)) 181 in (A,B,C,D):block`; 182 183(*Do eight rounds of backwards mixing*) 184val (inv_b_mix_def, inv_b_mix_ind) = Defn.tprove ( 185 Hol_defn "inv_b_mix" 186 `inv_b_mix i (b:block) (k:keysched) = 187 if i = 0 then b 188 else de_b_rnd(inv_b_mix (i-1) b k,i)`, 189 WF_REL_TAC `measure FST` THEN REPEAT PairRules.PGEN_TAC THEN DECIDE_TAC); 190 191val de_b_mix_def = Define ` 192 de_b_mix (b:block,k:keysched) = 193 let (A,B,C,D) = inv_b_mix 8 b k in 194 (A-FST(GETKEYS(k)), B-SND(GETKEYS(k)), 195 C-FST(GETKEYS(ROTKEYS(k))), D-SND(GETKEYS(ROTKEYS(k)))) 196 `; 197 198val _ = save_thm ("inv_f_mix_def", inv_f_mix_def); 199val _ = save_thm ("inv_f_mix_ind", inv_f_mix_ind); 200val _ = save_thm ("inv_core_def", inv_core_def); 201val _ = save_thm ("inv_core_ind", inv_core_ind); 202val _ = save_thm ("inv_b_mix_def", inv_b_mix_def); 203val _ = save_thm ("inv_b_mix_ind", inv_b_mix_ind); 204 205(*---------------------------------------------------------------------------*) 206(*-------------Forward and backward round operation inversion lemmas---------*) 207(*---------------------------------------------------------------------------*) 208 209(* -------------------First comes the foward mixing operations --------------*) 210val Fwd_Mix_Inversion = Q.store_thm 211 ("Fwd_Mix_Inversion", 212 `!b i. de_b_rnd(en_f_rnd(b,i),i) = b`, 213 SIMP_TAC std_ss [FORALL_BLOCK, en_f_rnd_def, de_b_rnd_def, LET_THM] 214 THEN SRW_TAC [] [WORD_LEFT_ADD_DISTRIB]); 215 216val [en_f_rnd] = decls "en_f_rnd"; 217val [de_b_rnd] = decls "de_b_rnd"; 218 219val Fwd_Mix_LEMMA = Q.store_thm 220("Fwd_Mix_LEMMA", 221 `!b:block k:keysched. de_b_mix(en_f_mix(b,k),k) = b`, 222 SIMP_TAC std_ss [FORALL_BLOCK] 223 THEN RESTR_EVAL_TAC [en_f_rnd, de_b_rnd] 224 THEN SRW_TAC [] [Fwd_Mix_Inversion]); 225 226(* ------------------Then the keyed transformation operations ---------------*) 227val PBETA_ss = simpLib.conv_ss 228 {name="PBETA",trace = 3,conv=K (K PairRules.PBETA_CONV), 229 key = SOME([],``(\(x:'a,y:'b). s1) s2:'c``)}; 230 231val Core_Inversion = Q.store_thm 232 ("Core_Inversion", 233 `!b k i. de_core_rnd(en_core_rnd(b,k,i),k,i) = b`, 234 SIMP_TAC std_ss [FORALL_BLOCK] 235 THEN SRW_TAC [] [en_core_rnd_def,de_core_rnd_def, LET_THM, UNCURRY]); 236 237val [en_core_rnd] = decls "en_core_rnd"; 238val [de_core_rnd] = decls "de_core_rnd"; 239 240val Keyed_Trans_LEMMA = Q.store_thm 241("Keyed_Trans_LEMMA", 242 `!b:block k:keysched. de_core(en_core(b,k),k) = b`, 243 SIMP_TAC std_ss [FORALL_BLOCK] 244 THEN RESTR_EVAL_TAC [en_core_rnd, de_core_rnd] 245 THEN RW_TAC std_ss [Core_Inversion]); 246 247(* -------------------Finally the backward mixing operations ----------------*) 248val Bwd_Mix_Inversion = Q.store_thm 249 ("Bwd_Mix_Inversion", 250 `!b i. de_f_rnd(en_b_rnd(b,i),i) = b`, 251 SIMP_TAC std_ss [FORALL_BLOCK, en_b_rnd_def, de_f_rnd_def, LET_THM] THEN 252 SRW_TAC [][wordsTheory.word_rol_def]); 253 254val Whitening_Inversion = Q.store_thm 255 ("Whitening_Inversion", 256 `!b k. PreWhitening(PostWhitening(b,k),k) = b`, 257 SIMP_TAC std_ss [FORALL_BLOCK] 258 THEN SRW_TAC [] [PreWhitening_def, PostWhitening_def]); 259 260val [en_b_rnd] = decls "en_b_rnd"; 261val [de_f_rnd] = decls "de_f_rnd"; 262 263val Bwd_Mix_LEMMA = Q.store_thm 264("Bwd_Mix_LEMMA", 265 `!b:block k:keysched. de_f_mix(en_b_mix(b,k),k) = b`, 266 SIMP_TAC std_ss [FORALL_BLOCK] THEN RESTR_EVAL_TAC [en_b_rnd, de_f_rnd] 267 THEN RW_TAC std_ss [Whitening_Inversion, Bwd_Mix_Inversion]); 268 269(*---------------------------------------------------------------------------*) 270(* Encrypt and Decrypt *) 271(*---------------------------------------------------------------------------*) 272val MARSEncrypt_def = Define ` 273 MARSEncrypt k b = en_b_mix( 274 en_core(en_f_mix(b,k),ROTKEYS(ROTKEYS(k))), 275 ROTKEYS18(k))`; 276 277val MARSDecrypt_def = Define ` 278 MARSDecrypt k b = de_b_mix( 279 de_core(de_f_mix(b,ROTKEYS18(k)), ROTKEYS(ROTKEYS(k))), k)`; 280 281(*---------------------------------------------------------------------------*) 282(* Main lemma *) 283(*---------------------------------------------------------------------------*) 284val MARS_LEMMA = Q.store_thm 285("MARS_LEMMA", 286 `!(plaintext:block) (keys:keysched). 287 MARSDecrypt keys (MARSEncrypt keys plaintext) = plaintext`, 288 RW_TAC std_ss [MARSEncrypt_def,MARSDecrypt_def] THEN 289 RW_TAC std_ss [Fwd_Mix_LEMMA, Keyed_Trans_LEMMA, Bwd_Mix_LEMMA]); 290 291(*---------------------------------------------------------------------------*) 292(* Sanity check *) 293(*---------------------------------------------------------------------------*) 294val keysched_length = Q.prove 295 (`!k. LENGTH (key_expansion k) = 40`, 296 SIMP_TAC std_ss [key_expansion_def, mul_def] 297 THEN RW_TAC list_ss [INIT_K_LENGTH, MUL_RND_LENGTH]); 298 299(*---------------------------------------------------------------------------*) 300(* Basic theorem about encryption/decryption *) 301(*---------------------------------------------------------------------------*) 302val MARS_def = Define 303 `MARS (key) = 304 let keys = LIST_TO_KEYS (key_expansion(key)) DUMMY_KEYS 305 in (MARSEncrypt keys, MARSDecrypt keys)`; 306 307val MARS_CORRECT = Q.store_thm 308 ("MARS_CORRECT", 309 `!key plaintext. 310 ((encrypt,decrypt) = MARS key) 311 ==> 312 (decrypt (encrypt plaintext) = plaintext)`, 313 RW_TAC std_ss [MARS_def,LET_THM,MARS_LEMMA]); 314 315val _ = export_theory(); 316