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