1app load ["word16Lib", "metisLib", "intLib"]; 2quietdec := true; 3open word16Lib word16Theory metisLib pairTheory intLib integerTheory; 4quietdec := false; 5 6new_constant ("minv", ``:word16->word16``); 7val minv_axiom = new_axiom("minv_axiom", ``!x. x * (minv x) = 1w``); 8 9(*- security stuff start here -*) 10(*- disable integer parsing here-*) 11intLib.deprecate_int(); 12 13val RESTR_EVAL_TAC = computeLib.RESTR_EVAL_TAC; 14 15val _ = type_abbrev("Block", Type`:word16 # word16 # word16 # word16`); 16val _ = type_abbrev("OddKey", Type`:word16 # word16 # word16 # word16`); 17val _ = type_abbrev("EvenKey", Type`:word16 # word16`); 18val _ = type_abbrev("InputKey", Type`:word16 # word16 # word16 # word16 19 # word16 # word16 # word16 # word16`); 20val _ = type_abbrev ("OddKeySched", Type`:OddKey#OddKey#OddKey#OddKey#OddKey#OddKey#OddKey#OddKey#OddKey`); 21val _ = type_abbrev ("EvenKeySched", Type`:EvenKey#EvenKey#EvenKey#EvenKey#EvenKey#EvenKey#EvenKey#EvenKey`); 22 23val FORALL_BLOCK = Q.store_thm 24("FORALL_BLOCK", 25 `(!b:Block. Q b) = 26 !w1 w2 w3 w4. 27 Q (w1,w2,w3,w4)`, 28 SIMP_TAC std_ss [FORALL_PROD]); 29 30val FORALL_ODDKEYSCHED = Q.prove 31(`(!x:OddKeySched. Q x) = !k1 k2 k3 k4 k5 k6 k7 k8 k9. 32 Q(k1,k2,k3,k4,k5,k6,k7,k8,k9)`, 33 EQ_TAC THEN RW_TAC std_ss [] THEN 34 `?a1 a2 a3 a4 a5 a6 a7 a8 a9. 35 x = (a1,a2,a3,a4,a5,a6,a7,a8,a9)` 36 by METIS_TAC [ABS_PAIR_THM] 37 THEN ASM_REWRITE_TAC[]); 38 39val FORALL_EVENKEYSCHED = Q.prove 40(`(!x:EvenKeySched. Q x) = !k1 k2 k3 k4 k5 k6 k7 k8. 41 Q(k1,k2,k3,k4,k5,k6,k7,k8)`, 42 EQ_TAC THEN RW_TAC std_ss [] THEN 43 `?a1 a2 a3 a4 a5 a6 a7 a8. 44 x = (a1,a2,a3,a4,a5,a6,a7,a8)` 45 by METIS_TAC [ABS_PAIR_THM] 46 THEN ASM_REWRITE_TAC[]); 47 48val FORALL_EVENKEY = Q.prove 49(`(!x:EvenKey. Q x) = !kw1 kw2. 50 Q(kw1,kw2)`, 51 EQ_TAC THEN RW_TAC std_ss [] THEN 52 `?a1 a2. 53 x = (a1,a2)` 54 by METIS_TAC [ABS_PAIR_THM] 55 THEN ASM_REWRITE_TAC[]); 56 57val FORALL_ODDKEY = Q.prove 58(`(!x:OddKey. Q x) = !kw1 kw2 kw3 kw4. 59 Q(kw1,kw2,kw3,kw4)`, 60 EQ_TAC THEN RW_TAC std_ss [] THEN 61 `?a1 a2 a3 a4. 62 x = (a1,a2,a3,a4)` 63 by METIS_TAC [ABS_PAIR_THM] 64 THEN ASM_REWRITE_TAC[]); 65 66val ZeroOddKey_def = Define `ZeroOddKey = (0w,0w,0w,0w) : OddKey`; 67val ZeroEvenKey_def = Define `ZeroEvenKey = (0w,0w) : EvenKey`; 68val ZeroOddKeys_def = 69 Define 70 `ZeroOddKeys = (ZeroOddKey,ZeroOddKey,ZeroOddKey,ZeroOddKey,ZeroOddKey, 71 ZeroOddKey,ZeroOddKey,ZeroOddKey,ZeroOddKey) : OddKeySched`; 72val ZeroEvenKeys_def = 73 Define 74 `ZeroEvenKeys = (ZeroEvenKey,ZeroEvenKey,ZeroEvenKey,ZeroEvenKey, 75 ZeroEvenKey,ZeroEvenKey,ZeroEvenKey,ZeroEvenKey) : EvenKeySched`; 76 77(*---Use Both Additive and Multiplicative Inverses Now---*) 78val InverseKey_def = Define `InverseKey (k1,k2,k3,k4) = ((minv k1), ~k3, ~k2, (minv k4)) : OddKey`; 79val InverseKeys_def = 80 Define 81 `InverseKeys (ok1,ok2,ok3,ok4,ok5,ok6,ok7,ok8,ok9) = 82 (InverseKey ok9,InverseKey ok8,InverseKey ok7,InverseKey ok6, 83 InverseKey ok5,InverseKey ok4,InverseKey ok3,InverseKey ok2, 84 InverseKey ok1) : OddKeySched`; 85 86val ReverseKeys_def = 87 Define 88 `ReverseKeys (ek1,ek2,ek3,ek4,ek5,ek6,ek7,ek8) = 89 (ek8,ek7,ek6,ek5,ek4,ek3,ek2,ek1) : EvenKeySched`; 90 91val RotateOddKeys_def = 92 Define 93 `RotateOddKeys (k1,k2,k3,k4,k5,k6,k7,k8,k9) = 94 (k2,k3,k4,k5,k6,k7,k8,k9,k1) : OddKeySched`; 95 96val RotateEvenKeys_def = 97 Define 98 `RotateEvenKeys (k1,k2,k3,k4,k5,k6,k7,k8) = 99 (k2,k3,k4,k5,k6,k7,k8,k1) : EvenKeySched`; 100 101(*-1st and 4th are multiplications now-*) 102val OddRound_def = Define 103 `OddRound ((Ka, Kb, Kc, Kd):OddKey) ((Xa, Xb, Xc, Xd):Block) = 104 (Xa * Ka, Xc + Kc, Xb + Kb,Xd * Kd ):Block`; 105 106val OddRound_Lemma1 = Q.store_thm 107("OddRound_Lemma1", 108 `!w1:word16 w2:word16. w1 + w2 + ~w2 = w1`, 109 SIMP_TAC std_ss [WORD_ADD_COMM] THEN 110 SIMP_TAC std_ss [WORD_ADD_ASSOC] THEN 111 ONCE_REWRITE_TAC [WORD_ADD_COMM] THEN 112 SIMP_TAC std_ss [WORD_ADD_ASSOC, WORD_ADD_RINV, WORD_ADD]); 113 114val OddRound_Lemma2 = Q.store_thm 115("OddRound_Lemma2", 116 `!w1:word16 w2:word16. w1 * w2 * (minv w2) = w1`, 117 REPEAT GEN_TAC THEN 118 `w1 * w2 * minv w2 = w1 * (w2 * minv w2)` by RW_TAC arith_ss [WORD_MULT_ASSOC]THEN 119 `w2 * minv w2 = 1w` by RW_TAC arith_ss [minv_axiom] THEN 120 METIS_TAC [WORD_MULT_CLAUSES]); 121 122val OddRound_Inversion = Q.store_thm 123("OddRound_Inversion", 124 `!s:Block k:OddKey. OddRound (InverseKey k) (OddRound k s) = s`, 125 SIMP_TAC std_ss [FORALL_BLOCK, FORALL_ODDKEY] THEN 126 RESTR_EVAL_TAC [] THEN 127 SIMP_TAC std_ss [OddRound_Lemma1, OddRound_Lemma2]); 128 129val Mangler1_def = Define `Mangler1 ((Yin:word16), (Zin:word16), (Ke:word16), (Kf:word16)) = ((Ke * Yin) + Zin) * Kf`; 130val Mangler2_def = Define `Mangler2 ((Yin:word16), (Ke:word16), (Yout:word16)) = (Ke * Yin) + Yout`; 131 132val Mangler1_Lemma1 = Q.store_thm 133("Mangler1_Lemma1", 134 `!w1 w2 w3 w4 w5 w6. w5 # Mangler1 (w1, w2, w3, w4) # (w6 # Mangler1 (w1, w2, w3, w4)) = w5 # w6`, 135 SIMP_TAC std_ss [WORD_EOR_ASSOC] THEN 136 SIMP_TAC std_ss [WORD_EOR_COMM] THEN 137 SIMP_TAC std_ss [WORD_EOR_ASSOC] THEN 138 ONCE_REWRITE_TAC [WORD_EOR_COMM] THEN 139 SIMP_TAC std_ss [WORD_EOR_ASSOC, WORD_EOR_INV, WORD_EOR_ID]); 140 141val Mangler1_Lemma2 = Q.store_thm 142("Mangler1_Lemma2", 143 `!w1 w2 w3 w4 w5. w5 # Mangler1 (w1, w2, w3, w4) # Mangler1 (w1, w2, w3, w4) = w5`, 144 SIMP_TAC std_ss [WORD_EOR_COMM] THEN 145 SIMP_TAC std_ss [WORD_EOR_ASSOC] THEN 146 ONCE_REWRITE_TAC [WORD_EOR_COMM] THEN 147 SIMP_TAC std_ss [WORD_EOR_ASSOC, WORD_EOR_INV, WORD_EOR_ID]); 148 149val Mangler2_Lemma1 = Q.store_thm 150("Mangler2_Lemma1", 151 `!w1 w2 w3 w4 w5. w4 # Mangler2 (w1, w2, w3) # (w5 # Mangler2 (w1, w2, w3)) = w4 # w5`, 152 SIMP_TAC std_ss [WORD_EOR_ASSOC] THEN 153 SIMP_TAC std_ss [WORD_EOR_COMM] THEN 154 SIMP_TAC std_ss [WORD_EOR_ASSOC] THEN 155 ONCE_REWRITE_TAC [WORD_EOR_COMM] THEN 156 SIMP_TAC std_ss [WORD_EOR_ASSOC, WORD_EOR_INV, WORD_EOR_ID]); 157 158val Mangler2_Lemma2 = Q.store_thm 159("Mangler2_Lemma2", 160 `!w1 w2 w3 w4. w4 # Mangler2 (w1, w2, w3) # Mangler2 (w1, w2, w3) = w4`, 161 SIMP_TAC std_ss [WORD_EOR_COMM] THEN 162 SIMP_TAC std_ss [WORD_EOR_ASSOC] THEN 163 ONCE_REWRITE_TAC [WORD_EOR_COMM] THEN 164 SIMP_TAC std_ss [WORD_EOR_ASSOC, WORD_EOR_INV, WORD_EOR_ID]); 165 166val EvenRound_def = Define 167 `EvenRound ((Ke, Kf):EvenKey) ((Xa, Xb, Xc, Xd):Block) = 168 let Yout = Mangler1 ((Xa # Xb), (Xc # Xd), Ke, Kf) in 169 let Zout = Mangler2 ((Xa # Xb), Ke, Yout) in 170 (Xa # Yout, Xb # Yout, Xc # Zout, Xd # Zout):Block`; 171 172val [Mangler1] = decls "Mangler1"; 173val [Mangler2] = decls "Mangler2"; 174 175val EvenRound_Inversion = Q.store_thm 176("EvenRound_Inversion", 177 `!s:Block k:EvenKey. EvenRound k (EvenRound k s) = s`, 178 SIMP_TAC std_ss [FORALL_BLOCK, FORALL_EVENKEY] THEN 179 RESTR_EVAL_TAC [Mangler1, Mangler2] THEN 180 SIMP_TAC std_ss [Mangler1_Lemma1, Mangler1_Lemma2, Mangler2_Lemma1, Mangler2_Lemma2]); 181 182 183val (Round_def,Round_ind) = 184 Defn.tprove 185 (Hol_defn 186 "Round" 187 `Round n (oddkeys: OddKeySched) (evenkeys: EvenKeySched) (state:Block) = 188 if (n = 0) then 189 state 190 else 191 if (EVEN n) then 192 Round (n-1) oddkeys (RotateEvenKeys evenkeys) (EvenRound (FST evenkeys) state) 193 else 194 Round (n-1) (RotateOddKeys oddkeys) evenkeys (OddRound (FST oddkeys) state)`, 195 WF_REL_TAC `measure (FST)`); 196 197val IdeaFwd_def = Define `IdeaFwd oddkeys evenkeys= Round 17 oddkeys evenkeys`; 198 199val [OddRound] = decls "OddRound"; 200val [EvenRound] = decls "EvenRound"; 201 202val IDEA_LEMMA = Q.store_thm 203("IDEA_LEMMA", 204 `!plaintext:Block oddkeys:OddKeySched evenkeys:EvenKeySched. 205 IdeaFwd (InverseKeys oddkeys) (ReverseKeys evenkeys) (IdeaFwd oddkeys evenkeys plaintext) = plaintext`, 206 SIMP_TAC std_ss [FORALL_ODDKEYSCHED, FORALL_EVENKEYSCHED] THEN 207 RESTR_EVAL_TAC [OddRound, EvenRound] THEN 208 SIMP_TAC std_ss [OddRound_Inversion, EvenRound_Inversion]); 209 210val (MakeEnKeys_def,MakeEnKeys_ind) = 211 Defn.tprove 212 (Hol_defn 213 "MakeEnKeys" 214 `MakeEnKeys n (K8::K7::K6::K5::K4::K3::K2::K1::rst) = 215 let (NK1, NK2, NK3, NK4, NK5, NK6, NK7, NK8) = 216 ((K2<<9) # (K3>>>7), (K3<<9) # (K4>>>7), 217 (K4<<9) # (K5>>>7), (K5<<9) # (K6>>>7), 218 (K6<<9) # (K7>>>7), (K7<<9) # (K8>>>7), 219 (K8<<9) # (K1>>>7), (K1<<9) # (K2>>>7)) 220 in 221 if n = 0 then 222 (NK4::NK3::NK2::NK1::K8::K7::K6::K5::K4::K3::K2::K1::rst) 223 else 224 MakeEnKeys (n-1) (NK8::NK7::NK6::NK5::NK4::NK3::NK2::NK1 225 ::K8::K7::K6::K5::K4::K3::K2::K1::rst)`, 226 WF_REL_TAC `measure (FST)`); 227 228val MakeKeys_def = Define 229 `MakeKeys ((K1, K2, K3, K4, K5, K6, K7, K8):InputKey) = 230 MakeEnKeys 6 [K8;K7;K6;K5;K4;K3;K2;K1]`; 231 232val ListToOddKeys_def = 233 Define 234 `(ListToOddKeys [] oddkeys = oddkeys) /\ 235 (ListToOddKeys ((k1::k2::k3::k4::k5::k6::t): word16 list) 236 ((ok1,ok2,ok3,ok4,ok5,ok6,ok7,ok8,ok9): OddKeySched) = 237 ListToOddKeys t ((k1,k2,k3,k4),ok1,ok2,ok3,ok4,ok5,ok6,ok7,ok8)) /\ 238 (ListToOddKeys ((k1::k2::k3::k4::t): word16 list) 239 ((ok1,ok2,ok3,ok4,ok5,ok6,ok7,ok8,ok9): OddKeySched) = 240 ListToOddKeys t ((k1,k2,k3,k4),ok1,ok2,ok3,ok4,ok5,ok6,ok7,ok8))`; 241 242val ListToEvenKeys_def = 243 Define 244 `(ListToEvenKeys [] evenkeys = evenkeys) /\ 245 (ListToEvenKeys ((k1::k2::k3::k4::k5::k6::t): word16 list) 246 ((ek1,ek2,ek3,ek4,ek5,ek6,ek7,ek8): EvenKeySched) = 247 ListToEvenKeys t ((k5,k6),ek1,ek2,ek3,ek4,ek5,ek6,ek7))`; 248 249val IDEA_def = Define `IDEA key = 250 let oddkeys = ListToOddKeys (MakeKeys key) ZeroOddKeys in 251 let evenkeys = ListToEvenKeys (MakeKeys key) ZeroEvenKeys in 252 (IdeaFwd oddkeys evenkeys, IdeaFwd (InverseKeys oddkeys) (ReverseKeys evenkeys))`; 253 254 255val IDEA_CORRECT = Q.store_thm 256 ("IDEA_CORRECT", 257 `!key plaintext. 258 ((encrypt,decrypt) = IDEA key) 259 ==> 260 (decrypt (encrypt plaintext) = plaintext)`, 261 RW_TAC std_ss [IDEA_def,LET_THM,IDEA_LEMMA]); 262