https://github.com/EasyCrypt/easycrypt
Tip revision: dc50f44bff4c40022c08e46832a16b676b3db0da authored by Pierre-Yves Strub on 26 May 2023, 09:54:58 UTC
Forbid the usage of [declare] for concrete modules.
Forbid the usage of [declare] for concrete modules.
Tip revision: dc50f44
PRP.eca
require import AllCore Distr.
pragma +implicits.
(** A PRP is a family of permutations F on domain D indexed by a
keyspace K equipped with a (lossless) distribution dK. **)
type D.
(** Security notions **)
(* -------------------------------------------------------------------- *)
abstract theory WeakPRP.
module type PRP = {
proc init(): unit
proc f(_ : D): D
}.
module type PRP_Oracles = {
proc f(_ : D): D
}.
module type Distinguisher (P : PRP_Oracles) = {
proc distinguish(): bool
}.
module IND (P : PRP) (D:Distinguisher) = {
proc main(): bool = {
var b;
P.init();
b <@ D(P).distinguish();
return b;
}
}.
end WeakPRP.
(* -------------------------------------------------------------------- *)
abstract theory StrongPRP.
module type PRP = {
proc init(): unit
proc f(_ : D): D
proc fi(_ : D): D
}.
module type SPRP_Oracles = {
proc f(_ : D): D
proc fi(_ : D): D
}.
module type Distinguisher (P : SPRP_Oracles) = {
proc distinguish(): bool
}.
module IND (P : PRP) (D:Distinguisher) = {
proc main(): bool = {
var b;
P.init();
b <@ D(P).distinguish();
return b;
}
}.
end StrongPRP.
(** Ideal and Real functionalities **)
(* -------------------------------------------------------------------- *)
abstract theory RP.
require import SmtMap FSet.
require import Dexcepted.
(*---*) import StdOrder.RealOrder RField.
op dD: { D distr | is_lossless dD } as dD_ll.
module RP = {
var m : (D,D) fmap
var mi: (D,D) fmap
proc init(): unit = {
m <- empty;
mi <- empty;
}
proc f(x:D): D = {
var y;
if (x \notin m) {
y <$ dD \ (rng m);
m.[x] <- y;
mi.[y] <- x;
}
return (oget m.[x]);
}
proc fi(y:D): D = {
var x;
if (y \notin mi) {
x <$ dD \ (rng mi);
mi.[y] <- x;
m.[x] <- y;
}
return (oget mi.[y]);
}
}.
(* -------------------------------------------------------------------- *)
pred is_permutation (m mi : (D,D) fmap) =
(forall x, x \in m => mi.[oget m.[x]] = Some x)
/\ (forall x, x \in mi => m.[oget mi.[x]] = Some x).
(* -------------------------------------------------------------------- *)
equiv f_perm: RP.f ~ RP.f:
={glob RP, x}
/\ is_permutation RP.m{1} RP.mi{1}
==> ={glob RP, res}
/\ is_permutation RP.m{1} RP.mi{1}.
proof.
proc; if=> //=; auto=> |> &2 is_perm x_notin_m yL.
rewrite supp_dexcepted rngE /= negb_exists=>- [] _ /= m__neq_yL.
split=> [x'|y']; rewrite !get_setE !mem_set.
+ case: (x' = x{2})=> //= x'_neq_x.
have [] mmi mim ^ /mmi mimx':= is_perm.
by rewrite mimx' domE; elim: (RP.m{2}.[x']) (m__neq_yL x')=> //= x0 ->.
by case: (y' = yL)=> //=; smt(domE).
qed.
(* -------------------------------------------------------------------- *)
equiv fi_perm: RP.fi ~ RP.fi:
={glob RP, y}
/\ is_permutation RP.m{1} RP.mi{1}
==> ={glob RP, res}
/\ is_permutation RP.m{1} RP.mi{1}.
proof.
proc; if=> //=; auto=> |> &2 is_perm y_notin_mi xL.
rewrite supp_dexcepted rngE /= negb_exists=>- [] _ /= mi__neq_xL.
split=> [x'|y']; rewrite !get_setE !mem_set.
+ case: (x' = xL)=> //=; smt(domE).
case: (y' = y{2})=> //= y'_neq_y.
have [] mmi mim ^ /mim mmiy':= is_perm.
by rewrite mmiy' domE; elim: (RP.mi{2}.[y']) (mi__neq_xL y')=> //= y0 ->.
qed.
(* -------------------------------------------------------------------- *)
(** TODO: brutal carry over from SmtMap -- needs more elegance **)
lemma leq_card_rng_dom (m:('a,'b) fmap):
card (frng m) <= card (fdom m).
proof.
elim/fset_ind: (fdom m) {-2}m (eq_refl (fdom m))=> {m} [m /fdom_eq0 ->|].
+ by rewrite frng0 fdom0 !fcards0.
move=> x s x_notin_s ih m dom_m.
have ->: m = (rem m x).[x <- oget m.[x]].
+ apply/fmap_eqP=> x'; rewrite get_setE remE; case: (x' = x)=> [->>|//].
have /fsetP /(_ x):= dom_m; rewrite in_fsetU in_fset1 /= mem_fdom domE.
by case: m.[x].
have ->: frng (rem m x).[x <- oget m.[x]] = frng (rem m x) `|` fset1 (oget m.[x]).
+ apply/fsetP=> y'; rewrite in_fsetU in_fset1 !mem_frng !rngE /=.
split=> [[] a|].
+ rewrite get_setE remE; case: (a = x)=> [->>|a_neq_x ma_y'].
+ rewrite -some_oget 1:-domE 1:-mem_fdom 1:dom_m 1:in_fsetU 1:in_fset1 //.
by move=> ->.
by left; exists a; rewrite remE a_neq_x.
case=> [[a]|->].
+ rewrite remE; case: (a = x)=> //= x_neq_a ma_y'.
by exists a; rewrite get_setE remE x_neq_a.
by exists x; rewrite get_set_sameE.
rewrite fcardU fsetI1 fun_if !fcard1 fcards0.
rewrite fdom_set fcardUI_indep 2:fcard1.
+ by apply/fsetP=> x0; rewrite in_fsetI fdom_rem !inE -andbA andNb.
rewrite StdOrder.IntOrder.ler_subl_addr; apply/StdOrder.IntOrder.ler_paddr.
+ by case: (mem (frng _) _).
apply/StdOrder.IntOrder.ler_add2r/ih/fsetP=> x0.
by rewrite fdom_rem dom_m !inE; case: (x0 = x).
qed.
lemma endo_dom_rng (m:('a,'a) fmap):
(exists x, x \notin m) =>
exists x, !rng m x.
proof.
elim=> x x_notin_m.
have h: 0 < card (((fdom m) `|` fset1 x) `\` (frng m)); last first.
+ have [a]: exists a, a \in (fdom m `|` fset1 x) `\` frng m.
+ have ->: forall b, b = !!b by done.
rewrite negb_exists /= -negP=> /in_eq_fset0 h'.
by move: h' h=> ->; rewrite fcards0.
by rewrite in_fsetD mem_frng=> - [] _ a_notin_rng_m; exists a.
rewrite fcardD fcardUI_indep.
+ by apply/fsetP=> x'; rewrite !inE mem_fdom /#.
rewrite fcard1 fsetIUl fcardUI_indep.
+ by apply/fsetP=> x'; rewrite !inE mem_fdom /#.
have ->: card (fset1 x `&` frng m) = if x \in (frng m) then 1 else 0.
+ smt (@FSet).
by move: x_notin_m; rewrite -mem_fdom; smt (leq_card_rng_dom @FSet).
qed.
lemma f_ll: is_full dD => islossless RP.f.
proof.
move=> dD_fu.
proc; if=> //=; auto=> /> &m h.
have [] x0 x0_notinr_m:= endo_dom_rng RP.m{m} _.
+ by exists x{m}.
rewrite -/predT weight_dexcepted.
case: {-1}(mu _ _ = mu _ _)
(eq_refl (mu dD predT = mu dD (rng RP.m{m})))=> //=.
rewrite eqT -subr_eq0 ltr0_neq0 //.
rewrite (@mu_split _ _ (rng RP.m{m})) /predI /predT /predC /=.
rewrite addrC addrA (addrC (-_)%Real) addrN add0r.
apply/(ltr_le_trans (mu dD (pred1 x0))).
+ by apply: dD_fu.
by apply/mu_sub=> x ->.
qed.
(* -------------------------------------------------------------------- *)
lemma fi_ll: is_full dD => islossless RP.fi.
proof.
move=> dD_fu.
proc; if=> //=; auto=> /> &m h.
have [] y0 y0_notinr_mi:= endo_dom_rng RP.mi{m} _.
+ by exists y{m}.
rewrite -/predT weight_dexcepted.
case: {-1}(mu _ _ = mu _ _)
(eq_refl (mu dD predT = mu dD (rng RP.mi{m})))=> //=.
rewrite eqT -subr_eq0 ltr0_neq0 //.
rewrite (@mu_split _ _ (rng RP.mi{m})) /predI /predT /predC /=.
rewrite addrC addrA (addrC (-_)%Real) addrN add0r.
apply/(ltr_le_trans (mu dD (pred1 y0))).
+ by apply: dD_fu.
by apply/mu_sub=> y ->.
qed.
abstract theory RP_RF.
require import List.
require (*--*) PRF Birthday.
op q : { int | 0 <= q } as ge0_q.
axiom dD_funi: is_funiform dD.
lemma dD_fu: is_full dD.
proof.
apply: funi_ll_full.
+ exact/dD_funi.
exact/dD_ll.
qed.
lemma dD_uni: is_uniform dD.
proof. exact/funi_uni/dD_funi. qed.
clone import PRF as PRFt with
type D <- D,
type R <- D.
clone import RF as PRFi with
op dR _ <- dD
proof * by smt(dD_ll)
rename "RF" as "PRFi".
(** The proof starts with some useful definitions and lemmas **)
(* In the proof, we consider the following bad event (applied to the
PRF's internal map):
"A collision occurs in map m whenever there exist distinct x and
x' that are both in m's domain and have the same image by m." *)
pred collision (m:(D,D) fmap) = exists x x',
x' <> x /\
x \in m /\ x' \in m /\ m.[x] = m.[x'].
(* Some useful facts about the bad event *)
lemma no_collision (m:(D,D) fmap):
!collision m <=>
forall x x',
x' = x \/
!x \in m \/
!x' \in m \/
m.[x] <> m.[x'].
proof.
rewrite /collision negb_exists /=; apply/forall_iff=> /= x.
by rewrite negb_exists /=; apply/forall_iff=> /= x'; rewrite !negb_and.
qed.
lemma collision_add (m:(D,D) fmap) x y:
!x \in m =>
collision m.[x <- y] <=> collision m \/ rng m y.
proof.
move=> x_notin_m; split=> [[z z' [z'_neq_z]]|].
+ rewrite mem_set=> -[z_in_m] [z'_in_m] mz_eq_mz'.
case (rng m y)=> //= y_notin_rngm.
by exists z z'; smt(@SmtMap).
move=> [[z z' [z'_neq_z] [z_in_m] [z'_in_m] mz_eq_mz']|].
+ exists z z'; rewrite z'_neq_z !mem_set !get_setE mz_eq_mz' z_in_m z'_in_m /=.
move/contra: (congr1 (dom m) z x); rewrite x_notin_m z_in_m=> -> //=.
by move/contra: (congr1 (dom m) z' x); rewrite x_notin_m z'_in_m=> -> //=.
rewrite rngE=> - /= [x'] mx'_y.
by exists x x'; smt(@SmtMap).
qed.
lemma collision_stable (m:(D,D) fmap) y y':
collision m =>
y \notin m =>
collision m.[y <- y'].
proof. by move=> h /collision_add /= ->; rewrite h. qed.
(** To factor out the difficult step, we parameterize the PRP by a
procedure that samples its output, and provide two instantiations
of it. **)
module type Sample_t = {
proc sample(X:D -> bool): D
}.
module Direct = {
proc sample(X:D -> bool): D = {
var r;
r <$ dD \ X;
return r;
}
}.
module Indirect = {
proc sample(X:D -> bool): D = {
var r;
r <$ dD;
if (X r) {
r <$ dD \ X;
}
return r;
}
}.
module PRPi'(S:Sample_t) = {
proc init = RP.init
proc f(x:D): D = {
var r;
if (x \notin RP.m) {
r <@ S.sample(rng RP.m);
RP.m.[x] <- r;
}
return oget RP.m.[x];
}
}.
lemma nosmt notin_supportIP (P : 'a -> bool) (d : 'a distr):
(exists a, support d a /\ !P a) <=> mu d P < mu d predT.
proof.
rewrite (@mu_split _ predT P) /predI /predT /predC /=.
rewrite (@exists_eq (fun a => support d a /\ !P a) (fun a => !P a /\ a \in d)) /=.
+ by move=> a /=; rewrite andbC.
by rewrite -(@witness_support (predC P)) -/(predC _) /#.
qed.
(* Some losslessness lemmas *)
lemma excepted_lossless (m:(D,D) fmap):
(exists x, x \notin m) =>
mu (dD \ (rng m)) predT = 1%r.
proof.
move=> /endo_dom_rng [x h]; rewrite dexcepted_ll 1:dD_ll //.
by rewrite -dD_ll; apply/notin_supportIP; exists x=> />; exact/dD_fu.
qed.
lemma excepted_lossless_mem (m:(D,D) fmap):
(exists x, x \notin m) =>
is_lossless (dD \ (mem (frng m))).
proof.
have ->: mem (frng m) = rng m.
+ by apply/fun_ext=> a; rewrite mem_frng.
exact/excepted_lossless.
qed.
phoare Indirect_ll: [Indirect.sample: exists x, support dD x /\ !X x ==> true] = 1%r.
proof.
proc; seq 1: (exists x, support dD x /\ !X x)=> //=.
+ by rnd (predT); auto; rewrite dD_ll /#.
if=> //=.
+ rnd (predT); auto=> /> &m x _ x_notin_X _.
rewrite dexcepted_ll 1:dD_ll // -dD_ll; apply/notin_supportIP; exists x.
by rewrite dD_fu.
by hoare; auto=> />.
qed.
lemma PRPi'_Indirect_ll: islossless PRPi'(Indirect).f.
proof.
proc; if=> //=; wp; call Indirect_ll.
auto=> /> &m x_notin_m.
have:= excepted_lossless (RP.m{m}) _.
+ by exists x{m}.
rewrite weight_dexcepted.
case (weight dD = mu dD (rng RP.m{m}))=> //=.
rewrite notin_supportIP /=.
by rewrite StdOrder.RealOrder.ltr_def=> -> /=; exact/mu_sub.
qed.
(** The proof is cut into 3 parts (sections):
- We first focus on proving
Pr[IND(PRPi'(Indirect),D).main() @ &m: res]
<= Pr[IND(PRFi,D).main() @ &m: res]
+ Pr[IND(PRFi,D).main() @ &m: collision PRFi.m].
- Second, we concretely bound (when the PRF oracle stops
answering queries after the q-th):
Pr[IND(PRFi,D).main() @ &m: collision PRFi.m]
<= q^2 * Pr[x = $uD: x = witness]
- We conclude by proving (difficult!)
Pr[IND(PRPi,D).main() @ &m: res]
= Pr[IND(PRPi'(Indirect),D).main() @ &m: res].
**)
section Upto.
declare module D <: PRFt.Distinguisher {-RP, -PRFi}.
declare axiom D_ll (O <: PRF_Oracles {-D}): islossless O.f => islossless D(O).distinguish.
local module PRP_indirect_bad = {
var bad : bool
proc init(): unit = {
RP.init();
bad <- false;
}
proc sample(X:D -> bool): D = {
var r;
r <$ dD;
if (X r) {
bad <- true;
r <$ dD \ X;
}
return r;
}
proc f(x:D): D = {
var r;
if (x \notin RP.m) {
r <@ sample(rng RP.m);
RP.m.[x] <- r;
}
return oget RP.m.[x];
}
}.
local lemma PRPi'_Indirect_eq &m:
Pr[IND(PRPi'(Indirect),D).main() @ &m: res]
= Pr[IND(PRP_indirect_bad,D).main() @ &m: res].
proof. by byequiv=> //=; proc; inline *; sim. qed.
(** Upto failure: if a collision does not occur in PRFi.m, then the
programs are equivalent **)
lemma pr_PRPi'_Indirect_PRFi &m:
`|Pr[IND(PRPi'(Indirect),D).main() @ &m: res] - Pr[IND(PRFi,D).main() @ &m: res]|
<= Pr[IND(PRFi,D).main() @ &m: collision PRFi.m].
proof.
rewrite (PRPi'_Indirect_eq &m).
byequiv: PRP_indirect_bad.bad=> //=; 2:by smt().
proc.
call (_: collision PRFi.m,
={m}(RP,PRFi) /\ (PRP_indirect_bad.bad{1} <=> collision PRFi.m{2}),
PRP_indirect_bad.bad{1} <=> collision PRFi.m{2}).
+ exact D_ll.
+ proc.
if=> //=; inline *.
swap{1} 1.
seq 1 2: (={x} /\
x{1} \notin RP.m{1} /\
PRFi.m{2} = RP.m.[x <- r0]{1} /\
((PRP_indirect_bad.bad \/ rng RP.m r0){1} <=> collision PRFi.m{2})).
+ auto => /> &1 &2 coll _ x_notin_m r _; split=> [|x0 x'].
+ rewrite rngE /= /collision=> - [x'] mx'; exists x{2} x'; smt(domE get_setE).
smt (rngE get_setE).
sp; if{1}.
+ conseq (_: _ ==> collision PRFi.m{2} /\ PRP_indirect_bad.bad{1})=> //.
auto=> /> &1 &2 x_notin_m coll_def rng_m_r; smt.
by auto; smt. (** FIXME: Investigate **)
move=> &2 bad; conseq (_: true ==> true: =1%r) (_: PRP_indirect_bad.bad ==> PRP_indirect_bad.bad)=> //=.
+ by proc; if=> //=; inline *; seq 2: PRP_indirect_bad.bad; [auto|if=> //=; auto].
proc; if=> //=; inline *.
seq 2: (X = rng RP.m /\ x \notin RP.m) 1%r 1%r 0%r _=> //=;
[auto|if=> //=; auto|hoare; auto]=> />;rewrite ?dD_ll //.
by move=> &hr x_notin_m r_in_rng_m; apply excepted_lossless; exists x{hr}.
move=> &1; conseq (_: collision PRFi.m ==> collision PRFi.m: =1%r)=> //=.
by proc; if; auto=> />; rewrite dD_ll //=; smt(domE get_setE).
inline *; auto=> />; split=> [|_].
+ by rewrite no_collision=> x x'; rewrite mem_empty.
move=> /> rL rR DL b mL DR mR [-> //| /#].
qed.
end section Upto.
(** This section proves the equivalence between the Ideal PRP and the
module PRPi'(Indirect) used in section Upto. **)
section PRPi_PRPi'_Indirect.
local clone include Dexcepted.TwoStepSampling with
type i <- unit,
type t <- D,
op dt _ <- dD
proof *.
(* The key is in proving that Direct.sample and Indirect.sample
define the same distribution. We do this by extensional equality
of distributions:
forall a, Pr[Direct.sample: res = a] = Pr[Indirect.sample: res = a]. *)
equiv eq_Direct_Indirect: Direct.sample ~ Indirect.sample: ={X} ==> ={res}.
proof.
proc.
rewrite equiv [{1} ll_direct_indirect_eq ((), fun _ => X) r ((), fun _ => X) r].
+ move=> />; exact dD_ll.
sp; seq 1 1: ((X0 = fun _ => X){1} /\ ={X} /\ r0{1} = r{2}); auto.
by if; auto.
qed.
(* The rest is easy *)
local equiv eq_PRPi_PRPi'_Indirect: RP.f ~ PRPi'(Indirect).f:
={x, RP.m} ==> ={res, RP.m}.
proof.
transitivity PRPi'(Direct).f (={RP.m,x} ==> ={RP.m,res}) (={RP.m,x} ==> ={RP.m,res}).
+ by move=> &1 &2 [->> ->>]; exists RP.m{2} x{2}.
+ done.
+ by proc; inline *; if=> //=; auto.
+ by proc; if=> //=; wp; call eq_Direct_Indirect.
qed.
declare module D <: Distinguisher { -RP }.
lemma pr_PRPi_PRPi'_Indirect &m:
Pr[IND(RP,D).main() @ &m: res] = Pr[IND(PRPi'(Indirect),D).main() @ &m: res].
proof.
byequiv=> //=.
proc.
call (_: ={RP.m}).
by apply eq_PRPi_PRPi'_Indirect.
by inline*; auto.
qed.
end section PRPi_PRPi'_Indirect.
section CollisionProbability.
declare module D <: Distinguisher {-RP, -PRFi}.
declare axiom D_ll (O <: PRF_Oracles {-D}): islossless O.f => islossless D(O).distinguish.
declare axiom D_bounded : hoare [D(PRFi).distinguish : PRFi.m = empty ==> card (fdom PRFi.m) <= q].
local clone import Birthday as BBound with
op q <- q,
type T <- D,
op uT <- dD,
op maxu <- witness
proof *.
realize ge0_q by apply ge0_q.
realize maxuP.
proof.
by move=> x; exact/StdOrder.RealOrder.lerr_eq/dD_funi.
qed.
(* We construct a Birthday Bound adversary from the IND
experiment. *)
local module (A:Adv) (S:ASampler) = {
(* We simulate an f-oracle using the s-oracle *)
module F = {
proc init = PRFi.init
proc f(x:D): D = {
var r;
if (x \notin PRFi.m) {
r <@ S.s();
PRFi.m.[x] <- r;
}
return oget PRFi.m.[x];
}
}
(* Recall from the Birthday clone that Birthday Bound adversaries
are restricted to make at most q oracle queries. *)
module IND = IND(F,D)
proc a(): unit = {
var b:bool;
b <@ IND.main();
}
}.
local lemma A_ll (S <: ASampler {-A}): islossless S.s => islossless A(S).a.
proof.
move=> S_ll; proc; inline*; wp.
call (_: true).
+ exact D_ll.
+ by proc; inline*; do!(sp; if=> //=; auto); wp; call S_ll.
by inline*; auto.
qed.
local equiv IND_Exp :
A(Sample).a ~ IND(PRFi,D).main : ={glob D} /\ size Sample.l{1} = 0 ==>
(collision PRFi.m{2} <=> !uniq Sample.l{1}) /\
size Sample.l{1} = card (fdom PRFi.m){2}.
proof.
proc; inline*; wp.
call (_: ={PRFi.m} /\
size Sample.l{1} = card (fdom PRFi.m){2} /\
(forall x, mem (frng PRFi.m) x <=> mem Sample.l x){1} /\
(collision PRFi.m{2} <=> !uniq Sample.l{1})).
+ proc; inline*.
if => //=.
auto => /> &1 &2 h1 h2 h3 h4 r _.
rewrite fdom_set fcardUI_indep 2:fcard1; 1: by rewrite fsetI1 mem_fdom h4.
smt(get_setE mem_frng rngE collision_add).
auto; smt (size_eq0 fdom0 fcards0 frng0 in_fset0 mem_empty).
qed.
local hoare IND_bounded : IND(PRFi,D).main : true ==> card (fdom PRFi.m) <= q.
proof. proc; call D_bounded; inline *;auto. qed.
lemma pr_PRFi_collision &m:
Pr[IND(PRFi,D).main() @ &m: collision PRFi.m]
<= (q*(q-1))%r/2%r * mu1 dD witness.
proof.
apply (ler_trans (Pr[Exp(Sample,A).main() @ &m: !uniq Sample.l])).
+ byequiv => //.
symmetry; proc *; inline Exp(Sample, A).main.
by call IND_Exp; inline *; auto => /#.
apply (pr_collision A A_ll _ &m).
conseq IND_Exp IND_bounded => /#.
qed.
lemma Conclusion &m:
`|Pr[IND(RP, D).main() @ &m: res]- Pr[IND(PRFi,D).main() @ &m: res]|
<= (q*(q-1))%r/2%r * mu1 dD witness.
proof.
move: (pr_PRPi_PRPi'_Indirect D &m) (pr_PRPi'_Indirect_PRFi D D_ll &m) (pr_PRFi_collision &m) => /#.
qed.
end section CollisionProbability.
module FBounder (F : PRF_Oracles) = {
var c:int
proc f(x:D): D = {
var r <- witness;
if (c < q) {
r <@ F.f(x);
c <- c + 1;
}
return r;
}
}.
module DBounder (D : Distinguisher) (F : PRF_Oracles) = {
proc distinguish(): bool = {
var b;
FBounder.c <- 0;
b <@ D(FBounder(F)).distinguish();
return b;
}
}.
section BOUNDER.
declare module D <: Distinguisher {-RP, -PRFi, -DBounder}.
declare axiom D_ll (O <: PRF_Oracles {-D}): islossless O.f => islossless D(O).distinguish.
lemma DBounder_ll (O <: PRF_Oracles{-DBounder(D)}):
islossless O.f => islossless DBounder(D, O).distinguish.
proof.
move=> hll; islossless.
by apply (D_ll (FBounder(O))); islossless.
qed.
hoare DBounder_card : DBounder(D, PRFi).distinguish : PRFi.m = empty ==> card (fdom PRFi.m) <= q.
proof.
proc.
call (: card (fdom PRFi.m) <= FBounder.c /\ FBounder.c <= q).
+ proc; sp; if => //.
inline *; sp; wp; if; auto; smt(fdom_set fcardU fcard1 fcard_ge0).
auto; smt(fdom0 fcards0 ge0_q).
qed.
lemma Conclusion_DBounder &m:
`|Pr[IND(RP, DBounder(D)).main() @ &m: res]- Pr[IND(PRFi,DBounder(D)).main() @ &m: res]|
<= (q*(q-1))%r/2%r * mu1 dD witness.
proof. apply (Conclusion (DBounder(D)) DBounder_ll DBounder_card &m). qed.
end section BOUNDER.
end RP_RF.
end RP.
(* -------------------------------------------------------------------- *)
abstract theory PseudoRP.
type K.
op dK: { K distr | is_lossless dK } as dK_ll.
op p : K -> D -> D.
op pi: K -> D -> D.
axiom pK k:
support dK k =>
cancel (p k) (pi k)
/\ cancel (pi k) (p k).
module type PseudoRP = {
proc keygen(): K
proc f(_ : K * D): D
proc fi(_ : K * D): D
}.
module PseudoRP = {
proc keygen() = {
var k;
k <$ dK;
return k;
}
proc f(k, x) = { return p k x; }
proc fi(k, x) = { return pi k x; }
}.
module PRP = {
var k : K
proc init() = { k <$ dK; }
proc f(x : D) = { return p k x; }
proc fi(x : D) = { return pi k x; }
}.
end PseudoRP.