examples/diningcryptos/basic_leakage_examplesScript.sml

138 val random = Define
139    `random = {(\s:string. (0:num))}`;
145 val example1_conv = SIMP_CONV arith_ss [high, low, random, lem1,lem2,lem3];
149    ``leakage (unif_prog_space (high (SUC (SUC (SUC 0)))) (low (SUC (SUC (SUC 0)))) random) M1 = 2``,
153                               ``random``)
154                         [high, low, random, lem1, lem2, lem3]
178 val example2_input_conv = SIMP_CONV arith_ss [high, low, random, lem1,lem2,lem3];
182    ``leakage (unif_prog_space (high (SUC (SUC (SUC 0)))) (low (SUC (SUC (SUC 0)))) random) M2 = 2``,
186                               ``random``)
187                         [high, low, random, lem1, lem2, lem3, w2n_11]
220 val random = Define
221    `random = {(\s:string. (0:num))}`;
240 val example3_lr_input_conv = SIMP_CONV set_ss [low, random];
244    ``leakage (unif_prog_space (high (SUC (SUC (SUC 0)))) low random) M3 = 2``,
247                               ``random``)
248                         [high, low, random, h1, h2, lem1, lem2, lem3, lem4, lem5, lem6, w2n_11]
279 val example4_lr_input_conv = SIMP_CONV set_ss [low, random];
283    ``leakage (unif_prog_space ((high (SUC (SUC (SUC 0))))) low random) M4 = inv 16 * (52 - 6 * lg 3)``,
286                               ``random``)
287                         [high, low, random, h1, h2, lem1, lem2, lem3, lem4, lem5, lem6]
324 val random = Define
325    `random = {(\s:string. (0:num))}`;
327 val example5_conv = SIMP_CONV arith_ss [high, low, random, lem1,lem2,lem3];
329 val example5_output_conv = SIMP_CONV arith_ss [high, low, random, lem1,lem2,lem3]
334    ``leakage (unif_prog_space (high (SUC (SUC (SUC 0)))) (low (SUC (SUC (SUC 0)))) random) M5 = 0``,
337                               ``random``)
338                         [high, low, random, lem1, lem2, lem3]
375 val random = Define
376    `random = {(\s:string. ([]:num list))}`;
378 val example5'_conv = SIMP_CONV list_string_ss [high, low, random, lem7, lem8, APPEND, PAIR_EQ];
380 val example5'_output_conv = SIMP_CONV list_string_ss [high, low, random, lem7, lem8, APPEND, PAIR_EQ]
382                             THENC SIMP_CONV list_string_ss [high, low, random, lem7, lem8, APPEND];
386    ``leakage (unif_prog_space (high (SUC (SUC (SUC 0)))) (low (SUC (SUC (SUC 0)))) random) M5' = 2``,
390                               ``random``)
391                         [high, low, random, lem7, lem8, APPEND]
404 (* Example 8:    out = high XOR random *)
412 val random = Define
413    `(random 0 = {(\s:string. if s = "random" then 0 else 0)}) /\
414     (random (SUC n) = (\s:string. if s = "random" then SUC n else 0)INSERT(random n))`;
421         then w2n (((n2w (H s "high")):word2) ?? (n2w (R s "random"))) else 0))`;
423 val example8_conv = SIMP_CONV arith_ss [high, low, random, lem1, lem2, lem3, w2n_11];
425 val example8_output_conv = SIMP_CONV arith_ss [high, low, random, lem1, lem2, lem3, w2n_11]
428                             THENC SIMP_CONV arith_ss [high, low, random, lem1, lem2, lem3, w2n_11];
432    ``leakage (unif_prog_space (high (SUC (SUC (SUC 0)))) low (random (SUC (SUC (SUC 0))))) M8 = 0``,
435                               ``random (SUC (SUC (SUC 0)))``)
436                         [high, low, random, lem1,lem2]
450 (* Example 8':   out = high XOR random *)
462    (``!n. random n = if (n=0) then
463                 {(\s:string. if s = "random" then 0 else 0)}
465                 (\s:string. if s = "random" then n else 0)INSERT(random (n-1))``,
466      Induct ++ RW_TAC arith_ss [random]);
470    ``visible_leakage (unif_prog_space (high 3) low (random 3)) M8 = 2``,
474 ++ `FINITE (random 3)`
478 ++ `~ ((high 3) CROSS low CROSS (random 3) = {})`