1(* Interative use: 2 quietdec := true; 3 app load ["MARS_SboxTheory","MARS_DataTheory"]; 4 open listTheory wordsTheory MARS_SboxTheory MARS_DataTheory; 5 quietdec := false; 6*) 7 8open HolKernel Parse boolLib bossLib 9 listTheory wordsTheory MARS_SboxTheory MARS_DataTheory; 10 11val _ = new_theory "MARS_keyExpansion"; 12 13(****************************************************************************) 14(****************************************************************************) 15(*------------------Key-Expansion function----------------------------------*) 16(*------------------kr is the number of words in the key bufferck[], 4<=kr<=14*) 17(*------------------K[] is the expaned key array,consisting of 40 words-----*) 18(*------------------T[] is a temporary array, consisting of 15 words--------*) 19(*------------------BB[] is a fixed table of four words---------------------*) 20(****************************************************************************) 21 22 23(*----------Now define some array operations on lists-----------------------*) 24(*----------"sub" returns the element at designated position ---------------*) 25(*----------"update" updates the element at designated position ------------*) 26 27val update_def = Define 28 `(update([], i:num, x) = []) /\ 29 (update(h::t, 0, x) = x::t) /\ 30 (update(h::t, SUC i, x) = h::update(t,i,x))`; 31 32 33val sub_def = Define 34 `(sub(h::t, 0) = h) /\ 35 (sub(h::t, SUC i) = sub (t,i))`; 36 37 38val LENGTH_UPDATE = Q.prove 39 (`!l i x. LENGTH (update(l, i, x)) = LENGTH l`, 40 Induct_on `l` THENL [ 41 RW_TAC list_ss [update_def], 42 Cases_on `i` THEN 43 RW_TAC list_ss [update_def]] 44 ); 45 46(* --------------------------------------------------------------------------*) 47(* some assistant functions *) 48(* --------------------------------------------------------------------------*) 49 50val l8b_def = Define `l8b x = x && 0xffw : word32`; 51val l9b_def = Define `l9b x = x && 0x1ffw : word32`; 52 53 54(*--------------Initialize T[] with the original Key data k[]--------------- *) 55(*----Note that the k[] should be in list form-------------------------------*) 56 57(*-------------------Initialize T[] with key data ---------------------------*) 58val Init_T_rnd = Define 59 `Init_T_rnd i (l:word32 list) k = 60 if i = 0 then [HD l] else 61 if i > k then (Init_T_rnd (i-1) l k) ++ [0w] else 62 if i = k then (Init_T_rnd (i-1) l k) ++ [n2w k] else 63 (Init_T_rnd (i-1) l k) ++ [sub(l, i)]`; 64 65val Init_T_def = Define `Init_T(key_list) = 66 Init_T_rnd 14 key_list (LENGTH key_list)`; 67 68(*--------------Computing 40 words of K[] based on T[]-----------------------*) 69(*--------------Each iteration computes 10 words ----------------------------*) 70 71val (linear_rnd_def, linear_rnd_ind) = Defn.tprove ( 72 Hol_defn "linear_rnd" 73 `linear_rnd i t j = 74 if i > 14 then t else 75 linear_rnd (i+1) 76 (update(t, i, ((sub(t, (i-7) MOD 15) ?? sub(t,(i-2) MOD 15)) #<< 3) ?? 77 (4w * n2w i + n2w j))) j`, 78 WF_REL_TAC `measure ($- 15 o FST)`); 79 80val linear_def = Define 81 `linear (t, j) = linear_rnd 0 t j`; 82 83(* Next stir the array T[ ] using four rounds of type-1 Feistel network *) 84val (stiring_rnd_def, stiring_rnd_ind) = Defn.tprove ( 85 Hol_defn "stiring_rnd" 86 `stiring_rnd i t j = 87 if i > 14 then t else 88 stiring_rnd (i+1) 89 (update(t, i, (sub(t,i) + Sbox(l9b(sub(t, (i-1) MOD 15)))) #<< 9)) j`, 90 WF_REL_TAC `measure ($- 15 o FST)`); 91 92val stiring_step_def = Define 93 `stiring_step (t, j) = stiring_rnd 0 t j`; 94 95val stiring_def = Define 96 `stiring (t, j) = 97 stiring_step(stiring_step(stiring_step(stiring_step(t,j),j),j),j)`; 98 99val store_10_words_def = Define 100 `store_10_words (t) = 101 [sub(t,0); sub(t,4); sub(t,8); sub(t,12); sub(t,1); 102 sub(t,5); sub(t,9); sub(t,13); sub(t,2); sub(t,6)]`; 103 104val Init_K_def = Define 105 `Init_K (t) = 106 let t1 = store_10_words(stiring(linear(t,0),0)) in 107 let t2 = store_10_words(stiring(linear(t1,1),1)) in 108 let t3 = store_10_words(stiring(linear(t2,2),2)) in 109 let t4 = store_10_words(stiring(linear(t3,3),3)) in 110 t1 ++ t2 ++ t3 ++ t4`; 111 112val INIT_K_LENGTH = Q.store_thm 113("INIT_K_LENGTH", 114 `!t. LENGTH (Init_K t) = 40`, 115 RW_TAC list_ss [Init_K_def, store_10_words_def] THEN 116 Q.UNABBREV_TAC `t1` THEN Q.UNABBREV_TAC `t2` THEN Q.UNABBREV_TAC `t3` THEN 117 Q.UNABBREV_TAC `t4` THEN 118 RW_TAC list_ss [LENGTH_APPEND, LENGTH] 119); 120 121 122(*--------------------Modify multiplication keys-----------------------------*) 123 124val BB_def = Define `BB = 125 [0xa4a8d57bw; 0x5b5d193bw; 0xc8a8309bw; 0x73f9a978w] : word32 list`; 126 127val gen_mask_def = Define ` 128 gen_mask(x:word32) = 129 let m = (~x ?? (x >> 1)) && 0x7fffffffw in 130 let m = m && (m >> 1) && (m >> 2) in 131 let m = m && (m >> 3) && (m >> 6) in 132 let m1 = m in 133 let m = m << 1 in 134 let m = m || (m << 1) in 135 let m = m || (m << 2) in 136 let m = m || (m << 4) in 137 let m = m || (m << 1) && (~x) && 0x80000000w 138 in if m1=0w then 0w else m && 0xfffffffcw`; 139 140val mul_rnd_def = Define ` 141 mul_rnd(k:word32 list,i:num) = 142 (* Record the two lowest bits of K[i], by setting j = K[i] & 3, and then 143 consider the word with these two bits set to 1, w = K[i] | 3 *) 144 let j = w2n (sub(k,i) && 0x3w) in 145 let w = sub(k,i) || 0x3w in 146 147 let m = gen_mask(w) in 148 149 let r = w2n(sub(k,i-1) && 0x1fw) in 150 let p = sub(BB,j) #<< r 151 in update(k, i, w ?? (p && m))`; 152 153val mul_def = Define ` 154 mul (k) = mul_rnd(mul_rnd(mul_rnd(mul_rnd(mul_rnd(mul_rnd(mul_rnd(mul_rnd 155 (mul_rnd(mul_rnd(mul_rnd(mul_rnd(mul_rnd(mul_rnd(mul_rnd(mul_rnd(k,35), 156 33),31),29),27),25),23),21),19),17),15),13),11),9),7),5)`; 157 158 159val MUL_RND_LENGTH = Q.store_thm 160("MUL_RND_LENGTH", 161 `!k i. LENGTH (mul_rnd (k, i)) = LENGTH k`, 162 SIMP_TAC std_ss [mul_rnd_def, LET_THM] 163 THEN RW_TAC list_ss [LENGTH_UPDATE] 164); 165 166 167val key_expansion_def = Define ` 168 key_expansion(k) = mul(Init_K(Init_T(k)))`; 169 170 171val KEY_EXPANSION_LENGTH = Q.store_thm 172("KEY_EXPANSION_LENGTH", 173 `!k. LENGTH (key_expansion k) = 40`, 174 SIMP_TAC std_ss [key_expansion_def, mul_def] 175 THEN RW_TAC list_ss [INIT_K_LENGTH, MUL_RND_LENGTH] 176); 177 178 179val _ = export_theory(); 180