1open HolKernel Parse boolLib bossLib listTheory rich_listTheory bitTheory 2 markerTheory pairTheory arithmeticTheory wordsTheory wordsLib 3 Serpent_Bitslice_UtilityTheory Serpent_Bitslice_SBoxTheory; 4 5val _ = new_theory "Serpent_Bitslice_KeySchedule"; 6 7(*number of rounds*) 8val R_def = Define `R = 32`; 9 10(* PHI: Constant used in the key schedule *) 11 12val PHI_def = Define `PHI = 0x9e3779b9w : word32`; 13 14val short2longKey_def = Define 15`short2longKey k kl = let nw256 = n2w (k MOD (2**kl)) in 16 nw256 || (1w<<kl) : word256`; 17 18(*used in making preKey*) 19val (makeSubKeyBitSlice_def,makeSubKeyBitSlice_termi) = Defn.tstore_defn( 20Hol_defn "makeSubKeyBitSlice" 21`makeSubKeyBitSlice (w_1::w_2::w_3::w_4::w_5::w_6::w_7::w_8::t) i 22 = let nl =((w_1 ?? w_3 ?? w_5 ?? w_8 ?? PHI ?? (n2w:num->word32) (131-i)) #>> 23 (32-11)) 24 ::(w_1::w_2::w_3::w_4::w_5::w_6::w_7::w_8::t) 25 in 26 if i = 0 27 then nl 28 else makeSubKeyBitSlice nl (i-1)`, 29 WF_REL_TAC `measure SND`); 30 31 32(*reversed preKey*) 33val makeRevPreKey_def = Define 34`makeRevPreKey longKey = let keySlices = word256to32l longKey in 35 myBUTLASTN 8 (makeSubKeyBitSlice keySlices 131)`; 36 37 38val revPreKey2SubKey_def = Define 39`revPreKey2SubKey revPreKey 40 = let w = REVERSE revPreKey 41 in 42 RND03 (EL 0 w, EL 1 w, EL 2 w, EL 3 w):: 43 RND02(EL 4 w, EL 5 w, EL 6 w, EL 7 w):: 44 RND01(EL 8 w, EL 9 w, EL 10 w, EL 11 w):: 45 RND00(EL 12 w, EL 13 w, EL 14 w, EL 15 w):: 46 RND31(EL 16 w, EL 17 w, EL 18 w, EL 19 w):: 47 RND30(EL 20 w, EL 21 w, EL 22 w, EL 23 w):: 48 RND29(EL 24 w, EL 25 w, EL 26 w, EL 27 w):: 49 RND28(EL 28 w, EL 29 w, EL 30 w, EL 31 w):: 50 RND27(EL 32 w, EL 33 w, EL 34 w, EL 35 w):: 51 RND26(EL 36 w, EL 37 w, EL 38 w, EL 39 w):: 52 RND25(EL 40 w, EL 41 w, EL 42 w, EL 43 w):: 53 RND24(EL 44 w, EL 45 w, EL 46 w, EL 47 w):: 54 RND23(EL 48 w, EL 49 w, EL 50 w, EL 51 w):: 55 RND22(EL 52 w, EL 53 w, EL 54 w, EL 55 w):: 56 RND21(EL 56 w, EL 57 w, EL 58 w, EL 59 w):: 57 RND20(EL 60 w, EL 61 w, EL 62 w, EL 63 w):: 58 RND19(EL 64 w, EL 65 w, EL 66 w, EL 67 w):: 59 RND18(EL 68 w, EL 69 w, EL 70 w, EL 71 w):: 60 RND17(EL 72 w, EL 73 w, EL 74 w, EL 75 w):: 61 RND16(EL 76 w, EL 77 w, EL 78 w, EL 79 w):: 62 RND15(EL 80 w, EL 81 w, EL 82 w, EL 83 w):: 63 RND14(EL 84 w, EL 85 w, EL 86 w, EL 87 w):: 64 RND13(EL 88 w, EL 89 w, EL 90 w, EL 91 w):: 65 RND12(EL 92 w, EL 93 w, EL 94 w, EL 95 w):: 66 RND11(EL 96 w, EL 97 w, EL 98 w, EL 99 w):: 67 RND10(EL 100 w, EL 101 w, EL 102 w, EL 103 w):: 68 RND09(EL 104 w, EL 105 w, EL 106 w, EL 107 w):: 69 RND08(EL 108 w, EL 109 w, EL 110 w, EL 111 w):: 70 RND07(EL 112 w, EL 113 w, EL 114 w, EL 115 w):: 71 RND06(EL 116 w, EL 117 w, EL 118 w, EL 119 w):: 72 RND05(EL 120 w, EL 121 w, EL 122 w, EL 123 w):: 73 RND04(EL 124 w, EL 125 w, EL 126 w, EL 127 w):: 74 RND03(EL 128 w, EL 129 w, EL 130 w, EL 131 w)::[]`; 75 76 77val makeKey_def = Define 78`makeKey userKey kl 79 = let longKey = short2longKey userKey kl 80 in 81 let revPreKey = makeRevPreKey longKey 82 in 83 revPreKey2SubKey revPreKey`; 84 85val makeSubKeyBitSliceLength = Q.store_thm( 86"makeSubKeyBitSliceLength", 87`!longKey n. 88 (LENGTH longKey>= 8) 89 ==> 90 (LENGTH (makeSubKeyBitSlice longKey n ) = n+LENGTH longKey+1)`, 91 Induct_on `n` THENL [ 92 FULL_SIMP_TAC list_ss [makeSubKeyBitSlice_def,LENGTH,LET_THM] THEN 93 RW_TAC std_ss [] THEN 94 `?v_1 v_2 v_3 v_4 v_5 v_6 v_7 v_8 t. 95 longKey = (v_1::v_2::v_3::v_4::v_5::v_6::v_7::v_8::t)` 96 by METIS_TAC [listInstGreaterEq8] THEN 97 FULL_SIMP_TAC list_ss [makeSubKeyBitSlice_def] THEN 98 METIS_TAC [LENGTH,SUC_ONE_ADD,ADD_COMM], 99 RW_TAC std_ss [] THEN 100 `?v_1 v_2 v_3 v_4 v_5 v_6 v_7 v_8 t. 101 longKey = (v_1::v_2::v_3::v_4::v_5::v_6::v_7::v_8::t)` 102 by METIS_TAC [listInstGreaterEq8] THEN 103 FULL_SIMP_TAC list_ss [makeSubKeyBitSlice_def] THEN 104 RW_TAC list_ss [] THEN 105 FULL_SIMP_TAC list_ss [Abbrev_def]]); 106 107val makeRevPreKeyLength = Q.store_thm( 108"makeRevPreKeyLength", 109`!userKey. 110 LENGTH (makeRevPreKey userKey) = 132`, 111 RW_TAC std_ss [makeRevPreKey_def,LET_THM] THEN 112 `LENGTH (word256to32l userKey) = 8` by METIS_TAC [word256to32lLength] THEN 113 `LENGTH (word256to32l userKey)>= 8` by RW_TAC arith_ss [] THEN 114 `LENGTH (makeSubKeyBitSlice (word256to32l userKey) 131) = 115 131+LENGTH (word256to32l userKey) +1` 116 by METIS_TAC [makeSubKeyBitSliceLength,LENGTH_REVERSE] THEN 117 `8 <= LENGTH (makeSubKeyBitSlice (word256to32l userKey) 131)` 118 by FULL_SIMP_TAC arith_ss [] THEN 119 FULL_SIMP_TAC list_ss [LENGTH_myBUTLASTN,LENGTH_REVERSE]); 120 121(*only length matters in functional correctness*) 122val makeKeyLength = Q.store_thm( 123"makeKeyLength", 124`!userKey kl. 125 LENGTH (makeKey userKey kl) = 33`, 126 RW_TAC list_ss [makeKey_def,revPreKey2SubKey_def,LET_THM]); 127 128val _ = export_theory(); 129