1(* 2app load ["bossLib", "metisLib", "arithmeticTheory", "pred_setTheory", 3 "pred_setLib", "stringLib", 4 "listTheory", "state_transformerTheory", "probabilityTheory", 5 "formalizeUseful", "combinTheory", "pairTheory", "realTheory", 6 "realLib", "extra_boolTheory", "jrhUtils", "extra_pred_setTheory", "extra_listTheory", 7 "realSimps", "extra_realTheory", "measureTheory", "numTheory", 8 "simpLib", "seqTheory", "subtypeTheory", "transcTheory", 9 "limTheory", "stringTheory", "rich_listTheory", "stringSimps", 10 "listSimps", "lebesgueTheory", "informationTheory", 11 "extra_stringTheory", "extra_stringLib", "leakageTheory", "leakageLib", 12 "wordsTheory", "wordsLib"]; 13*) 14 15open HolKernel Parse boolLib bossLib metisLib arithmeticTheory pred_setTheory 16 pred_setLib stringLib 17 listTheory state_transformerTheory 18 probabilityTheory formalizeUseful extra_numTheory combinTheory 19 pairTheory realTheory realLib extra_boolTheory jrhUtils 20 extra_pred_setTheory realSimps extra_realTheory measureTheory numTheory 21 simpLib seqTheory subtypeTheory extra_listTheory 22 transcTheory limTheory stringTheory rich_listTheory stringSimps listSimps 23 lebesgueTheory informationTheory extra_stringTheory extra_stringLib leakageTheory 24 leakageLib wordsTheory wordsLib; 25 26open real_sigmaTheory; 27 28val _ = new_theory "basic_leakage_examples"; 29 30infixr 0 ++ << || THENC ORELSEC ORELSER ##;infix 1 >>;val op ++ = op THEN;val op << = op THENL;val op >> = op THEN1;val op || = op ORELSE;val REVERSE = Tactical.REVERSE;val Simplify = RW_TAC arith_ss;val Suff = PARSE_TAC SUFF_TAC;val Know = PARSE_TAC KNOW_TAC;val Rewr = DISCH_THEN (REWRITE_TAC o wrap);val Rewr' = DISCH_THEN (ONCE_REWRITE_TAC o wrap);val Cond = DISCH_THEN (fn mp_th => let val cond = fst (dest_imp (concl mp_th)) in KNOW_TAC cond << [ALL_TAC, DISCH_THEN (MP_TAC o MP mp_th)] end);val POP_ORW = POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]); 31 32val safe_set_ss = (simpLib.++ (bool_ss, PRED_SET_ss)); 33 34val set_ss = (simpLib.++ (arith_ss, PRED_SET_ss)); 35 36val list_string_ss = (simpLib.++ (list_ss, STRING_ss)); 37 38fun TRY2_TAC t1 t2 state = let 39 val (a1,f1) = t1 state handle HOL_ERR _ => ALL_TAC state 40 in if length a1 = 0 then (a1,f1) else t2 state end; 41 42 43val lem1 = prove 44 (``!(s:string) (n:num) (m:num). ((\s'. (if s' = s then n else 0)) = 45 (\s'. (if s' = s then m else 0))) = 46 (n = m)``,METIS_TAC []); 47 48val lem2 = prove 49 (``!(s:string) (n:num). ((\s'. (if s' = s then n else 0)) = (\s'. 0)) = (n = 0)``, 50 METIS_TAC []); 51 52val lem3 = prove 53 (``!(s:string) (n:num). ((\s'. 0) = (\s'. (if s' = s then n else 0))) = (n = 0)``, 54 METIS_TAC []); 55 56val lem4 = prove 57 (``!(n1:num)(n2:num)(m1:num)(m2:num). 58 ((\s'. (if s' = "h2" then m1 else (if s' = "h1" then n1 else 0))) = 59 (\s'. (if s' = "h2" then m2 else (if s' = "h1" then n2 else 0)))) = 60 ((n1=n2)/\(m1=m2))``, 61 REPEAT STRIP_TAC ++ EQ_TAC 62 >> (ONCE_REWRITE_TAC [FUN_EQ_THM] 63 ++ SPOSE_NOT_THEN STRIP_ASSUME_TAC 64 ++ Cases_on `n1 = n2` 65 >> (Q.PAT_X_ASSUM `!x. (if x = "h2" then m1 else (if x = "h1" then n1 else 0)) = 66 (if x = "h2" then m2 else (if x = "h1" then n2 else 0))` 67 (MP_TAC o Q.SPEC `"h2"`) ++ RW_TAC std_ss []) 68 ++ Q.PAT_X_ASSUM `!x. (if x = "h2" then m1 else (if x = "h1" then n1 else 0)) = 69 (if x = "h2" then m2 else (if x = "h1" then n2 else 0))` 70 (MP_TAC o Q.SPEC `"h1"`) ++ SRW_TAC [] []) 71 ++ RW_TAC std_ss []); 72 73val lem5 = prove 74 (``!(m1:num)(m2:num)(n2:num). 75 ((\s'. (if s' = "h2" then m1 else 0)) = 76 (\s'. (if s' = "h2" then m2 else (if s' = "h1" then n2 else 0)))) = 77 ((n2=0)/\(m1=m2))``, 78 REPEAT STRIP_TAC ++ EQ_TAC 79 >> (ONCE_REWRITE_TAC [FUN_EQ_THM] 80 ++ SPOSE_NOT_THEN STRIP_ASSUME_TAC 81 ++ Cases_on `n2=0` 82 >> (Q.PAT_X_ASSUM `!x. (if x = "h2" then m1 else 0) = 83 (if x = "h2" then m2 else (if x = "h1" then n2 else 0))` 84 (MP_TAC o Q.SPEC `"h2"`) ++ RW_TAC std_ss []) 85 ++ Q.PAT_X_ASSUM `!x. (if x = "h2" then m1 else 0) = 86 (if x = "h2" then m2 else (if x = "h1" then n2 else 0))` 87 (MP_TAC o Q.SPEC `"h1"`) ++ SRW_TAC [] []) 88 ++ RW_TAC std_ss []); 89 90val lem6 = prove 91 (``!(n:num)(m:num). 92 ((\s'. (if s' = "h2" then m else (if s' = "h1" then n else 0))) = 93 (\s'. 0)) = 94 ((n=0)/\(m=0))``, 95 REPEAT STRIP_TAC ++ EQ_TAC 96 >> (ONCE_REWRITE_TAC [FUN_EQ_THM] 97 ++ SPOSE_NOT_THEN STRIP_ASSUME_TAC 98 ++ Cases_on `n = 0` 99 >> (Q.PAT_X_ASSUM `!x. (if x = "h2" then m else (if x = "h1" then n else 0)) = 0` 100 (MP_TAC o Q.SPEC `"h2"`) ++ RW_TAC std_ss []) 101 ++ Q.PAT_X_ASSUM `!x. (if x = "h2" then m else (if x = "h1" then n else 0)) = 0` 102 (MP_TAC o Q.SPEC `"h1"`) ++ SRW_TAC [] []) 103 ++ RW_TAC std_ss []); 104 105val lem7 = prove 106 (``!(s:string) (n:num) (m:num). ((\s'. (if s' = s then [n] else [])) = 107 (\s'. (if s' = s then [m] else []))) = 108 (n = m)``, 109 REPEAT STRIP_TAC ++ EQ_TAC 110 >> (RW_TAC list_ss [FUN_EQ_THM] ++ POP_ASSUM (MP_TAC o Q.SPEC `s`) 111 ++ RW_TAC std_ss []) 112 ++ RW_TAC std_ss []); 113 114val lem8 = prove 115 (``!(n1:num) (n2:num) (n3:num) (m1:num) (m2:num) (m3:num). 116 ((\s'. (if (s' = "out") then [n1;n2] else 117 (if (s' = "low") then [n3] else []))) = 118 (\s'. (if (s' = "out") then [m1;m2] else 119 (if (s' = "low") then [m3] else [])))) = 120 ((n1 = m1) /\ (n2 = m2) /\ (n3 = m3))``, 121 REPEAT STRIP_TAC ++ EQ_TAC 122 >> (RW_TAC list_ss [FUN_EQ_THM] 123 << [POP_ASSUM (MP_TAC o Q.SPEC `"out"`) ++ RW_TAC std_ss [], 124 POP_ASSUM (MP_TAC o Q.SPEC `"out"`) ++ RW_TAC std_ss [], 125 POP_ASSUM (MP_TAC o Q.SPEC `"low"`) ++ RW_TAC string_ss []]) 126 ++ RW_TAC std_ss []); 127 128(* *************************** *) 129(* Example 1: out = high + low *) 130(* TOTAL LEAKAGE *) 131(* *************************** *) 132 133val high = Define 134 `(high 0 = {(\s:string. if s = "high" then 0 else 0)}) /\ 135 (high (SUC n) = (\s:string. if s = "high" then SUC n else 0)INSERT(high n))`; 136 137val low = Define 138 `(low 0 = {(\s:string. if s = "low" then 0 else 0)}) /\ 139 (low (SUC n) = (\s:string. if s = "low" then SUC n else 0)INSERT(low n))`; 140 141val random = Define 142 `random = {(\s:string. (0:num))}`; 143 144val M1 = Define 145 `M1 = (\s: ((num,num,num) prog_state). (\s':string. if (s' = "out") 146 then (H s "high") + (L s "low") else 0))`; 147 148val example1_conv = SIMP_CONV arith_ss [high, low, random, lem1,lem2,lem3]; 149 150val leakage_example1 = store_thm 151 ("leakage_example1", 152 ``leakage (unif_prog_space (high (SUC (SUC (SUC 0)))) (low (SUC (SUC (SUC 0)))) random) M1 = 2``, 153CONV_TAC (RATOR_CONV (RAND_CONV ( 154 LEAKAGE_COMPUTE_CONV (``high (SUC (SUC (SUC 0)))``, 155 ``low (SUC (SUC (SUC 0)))``, 156 ``random``) 157 [high, low, random, lem1, lem2, lem3] 158 [M1, H_def, L_def, FST, SND] 159 example1_conv example1_conv example1_conv 160 example1_conv example1_conv example1_conv example1_conv))) 161++ SIMP_TAC real_ss [lg_1, lg_inv, GSYM REAL_INV_1OVER] 162++ `lg 4 = 2` 163 by (`4 = 2 pow 2` by RW_TAC real_ss [pow] ++ POP_ORW ++ RW_TAC std_ss [lg_pow]) 164++ RW_TAC real_ss [] 165++ ONCE_REWRITE_TAC [REAL_MUL_COMM] ++ RW_TAC std_ss [GSYM real_div] 166++ (MP_TAC o Q.SPECL [`32`,`2`,`16`]) REAL_EQ_LDIV_EQ 167++ RW_TAC real_ss []); 168 169(* ******************************** *) 170(* Example 2: out = high XOR low *) 171(* TOTAL LEAKAGE *) 172(* ******************************** *) 173 174val M2 = Define 175 `M2 = (\s: ((num,num,num) prog_state). (\s':string. if (s' = "out") 176 then w2n (((n2w (H s "high")):word2) ?? (n2w (L s "low"))) else 0))`; 177 178val example2_output_conv = SIMP_CONV arith_ss [lem1,lem2,lem3, w2n_11] 179 THENC (FIND_CONV ``w2n(a ?? b)`` WORD_EVAL_CONV); 180 181val example2_input_conv = SIMP_CONV arith_ss [high, low, random, lem1,lem2,lem3]; 182 183val leakage_example2 = store_thm 184 ("leakage_example2", 185 ``leakage (unif_prog_space (high (SUC (SUC (SUC 0)))) (low (SUC (SUC (SUC 0)))) random) M2 = 2``, 186CONV_TAC (RATOR_CONV (RAND_CONV ( 187 LEAKAGE_COMPUTE_CONV (``high (SUC (SUC (SUC 0)))``, 188 ``low (SUC (SUC (SUC 0)))``, 189 ``random``) 190 [high, low, random, lem1, lem2, lem3, w2n_11] 191 [M2, H_def, L_def, FST, SND] 192 example2_input_conv example2_input_conv example2_input_conv 193 example2_input_conv example2_input_conv example2_input_conv 194 example2_output_conv))) 195++ SIMP_TAC real_ss [lg_1, lg_inv, GSYM REAL_INV_1OVER] 196++ `lg 4 = 2` 197 by (`4 = 2 pow 2` by RW_TAC real_ss [pow] ++ POP_ORW ++ RW_TAC std_ss [lg_pow]) 198++ RW_TAC real_ss [] 199++ ONCE_REWRITE_TAC [REAL_MUL_COMM] ++ RW_TAC std_ss [GSYM real_div] 200++ (MP_TAC o Q.SPECL [`32`,`2`,`16`]) REAL_EQ_LDIV_EQ 201++ RW_TAC real_ss []); 202 203(* ********************************** *) 204(* Example 3: out = h1 XOR h2 *) 205(* 2 BITS: match of bits of h1 and h2 *) 206(* ********************************** *) 207 208val h1 = Define 209 `(h1 0 = {(\s:string. if s = "h1" then 0 else 0)}) /\ 210 (h1 (SUC n) = (\s:string. if s = "h1" then SUC n else 0)INSERT(h1 n))`; 211 212val h2 = Define 213 `(h2 l 0 = IMAGE (\s: num state. (\s':string. if s' = "h2" then 0 else s s')) l) /\ 214 (h2 l (SUC n) = (IMAGE (\s: num state. (\s':string. if s' = "h2" then (SUC n) else s s')) l) UNION 215 (h2 l n))`; 216 217val high = Define 218 `high n = h2 (h1 n) n`; 219 220val low = Define 221 `low = {(\s:string. (0:num))}`; 222 223val random = Define 224 `random = {(\s:string. (0:num))}`; 225 226val M3 = Define 227 `M3 = (\s: ((num,num,num) prog_state). (\s':string. if (s' = "out") 228 then w2n (((n2w (H s "h1")):word2) ?? (n2w (H s "h2"))) else 0))`; 229 230val example3_output_conv = SIMP_CONV string_ss [lem1, lem2, lem3, lem4, lem5, lem6, w2n_11] 231 THENC (TRY_CONV (FIND_CONV ``(x:string)=(y:string)`` string_EQ_CONV)) 232 THENC (TRY_CONV (FIND_CONV ``w2n(a ?? b)`` WORD_EVAL_CONV)); 233 234val example3_h_conv = SIMP_CONV arith_ss [lem1, lem2, lem3, lem4, lem5, lem6, w2n_11] 235 THENC (TRY_CONV (FIND_CONV ``(a ?? b) = (c ?? d)`` WORD_EVAL_CONV)); 236 237val example3_lr_conv = SIMP_CONV arith_ss [lem1, lem2, lem3, lem4, lem5, lem6]; 238 239val example3_h_input_conv = SIMP_CONV set_ss [high, h1, h2] 240THENC (FIND_CONV ``x UNION y`` 241 (UNION_CONV (SIMP_CONV set_ss [lem1, lem2, lem3, lem4, lem5, lem6]))); 242 243val example3_lr_input_conv = SIMP_CONV set_ss [low, random]; 244 245val leakage_example3 = store_thm 246 ("leakage_example3", 247 ``leakage (unif_prog_space (high (SUC (SUC (SUC 0)))) low random) M3 = 2``, 248CONV_TAC (RATOR_CONV (RAND_CONV (LEAKAGE_COMPUTE_CONV (``high (SUC (SUC (SUC 0)))``, 249 ``low``, 250 ``random``) 251 [high, low, random, h1, h2, lem1, lem2, lem3, lem4, lem5, lem6, w2n_11] 252 [M3, H_def, L_def, FST, SND, w2n_11] 253 example3_h_input_conv example3_lr_input_conv example3_lr_input_conv 254 example3_h_conv example3_lr_conv example3_lr_conv 255 example3_output_conv))) 256++ RW_TAC real_ss [lg_1, lg_inv, GSYM REAL_INV_1OVER, lg_mul, lg_2] 257++ `lg 4 = 2` 258 by (`4 = 2 pow 2` by RW_TAC real_ss [pow] ++ POP_ORW ++ RW_TAC std_ss [lg_pow]) 259++ `lg 16 = 4` 260 by (`16 = 2 pow 4` by RW_TAC real_ss [pow] ++ POP_ORW ++ RW_TAC std_ss [lg_pow]) 261++ ONCE_REWRITE_TAC [REAL_MUL_COMM] 262++ RW_TAC real_ss [GSYM real_div]); 263 264(* *************************** *) 265(* Example 4: out = h1 + h2 *) 266(* PARTIAL LEAKAGE *) 267(* *************************** *) 268 269val M4 = Define 270 `M4 = (\s: ((num,num,num) prog_state). (\s':string. if (s' = "out") 271 then (H s "h1") + (H s "h2") else 0))`; 272 273val example4_output_conv = SIMP_CONV string_ss [lem1, lem2, lem3, lem4, lem5, lem6] 274 THENC (TRY_CONV (FIND_CONV ``(x:string)=(y:string)`` string_EQ_CONV)); 275 276val example4_dup_conv = SIMP_CONV arith_ss [lem1, lem2, lem3, lem4, lem5, lem6]; 277 278val example4_h_input_conv = SIMP_CONV set_ss [high, h1, h2] 279THENC (FIND_CONV ``x UNION y`` 280 (UNION_CONV (SIMP_CONV set_ss [lem1, lem2, lem3, lem4, lem5, lem6]))); 281 282val example4_lr_input_conv = SIMP_CONV set_ss [low, random]; 283 284val leakage_example4 = store_thm 285 ("leakage_example4", 286 ``leakage (unif_prog_space ((high (SUC (SUC (SUC 0))))) low random) M4 = inv 16 * (52 - 6 * lg 3)``, 287CONV_TAC (RATOR_CONV (RAND_CONV (LEAKAGE_COMPUTE_CONV (``high (SUC (SUC (SUC 0)))``, 288 ``low``, 289 ``random``) 290 [high, low, random, h1, h2, lem1, lem2, lem3, lem4, lem5, lem6] 291 [M4, H_def, L_def, FST, SND, w2n_11] 292 example4_h_input_conv example4_lr_input_conv example4_lr_input_conv 293 example4_dup_conv example4_dup_conv example4_dup_conv 294 example4_output_conv))) 295++ RW_TAC real_ss [lg_1, lg_mul, lg_2, lg_inv, GSYM REAL_INV_1OVER, real_div] 296++ `lg 8 = 3` by (`8 = 2 pow 3` by RW_TAC real_ss [pow] ++ POP_ORW ++ RW_TAC std_ss [lg_pow]) 297++ `lg 4 = 2` by (`4 = 2 pow 2` by RW_TAC real_ss [pow] ++ POP_ORW ++ RW_TAC std_ss [lg_pow]) 298++ `lg 16 = 4` by (`16 = 2 pow 4` by RW_TAC real_ss [pow] ++ POP_ORW ++ RW_TAC std_ss [lg_pow]) 299++ RW_TAC real_ss [REAL_INV_EQ_0] 300++ REPEAT (POP_ASSUM (K ALL_TAC)) 301++ REAL_ARITH_TAC); 302 303(* *************************** *) 304(* Example 5: intermed. leak *) 305(* No leakage *) 306(* *************************** *) 307 308val assign1 = Define 309 `assign1 = (\s: ((num,num,num) prog_state). (\s':string. if (s' = "out") 310 then (H s "high") else 0))`; 311 312val assign2 = Define 313 `assign2 = (\s: ((num,num,num) prog_state). (\s':string. if (s' = "out") 314 then (L s "low") else 0))`; 315 316val M5 = Define 317 `M5 = (\s: ((num,num,num) prog_state). assign2 ((H s, assign1 s), R s))`; 318 319val high = Define 320 `(high 0 = {(\s:string. if s = "high" then 0 else 0)}) /\ 321 (high (SUC n) = (\s:string. if s = "high" then SUC n else 0)INSERT(high n))`; 322 323val low = Define 324 `(low 0 = {(\s:string. if s = "low" then 0 else 0)}) /\ 325 (low (SUC n) = (\s:string. if s = "low" then SUC n else 0)INSERT(low n))`; 326 327val random = Define 328 `random = {(\s:string. (0:num))}`; 329 330val example5_conv = SIMP_CONV arith_ss [high, low, random, lem1,lem2,lem3]; 331 332val example5_output_conv = SIMP_CONV arith_ss [high, low, random, lem1,lem2,lem3] 333 THENC (TRY_CONV (FIND_CONV ``(x:string)=(y:string)`` string_EQ_CONV)); 334 335val leakage_example5 = store_thm 336 ("leakage_example5", 337 ``leakage (unif_prog_space (high (SUC (SUC (SUC 0)))) (low (SUC (SUC (SUC 0)))) random) M5 = 0``, 338CONV_TAC (RATOR_CONV (RAND_CONV (LEAKAGE_COMPUTE_CONV (``high (SUC (SUC (SUC 0)))``, 339 ``low (SUC (SUC (SUC 0)))``, 340 ``random``) 341 [high, low, random, lem1, lem2, lem3] 342 [M5, assign1, assign2, H_def, L_def, FST, SND] 343 example5_conv example5_conv example5_conv 344 345 example5_conv example5_conv example5_conv 346 example5_output_conv))) 347++ RW_TAC real_ss [REAL_DIV_REFL, lg_1]); 348 349(* *************************** *) 350(* Example 5': intermed. leak *) 351(* total leakage *) 352(* *************************** *) 353 354val state_update = Define 355 `state_update name value = (\s:(num list) state. (\n:string. if (n=name) then value else s n))`; 356 357val state_append = Define 358 `state_append name value = (\s:(num list) state. 359 state_update name ((if (value=[]) then [] else [HD value])++(s name)) s)`; 360 361val assign1 = Define 362 `assign1 = (\s: ((num list,num list,num list) prog_state). state_update "out" (H s "high") (L s))`; 363 364val assign2 = Define 365 `assign2 = (\s: ((num list,num list,num list) prog_state). state_append "out" (L s "low") (L s))`; 366 367val M5' = Define 368 `M5' = (\s: ((num list,num list,num list) prog_state). assign2 ((H s, assign1 s), R s))`; 369 370val high = Define 371 `(high 0 = {(\s:string. if s = "high" then [0] else [])}) /\ 372 (high (SUC n) = (\s:string. if s = "high" then [SUC n] else [])INSERT(high n))`; 373 374val low = Define 375 `(low 0 = {(\s:string. if s = "low" then [0] else [])}) /\ 376 (low (SUC n) = (\s:string. if s = "low" then [SUC n] else [])INSERT(low n))`; 377 378val random = Define 379 `random = {(\s:string. ([]:num list))}`; 380 381val example5'_conv = SIMP_CONV list_string_ss [high, low, random, lem7, lem8, APPEND, PAIR_EQ]; 382 383val example5'_output_conv = SIMP_CONV list_string_ss [high, low, random, lem7, lem8, APPEND, PAIR_EQ] 384 THENC (TRY_CONV (FIND_CONV ``(x:string)=(y:string)`` string_EQ_CONV)) 385 THENC SIMP_CONV list_string_ss [high, low, random, lem7, lem8, APPEND]; 386 387val leakage_example5' = store_thm 388 ("leakage_example5'", 389 ``leakage (unif_prog_space (high (SUC (SUC (SUC 0)))) (low (SUC (SUC (SUC 0)))) random) M5' = 2``, 390PURE_REWRITE_TAC [M5', state_update, state_append, assign1, assign2] 391++ CONV_TAC (RATOR_CONV (RAND_CONV (LEAKAGE_COMPUTE_CONV (``high (SUC (SUC (SUC 0)))``, 392 ``low (SUC (SUC (SUC 0)))``, 393 ``random``) 394 [high, low, random, lem7, lem8, APPEND] 395 [H_def, L_def, FST, SND, APPEND] 396 example5'_conv example5'_conv example5'_conv 397 example5'_output_conv example5'_output_conv example5'_output_conv 398 example5'_output_conv))) 399++ RW_TAC real_ss [lg_1, lg_inv, GSYM REAL_INV_1OVER] 400++ `lg 4 = 2` by (`4 = 2 pow 2` by RW_TAC real_ss [pow] ++ POP_ORW ++ RW_TAC std_ss [lg_pow]) 401++ RW_TAC real_ss [] 402++ ONCE_REWRITE_TAC [REAL_MUL_COMM] ++ RW_TAC std_ss [GSYM real_div] 403++ (MP_TAC o Q.SPECL [`32`,`2`,`16`]) REAL_EQ_LDIV_EQ 404++ RW_TAC real_ss []); 405 406(* *********************************** *) 407(* Example 8: out = high XOR random *) 408(* NO LEAKAGE (hidden prob) *) 409(* *********************************** *) 410 411val high = Define 412 `(high 0 = {(\s:string. if s = "high" then 0 else 0)}) /\ 413 (high (SUC n) = (\s:string. if s = "high" then SUC n else 0)INSERT(high n))`; 414 415val random = Define 416 `(random 0 = {(\s:string. if s = "random" then 0 else 0)}) /\ 417 (random (SUC n) = (\s:string. if s = "random" then SUC n else 0)INSERT(random n))`; 418 419val low = Define 420 `low = {(\s:string. (0:num))}`; 421 422val M8 = Define 423 `M8 = (\s: ((num,num,num) prog_state). (\s':string. if (s' = "out") 424 then w2n (((n2w (H s "high")):word2) ?? (n2w (R s "random"))) else 0))`; 425 426val example8_conv = SIMP_CONV arith_ss [high, low, random, lem1, lem2, lem3, w2n_11]; 427 428val example8_output_conv = SIMP_CONV arith_ss [high, low, random, lem1, lem2, lem3, w2n_11] 429 THENC (TRY_CONV (FIND_CONV ``(x:string)=(y:string)`` string_EQ_CONV)) 430 THENC (TRY_CONV (FIND_CONV ``w2n(a ?? b)`` WORD_EVAL_CONV)) 431 THENC SIMP_CONV arith_ss [high, low, random, lem1, lem2, lem3, w2n_11]; 432 433val leakage_example8 = store_thm 434 ("leakage_example8", 435 ``leakage (unif_prog_space (high (SUC (SUC (SUC 0)))) low (random (SUC (SUC (SUC 0))))) M8 = 0``, 436CONV_TAC (RATOR_CONV (RAND_CONV (LEAKAGE_COMPUTE_CONV (``high (SUC (SUC (SUC 0)))``, 437 ``low``, 438 ``random (SUC (SUC (SUC 0)))``) 439 [high, low, random, lem1,lem2] 440 [M8, H_def, R_def, FST, SND, lem1,lem2, lem3] 441 example8_conv example8_conv example8_conv 442 example8_output_conv example8_conv example8_output_conv 443 example8_output_conv))) 444++ RW_TAC real_ss [lg_mul, lg_2, lg_1, lg_inv, GSYM REAL_INV_1OVER] 445++ `lg 4 = 2` 446 by (`4 = 2 pow 2` by RW_TAC real_ss [pow] ++ POP_ORW ++ RW_TAC std_ss [lg_pow]) 447++ `lg 16 = 4` 448 by (`16 = 2 pow 4` by RW_TAC real_ss [pow] ++ POP_ORW ++ RW_TAC std_ss [lg_pow]) 449++ ONCE_REWRITE_TAC [REAL_MUL_COMM] 450++ RW_TAC real_ss [GSYM real_div]); 451 452(* *********************************** *) 453(* Example 8': out = high XOR random *) 454(* TOTAL LEAKAGE (visible prob) *) 455(* *********************************** *) 456 457val high_thm = prove 458 (``!n. high n = if (n=0) then 459 {(\s:string. if s = "high" then 0 else 0)} 460 else 461 (\s:string. if s = "high" then n else 0)INSERT(high (n-1))``, 462 Induct ++ RW_TAC arith_ss [high]); 463 464val random_thm = prove 465 (``!n. random n = if (n=0) then 466 {(\s:string. if s = "random" then 0 else 0)} 467 else 468 (\s:string. if s = "random" then n else 0)INSERT(random (n-1))``, 469 Induct ++ RW_TAC arith_ss [random]); 470 471val leakage_example8' = store_thm 472 ("leakage_example8'", 473 ``visible_leakage (unif_prog_space (high 3) low (random 3)) M8 = 2``, 474`FINITE (high 3)` 475 by (NTAC 4 (ONCE_REWRITE_TAC [high_thm]) 476 ++ RW_TAC set_ss []) 477++ `FINITE (random 3)` 478 by (NTAC 4 (ONCE_REWRITE_TAC [random_thm]) 479 ++ RW_TAC set_ss []) 480++ `FINITE (low)` by RW_TAC set_ss [low] 481++ `~ ((high 3) CROSS low CROSS (random 3) = {})` 482 by (RW_TAC std_ss [Once EXTENSION] 483 ++ NTAC 4 (ONCE_REWRITE_TAC [high_thm, random_thm, low]) 484 ++ RW_TAC set_ss [] 485 ++ Q.EXISTS_TAC `(((\s.0),(\s.0)),(\s.0))` 486 ++ RW_TAC std_ss []) 487++ ASM_SIMP_TAC std_ss 488 [unif_prog_space_visible_leakage_computation_reduce] 489++ NTAC 4 (ONCE_REWRITE_TAC [high_thm, random_thm, low]) 490++ RW_TAC set_ss [CROSS_EQNS, lem1, lem2] 491++ CONV_TAC (FIND_CONV ``x UNION y`` (UNION_CONV (SIMP_CONV set_ss [lem1,lem2]))) 492++ RW_TAC set_ss [CROSS_EQNS, lem1, lem2, M8, H_def, R_def] 493++ CONV_TAC (FIND_CONV ``x UNION y`` 494 (UNION_CONV (SIMP_CONV set_ss [lem1,lem2, w2n_11] 495 THENC (FIND_CONV ``(a ?? b) = (c ?? d)`` WORD_EVAL_CONV)))) 496++ CONV_TAC (REPEATC (SIMP_CONV set_ss [REAL_SUM_IMAGE_THM] 497 THENC (FIND_CONV ``x DELETE y`` 498 (DELETE_CONV (SIMP_CONV arith_ss [PAIR_EQ,lem1,lem2,lem3, w2n_11] 499 THENC (FIND_CONV ``(a ?? b) = (c ?? d)`` 500 WORD_EVAL_CONV)))) 501 THENC (SIMP_CONV arith_ss [lem1,lem2,lem3, w2n_11])) 502 THENC (FIND_CONV ``(a ?? b) = (c ?? d)`` WORD_EVAL_CONV)) 503++ RW_TAC real_ss [lg_1, lg_inv, GSYM REAL_INV_1OVER] 504++ `lg 4 = 2` 505 by (`4 = 2 pow 2` by RW_TAC real_ss [pow] ++ POP_ORW ++ RW_TAC std_ss [lg_pow]) 506++ ONCE_REWRITE_TAC [REAL_MUL_COMM] 507++ RW_TAC real_ss [GSYM real_div]); 508 509(* *********************************** *) 510 511val flip_example_lem = prove 512 (``!(s:string). ~((\s'. s' = s) = (\s'. F))``,METIS_TAC []); 513 514val M = Define 515 `M = (\s: ((bool,bool,bool) prog_state). (\s':string. if (s' = "out") 516 then (if (R s "r") then (L s "l") else (H s "h")) else F))`; 517 518val hidden_flip_example = store_thm 519 ("hidden_flip_example", 520 ``leakage (unif_prog_space {(\s:string. s = "h");(\s:string.F)} 521 {(\s:string. s = "l");(\s:string.F)} 522 {(\s:string. s = "r");(\s:string.F)}) M = 3/2 - (3 * lg 3)/4``, 523`~ ({(\s:string. s = "h");(\s:string.F)} CROSS 524 {(\s:string. s = "l");(\s:string.F)} CROSS 525 {(\s:string. s = "r");(\s:string.F)} = {})` 526 by (RW_TAC set_ss [Once EXTENSION] 527 ++ Q.EXISTS_TAC `(((\s.F),(\s.F)),(\s.F))` 528 ++ RW_TAC std_ss []) 529++ ASM_SIMP_TAC set_ss 530 [unif_prog_space_leakage_computation_reduce] 531++ RW_TAC set_ss [CROSS_EQNS, lem1, flip_example_lem] 532++ CONV_TAC (FIND_CONV ``x UNION y`` (UNION_CONV (SIMP_CONV set_ss [flip_example_lem, lem1]))) 533++ RW_TAC set_ss [CROSS_EQNS, lem1, M, H_def, L_def, R_def] 534++ CONV_TAC (FIND_CONV ``x UNION y`` (UNION_CONV (SIMP_CONV set_ss [flip_example_lem, lem1]))) 535++ CONV_TAC (REPEATC (SIMP_CONV set_ss [REAL_SUM_IMAGE_THM] 536 THENC (FIND_CONV ``x DELETE y`` 537 (DELETE_CONV (SIMP_CONV arith_ss [PAIR_EQ, flip_example_lem]))) 538 THENC SIMP_CONV arith_ss [flip_example_lem])) 539++ SIMP_TAC real_ss [lg_1, lg_inv, GSYM REAL_INV_1OVER, lg_2, REAL_MUL_LINV] 540++ `lg 4 = 2` 541 by (`4 = 2 pow 2` by RW_TAC real_ss [pow] ++ POP_ORW ++ RW_TAC std_ss [lg_pow]) 542++ RW_TAC real_ss [lg_mul, REAL_INV_POS, lg_inv] 543++ Q.ABBREV_TAC `foo = 3 * lg 3` 544++ `3 * (~2 + lg 3) + (~2 + 3 * (~2 + lg 3)) = 545 ~14 + 2 * foo` 546 by (Q.UNABBREV_TAC `foo` ++ REAL_ARITH_TAC) 547++ POP_ORW 548++ RW_TAC real_ss [REAL_ADD_ASSOC, real_sub, REAL_NEG_ADD] 549++ ONCE_REWRITE_TAC [REAL_MUL_COMM] 550++ RW_TAC std_ss [GSYM real_div] 551++ (MP_TAC o Q.SPECL [`(12 + ~(2 * foo))`,`3 / 2 + ~foo / 4`,`8`]) REAL_EQ_LDIV_EQ 552++ RW_TAC real_ss [REAL_ADD_RDISTRIB] 553++ RW_TAC std_ss [real_div, Once (GSYM REAL_MUL_ASSOC)] 554++ `inv 4 * 8 = 2` by (ONCE_REWRITE_TAC [REAL_MUL_COMM] ++ RW_TAC real_ss [GSYM real_div]) 555++ POP_ORW 556++ REAL_ARITH_TAC); 557 558 559val visible_flip_example = store_thm 560 ("visible_flip_example", 561 ``visible_leakage (unif_prog_space {(\s:string. s = "h");(\s:string.F)} 562 {(\s:string. s = "l");(\s:string.F)} 563 {(\s:string. s = "r");(\s:string.F)}) M = 1/2``, 564`~ ({(\s:string. s = "h");(\s:string.F)} CROSS 565 {(\s:string. s = "l");(\s:string.F)} CROSS 566 {(\s:string. s = "r");(\s:string.F)} = {})` 567 by (RW_TAC set_ss [Once EXTENSION] 568 ++ Q.EXISTS_TAC `(((\s.F),(\s.F)),(\s.F))` 569 ++ RW_TAC std_ss []) 570++ ASM_SIMP_TAC set_ss 571 [unif_prog_space_visible_leakage_computation_reduce] 572++ RW_TAC set_ss [CROSS_EQNS, flip_example_lem] 573++ CONV_TAC (FIND_CONV ``x UNION y`` (UNION_CONV (SIMP_CONV set_ss [flip_example_lem]))) 574++ RW_TAC set_ss [CROSS_EQNS, lem1, M, H_def, L_def, R_def] 575++ CONV_TAC (FIND_CONV ``x UNION y`` (UNION_CONV (SIMP_CONV set_ss [flip_example_lem]))) 576++ CONV_TAC (REPEATC (SIMP_CONV set_ss [REAL_SUM_IMAGE_THM] 577 THENC (FIND_CONV ``x DELETE y`` 578 (DELETE_CONV (SIMP_CONV arith_ss [PAIR_EQ, flip_example_lem]))) 579 THENC SIMP_CONV arith_ss [flip_example_lem])) 580++ SIMP_TAC real_ss [lg_1, lg_inv, GSYM REAL_INV_1OVER, lg_2, REAL_MUL_LINV] 581++ ONCE_REWRITE_TAC [REAL_MUL_COMM] ++ RW_TAC real_ss [GSYM real_div, REAL_INV_1OVER]); 582val _ = export_theory (); 583