examples/diningcryptos/basic_leakage_examplesScript.sml

141 val random = Define
142    `random = {(\s:string. (0:num))}`;
148 val example1_conv = SIMP_CONV arith_ss [high, low, random, lem1,lem2,lem3];
152    ``leakage (unif_prog_space (high (SUC (SUC (SUC 0)))) (low (SUC (SUC (SUC 0)))) random) M1 = 2``,
156                               ``random``)
157                         [high, low, random, lem1, lem2, lem3]
181 val example2_input_conv = SIMP_CONV arith_ss [high, low, random, lem1,lem2,lem3];
185    ``leakage (unif_prog_space (high (SUC (SUC (SUC 0)))) (low (SUC (SUC (SUC 0)))) random) M2 = 2``,
189                               ``random``)
190                         [high, low, random, lem1, lem2, lem3, w2n_11]
223 val random = Define
224    `random = {(\s:string. (0:num))}`;
243 val example3_lr_input_conv = SIMP_CONV set_ss [low, random];
247    ``leakage (unif_prog_space (high (SUC (SUC (SUC 0)))) low random) M3 = 2``,
250                               ``random``)
251                         [high, low, random, h1, h2, lem1, lem2, lem3, lem4, lem5, lem6, w2n_11]
282 val example4_lr_input_conv = SIMP_CONV set_ss [low, random];
286    ``leakage (unif_prog_space ((high (SUC (SUC (SUC 0))))) low random) M4 = inv 16 * (52 - 6 * lg 3)``,
289                               ``random``)
290                         [high, low, random, h1, h2, lem1, lem2, lem3, lem4, lem5, lem6]
327 val random = Define
328    `random = {(\s:string. (0:num))}`;
330 val example5_conv = SIMP_CONV arith_ss [high, low, random, lem1,lem2,lem3];
332 val example5_output_conv = SIMP_CONV arith_ss [high, low, random, lem1,lem2,lem3]
337    ``leakage (unif_prog_space (high (SUC (SUC (SUC 0)))) (low (SUC (SUC (SUC 0)))) random) M5 = 0``,
340                               ``random``)
341                         [high, low, random, lem1, lem2, lem3]
378 val random = Define
379    `random = {(\s:string. ([]:num list))}`;
381 val example5'_conv = SIMP_CONV list_string_ss [high, low, random, lem7, lem8, APPEND, PAIR_EQ];
383 val example5'_output_conv = SIMP_CONV list_string_ss [high, low, random, lem7, lem8, APPEND, PAIR_EQ]
385                             THENC SIMP_CONV list_string_ss [high, low, random, lem7, lem8, APPEND];
389    ``leakage (unif_prog_space (high (SUC (SUC (SUC 0)))) (low (SUC (SUC (SUC 0)))) random) M5' = 2``,
393                               ``random``)
394                         [high, low, random, lem7, lem8, APPEND]
407 (* Example 8:    out = high XOR random *)
415 val 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))`;
424         then w2n (((n2w (H s "high")):word2) ?? (n2w (R s "random"))) else 0))`;
426 val example8_conv = SIMP_CONV arith_ss [high, low, random, lem1, lem2, lem3, w2n_11];
428 val example8_output_conv = SIMP_CONV arith_ss [high, low, random, lem1, lem2, lem3, w2n_11]
431                             THENC SIMP_CONV arith_ss [high, low, random, lem1, lem2, lem3, w2n_11];
435    ``leakage (unif_prog_space (high (SUC (SUC (SUC 0)))) low (random (SUC (SUC (SUC 0))))) M8 = 0``,
438                               ``random (SUC (SUC (SUC 0)))``)
439                         [high, low, random, lem1,lem2]
453 (* Example 8':   out = high XOR random *)
465    (``!n. random n = if (n=0) then
466                 {(\s:string. if s = "random" then 0 else 0)}
468                 (\s:string. if s = "random" then n else 0)INSERT(random (n-1))``,
469      Induct ++ RW_TAC arith_ss [random]);
473    ``visible_leakage (unif_prog_space (high 3) low (random 3)) M8 = 2``,
477 ++ `FINITE (random 3)`
481 ++ `~ ((high 3) CROSS low CROSS (random 3) = {})`