1 | require import Pred. |
---|

2 | require import FMap. |
---|

3 | require import FSet. |
---|

4 | |
---|

5 | type from. |
---|

6 | type to. |
---|

7 | |
---|

8 | op dsample : to distr. (* Distribution to use on the target type *) |
---|

9 | |
---|

10 | (* A signature for random oracles from "from" to "to". *) |
---|

11 | module type Oracle = { |
---|

12 | proc init():unit |
---|

13 | proc o(x:from):to |
---|

14 | }. |
---|

15 | |
---|

16 | module type AdvRO = { proc o(x:from):to }. |
---|

17 | |
---|

18 | theory ROM. |
---|

19 | (* Bare random oracle for use in schemes *) |
---|

20 | module RO:Oracle = { |
---|

21 | var m : (from, to) map |
---|

22 | |
---|

23 | proc init() : unit = { |
---|

24 | m = FMap.empty; |
---|

25 | } |
---|

26 | |
---|

27 | proc o(x:from) : to = { |
---|

28 | var y : to; |
---|

29 | y = $dsample; |
---|

30 | if (!in_dom x m) m.[x] = y; |
---|

31 | return oget (m.[x]); |
---|

32 | } |
---|

33 | }. |
---|

34 | |
---|

35 | lemma lossless_init : islossless RO.init. |
---|

36 | proof. |
---|

37 | (* FILL ME *) |
---|

38 | qed. |
---|

39 | |
---|

40 | (* use the rnd tactic with predicate True *) |
---|

41 | lemma lossless_o : mu dsample True = 1%r => islossless RO.o. |
---|

42 | proof. |
---|

43 | (* FILL ME *) |
---|

44 | qed. |
---|

45 | |
---|

46 | equiv upto_o v: RO.o ~ RO.o : |
---|

47 | !mem v (dom RO.m){2} /\ ={x} /\ eq_except RO.m{1} RO.m{2} v ==> |
---|

48 | !mem v (dom RO.m){2} => ={res} /\ eq_except RO.m{1} RO.m{2} v. |
---|

49 | proof. |
---|

50 | (* FILL ME *) |
---|

51 | qed. |
---|

52 | |
---|

53 | lemma lossless_o_in_dom v: |
---|

54 | mu dsample True = 1%r => |
---|

55 | phoare[ RO.o: mem v (dom RO.m) ==> mem v (dom RO.m)] = 1%r. |
---|

56 | proof. |
---|

57 | (* FILL ME *) |
---|

58 | qed. |
---|

59 | |
---|

60 | theory UpTo. |
---|

61 | type result. |
---|

62 | |
---|

63 | module type Adv (RO:AdvRO)= { |
---|

64 | proc a1 () : from |
---|

65 | proc a2 (to:to) : result |
---|

66 | }. |
---|

67 | |
---|

68 | module Gfail(A:Adv) = { |
---|

69 | module A_ = A(RO) |
---|

70 | |
---|

71 | proc main () : from * result = { |
---|

72 | var fr, to, r; |
---|

73 | |
---|

74 | RO.init(); |
---|

75 | fr = A_.a1(); |
---|

76 | to = RO.o(fr); |
---|

77 | r = A_.a2(to); |
---|

78 | return (fr, r); |
---|

79 | } |
---|

80 | }. |
---|

81 | |
---|

82 | module Gfail'(A:Adv) = { |
---|

83 | module A_ = A(RO) |
---|

84 | |
---|

85 | proc main () : from * result = { |
---|

86 | var fr, to, r; |
---|

87 | |
---|

88 | RO.init(); |
---|

89 | fr = A_.a1(); |
---|

90 | to = $dsample; |
---|

91 | r = A_.a2(to); |
---|

92 | return (fr, r); |
---|

93 | } |
---|

94 | }. |
---|

95 | |
---|

96 | (* use the call tactic for abstract procedures with up to failure *) |
---|

97 | lemma Fail (A<:Adv{RO}): |
---|

98 | mu dsample True = 1%r => |
---|

99 | (forall (RO0 <: AdvRO {A}), islossless RO0.o => islossless A(RO0).a2) => |
---|

100 | equiv [Gfail(A).main ~ Gfail'(A).main: |
---|

101 | ={glob A} ==> |
---|

102 | let (fr,xxx) = res{2} in |
---|

103 | !(mem fr (dom RO.m)){2} => ={res, glob A} /\ eq_except RO.m{1} RO.m{2} fr]. |
---|

104 | proof. |
---|

105 | (* FILL ME *) |
---|

106 | qed. |
---|

107 | end UpTo. |
---|

108 | end ROM. |
---|

109 | |
---|