From 2ca18f4ee1b34be793299dbd86be4fc5bc1a304b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Dupressoir?= Date: Wed, 3 Jun 2026 15:30:49 +0100 Subject: [PATCH] [cryptolib] generalize PRF definitions, PRP<->PRF MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This takes a swipe at cleaning up the PRF and PRP theories, as well as the associated switching lemmas. This should bring them more in line with modern EasyCrypt practice while also making them better examples of modern EasyCrypt development themselves—perhaps serving as advanced tutorials. --- theories/crypto/PRF.eca | 27 +- theories/crypto/prp_prf/RP_RF.eca | 307 +++++++++ theories/crypto/prp_prf/Strong_RP_RF.eca | 771 +++++++++-------------- 3 files changed, 629 insertions(+), 476 deletions(-) create mode 100644 theories/crypto/prp_prf/RP_RF.eca diff --git a/theories/crypto/PRF.eca b/theories/crypto/PRF.eca index 8725b35214..4de755096e 100644 --- a/theories/crypto/PRF.eca +++ b/theories/crypto/PRF.eca @@ -57,30 +57,23 @@ end RF. abstract theory PseudoRF. type K. -op dK: { K distr | is_lossless dK } as dK_ll. - -op F : K -> D -> R. - module type PseudoRF = { proc keygen(): K - proc f(_ : K * D): R + proc f(_: K * D): R }. -module PseudoRF = { - proc keygen() = { - var k; +module PRF (P : PseudoRF) = { + var k : K - k <$ dK; - return k; + proc init() = { + k <@ P.keygen(); } - proc f(k, x) = { return F k x; } -}. - -module PRF = { - var k : K + proc f(x: D) = { + var r; - proc init() = { k <$ dK; } - proc f(x: D) = { return F k x; } + r <@ P.f(k, x); + return r; + } }. end PseudoRF. diff --git a/theories/crypto/prp_prf/RP_RF.eca b/theories/crypto/prp_prf/RP_RF.eca new file mode 100644 index 0000000000..5247596981 --- /dev/null +++ b/theories/crypto/prp_prf/RP_RF.eca @@ -0,0 +1,307 @@ +require import AllCore Distr List FSet FMap. +require import Dexcepted. +require (*--*) PRP. +(*---*) import RField StdOrder.RealOrder. + +require (*--*) FelTactic. + +(** We assume a finite domain D, equipped with a full and lossless +distribution. (We need fullness and losslessness to know that +resampling always works.) **) +type D. + +op [lossless full] dD: D distr. +op hmin_dD: { real | forall x, mu1 dD x <= hmin_dD } as hmin_dDP. + +lemma ge0_hmin_dD: 0%r <= hmin_dD. +proof. +apply: (ler_trans (mu1 dD witness)). ++ exact: ge0_mu. +exact: hmin_dDP. +qed. + +(** and a type K equipped with a lossless distribution **) +type K. + +clone import PRP as PRPt with + type D <- D +proof *. + +clone import StrongPRP as PRPSec +proof *. + +clone import RP as PRPi with + op dD <- dD +proof * +rename "RP" as "PRPi". +realize dD_ll by exact: dD_ll. + +clone import PRF as PRFt with + type D <- D, + type R <- D +proof *. + +clone import RF with + op dR _ <- dD +proof * +rename "RF" as "PRFi". +realize dR_ll by rewrite dD_ll. + +module Count (P: PRF): PRF = { + var count: int + + proc init() = { + P.init(); + count <- 0; + } + + proc f(x) = { + var r; + + r <@ P.f(x); + count <- count + 1; + return r; + } +}. + +section. + +(** The following is a proof that holds **) +(** For all lossless distinguisher D ... **) +declare module D <: Distinguisher { -PRPi, -PRFi, -Count }. +declare axiom D_ll (O <: PRF_Oracles {-D}): islossless O.f => islossless D(O).distinguish. + +(** ... that makes at most q queries for some non-negative q. **) +declare op q : { int | 0 <= q } as ge0_q. +declare axiom D_count (O <: PRF { -D, -Count }) c0: + hoare [D(Count(O)).distinguish: Count.count = c0 ==> Count.count <= c0 + q]. + +(** We make use of a generic principle for sampling in a conditional + distribution **) +local clone import TwoStepSampling with + type i <- unit, + type t <- D, + op dt _ <- dD +proof *. + +(** And we put some work into turning our random function (PRFi) and + random permutation (PRPi) into part of a distinguisher against a + sampling procedure. **) +local module type Sample_t = { + proc sample(X: D -> bool): D +}. + +local module Direct : Sample_t = { + proc sample(X) = { + var r; + + r <@ S.direct((), fun _=> X); + return r; + } +}. + +local module Indirect : Sample_t = { + proc sample(X) = { + var r; + + r <@ S.indirect((), fun _=> X); + return r; + } +}. + +local equiv eq_Direct_Indirect: + Direct.sample ~ Indirect.sample: ={X} ==> ={res}. +proof. +by proc; call ll_direct_indirect_eq; auto; rewrite dD_ll. +qed. + +local module PRPi' (S:Sample_t) = { + proc init = PRPi.init + + proc f(x:D): D = { + var r; + if (x \notin PRPi.m) { + r <@ S.sample(rng PRPi.m); + PRPi.m.[x] <- r; + } + return oget PRPi.m.[x]; + } +}. + +(* We need bad flags *) +local module PRFi'_bad = { + var bad: bool + + proc init() = { + PRPi.init(); + bad <- false; + } + + proc f(x: D): D = { + var r; + + if (x \notin PRPi.m) { + r <$ dD; + bad <- bad \/ rng PRPi.m r; + PRPi.m.[x] <- r; + } + return oget PRPi.m.[x]; + } +}. + +local module PRPi'_bad = { + proc init() = { + PRPi.init(); + PRFi'_bad.bad <- false; + } + + proc f(x: D): D = { + var r; + + if (x \notin PRPi.m) { + r <$ dD; + if (rng PRPi.m r) { + PRFi'_bad.bad <- true; + r <$ dD \ (rng PRPi.m); + } + PRPi.m.[x] <- r; + } + return oget PRPi.m.[x]; + } +}. + +(* FIXME: lift out and share with Strong RP RF *) +local lemma 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. + +local 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; rewrite dD_fu. +qed. + +(** We split this into extremely small steps, but this is not + necessary **) +local lemma pr_PRPi_PRPi'_Direct &m: + Pr[IND(PRPi, D).main() @ &m: res] + = Pr[IND(PRPi'(Direct), D).main() @ &m:res]. +proof. +byequiv=> //; proc; call (: ={PRPi.m}). ++ by proc; if=> //; inline *; auto. +by inline *; auto. +qed. + +local lemma pr_PRPi'_Direct_PRPi'_Indirect &m: + Pr[IND(PRPi'(Direct), D).main() @ &m: res] + = Pr[IND(PRPi'(Indirect), D).main() @ &m: res]. +proof. +byequiv=> //; proc; call (: ={PRPi.m}). ++ proc; if=> //; auto. + by call eq_Direct_Indirect; auto=> |>; rewrite dD_ll. +by inline *; auto. +qed. + +local lemma pr_PRPi'_Indirect_PRPi'_bad &m: + Pr[IND(PRPi'(Indirect), D).main() @ &m: res] + = Pr[IND(PRPi'_bad, D).main() @ &m: res]. +proof. +byequiv=> //; proc; call (: ={PRPi.m}). ++ proc; if=> //; inline *. + do ! cfold {1} 1. + seq 1 1: (#pre /\ r1{1} = r{2}); 1:by auto. + by if=> //; auto. +by inline *; auto. +qed. + +local lemma pr_PRFi'_PRFi &m: + Pr[IND(PRFi, D).main() @ &m: res] + = Pr[IND(PRFi'_bad, D).main() @ &m: res]. +proof. +byequiv=> //; proc; call (: ={m}(PRFi, PRPi)); 1:by sim. +by inline *; auto. +qed. + +local lemma pr_PRPi'_Indirect_PRFi &m: + `| Pr[IND(PRPi'_bad, D).main() @ &m: res] + - Pr[IND(PRFi, D).main() @ &m: res]| + <= Pr[IND(PRFi'_bad, D).main() @ &m: PRFi'_bad.bad]. +proof. +rewrite pr_PRFi'_PRFi; byequiv: PRFi'_bad.bad=> //=; 2:smt(). +proc. +call (: PRFi'_bad.bad + , !PRFi'_bad.bad{2} /\ ={PRPi.m} /\ ={PRFi'_bad.bad} + , PRFi'_bad.bad{2} /\ ={PRFi'_bad.bad}). ++ exact: D_ll. ++ proc; if=> //=; inline *. + seq 1 1: (#pre /\ ={r}); 1:by auto. + if {1}; auto=> |> &1 _ x_notin_m _. + by apply: excepted_lossless; exists x{1}. ++ move=> &2 bad; proc; if; 2:by auto. + seq 1: (PRFi'_bad.bad{2} /\ PRFi'_bad.bad = PRFi'_bad.bad{2} /\ x \notin PRPi.m)=> //. + + by auto=> |>; rewrite dD_ll. + + if; auto=> |> &1 _ x_notin_m _ @/predT /=. + by apply: excepted_lossless; exists x{1}. + + by hoare; auto. + + by move=> &1; proc; if; auto=> |>; rewrite dD_ll. +by inline *; auto=> |> /#. +qed. + +import StdBigop.Bigreal BRA. + +local lemma pr_PRFi'_bad &m: + Pr[IND(PRFi'_bad, D).main() @ &m: PRFi'_bad.bad] + <= (q^2 - q)%r / 2%r * hmin_dD. +proof. +(** This is easier than instantiating Birthday bound, still **) +have ->: Pr[IND(PRFi'_bad, D).main() @ &m: PRFi'_bad.bad] + = Pr[IND(Count(PRFi'_bad), D).main() @ &m: PRFi'_bad.bad /\ Count.count <= q]. ++ byequiv (: ={glob D} ==> ={PRFi'_bad.bad} /\ Count.count{2} <= q)=> //. + conseq (: _ ==> ={PRFi'_bad.bad}) _ (: _ ==> Count.count <= q)=> //. + + by proc; call (D_count PRFi'_bad 0); inline *; auto. + proc; call (: ={PRPi.m, PRFi'_bad.bad})=> //. + + by proc; inline *; sp; if; auto. + by inline *; auto. +fel 1 (Count.count) (fun i=> i%r * hmin_dD) q + PRFi'_bad.bad + [] (card (frng PRPi.m) <= Count.count)=> //. ++ by rewrite -mulr_suml sumidE 1:ge0_q mulrDr expr2 mulrN1. ++ by inline *; auto=> |>; rewrite frng0 fcards0. ++ exlim Count.count=> c; conseq (: _: <= (c%r * hmin_dD))=> //. + proc; inline *; sp; if=> //. + + wp; rnd (rng PRPi.m); auto=> |> &0 ge0_count lt_count_q. + move=> _ size_rng_m _; rewrite (mu_eq _ _ (mem (frng PRPi.m{0}))). + + by move=> x; rewrite mem_frng. + apply: (ler_trans ((card (frng PRPi.m{0}))%r * hmin_dD)). + + by apply: Mu_mem.mu_mem_le=> x _; exact: hmin_dDP. + apply: ler_wpmul2r; 1:exact: ge0_hmin_dD. + by apply: le_fromint=> /#. + by hoare; auto=> |>; smt(ge0_hmin_dD). ++ move=> c; proc; inline *; sp; if; auto=> |>; 2:smt(). + move=> &0 card_rng_m x_notin_m r _; split=> [/#|]. + have ->: frng PRPi.m.[x <- r]{0} = frng PRPi.m{0} `|` fset1 r. + + apply: fsetP=> z; rewrite in_fsetU1 !mem_frng. + rewrite rng_set; congr; congr. + apply: fmap_eqP=> z0; rewrite remE. + case: (z0 = x{0})=> |>. + by move: x_notin_m; rewrite domE=> /= ->. + by rewrite fcardU1; smt(). +qed. + +lemma RP_RF_Switching &m: + `| Pr[IND(PRPi, D).main() @ &m: res] + - Pr[IND(PRFi, D).main() @ &m: res]| + <= (q ^ 2 - q)%r / 2%r * hmin_dD. +proof. +rewrite (pr_PRPi_PRPi'_Direct &m) (pr_PRPi'_Direct_PRPi'_Indirect &m). +rewrite (pr_PRPi'_Indirect_PRPi'_bad &m). +smt(pr_PRPi'_Indirect_PRFi pr_PRFi'_bad). +qed. +end section. diff --git a/theories/crypto/prp_prf/Strong_RP_RF.eca b/theories/crypto/prp_prf/Strong_RP_RF.eca index 435ecbadcf..735dfe8257 100644 --- a/theories/crypto/prp_prf/Strong_RP_RF.eca +++ b/theories/crypto/prp_prf/Strong_RP_RF.eca @@ -5,55 +5,62 @@ require (*--*) PRP. require (*--*) FelTactic. -(** We assume a finite domain D, equipped with its uniform +(** We assume a finite domain D, equipped with a full and lossless distribution. **) type D. -op uD: { D distr | is_uniform uD /\ is_lossless uD /\ is_full uD } as uD_uf_fu. +op [lossless full] dD: D distr. -(** and a type K equipped with a lossless distribution **) +op hmin_dD: { real | forall d, mu1 dD d <= hmin_dD } as hmin_dDP. + +lemma ge0_hmin_dD: 0%r <= hmin_dD. +proof. +apply: (ler_trans (mu1 dD witness)). ++ exact: ge0_mu. +exact: hmin_dDP. +qed. + +(** and a type K **) type K. -op dK: { K distr | is_lossless dK } as dK_ll. clone import PRP as PRPt with - type D <- D. + type D <- D +proof *. -clone import StrongPRP as PRPSec. +clone import StrongPRP as PRPSec +proof *. clone import RP as PRPi with - op dD <- uD -proof * by smt(uD_uf_fu) + op dD <- dD +proof * rename "RP" as "PRPi". +realize dD_ll by smt(dD_ll). (* This is an "Almost (Random Permutation)" (the Almost applies to Permutation) *) (* We keep track of collisions explicitly because it's going to be useful anyway *) module ARP = { - var coll : bool - var m, mi: (D,D) fmap + var m, mi: (D, D) fmap proc init(): unit = { m <- empty; mi <- empty; - coll <- false; } - proc f(x : D) = { + proc f(x: D) = { var y; if (x \notin m) { - y <$ uD; - coll <- coll \/ rng m y; + y <$ dD; m.[x] <- y; mi.[y] <- x; } return oget m.[x]; } - proc fi(y : D) = { + proc fi(y: D) = { var x; if (y \notin mi) { - x <$ uD; - coll <- coll \/ rng mi x; + x <$ dD; m.[x] <- y; mi.[y] <- x; } @@ -61,41 +68,86 @@ module ARP = { } }. -op q : { int | 0 <= q } as ge0_q. +module Count (P : PRP) = { + var count: int + + proc init() = { + P.init(); + count <- 0; + } + + proc f(x) = { + var r; + + r <@ P.f(x); + count <- count + 1; + return r; + } + + proc fi(x) = { + var r; + + r <@ P.fi(x); + count <- count + 1; + return r; + } +}. + +section. -(** 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 +declare module D <: Distinguisher { -PRPi, -ARP, -Count }. +declare axiom D_ll (O <: SPRP_Oracles { -D }): + islossless O.f + => islossless O.fi + => islossless D(O).distinguish. + +declare op q : { int | 0 <= q } as ge0_q. +declare axiom D_count (P <: PRP { -D, -Count }) c: + hoare [D(Count(P)).distinguish: Count.count = c ==> Count.count <= c + q]. + +local clone import TwoStepSampling with + type i <- unit, + type t <- D, + op dt _ <- dD +proof *. + +local module type Sample_t = { + proc sample(_: D -> bool): D }. -module Direct = { - proc sample(X:D -> bool): D = { +local module Direct: Sample_t = { + proc sample(X) = { var r; - r <$ uD \ X; + r <@ S.direct((), fun _=> X); return r; } }. -module Indirect = { - proc sample(X:D -> bool): D = { +local module Indirect: Sample_t = { + proc sample(X) = { var r; - r <$ uD; - if (X r) { - r <$ uD \ X; - } + r <@ S.indirect((), fun _=> X); return r; } }. -module PRPi'(S:Sample_t) = { - proc init = PRPi.init +local equiv eq_Direct_Indirect: + Direct.sample ~ Indirect.sample: ={X} ==> ={res}. +proof. by proc; call ll_direct_indirect_eq; auto; smt(dD_ll). qed. + +local module PRPi' (S: Sample_t) = { + var bad: bool + + proc init() = { + PRPi.init(); + bad <- false; + } proc f(x:D): D = { var r; + if (x \notin PRPi.m) { r <@ S.sample(rng PRPi.m); PRPi.m.[x] <- r; @@ -106,6 +158,7 @@ module PRPi'(S:Sample_t) = { proc fi(x:D): D = { var r; + if (x \notin PRPi.mi) { r <@ S.sample(rng PRPi.mi); PRPi.mi.[x] <- r; @@ -115,10 +168,76 @@ module PRPi'(S:Sample_t) = { } }. -(* Some losslessness lemmas *) -(* FIXME: cleanup *) +local module ARP_bad = { + var bad: bool + + proc init() = { + ARP.init(); + bad <- false; + } + + proc f(x) = { + var y; + + if (x \notin ARP.m) { + y <$ dD; + bad <- bad \/ rng ARP.m y; + ARP.m.[x] <- y; + ARP.mi.[y] <- x; + } + return oget ARP.m.[x]; + } + + proc fi(y) = { + var x; + + if (y \notin ARP.mi) { + x <$ dD; + bad <- bad \/ rng ARP.mi x; + ARP.m.[x] <- y; + ARP.mi.[y] <- x; + } + return oget ARP.mi.[y]; + } +}. + +local module PRPi'_bad = { + proc init() = { + PRPi.init(); + ARP_bad.bad <- false; + } + + proc f(x) = { + var y; + + if (x \notin PRPi.m) { + y <$ dD; + if (rng PRPi.m y) { + ARP_bad.bad <- true; + y <$ dD \ rng PRPi.m; + } + PRPi.m.[x] <- y; + PRPi.mi.[y] <- x; + } + return oget PRPi.m.[x]; + } + + proc fi(y) = { + var x; + + if (y \notin PRPi.mi) { + x <$ dD; + if (rng PRPi.mi x) { + ARP_bad.bad <- true; + x <$ dD \ rng PRPi.mi; + } + PRPi.m.[x] <- y; + PRPi.mi.[y] <- x; + } + return oget PRPi.mi.[y]; + } +}. -(* FIXME: Duplicate lemmas with RP_RF *) lemma notin_supportIP (P : 'a -> bool) (d : 'a distr): (exists a, support d a /\ !P a) <=> mu d P < mu d predT. proof. @@ -130,447 +249,181 @@ qed. lemma excepted_lossless (m:(D,D) fmap): (exists x, x \notin m) => - mu (uD \ (rng m)) predT = 1%r. + mu (dD \ (rng m)) predT = 1%r. proof. -move=> /endo_dom_rng [x h]; rewrite dexcepted_ll //. -+ smt(uD_uf_fu). -have [?[<- @/is_full Hsupp]]:= uD_uf_fu. -apply/notin_supportIP;exists x => />;apply Hsupp. +move=> /endo_dom_rng [x h]; rewrite dexcepted_ll // 1:dD_ll. +by rewrite -dD_ll; apply: notin_supportIP; exists x; rewrite dD_fu. qed. -phoare Indirect_ll: [Indirect.sample: exists x, support uD x /\ !X x ==> true] = 1%r. +local lemma rng_set_subset_rngU1 (m : ('a, 'b) fmap) (x : 'a) y: + forall z, rng m.[x <- y] z => predU (rng m) (pred1 y) z. proof. -proc; seq 1: (exists x, support uD x /\ !X x)=> //=. -+ by rnd (predT); skip; smt(uD_uf_fu). -if=> //=. -+ rnd (predT); skip. - move=> /> &0; rewrite dexceptedE predTI mu_not. - move=> x x_in_uD x_notin_X r_in_X. - apply/mulrV/ltr0_neq0/subr_gt0/notin_supportIP. - by exists x. -by hoare; rnd=> //=; skip=> &hr ->. +move=> z; rewrite /predU /pred1 /= (rngE m.[_ <- _])=> /= - [] x0. +rewrite get_setE; case: (x0 = x)=> |> _ m_x0; left; rewrite rngE /=. +by exists x0. qed. -lemma PRPi'_Indirect_f_ll: islossless PRPi'(Indirect).f. +local lemma frng_set_subset_rngU1 (m : ('a, 'b) fmap) (x : 'a) y: + frng m.[x <- y] \subset frng m `|` fset1 y. proof. -proc; if=> //=; auto; call Indirect_ll. -skip=> /> &hr x_notin_m. -have [x0] x0_notinr_m := endo_dom_rng PRPi.m{hr} _; first by exists x{hr}. -by exists x0; rewrite x0_notinr_m /=; smt(uD_uf_fu). +by move=> z; rewrite in_fsetU1 !mem_frng=> /rng_set_subset_rngU1. qed. -lemma PRPi'_Indirect_fi_ll: islossless PRPi'(Indirect).fi. +(** We split this into extremely small steps, but this is not + necessary **) +local lemma pr_PRPi_PRPi'_Direct &m: + Pr[IND(PRPi, D).main() @ &m: res] + = Pr[IND(PRPi'(Direct), D).main() @ &m:res]. proof. -proc; if=> //=; auto; call Indirect_ll. -skip=> /> &hr x_notin_mi. -have [x0] x0_notinr_mi := endo_dom_rng PRPi.mi{hr} _; first by exists x{hr}. -by exists x0; rewrite x0_notinr_mi; smt(uD_uf_fu). +byequiv=> //; proc; call (: ={glob PRPi}). ++ by proc; if=> //; inline *; auto=> |> &2 _ y _; rewrite get_set_sameE. ++ by proc; if=> //; inline *; auto=> |> &2 _ y _; rewrite get_set_sameE. +by inline *; auto. 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]. - - Purists are then invited to turn the security statement about - restricted oracles into a security statement about restricted - adversaries. **) -section Upto. - declare module D <: Distinguisher {-PRPi, -ARP}. - declare axiom D_ll (O <: SPRP_Oracles {-D}): islossless O.f => islossless O.fi => islossless D(O).distinguish. - - local module PRP_indirect_bad = { - var bad : bool - - proc init(): unit = { - PRPi.init(); - bad <- false; - } - - proc sample(X:D -> bool): D = { - var r; - - r <$ uD; - if (X r) { - bad <- true; - r <$ uD \ X; - } - return r; - } - - proc f(x:D): D = { - var r; - if (x \notin PRPi.m) { - r <@ sample(rng PRPi.m); - PRPi.m.[x] <- r; - PRPi.mi.[oget PRPi.m.[x]] <- x; - } - return oget PRPi.m.[x]; - } - - proc fi(y:D): D = { - var r; - if (y \notin PRPi.mi) { - r <@ sample(rng PRPi.mi); - PRPi.mi.[y] <- r; - PRPi.m.[oget PRPi.mi.[y]] <- y; - } - return oget PRPi.mi.[y]; - } - }. - - 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_ARP &m: - `|Pr[IND(PRPi'(Indirect),D).main() @ &m: res] - - Pr[IND(ARP,D).main() @ &m: res]| - <= Pr[IND(ARP,D).main() @ &m: ARP.coll]. - proof. - rewrite (PRPi'_Indirect_eq &m). - byequiv: PRP_indirect_bad.bad=> //=; 2:smt(). - proc. - call (_: ARP.coll, - !PRP_indirect_bad.bad{1} /\ ={m,mi}(PRPi,ARP), - (PRP_indirect_bad.bad{1} <=> ARP.coll{2})). - + exact D_ll. - + proc. if=> //=; inline *. - swap{1} 1. - seq 1 4: (={x} /\ - x{1} \notin PRPi.m{1} /\ - ARP.m{2} = PRPi.m.[x <- r0]{1} /\ - ARP.mi{2} = PRPi.mi.[r0 <- x]{1} /\ - ((PRP_indirect_bad.bad \/ rng PRPi.m r0){1} <=> ARP.coll{2})). - by auto=> /#. - sp; if{1}. - conseq (_: PRP_indirect_bad.bad{1} /\ ARP.coll{2})=> //=. - auto; progress [-split]; split=> //= [|_]. - by apply/excepted_lossless => /#. - by progress; right. - by auto; progress [-split]; rewrite H0 /= => -> /=; rewrite get_setE. - + 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 PRPi.m /\ x \notin PRPi.m) 1%r 1%r 0%r _ => //=. - by auto; rewrite -/predT; smt(uD_uf_fu). - by if=> //=; auto=> /> *; apply/excepted_lossless => /#. - by hoare; auto. - + move=> &1. - proc; if; auto; progress [-split]; rewrite -/predT; split=> //= [|_]; 1:smt(uD_uf_fu). - by progress [-split]; rewrite H. - + proc. if=> //=; inline *. - swap{1} 1. - seq 1 4: (={y} /\ - y{1} \notin PRPi.mi{1} /\ - ARP.m{2} = PRPi.m.[r0 <- y]{1} /\ - ARP.mi{2} = PRPi.mi.[y <- r0]{1} /\ - ((PRP_indirect_bad.bad \/ rng PRPi.mi r0){1} <=> ARP.coll{2})). - by auto=> /#. - sp; if{1}. - conseq (_: PRP_indirect_bad.bad{1} /\ ARP.coll{2})=> //=. - auto; progress [-split]; split=> //= [|_]. - by apply/excepted_lossless => /#. - by progress; right. - by auto; progress [-split]; rewrite H0 => /= ->; rewrite get_setE. - + 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 PRPi.mi /\ y \notin PRPi.mi) 1%r 1%r 0%r _ => //=. - by auto; rewrite -/predT; smt(uD_uf_fu). - by if=> //=; auto=> /> *; apply/excepted_lossless => /#. - by hoare; auto. - + move=> &1. - proc; if; auto; progress [-split]; rewrite -/predT; split=> //= [|_]; 1:smt(uD_uf_fu). - by progress [-split]; rewrite H. - by inline *; auto; progress => /#. - qed. -end section Upto. - -(** We now bound the probability of collisions. We cannot do so - by instantiating the generic Birthday Bound result. It's still - the Birthday Bound, though, just not generic: - Pr[IND(ARP,DBounder(D)).main() @ &m: ARP.coll] - <= q^2 * Pr[x = $uD: x = witness], - - where DBounder prevents the distinguisher from calling the - f-oracle more than q times. **) -module DBounder (D : Distinguisher) (F : SPRP_Oracles) = { - module FBounder = { - var c:int - - proc f(x:D): D = { - var r <- witness; - - if (c < q) { - r <@ F.f(x); - c <- c + 1; - } - return r; - } - - proc fi(x:D): D = { - var r <- witness; - - if (c < q) { - r <@ F.fi(x); - c <- c + 1; - } - return r; - } - } - - proc distinguish(): bool = { - var b; - - FBounder.c <- 0; - b <@ D(FBounder).distinguish(); - return b; - } -}. - -section CollisionProbability. - require import Mu_mem. - (*---*) import StdBigop StdRing StdOrder. - (*---*) import Bigreal.BRA RField RField.AddMonoid IntOrder. - - declare module D <: Distinguisher {-ARP, -DBounder}. - declare axiom D_ll (O <: SPRP_Oracles {-D}): islossless O.f => islossless O.fi => islossless D(O).distinguish. - - local module FEL (D : Distinguisher) = { - var c : int - - module FBounder = { - proc f(x:D): D = { - var r <- witness; +local lemma pr_PRPi'_Direct_PRPi'_Indirect &m: + Pr[IND(PRPi'(Direct), D).main() @ &m: res] + = Pr[IND(PRPi'(Indirect), D).main() @ &m: res]. +proof. +byequiv=> //; proc; call (: ={glob PRPi}). ++ proc; if=> //; auto. + by call eq_Direct_Indirect; auto=> |>; rewrite dD_ll. ++ proc; if=> //; auto. + by call eq_Direct_Indirect; auto=> |>; rewrite dD_ll. +by inline *; auto. +qed. - if (c < q) { - if (card (frng ARP.m) < q) { - r <@ ARP.f(x); - } - c <- c + 1; - } - return r; - } +local lemma pr_PRPi'_Indirect_PRPi'_bad &m: + Pr[IND(PRPi'(Indirect), D).main() @ &m: res] + = Pr[IND(PRPi'_bad, D).main() @ &m: res]. +proof. +byequiv=> //; proc; call (: ={glob PRPi}). ++ proc; if=> //; inline *. + do ! cfold {1} 1. + seq 1 1: (#pre /\ r1{1} = y{2}); 1:by auto. + if=> //; auto=> |>. + + by move=> &2 _ _ y _; rewrite get_set_sameE. + by move=> &2; rewrite get_set_sameE. ++ proc; if=> //; inline *. + do ! cfold {1} 1. + seq 1 1: (#pre /\ r1{1} = x{2}); 1:by auto. + if=> //; auto=> |>. + + by move=> &2 _ _ y _; rewrite get_set_sameE. + by move=> &2; rewrite get_set_sameE. +by inline *; auto. +qed. - proc fi(x:D): D = { - var r <- witness; +local lemma pr_ARP_ARP_bad &m: + Pr[IND(ARP, D).main() @ &m: res] + = Pr[IND(ARP_bad, D).main() @ &m: res]. +proof. +byequiv=> //; proc; call (: ={glob ARP}); 1,2:by sim. +by inline *; auto. +qed. - if (c < q) { - if (card (frng ARP.mi) < q) { - r <@ ARP.fi(x); - } - c <- c + 1; - } - return r; - } - } +local lemma pr_PRP_bad_ARP_bad &m: + `| Pr[IND(PRPi'_bad, D).main() @ &m: res] + - Pr[IND(ARP, D).main() @ &m: res]| + <= Pr[IND(ARP_bad, D).main() @ &m: ARP_bad.bad]. +proof. +rewrite pr_ARP_ARP_bad; byequiv: ARP_bad.bad=> //=; 2:smt(). +proc. +call (: ARP_bad.bad + , !ARP_bad.bad{2} /\ ={m, mi}(PRPi, ARP) /\ ={ARP_bad.bad} + , ARP_bad.bad{2} /\ ={ARP_bad.bad}). ++ exact: D_ll. ++ proc; if=> //=; inline *. + seq 1 1: (#pre /\ ={y}); 1:by auto. + if {1}; auto=> |> &1 _ x_notin_m _. + by apply: excepted_lossless; exists x{1}. ++ move=> &2 bad; proc; if; 2:by auto. + seq 1: (ARP_bad.bad{2} /\ ARP_bad.bad = ARP_bad.bad{2} /\ x \notin PRPi.m)=> //. + + by auto=> |>; rewrite dD_ll. + + if; auto=> |> &1 _ x_notin_m _ @/predT /=. + by apply: excepted_lossless; exists x{1}. + + by hoare; auto. + + by move=> &1; proc; if; auto=> |>; rewrite dD_ll. ++ proc; if=> //=; inline *. + seq 1 1: (#pre /\ ={x}); 1:by auto. + if {1}; auto=> |> &1 _ y_notin_m _. + by apply: excepted_lossless; exists y{1}. ++ move=> &2 bad; proc; if; 2:by auto. + seq 1: #pre=> //. + + by auto=> |>; rewrite dD_ll. + + if; auto=> |> &1 _ x_notin_m _ @/predT /=. + by apply: excepted_lossless; exists y{1}. + + by hoare; auto. + + by move=> &1; proc; if; auto=> |>; rewrite dD_ll. +by inline *; auto=> |> /#. +qed. - proc main(): bool = { - var b : bool; +import StdBigop.Bigreal BRA. - ARP.init(); - c <- 0; - b <@ D(FBounder).distinguish(); - return b; - } - }. - - lemma pr_PRFi_collision &m: - Pr[IND(ARP,DBounder(D)).main() @ &m: ARP.coll] - <= (q^2 - q)%r / 2%r * mu uD (pred1 witness). - proof. - have ->: Pr[IND(ARP,DBounder(D)).main() @ &m: ARP.coll] - = Pr[IND(ARP,DBounder(D)).main() @ &m: ARP.coll /\ DBounder.FBounder.c <= q]. - + byequiv=> //=; conseq (_: ={glob D} ==> ={ARP.coll,DBounder.FBounder.c}) - (_: true ==> DBounder.FBounder.c <= q)=> //=. - * proc; inline *; wp; call (_: DBounder.FBounder.c <= q). - - by proc; sp; if=> //=; inline*; sp; if=> //=; auto=> /#. - - by proc; sp; if=> //=; inline*; sp; if=> //=; auto=> /#. - by auto=> /=; apply/ge0_q. - by sim. - have ->: Pr[IND(ARP,DBounder(D)).main() @ &m: ARP.coll /\ DBounder.FBounder.c <= q] - = Pr[FEL(D).main() @ &m: ARP.coll /\ FEL.c <= q]. - + byequiv=> //=; proc; inline *; wp. - call (_: ={glob ARP} /\ ={c}(DBounder.FBounder,FEL) /\ card (frng ARP.m){1} <= FEL.c{2} /\ card (frng ARP.mi){1} <= FEL.c{2}). - * proc; sp; if=> //=. rcondt{2} 1; first by auto=> /#. - inline *; sp; if=> //=; auto => [/>|/>/#]. - progress. - - apply/(ler_trans (card (frng ARP.m{2} `|` fset1 yL))). - + apply/subset_leq_fcard=> x'; rewrite !inE !mem_frng !rngE=> - /= [x0]. - rewrite get_setE; case: (x0 = x{2})=> [<<- /= ->|_ mx0] //. - by left; exists x0. - by rewrite fcardU fcard1; smt(fcard_ge0). - - apply/(ler_trans (card (frng ARP.mi{2} `|` fset1 x{2}))). - + apply/subset_leq_fcard=> x'; rewrite !inE !mem_frng !rngE=> - /= [x0]. - rewrite get_setE; case: (x0 = yL)=> [<<- //|_ mx0]. - by left; exists x0. - by rewrite fcardU fcard1; smt(fcard_ge0). - * proc; sp; if=> //=. rcondt{2} 1; first by auto=> /#. - inline *; sp; if=> //=; auto => [/>|/>/#]. - progress. - - apply/(ler_trans (card (frng ARP.m{2} `|` fset1 x{2}))). - + apply/subset_leq_fcard=> x'; rewrite !inE !mem_frng !rngE=> - /= [x0]. - rewrite get_setE; case: (x0 = x0L)=> [<<- //|_ mx0]. - by left; exists x0. - by rewrite fcardU fcard1; smt(fcard_ge0). - - apply/(ler_trans (card (frng ARP.mi{2} `|` fset1 x0L))). - + apply/subset_leq_fcard=> x'; rewrite !inE !mem_frng !rngE=> - /= [x0]. - rewrite get_setE; case: (x0 = x{2})=> [<<- //|_ mx0]. - by left; exists x0. - by rewrite fcardU fcard1; smt(fcard_ge0). - by auto=> />; rewrite frng0 fcards0. - fel 2 FEL.c (fun x, x%r * mu uD (pred1 witness)) q (ARP.coll) - [FEL(D).FBounder.f: (FEL.c < q); FEL(D).FBounder.fi: (FEL.c < q)] - (card (fdom ARP.m) <= FEL.c /\ card (fdom ARP.mi) <= FEL.c)=> //. - + rewrite -mulr_suml Bigreal.sumidE 1:ge0_q. - by rewrite expr2;smt(mu_bounded ge0_q). - + by inline*; auto=> />; rewrite fdom0 fcards0. - + exists*FEL.c;elim*=> c. - conseq(:_==>_ : (c%r * mu1 uD witness))=> />. - proc; sp; rcondt 1=> //. - inline *; sp; if=> //=; last first. - * hoare; auto=> // /> &hr 6?. - by apply/RealOrder.mulr_ge0; smt(mu_bounded ge0_q). - sp; if=> //=. - * wp; rnd (rng ARP.m); skip. - progress. - - apply/(RealOrder.ler_trans ((card (frng ARP.m{hr}))%r * mu uD (pred1 witness))). - have ->: rng ARP.m{hr} = mem (frng ARP.m{hr}). - + by apply/fun_ext=> x; rewrite mem_frng. - apply/mu_mem_le; move=> x _; have [] uD_suf [] ? uD_fu:= uD_uf_fu. - apply/RealOrder.lerr_eq/uD_suf; 1,2:rewrite uD_fu //. - by apply/RealOrder.ler_wpmul2r; smt(mu_bounded lt_fromint ltrW leq_card_rng_dom). - - by move: H9;rewrite H1. - * by hoare; auto=> //=; smt(RealOrder.mulr_ge0 mu_bounded ge0_q). - + move=> c; proc. rcondt 2; 1:by auto. - sp; if=> //=. - * inline*;sp;if;auto; 2:smt(). - move=> &hr /> + + + + + y />. - by rewrite !fdom_set !fcardU !fcard1; smt(fcard_ge0). - * by auto=> /#. - + by move=> b c; proc; rcondf 2; auto. - + exists*FEL.c;elim*=> c. - conseq(:_==>_ : (c%r * mu1 uD witness));progress. - proc; sp; rcondt 1=> //=. - inline *; sp; if=> //=; last by hoare; auto; smt(RealOrder.mulr_ge0 mu_bounded ge0_q). - sp; if=> //=. - * wp; rnd (rng ARP.mi); skip. - progress. - - apply/(RealOrder.ler_trans ((card (frng ARP.mi{hr}))%r * mu uD (pred1 witness))). - have ->: rng ARP.mi{hr} = mem (frng ARP.mi{hr}). - + by apply/fun_ext=> x; rewrite mem_frng. - apply/mu_mem_le; move=> x _; have [] uD_suf [] _ uD_fu:= uD_uf_fu. - apply/RealOrder.lerr_eq/uD_suf; 1,2:rewrite uD_fu //. - apply: RealOrder.ler_wpmul2r. - + exact: ge0_mu. - + exact/le_fromint/(lez_trans _ _ _ (leq_card_rng_dom _)). - - by move: H9; rewrite H1. - * by hoare; auto; smt(RealOrder.mulr_ge0 mu_bounded ge0_q). - + move=> c; proc; rcondt 2; 1:by auto. - sp; if=> //=. - * inline*;sp;if;auto; 2:smt(). - move=> &hr /> + + + + + x. - by rewrite !fdom_set !fcardU !fcard1; smt(fcard_ge0). - * by auto=> /#. - + by move=> b c; proc; rcondf 2; auto. - qed. -end section CollisionProbability. - -(* We pull together the results of the first two sections *) -lemma PartialConclusion (D <: Distinguisher {-PRPi, -ARP, -DBounder}) &m: - (forall (O <: SPRP_Oracles {-D}), islossless O.f => islossless O.fi => islossless D(O).distinguish) => - `|Pr[IND(PRPi'(Indirect),DBounder(D)).main() @ &m: res] - - Pr[IND(ARP,DBounder(D)).main() @ &m: res]| - <= (q^2 - q)%r / 2%r * mu uD (pred1 witness). +local lemma pr_ARP_bad &m: + Pr[IND(ARP_bad, D).main() @ &m: ARP_bad.bad] + <= (q^2 - q)%r / 2%r * hmin_dD. proof. -move=> D_ll. -have:= pr_PRFi_collision D D_ll &m. -have /#:= pr_PRPi'_Indirect_ARP (DBounder(D)) _ &m. -move=> O O_f_ll O_fi_ll; proc. -call (D_ll (<: DBounder(D,O).FBounder) _ _). - by proc; sp; if=> //=; wp; call O_f_ll. - by proc; sp; if=> //=; wp; call O_fi_ll. -by auto. +have ->: Pr[IND(ARP_bad, D).main() @ &m: ARP_bad.bad] + = Pr[IND(Count(ARP_bad), D).main() @ &m: ARP_bad.bad /\ Count.count <= q]. ++ byequiv (: ={glob D} ==> ={ARP_bad.bad} /\ Count.count{2} <= q)=> //. + conseq (: _ ==> ={ARP_bad.bad}) _ (: _ ==> Count.count <= q)=> //. + + by proc; call (D_count ARP_bad 0); inline *; auto. + proc; call (: ={ARP.m, ARP.mi, ARP_bad.bad})=> //. + + by proc; inline *; sp; if; auto=> |>. + + by proc; inline *; sp; if; auto. + by inline *; auto. +fel 1 (Count.count) (fun i=> i%r * hmin_dD) q + ARP_bad.bad + [] (card (frng ARP.m) <= Count.count /\ card (frng ARP.mi) <= Count.count)=> //. ++ by rewrite -mulr_suml sumidE 1:ge0_q mulrDr expr2 mulrN1. ++ by inline *; auto=> |>; rewrite frng0 fcards0. ++ exlim Count.count=> c; conseq (: _: <= (c%r * hmin_dD))=> //. + proc; inline *; sp; if=> //. + + wp; rnd (rng ARP.m); auto=> |> &0 ge0_count lt_count_q. + move=> _ size_rng_m _ _; rewrite (mu_eq _ _ (mem (frng ARP.m{0}))). + + by move=> x; rewrite mem_frng. + apply: (ler_trans ((card (frng ARP.m{0}))%r * hmin_dD)). + + by apply: Mu_mem.mu_mem_le=> x _; exact: hmin_dDP. + apply: ler_wpmul2r; 1:exact: ge0_hmin_dD. + by apply: le_fromint=> /#. + by hoare; auto=> |>; smt(ge0_hmin_dD). ++ move=> c; proc; inline *; sp; if; auto=> |>; 2:smt(). + move=> &0 card_rng_m card_rng_mi x_notin_m r _; split=> [/#|]. + split. + + apply: (lez_trans (card (frng ARP.m{0} `|` fset1 r))). + + exact/subset_leq_fcard/frng_set_subset_rngU1. + by rewrite fcardU1 /#. + apply: (lez_trans (card (frng ARP.mi{0} `|` fset1 x{0}))). + + exact/subset_leq_fcard/frng_set_subset_rngU1. + by rewrite fcardU1 /#. ++ exlim Count.count=> c; conseq (: _: <= (c%r * hmin_dD))=> //. + proc; inline *; sp; if=> //. + + wp; rnd (rng ARP.mi); auto=> |> &0 ge0_count lt_count_q. + move=> _ _ size_rng_mi _; rewrite (mu_eq _ _ (mem (frng ARP.mi{0}))). + + by move=> x; rewrite mem_frng. + apply: (ler_trans ((card (frng ARP.mi{0}))%r * hmin_dD)). + + by apply: Mu_mem.mu_mem_le=> x _; exact: hmin_dDP. + apply: ler_wpmul2r; 1:exact: ge0_hmin_dD. + by apply: le_fromint=> /#. + by hoare; auto=> |>; smt(ge0_hmin_dD). ++ move=> c; proc; inline *; sp; if; auto=> |>; 2:smt(). + move=> &0 card_rng_m card_rng_mi x_notin_m r _; split=> [/#|]. + split. + + apply: (lez_trans (card (frng ARP.m{0} `|` fset1 x{0}))). + + exact/subset_leq_fcard/frng_set_subset_rngU1. + by rewrite fcardU1 /#. + apply: (lez_trans (card (frng ARP.mi{0} `|` fset1 r))). + + exact/subset_leq_fcard/frng_set_subset_rngU1. + by rewrite fcardU1 /#. qed. -(** 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 _ <- uD - 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. - outline {1} 1 by { r <@ S.direct((), fun _ => X); }. - rewrite equiv[{1} 1 ll_direct_indirect_eq ((), fun _ => X :@ r)]. - + auto=> />; exact dD_ll. - inline S.indirect. - by sp; seq 1 1 : (#pre /\ r0{1} = r{2}); auto; if; auto. - qed. - - (* The rest is easy *) - local equiv eq_PRPi_PRPi'_f_Indirect: PRPi.f ~ PRPi'(Indirect).f: - ={x, PRPi.m, PRPi.mi} ==> ={res, PRPi.m, PRPi.mi}. - proof. - transitivity PRPi'(Direct).f (={PRPi.m,PRPi.mi,x} ==> ={PRPi.m,PRPi.mi,res}) (={PRPi.m,PRPi.mi,x} ==> ={PRPi.m,PRPi.mi,res}). - + by move=> &1 &2 [->> [->> ->>]]; exists PRPi.m{2} PRPi.mi{2} x{2}. - + done. - + by proc; inline *; if=> //=; auto; progress; rewrite get_setE. - + by proc; if=> //=; wp; call eq_Direct_Indirect. - qed. - - local equiv eq_PRPi_PRPi'_fi_Indirect: PRPi.fi ~ PRPi'(Indirect).fi: - y{1} = x{2} /\ ={PRPi.m, PRPi.mi} ==> ={res, PRPi.m, PRPi.mi}. - proof. - transitivity PRPi'(Direct).fi (={PRPi.m,PRPi.mi} /\ y{1} = x{2} ==> ={PRPi.m,PRPi.mi,res}) (={PRPi.m,PRPi.mi,x} ==> ={PRPi.m,PRPi.mi,res}). - + by move=> &1 &2 [->> [->> ->>]]; exists PRPi.m{2} PRPi.mi{2} x{2}. - + done. - + by proc; inline *; if=> //=; auto; progress; rewrite get_setE. - + by proc; if=> //=; wp; call eq_Direct_Indirect. - qed. - - declare module D <: Distinguisher {-PRPi}. - - lemma pr_PRPi_PRPi'_Indirect &m: - Pr[IND(PRPi,D).main() @ &m: res] = Pr[IND(PRPi'(Indirect),D).main() @ &m: res]. - proof. - byequiv=> //=. - proc. - call (_: ={PRPi.m,PRPi.mi}). - by apply eq_PRPi_PRPi'_f_Indirect. - by apply eq_PRPi_PRPi'_fi_Indirect. - by inline*; auto. - qed. -end section PRPi_PRPi'_Indirect. - -lemma Conclusion (D <: Distinguisher {-PRPi, -ARP, -DBounder}) &m: - (forall (O <: SPRP_Oracles {-D}), islossless O.f => islossless O.fi => islossless D(O).distinguish) => - `|Pr[IND(PRPi,DBounder(D)).main() @ &m: res] - - Pr[IND(ARP,DBounder(D)).main() @ &m: res]| - <= (q^2 - q)%r / 2%r * mu uD (pred1 witness). +lemma Strong_RP_RF_Switching &m: + `| Pr[IND(PRPi, D).main() @ &m: res] + - Pr[IND(ARP, D).main() @ &m: res]| + <= (q ^ 2 - q)%r / 2%r * hmin_dD. proof. -move=> D_ll. -by rewrite (pr_PRPi_PRPi'_Indirect (DBounder(D)) &m) (PartialConclusion D &m D_ll). +rewrite (pr_PRPi_PRPi'_Direct &m) (pr_PRPi'_Direct_PRPi'_Indirect &m). +rewrite (pr_PRPi'_Indirect_PRPi'_bad &m). +smt(pr_PRP_bad_ARP_bad pr_ARP_bad). qed. +end section.