1(* Serpent optimized cipher 2 This is an Standard ML implementation of the optimized Serpent encryption algorithm, 3 which is a candidate in Advanced Encryption Standard. 4 For detailed information about MARS, please refer to 5 http://www.cl.cam.ac.uk/~rja14/serpent.html 6*) 7 8open HolKernel Parse boolLib bossLib listTheory rich_listTheory bitTheory 9 wordsTheory wordsLib pairTheory arithmeticTheory 10 Serpent_Bitslice_UtilityTheory Serpent_Bitslice_SBoxTheory; 11 12val _ = new_theory "Serpent_Bitslice"; 13 14(*****************TRANSFORMATION*******************************) 15 16val transform_def = Define` 17 transform (x0:word32, x1:word32, x2:word32, x3:word32)= 18 (let y0 = x0 #>> (32 - 13) in 19 let y2 = x2 #>> (32 - 3) in 20 let y1 = (x1 ?? y0) ?? y2 in 21 let y3 = (x3 ?? y2) ?? y0 << 3 in 22 let y11 = y1 #>> (32 - 1) in 23 let y31 = y3 #>> (32 - 7) in 24 let y01 = (y0 ?? y11) ?? y31 in 25 let y21 = (y2 ?? y31) ?? y11 << 7 in 26 let y02 = y01 #>> (32 - 5) in 27 let y22 = y21 #>> (32 - 22) in 28 (y02,y11,y22,y31))`; 29 30val inv_transform_def = Define` 31 inv_transform (x0:word32, x1:word32, x2:word32, x3:word32)= 32 (let y2 = x2 #>> 22 in 33 let y0 = x0 #>> 5 in 34 let y21 = (y2 ?? x3) ?? x1 << 7 in 35 let y01 = (y0 ?? x1) ?? x3 in 36 let y3 = x3 #>> 7 in 37 let y1 = x1 #>> 1 in 38 let y31 = (y3 ?? y21) ?? y01 << 3 in 39 let y11 = (y1 ?? y01) ?? y21 in 40 let y22 = y21 #>> 3 in 41 let y02 = y01 #>> 13 in 42 (y02,y11,y22,y31))`; 43 44val transform_THM = Q.store_thm ( 45"transform_THM", 46`!v. inv_transform (transform v) = v`, 47 SIMP_TAC std_ss [FORALL_PROD,transform_def,inv_transform_def,LET_THM] THEN 48 SRW_TAC [] []); 49 50(********************************APPLYING KEYING**************************) 51val keying_def = Define 52`keying (x0:word32, x1:word32, x2:word32, x3:word32) 53 (subkey0:word32, subkey1:word32, subkey2:word32, subkey3:word32) 54 = (x0 ?? subkey0, x1 ?? subkey1, x2 ?? subkey2,x3 ?? subkey3)`; 55 56val keying_THM = Q.store_thm ( 57"keying_THM", 58`!d sk. 59 keying (keying d sk) sk = d`, 60 SIMP_TAC std_ss [FORALL_PROD,keying_def] THEN SRW_TAC [] []); 61 62(**************************BLOCK ENCRYPTION******************************) 63val f_def = Define `f a (op,sk) = op a sk`; 64 65val encryptRnd00_def = Define 66 `encryptRnd00 a b = transform (RND00 (keying a b))`; 67val encryptRnd01_def = Define 68 `encryptRnd01 a b = transform (RND01 (keying a b))`; 69val encryptRnd02_def = Define 70 `encryptRnd02 a b = transform (RND02 (keying a b))`; 71val encryptRnd03_def = Define 72 `encryptRnd03 a b = transform (RND03 (keying a b))`; 73val encryptRnd04_def = Define 74 `encryptRnd04 a b = transform (RND04 (keying a b))`; 75val encryptRnd05_def = Define 76 `encryptRnd05 a b = transform (RND05 (keying a b))`; 77val encryptRnd06_def = Define 78 `encryptRnd06 a b = transform (RND06 (keying a b))`; 79val encryptRnd07_def = Define 80 `encryptRnd07 a b = transform (RND07 (keying a b))`; 81val encryptRnd08_def = Define 82 `encryptRnd08 a b = transform (RND08 (keying a b))`; 83val encryptRnd09_def = Define 84 `encryptRnd09 a b = transform (RND09 (keying a b))`; 85val encryptRnd10_def = Define 86 `encryptRnd10 a b = transform (RND10 (keying a b))`; 87val encryptRnd11_def = Define 88 `encryptRnd11 a b = transform (RND11 (keying a b))`; 89val encryptRnd12_def = Define 90 `encryptRnd12 a b = transform (RND12 (keying a b))`; 91val encryptRnd13_def = Define 92 `encryptRnd13 a b = transform (RND13 (keying a b))`; 93val encryptRnd14_def = Define 94 `encryptRnd14 a b = transform (RND14 (keying a b))`; 95val encryptRnd15_def = Define 96 `encryptRnd15 a b = transform (RND15 (keying a b))`; 97val encryptRnd16_def = Define 98 `encryptRnd16 a b = transform (RND16 (keying a b))`; 99val encryptRnd17_def = Define 100 `encryptRnd17 a b = transform (RND17 (keying a b))`; 101val encryptRnd18_def = Define 102 `encryptRnd18 a b = transform (RND18 (keying a b))`; 103val encryptRnd19_def = Define 104 `encryptRnd19 a b = transform (RND19 (keying a b))`; 105val encryptRnd20_def = Define 106 `encryptRnd20 a b = transform (RND20 (keying a b))`; 107val encryptRnd21_def = Define 108 `encryptRnd21 a b = transform (RND21 (keying a b))`; 109val encryptRnd22_def = Define 110 `encryptRnd22 a b = transform (RND22 (keying a b))`; 111val encryptRnd23_def = Define 112 `encryptRnd23 a b = transform (RND23 (keying a b))`; 113val encryptRnd24_def = Define 114 `encryptRnd24 a b = transform (RND24 (keying a b))`; 115val encryptRnd25_def = Define 116 `encryptRnd25 a b = transform (RND25 (keying a b))`; 117val encryptRnd26_def = Define 118 `encryptRnd26 a b = transform (RND26 (keying a b))`; 119val encryptRnd27_def = Define 120 `encryptRnd27 a b = transform (RND27 (keying a b))`; 121val encryptRnd28_def = Define 122 `encryptRnd28 a b = transform (RND28 (keying a b))`; 123val encryptRnd29_def = Define 124 `encryptRnd29 a b = transform (RND29 (keying a b))`; 125val encryptRnd30_def = Define 126 `encryptRnd30 a b = transform (RND30 (keying a b))`; 127val encryptRnd31_1_def = Define 128 `encryptRnd31_1 a b31 = RND31 (keying a b31)`; 129val encryptRnd31_2_def = Define 130 `encryptRnd31_2 a b32 = keying a b32`; 131 132val decryptRnd00_1_def = Define 133 `decryptRnd00_1 a b32 = keying a b32`; 134val decryptRnd00_2_def = Define 135 `decryptRnd00_2 a b31 = keying (InvRND31 a) b31`; 136val decryptRnd01_def = Define 137 `decryptRnd01 a b = keying (InvRND30 (inv_transform a)) b`; 138val decryptRnd02_def = Define 139 `decryptRnd02 a b = keying (InvRND29 (inv_transform a)) b`; 140val decryptRnd03_def = Define 141 `decryptRnd03 a b = keying (InvRND28 (inv_transform a)) b`; 142val decryptRnd04_def = Define 143 `decryptRnd04 a b = keying (InvRND27 (inv_transform a)) b`; 144val decryptRnd05_def = Define 145 `decryptRnd05 a b = keying (InvRND26 (inv_transform a)) b`; 146val decryptRnd06_def = Define 147 `decryptRnd06 a b = keying (InvRND25 (inv_transform a)) b`; 148val decryptRnd07_def = Define 149 `decryptRnd07 a b = keying (InvRND24 (inv_transform a)) b`; 150val decryptRnd08_def = Define 151 `decryptRnd08 a b = keying (InvRND23 (inv_transform a)) b`; 152val decryptRnd09_def = Define 153 `decryptRnd09 a b = keying (InvRND22 (inv_transform a)) b`; 154val decryptRnd10_def = Define 155 `decryptRnd10 a b = keying (InvRND21 (inv_transform a)) b`; 156val decryptRnd11_def = Define 157 `decryptRnd11 a b = keying (InvRND20 (inv_transform a)) b`; 158val decryptRnd12_def = Define 159 `decryptRnd12 a b = keying (InvRND19 (inv_transform a)) b`; 160val decryptRnd13_def = Define 161 `decryptRnd13 a b = keying (InvRND18 (inv_transform a)) b`; 162val decryptRnd14_def = Define 163 `decryptRnd14 a b = keying (InvRND17 (inv_transform a)) b`; 164val decryptRnd15_def = Define 165 `decryptRnd15 a b = keying (InvRND16 (inv_transform a)) b`; 166val decryptRnd16_def = Define 167 `decryptRnd16 a b = keying (InvRND15 (inv_transform a)) b`; 168val decryptRnd17_def = Define 169 `decryptRnd17 a b = keying (InvRND14 (inv_transform a)) b`; 170val decryptRnd18_def = Define 171 `decryptRnd18 a b = keying (InvRND13 (inv_transform a)) b`; 172val decryptRnd19_def = Define 173 `decryptRnd19 a b = keying (InvRND12 (inv_transform a)) b`; 174val decryptRnd20_def = Define 175 `decryptRnd20 a b = keying (InvRND11 (inv_transform a)) b`; 176val decryptRnd21_def = Define 177 `decryptRnd21 a b = keying (InvRND10 (inv_transform a)) b`; 178val decryptRnd22_def = Define 179 `decryptRnd22 a b = keying (InvRND09 (inv_transform a)) b`; 180val decryptRnd23_def = Define 181 `decryptRnd23 a b = keying (InvRND08 (inv_transform a)) b`; 182val decryptRnd24_def = Define 183 `decryptRnd24 a b = keying (InvRND07 (inv_transform a)) b`; 184val decryptRnd25_def = Define 185 `decryptRnd25 a b = keying (InvRND06 (inv_transform a)) b`; 186val decryptRnd26_def = Define 187 `decryptRnd26 a b = keying (InvRND05 (inv_transform a)) b`; 188val decryptRnd27_def = Define 189 `decryptRnd27 a b = keying (InvRND04 (inv_transform a)) b`; 190val decryptRnd28_def = Define 191 `decryptRnd28 a b = keying (InvRND03 (inv_transform a)) b`; 192val decryptRnd29_def = Define 193 `decryptRnd29 a b = keying (InvRND02 (inv_transform a)) b`; 194val decryptRnd30_def = Define 195 `decryptRnd30 a b = keying (InvRND01 (inv_transform a)) b`; 196val decryptRnd31_def = Define 197 `decryptRnd31 a b = keying (InvRND00 (inv_transform a)) b`; 198 199val encryptSchedule_def = Define 200`encryptSchedule = encryptRnd00::encryptRnd01::encryptRnd02::encryptRnd03:: 201 encryptRnd04::encryptRnd05::encryptRnd06::encryptRnd07:: 202 encryptRnd08::encryptRnd09::encryptRnd10::encryptRnd11:: 203 encryptRnd12::encryptRnd13::encryptRnd14::encryptRnd15:: 204 encryptRnd16::encryptRnd17::encryptRnd18::encryptRnd19:: 205 encryptRnd20::encryptRnd21::encryptRnd22::encryptRnd23:: 206 encryptRnd24::encryptRnd25::encryptRnd26::encryptRnd27:: 207 encryptRnd28::encryptRnd29::encryptRnd30::encryptRnd31_1::encryptRnd31_2::[]`; 208 209 210val decryptSchedule_def = Define 211`decryptSchedule = decryptRnd00_1::decryptRnd00_2::decryptRnd01:: 212 decryptRnd02::decryptRnd03:: 213 decryptRnd04::decryptRnd05::decryptRnd06::decryptRnd07:: 214 decryptRnd08::decryptRnd09::decryptRnd10::decryptRnd11:: 215 decryptRnd12::decryptRnd13::decryptRnd14::decryptRnd15:: 216 decryptRnd16::decryptRnd17::decryptRnd18::decryptRnd19:: 217 decryptRnd20::decryptRnd21::decryptRnd22::decryptRnd23:: 218 decryptRnd24::decryptRnd25::decryptRnd26::decryptRnd27:: 219 decryptRnd28::decryptRnd29::decryptRnd30::decryptRnd31::[]`; 220 221 222val serpent_encrypt_def = Define 223 `serpent_encrypt plaintext subkeys = 224 let opKey = ZIP (encryptSchedule, subkeys) 225 in 226 FOLDL f plaintext opKey`; 227 228val serpent_decrypt_def = Define 229 `serpent_decrypt ciphertext subkeys = 230 let opKey = ZIP (decryptSchedule, REVERSE subkeys) 231 in 232 FOLDL f ciphertext opKey`; 233 234(*********************FUNCTIONAL CORRECTNESS********************) 235 236val serpent_THM = Q.store_thm( 237"serpent_THM", 238`!pt sk. 239 (LENGTH sk = 33) 240 ==> 241 (serpent_decrypt (serpent_encrypt pt sk) sk = pt)`, 242 RW_TAC list_ss [serpent_decrypt_def,serpent_encrypt_def,LET_THM] THEN 243 `?v_0 v_1 v_2 v_3 v_4 v_5 v_6 v_7 v_8 v_9 v_10 v_11 244 v_12 v_13 v_14 v_15 v_16 v_17 v_18 v_19 v_20 v_21 v_22 245 v_23 v_24 v_25 v_26 v_27 v_28 v_29 v_30 v_31 v_32. 246 sk =[v_0; v_1; v_2; v_3; v_4; v_5; v_6; v_7; v_8; v_9; v_10; v_11; 247 v_12; v_13; v_14; v_15; v_16; v_17; v_18; v_19; v_20; v_21; v_22; 248 v_23; v_24; v_25; v_26; v_27; v_28; v_29; v_30; v_31; v_32]` 249 by METIS_TAC [listInstEq33] THEN 250 RW_TAC list_ss [encryptSchedule_def, decryptSchedule_def,f_def, 251 encryptRnd00_def,encryptRnd01_def,encryptRnd02_def,encryptRnd03_def, 252 encryptRnd04_def,encryptRnd05_def,encryptRnd06_def,encryptRnd07_def, 253 encryptRnd08_def,encryptRnd09_def,encryptRnd10_def,encryptRnd11_def, 254 encryptRnd12_def,encryptRnd13_def,encryptRnd14_def,encryptRnd15_def, 255 encryptRnd16_def,encryptRnd17_def,encryptRnd18_def,encryptRnd19_def, 256 encryptRnd20_def,encryptRnd21_def,encryptRnd22_def,encryptRnd23_def, 257 encryptRnd24_def,encryptRnd25_def,encryptRnd26_def,encryptRnd27_def, 258 encryptRnd28_def,encryptRnd29_def,encryptRnd30_def,encryptRnd31_1_def, 259 encryptRnd31_2_def, 260 decryptRnd00_1_def,decryptRnd00_2_def,decryptRnd01_def,decryptRnd02_def, 261 decryptRnd03_def,decryptRnd04_def,decryptRnd05_def,decryptRnd06_def, 262 decryptRnd07_def,decryptRnd08_def,decryptRnd09_def,decryptRnd10_def, 263 decryptRnd11_def,decryptRnd12_def,decryptRnd13_def,decryptRnd14_def, 264 decryptRnd15_def,decryptRnd16_def,decryptRnd17_def,decryptRnd18_def, 265 decryptRnd19_def,decryptRnd20_def,decryptRnd21_def,decryptRnd22_def, 266 decryptRnd23_def,decryptRnd24_def,decryptRnd25_def,decryptRnd26_def, 267 decryptRnd27_def,decryptRnd28_def,decryptRnd29_def,decryptRnd30_def, 268 decryptRnd31_def, 269 270 RND00_THM,RND01_THM,RND02_THM,RND03_THM, 271 RND04_THM,RND05_THM,RND06_THM,RND07_THM, 272 RND08_THM,RND09_THM,RND10_THM,RND11_THM, 273 RND12_THM,RND13_THM,RND14_THM,RND15_THM, 274 RND16_THM,RND17_THM,RND18_THM,RND19_THM, 275 RND20_THM,RND21_THM,RND22_THM,RND23_THM, 276 RND24_THM,RND25_THM,RND26_THM,RND27_THM, 277 RND28_THM,RND29_THM,RND30_THM,RND31_THM, 278 keying_THM,transform_THM]); 279 280val _ = export_theory(); 281