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