From 8a1904b30f5d171687f6f20cf59ed03de0faab50 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, PRP 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. --- examples/MEE-CBC/CBC.eca | 628 +++++++---------- examples/MEE-CBC/FunctionalSpec.ec | 97 +-- examples/MEE-CBC/MAC_then_Pad_then_CBC.eca | 474 +++++++------ examples/MEE-CBC/RCPA_CMA.ec | 2 +- theories/crypto/Birthday.eca | 126 +--- theories/crypto/PRF.eca | 154 +++- theories/crypto/PRP.eca | 774 +++++++-------------- theories/crypto/prp_prf/RP_RF.eca | 418 +++++++++++ theories/crypto/prp_prf/Strong_RP_RF.eca | 576 --------------- theories/crypto/prp_prf/Weak_RP_RF.eca | 297 ++++++++ 10 files changed, 1709 insertions(+), 1837 deletions(-) create mode 100644 theories/crypto/prp_prf/RP_RF.eca delete mode 100644 theories/crypto/prp_prf/Strong_RP_RF.eca create mode 100644 theories/crypto/prp_prf/Weak_RP_RF.eca diff --git a/examples/MEE-CBC/CBC.eca b/examples/MEE-CBC/CBC.eca index 919539f18a..c9525238d1 100644 --- a/examples/MEE-CBC/CBC.eca +++ b/examples/MEE-CBC/CBC.eca @@ -2,13 +2,10 @@ symmetric encryption scheme **when used with random IVs** ***) require import AllCore Int Real Distr List FSet FMap. require import StdRing StdOrder DList. -require (*ab*) PRP PRF SKE_INDR. (* Definitions and Security Notions *) +require (*ab*) SKE_INDR. (* Definitions and Security Notions *) (*---*) import RField RealOrder. -(* -------------------------------------------------------------------- *) -(** Parameters and Constants *) -op q : {int | 0 < q} as gt0_q. (* number of queries *) -op ell : {int | 0 < ell} as gt0_ell. (* maximal number of blocks in message *) +require (*ab*) Weak_RP_RF Birthday. (* -------------------------------------------------------------------- *) (** An abstract type for keys **) @@ -56,26 +53,34 @@ axiom bijective_P (k : key): /\ cancel (Pi k) (P k). (** We instantiate library definitions for brevity **) -clone import PRP as PRPt with - type D <- block. +clone import Weak_RP_RF as RP_RF with + type D <- block, + op dD <- dBlock, + op hmin_dD <- mu1 dBlock witness, + type K <- key +proof * by smt(dBlock_uffu). -clone import WeakPRP as PRPSec. +import PRFt PRPt PRPSec RP_RF.RF PRPi. clone import PseudoRP as PRPr with - type K <- key, - op dK <- dKey, - op p <- P, - op pi <- Pi -proof * by smt(dKey_uffu bijective_P). - -clone import RP as PRPi with - op dD <- dBlock -rename "RP" as "PRPi" -proof * by smt(dBlock_uffu). + type K <- key +proof *. + +module PseudoRP : PseudoRP = { + proc keygen() = { + var k; + + k <$ dKey; + return k; + } + + proc p(k, x) = { return P k x; } + proc pi(k, y) = { return Pi k y; } +}. (*-------------------------------------------------------------------- *) (** The CBC construction turning a PRP into an explicit-IV SKE scheme **) -module CBC(P : PseudoRP) = { +module CBC (P : PseudoRP) = { proc keygen = P.keygen proc enc(key:key,iv:block,p:block list): block list = { @@ -86,7 +91,7 @@ module CBC(P : PseudoRP) = { i <- 0; while (i < size p) { pi <- nth witness p i; - s <@ P.f(key,(s + pi)); + s <@ P.p(key,(s + pi)); c <- c ++ [s]; i <- i + 1; } @@ -101,7 +106,7 @@ module CBC(P : PseudoRP) = { s <- iv; while (i < size c) { ci <- nth witness c i; - pi <@ P.fi(key,ci); + pi <@ P.pi(key,ci); p <- p ++ [s + pi]; s <- ci; i <- i + 1; @@ -199,16 +204,7 @@ end section Random_Ideal. longer need the inverse permutation for decryption... We will never make use of a concrete PRF (only use the ideal one), so we don't instantiate F **) -clone import PRF as PRFt with - type D <- block, - type R <- block. - -clone import RF as PRFi with - op dR _ <- dBlock -rename "RF" as "PRFi" -proof * by smt (dBlock_uffu). - -module CBC_Oracle (P:PRF) = { +module CBC_Oracle (P : PRF) = { proc init = P.init proc enc(p:block list): block list = { @@ -267,11 +263,11 @@ lemma CBC_Oracle_enc_eq (P <: PRF) ={p} /\ I (glob P){1} (glob P'){2} ==> ={res} /\ I (glob P){1} (glob P'){2}]. proof. - move=> P_f_eq. - proc; while ( ={i, s, p, c} - /\ I (glob P){1} (glob P'){2}). - by wp; call P_f_eq; auto. - by auto. +move=> P_f_eq. +proc; while ( ={i, s, p, c} + /\ I (glob P){1} (glob P'){2}). ++ by wp; call P_f_eq; auto. +by auto. qed. lemma CPA_direct_eq (P <: PRF) @@ -284,11 +280,11 @@ lemma CPA_direct_eq (P <: PRF) Pr[INDR_CPA_direct(CBC_Oracle(P),A).main() @ &m: res] = Pr[INDR_CPA_direct(CBC_Oracle(P'),A).main() @ &m: res]. proof. - move=> P_init_eq P_f_eq &m A. - byequiv=> //=. - proc; call (_: I (glob P){1} (glob P'){2}). - exact/(CBC_Oracle_enc_eq P P' I P_f_eq). - by call P_init_eq. +move=> P_init_eq P_f_eq &m A. +byequiv=> //=. ++ proc; call (_: I (glob P){1} (glob P'){2}). + + exact/(CBC_Oracle_enc_eq P P' I P_f_eq). + by call P_init_eq. qed. section Cleanup. @@ -301,7 +297,7 @@ section Cleanup. }. local equiv enc_eq: - RCPA_Wrap(IV_Wrap(CBC(PseudoRP))).enc ~ CBC_Oracle(PRP).enc: + RCPA_Wrap(IV_Wrap(CBC(PseudoRP))).enc ~ CBC_Oracle(PRP(PseudoRP)).enc: ={arg} /\ ={k}(RCPA_Wrap,PRP) ==> ={res} /\ ={k}(RCPA_Wrap,PRP). proof. proc; inline *; wp. @@ -314,7 +310,7 @@ section Cleanup. local lemma success_eq &m: Pr[INDR_CPA(IV_Wrap(CBC(PseudoRP)),A).main() @ &m: res] - = Pr[INDR_CPA_direct(CBC_Oracle(PRP),A).main() @ &m: res]. + = Pr[INDR_CPA_direct(CBC_Oracle(PRP(PseudoRP)),A).main() @ &m: res]. proof. byequiv=> //=; proc. call (_: ={k}(RCPA_Wrap,PRP)); @@ -348,7 +344,7 @@ section Cleanup. lemma cleanup &m: `|Pr[INDR_CPA(IV_Wrap(CBC(PseudoRP)),A).main() @ &m: res] - Pr[INDR_CPA(Random,A).main() @ &m: res]| - = `|Pr[INDR_CPA_direct(CBC_Oracle(PRP),A).main() @ &m: res] + = `|Pr[INDR_CPA_direct(CBC_Oracle(PRP(PseudoRP)),A).main() @ &m: res] - Pr[INDR_CPA_direct(CBC_Oracle(Sample),A).main() @ &m: res]|. proof. by rewrite (success_eq &m) (success_eq_random &m). qed. end section Cleanup. @@ -356,7 +352,7 @@ end section Cleanup. (** Step 1: Decompose the advantage into manageable sub-problems **) (* We push the CBC construction out and into an adversary against the PRP/RP/RF *) -module PRPF_Adv(A:RCPA_Adversary, F:PRF_Oracles) = { +module PRPF_Adv (A:RCPA_Adversary) (F:PRF_Oracles) = { module O = { proc enc(p:block list): block list = { var s, c, i, pi; @@ -380,25 +376,25 @@ module PRPF_Adv(A:RCPA_Adversary, F:PRF_Oracles) = { section Decomposition. declare module A <: RCPA_Adversary { -RCPA_Wrap, -PRP, -PRPi, -PRFi }. - local lemma refactor_abstract (O <: PRP {-A}) &m: - Pr[INDR_CPA_direct(CBC_Oracle(O),A).main() @ &m: res] + local lemma refactor_abstract (O <: WeakPRP {-A}) &m: + Pr[INDR_CPA_direct(CBC_Oracle(O),A).main() @ &m: res] = Pr[IND(O,PRPF_Adv(A)).main() @ &m: res]. proof. by byequiv=> //=; proc; inline *; sim. qed. lemma CBC_PRP_RF &m: - `|Pr[INDR_CPA_direct(CBC_Oracle(PRP),A).main() @ &m: res] + `| Pr[INDR_CPA_direct(CBC_Oracle(PRP(PseudoRP)),A).main() @ &m: res] - Pr[INDR_CPA_direct(CBC_Oracle(Sample),A).main() @ &m: res]| - <= `|Pr[INDR_CPA_direct(CBC_Oracle(PRFi),A).main() @ &m: res] + <= `| Pr[INDR_CPA_direct(CBC_Oracle(PRFi),A).main() @ &m: res] - Pr[INDR_CPA_direct(CBC_Oracle(Sample),A).main() @ &m: res]| - + `|Pr[IND(PRP,PRPF_Adv(A)).main() @ &m: res] + + `| Pr[IND(PRP(PseudoRP),PRPF_Adv(A)).main() @ &m: res] - Pr[IND(PRPi,PRPF_Adv(A)).main() @ &m: res]| (* Adv^{prp}_{P}(PRP_Adv(A)) *) - + `|Pr[IND(PRPi,PRPF_Adv(A)).main() @ &m: res] + + `| Pr[IND(PRPi,PRPF_Adv(A)).main() @ &m: res] - Pr[IND(PRFi,PRPF_Adv(A)).main() @ &m: res]|. proof. - rewrite (refactor_abstract PRP &m). - rewrite (refactor_abstract PRFi &m). - rewrite (refactor_abstract Sample &m). - smt(). (* triangular inequality *) + rewrite (refactor_abstract (PRP(PseudoRP)) &m). + rewrite (refactor_abstract PRFi &m). + rewrite (refactor_abstract Sample &m). + smt(). (* triangular inequality *) qed. end section Decomposition. @@ -409,7 +405,7 @@ end section Decomposition. ** ** `|Pr[INDR_CPA_direct(CBC_Oracle(PRFa.PRFi),A).main() @ &m: res] ** - Pr[INDR_CPA_direct(CBC_Oracle(Sample),A).main() @ &m: res]| - ** <= Pr[INDR_CPA_direct(Compute,A).main() @ &m: res] + ** <= Pr[INDR_CPA_direct(Compute,A).main() @ &m: Compute.bad] **) module Compute = { var bad: bool @@ -464,17 +460,17 @@ section Reduce. }. local lemma doublequery_eq (F <: PRF {-A, -DoubleQuery}) &m: - Pr[INDR_CPA_direct(CBC_Oracle(F),A).main() @ &m: res] + Pr[INDR_CPA_direct(CBC_Oracle(F),A).main() @ &m: res] = Pr[INDR_CPA_direct(CBC_Oracle(DoubleQuery(F)),A).main() @ &m: res]. proof. - byequiv=> //=; proc. - call (_: ={glob F}). - proc; while (={i, s, p, c, glob F}). - wp; call (_: ={glob F, arg} ==> ={glob F, res}). - by proc *; inline *; wp; call (_: true); wp. - by auto. + byequiv=> //=; proc. + call (_: ={glob F}). + + proc; while (={i, s, p, c, glob F}). + + wp; call (_: ={glob F, arg} ==> ={glob F, res}). + + by proc *; inline *; wp; call (_: true); wp. by auto. - by inline *; call (_: true); auto. + by auto. + by inline *; call (_: true); auto. qed. local equiv DQ_Sample_Compute_eq: @@ -482,105 +478,98 @@ section Reduce. ={bad,qs}(DoubleQuery,Compute) /\ ={arg} ==> ={bad,qs}(DoubleQuery,Compute) /\ ={res}. proof. - proc; inline*; case (size p{1} = 0). - rcondf{1} 4; 1:by auto=> /#. - by rcondf{2} 3; auto=> /#. - splitwhile{1} 4: (i < size p - 1). - rcondt{1} 5=> [&m|]. - while (0 <= i < size p); - by auto; smt (size_ge0). - rcondf{1} 15=> [&m|]. - auto; while (0 <= i < size p); - by auto; smt (size_ge0). - rcondt{2} 3; 1:by auto; smt (size_ge0). - auto=> //=. - while ( ={p, c} - /\ i{1} = i{2} - 1 - /\ 0 <= i{1} < size p{1} - /\ Compute.bad{2} - = (DoubleQuery.bad{1} \/ mem DoubleQuery.qs (s + nth witness p i)){1} - /\ Compute.qs{2} = (DoubleQuery.qs `|` (fset1 (s + nth witness p i))){1}). - wp; rnd (fun x => x + pi{2}); auto=> /> &1 &2 ge0_iP _ _ lt_i_szp. - case: (mem DoubleQuery.qs{1} _)=> //=. - split=> [sR _|_]; 1:smt(addbA addbK addbC add0b). (* TODO: instantiate ring structure *) - split=> [|_ r _]; 1:smt (dBlock_uffu). - split=> [|_]; 1:smt (dBlock_uffu). - split=> [|_]; 1:smt (addbA addbK addbC add0b). (* TODO: instantiate ring structure *) - by split=> [|/#]; - split; [congr; congr; smt(addbA addbK addbC add0b) | smt()]. (* TODO: instantiate ring structure *) - split=> [sR _ |_]; 1:smt (addbA addbK addbC add0b). (* TODO: instantiate ring structure *) + proc; inline*; case (size p{1} = 0). + + rcondf{1} 4; 1:by auto=> /#. + by rcondf{2} 3; auto=> /#. + splitwhile{1} 4: (i < size p - 1). + rcondt{1} 5=> [&m|]. + + by while (i < size p); auto; smt(size_ge0). + rcondf{1} 15=> [&m|]. + + by auto; while (i < size p); auto; smt(size_ge0). + rcondt {2} 3; 1: by auto; smt(size_ge0). + auto=> //=. + while (={p, c} + /\ i{1} = i{2} - 1 + /\ 0 <= i{1} < size p{1} + /\ ( Compute.bad{2} + <=> (DoubleQuery.bad{1} \/ mem DoubleQuery.qs (s + nth witness p i)){1}) + /\ Compute.qs{2} = (DoubleQuery.qs `|` (fset1 (s + nth witness p i))){1}). + wp; rnd (fun x => x + pi{2}); auto=> /> &1 &2 ge0_iP _ _ lt_i_szp. + case: (mem DoubleQuery.qs{1} _)=> //=. + + split=> [sR _|_]; 1:smt(addbA addbK addbC add0b). (* TODO: instantiate ring structure *) split=> [|_ r _]; 1:smt (dBlock_uffu). - split=> [|_]; 1:smt (dBlock_uffu). - split=> [|_]; 1:smt (addbA addbK addbC add0b). (* TODO: instantiate ring structure *) -split. - by move=> h; rewrite -addbA Block.subrr Block.addr0 /= /#. - by move=> h; rewrite -addbA Block.subrr Block.addr0 /= /#. - wp; rnd (fun x => x + pi{2}). - auto=> /> &2 szp_neq_0; split=> [|_]; 1:smt (addbA addbK addbC add0b). (* TODO: instantiate ring structure *) - split=> [|_ s _]; 1:smt (dBlock_uffu). - split=> [|_]; 1:smt (dBlock_uffu). - split=> [|_]; 1:smt (addbA addbK addbC add0b). (* TODO: instantiate ring structure *) - smt (size_ge0). + split=> [|->]; 1:smt(addbA addbK addbC add0b). (* TODO: instantiate ring structure *) + split; 1:smt(addbA addbK addbC add0b). (* TODO: instantiate ring structure *) + smt(). + split=> [sR _ |_]; 1:smt (addbA addbK addbC add0b). (* TODO: instantiate ring structure *) + split=> [|_ r _]; 1:smt (dBlock_uffu). + split=> [|->]; 1:smt (addbA addbK addbC add0b). (* TODO: instantiate ring structure *) + + smt(addbA addbK addbC add0b). + wp; rnd (fun x => x + pi{2}). + auto=> /> &2 szp_neq_0; split=> [|_]; 1:smt (addbA addbK addbC add0b). (* TODO: instantiate ring structure *) + split=> [|_ s _]; 1:smt (dBlock_uffu). + split=> [|_]; 1:smt(addbA addbK addbC add0b). + smt(size_ge0). qed. local lemma DQ_Sample_Compute_pr &m: Pr[INDR_CPA_direct(CBC_Oracle(DoubleQuery(Sample)),A).main() @ &m: DoubleQuery.bad] = Pr[INDR_CPA_direct(Compute,A).main() @ &m: Compute.bad]. proof. - byequiv=> //=. - proc. call (_: ={bad,qs}(DoubleQuery,Compute)). - by conseq DQ_Sample_Compute_eq. - by inline *; auto. + byequiv=> //=; proc. + call (: ={bad,qs}(DoubleQuery,Compute)). + + by conseq DQ_Sample_Compute_eq. + by inline *; auto. qed. lemma CBC_upto &m: - `|Pr[INDR_CPA_direct(CBC_Oracle(PRFi),A).main() @ &m: res] - - Pr[INDR_CPA_direct(CBC_Oracle(Sample),A).main() @ &m: res]| + `| Pr[INDR_CPA_direct(CBC_Oracle(PRFi),A).main() @ &m: res] + - Pr[INDR_CPA_direct(CBC_Oracle(Sample),A).main() @ &m: res]| <= Pr[INDR_CPA_direct(Compute,A).main() @ &m: Compute.bad]. proof. - rewrite -(DQ_Sample_Compute_pr &m) (doublequery_eq PRFi &m) (doublequery_eq Sample &m). - byequiv: DoubleQuery.bad=> //=; 2:smt ml=0. - proc. - call (_: DoubleQuery.bad, - ={glob DoubleQuery} - /\ forall x, mem DoubleQuery.qs{1} x <=> dom PRFi.m{1} x, - ={DoubleQuery.bad}). - + exact/A_distinguish_ll. - + proc. - while ( ={DoubleQuery.bad, i, p} - /\ (!DoubleQuery.bad{2} - => ={s, c, glob DoubleQuery} - /\ forall x, mem DoubleQuery.qs{1} x <=> dom PRFi.m{1} x)). - case (DoubleQuery.bad{2}). - inline *. - seq 4 4: (DoubleQuery.bad{2} /\ ={DoubleQuery.bad, i, p}). - by auto=> /#. - by if{1}; auto; smt (dBlock_uffu). - wp; inline *; sp 2 2; if; 1:smt ml=0. - * rcondf{1} 3; 1:by auto=> /#. - by auto; smt (dD_ll). - * rcondt{1} 2; 1:by auto=> /#. - auto=> /> &1 &2 ih lt_i_szp /ih [#] !->> eq_qs h m _. - by rewrite !get_setE => //= b; rewrite mem_set !inE eq_qs. - by auto; smt ml=0. - + move=> &2 bad; proc. - while ( DoubleQuery.bad = DoubleQuery.bad{2} - /\ 0 <= i <= size p) - (size p - i). - move=> z; inline *; sp; if=> //=; auto=> />; 2:smt ml=0. - by rewrite -/predT; smt (dBlock_uffu). - by auto=> />; rewrite -/predT; smt (dBlock_uffu size_ge0). - + move=> &1; proc. - while ( DoubleQuery.bad - /\ DoubleQuery.bad{1} = DoubleQuery.bad - /\ 0 <= i <= size p) - (size p - i). - by move=> z; inline *; auto=> />; rewrite -/predT; smt (dBlock_uffu size_ge0). - by auto=> />; rewrite -/predT; smt (dBlock_uffu size_ge0). - inline *; auto=> />. - split=> [|_]. - + by move=> x; rewrite mem_empty in_fset0. - by move=> rL rR gaL mL qsL badL gaR []. + rewrite -(DQ_Sample_Compute_pr &m) (doublequery_eq PRFi &m) (doublequery_eq Sample &m). + byequiv: DoubleQuery.bad=> //=; 2:smt ml=0. + proc. + call (: DoubleQuery.bad + , ={glob DoubleQuery} + /\ forall x, mem DoubleQuery.qs{1} x <=> dom PRFi.m{1} x + , ={DoubleQuery.bad}). + + exact/A_distinguish_ll. + + proc. + while (={DoubleQuery.bad, i, p} + /\ (!DoubleQuery.bad{2} + => ={s, c, glob DoubleQuery} + /\ forall x, mem DoubleQuery.qs{1} x <=> dom PRFi.m{1} x)). + + case (DoubleQuery.bad{2}). + + inline *. + seq 4 4: (DoubleQuery.bad{2} /\ ={DoubleQuery.bad, i, p}). + + by auto=> /#. + by if{1}; auto; smt(dBlock_uffu). + wp; inline *; sp 2 2; if=> [/#||]. + + rcondf{1} 3; 1: by auto=> /#. + by auto; smt(dD_ll). + + rcondt{1} 2; 1: by auto=> /#. + auto=> /> &1 &2 ih lt_i_szp /ih [#] !->> eq_qs h m _. + by rewrite !get_setE => //= b; rewrite mem_set !inE eq_qs. + by auto; smt(). + + move=> &2 bad; proc. + while (DoubleQuery.bad = DoubleQuery.bad{2} + /\ 0 <= i <= size p) + (size p - i). + + move=> z; inline *; sp; if=> //=; auto=> [/>|/#]. + by rewrite -/predT; smt(dBlock_uffu). + by auto=> />; rewrite -/predT; smt (dBlock_uffu size_ge0). + + move=> &1; proc. + while (DoubleQuery.bad + /\ DoubleQuery.bad{1} = DoubleQuery.bad + /\ 0 <= i <= size p) + (size p - i). + by move=> z; inline *; auto=> />; rewrite -/predT; smt(dBlock_uffu size_ge0). + by auto=> />; rewrite -/predT; smt(dBlock_uffu size_ge0). + inline *; auto=> />. + split=> [|_]. + + by move=> x; rewrite mem_empty in_fset0. + by move=> rL rR gaL mL qsL badL gaR []. qed. end section Reduce. @@ -595,268 +584,189 @@ end section Reduce. **) lemma reduction (A <: RCPA_Adversary { -RCPA_Wrap, -PRP, -PRPi, -PRFi, -Compute }) &m: (forall (O <: RCPA_Oracles {-A}), islossless O.enc => islossless A(O).distinguish) => - `|Pr[INDR_CPA(IV_Wrap(CBC(PseudoRP)),A).main() @ &m: res] + `| Pr[INDR_CPA(IV_Wrap(CBC(PseudoRP)),A).main() @ &m: res] - Pr[INDR_CPA(Random,A).main() @ &m: res]| - <= `|Pr[IND(PRP,PRPF_Adv(A)).main() @ &m: res] + <= `| Pr[IND(PRP(PseudoRP),PRPF_Adv(A)).main() @ &m: res] - Pr[IND(PRPi,PRPF_Adv(A)).main() @ &m: res]| - + `|Pr[IND(PRPi,PRPF_Adv(A)).main() @ &m: res] + + `| Pr[IND(PRPi,PRPF_Adv(A)).main() @ &m: res] - Pr[IND(PRFi,PRPF_Adv(A)).main() @ &m: res]| + Pr[INDR_CPA_direct(Compute,A).main() @ &m: Compute.bad]. proof. - move=> A_run_ll. - rewrite (cleanup A &m). - have:= (CBC_PRP_RF A &m). - have:= (CBC_upto A A_run_ll &m). - smt ml=0. +move=> A_run_ll. +rewrite (cleanup A &m). +have:= (CBC_PRP_RF A &m). +have:= (CBC_upto A A_run_ll &m). +smt(). qed. -(** We now bound the last two terms for bounded adversaries. - ** - ** * `|Pr[IND(PRPi,PRPF_Adv(A)).main() @ &m: res] - ** - Pr[IND(PRFa.PRFi,PRPF_Adv(A)).main() @ &m: res]| - ** <= (q*l)^2 * mu uD (pred1 witness), and - ** - ** * Pr[INDR_CPA_direct(Compute,A).main() @ &m: Compute.bad] - ** <= (q*l)^2 / |block|, - ** - ** where q is a bound on the number of encryption queries - ** and l is a bound on their length. - ** - ** We avoid simply bounding using the total number of blocks fed into - ** the PRP so that the addition of padding does not make us lose too - ** much precision... - ** - **) -module OracleBounder(O:RCPA_full) = { - var qC : int +module C (O : RCPA_full) : RCPA_full = { + var c : int - proc init(): unit = { - O.init(); - qC <- 0; + proc init() = { + O.init(); + c <- 0; } - proc enc(p:block list): block list = { - var i; - var r <- []; + proc enc(p : block list) : block list = { + var r : block list; + + r <@ O.enc(p); + c <- c + (size p); - if (qC < q /\ size p <= ell) { - r <@ O.enc(p); - qC <- qC + 1; - } else { - i <- 0; - while (i <= size p) { - r <- witness::r; - i <- i + 1; - } - } return r; } }. -module QueryBounder(A:RCPA_Adversary, O:RCPA_Oracles) = { - module O' = { - proc enc(p:block list): block list = { - var i; - var r <- []; - - if (OracleBounder.qC < q /\ size p <= ell) { - r <@ O.enc(p); - OracleBounder.qC <- OracleBounder.qC + 1; - } else { - i <- 0; - while (i <= size p) { - r <- r ++ [witness]; - i <- i + 1; - } - } - return r; - } - } - - proc distinguish(): bool = { - var b; - - OracleBounder.qC <- 0; - b <@ A(O').distinguish(); - return b; - } +module D (O : RCPA_Oracles) = { + proc init() = { } + proc enc = O.enc }. section Probability_RP_RF. - declare module A <: RCPA_Adversary { -PRPi, -PRFi, -QueryBounder }. + declare module A <: RCPA_Adversary { -PRPi, -PRFi, -C, -PRFt.Count, -PRPSec.Count }. declare axiom A_run_ll (O <: RCPA_Oracles { -A }): islossless O.enc => islossless A(O).distinguish. - local clone PRPi_RF as RP_RFc with - op q <- q * ell - proof * by smt (dBlock_uffu IntOrder.divr_ge0 gt0_q gt0_ell). + declare op q : { int | 0 <= q } as ge0_q. + declare op ell : { int | 0 <= ell } as ge0_ell. + + declare axiom A_run_q c: + hoare [A(C(D(PRPF_Adv(A, PRFi).O))).distinguish: C.c = c ==> C.c <= c + q * ell]. + + local equiv transfer_qbound c: + PRPF_Adv(A, PRFt.Count(PRFi)).distinguish ~ A(C(D(PRPF_Adv(A, PRFi).O))).distinguish: + ={glob A, glob PRFi} /\ PRFt.Count.c{1} - C.c{2} = c ==> PRFt.Count.c{1} - C.c{2} = c. + proof. + proc (={glob PRFi} /\ PRFt.Count.c{1} - C.c{2} = c)=> //. + proc; inline *; cfold {2} 1; wp. + while (={glob PRFi, i, p, s, c} /\ PRFt.Count.c{1} - C.c{2} = c + i{1} /\ (0 <= i <= size p){1}). + + by wp; sp; conseq (: ={PRFi.m})=> [/#|]; sim. + by auto=> |>; smt(size_ge0). + qed. lemma Bound_by_PRP_PRF &m: - `|Pr[IND(PRPi,PRPF_Adv(QueryBounder(A))).main() @ &m: res] - - Pr[IND(PRFi,PRPF_Adv(QueryBounder(A))).main() @ &m: res]| - <= ((q * ell)*(q * ell - 1))%r/2%r * mu dBlock (pred1 witness). + `| Pr[IND(PRPi,PRPF_Adv(A)).main() @ &m: res] + - Pr[IND(PRFi,PRPF_Adv(A)).main() @ &m: res]| + <= ((q * ell)*(q * ell - 1))%r/2%r * mu1 dBlock witness. proof. - have ->: Pr[IND(PRPi,PRPF_Adv(QueryBounder(A))).main() @ &m: res] - = Pr[RP_RFc.PRFt.IND(PRPi,RP_RFc.DBounder(PRPF_Adv(QueryBounder(A)))).main() @ &m: res]. - byequiv=> //=. - proc; inline *; auto. - call (_: ={PRPi.m, OracleBounder.qC} - /\ 0 <= OracleBounder.qC{2} <= q - /\ 0 <= RP_RFc.FBounder.c{2} <= OracleBounder.qC{2} * ell). - proc; inline *; sp; if=> //=; 2:by while (={i, p, r}); auto. - wp; while ( ={i0, p0, r, s, c, PRPi.m} - /\ 0 <= OracleBounder.qC{2} < q - /\ 0 <= i0{2} <= size p0{2} <= ell - /\ 0 <= RP_RFc.FBounder.c{2} <= OracleBounder.qC{2} * ell + i0{2}). - rcondt{2} 4; first auto; progress. - by have: RP_RFc.FBounder.c{hr} <= (q - 1) * ell + i0{hr}; smt ml=0. - by sp; if=> //=; auto=> /#. - by auto=> />; smt (size_ge0). - by auto=> />; smt (gt0_q). - have ->: Pr[IND(PRFi,PRPF_Adv(QueryBounder(A))).main() @ &m: res] - = Pr[RP_RFc.PRFt.IND(RP_RFc.PRFi.PRFi,RP_RFc.DBounder(PRPF_Adv(QueryBounder(A)))).main() @ &m: res]. - byequiv=> //=. - proc; inline *; auto. - call (_: ={OracleBounder.qC} - /\ ={m}(PRFi,RP_RFc.PRFi.PRFi) - /\ 0 <= OracleBounder.qC{2} <= q - /\ 0 <= RP_RFc.FBounder.c{2} <= OracleBounder.qC{2} * ell). - proc; inline *; sp; if=> //=; 2:by while (={i, p, r}); auto. - wp; while ( ={i0, p0, r, s, c} - /\ ={m}(PRFi,RP_RFc.PRFi.PRFi) - /\ 0 <= OracleBounder.qC{2} < q - /\ 0 <= i0{2} <= size p0{2} <= ell - /\ 0 <= RP_RFc.FBounder.c{2} <= OracleBounder.qC{2} * ell + i0{2}). - rcondt{2} 4; first auto; progress. - by have: RP_RFc.FBounder.c{hr} <= (q - 1) * ell + i0{hr}; smt ml=0. - by sp; if=> //=; auto=> /#. - by auto; smt (size_ge0). - by auto; smt (gt0_q). - apply/(RP_RFc.Conclusion_DBounder (PRPF_Adv(QueryBounder(A))) _ &m). - move=> O O_f_ll. - proc. call (A_run_ll (<: QueryBounder(A,PRPF_Adv(QueryBounder(A),O).O).O') _). - + proc; inline *; sp; if=> //=. - + wp; while true (size p0 - i0). - + by auto; call O_f_ll; auto=> /#. - by auto; rewrite -/predT; smt (dBlock_uffu). - by while true (size p + 1 - i); auto=> /#. - by auto. + move: (RP_RF_Switching (PRPF_Adv(A)) _ (q * ell) _ _ &m). + + move=> O f_ll. + apply: (A_run_ll (<: PRPF_Adv(A, O).O)). + proc. + while (0 <= i <= size p) (size p - i); auto. + + by call f_ll; auto=> /#. + smt(dBlock_uffu size_ge0). + + smt(ge0_q ge0_ell). + + move=> c; exlim C.c => c'. + by conseq (transfer_qbound (c - c')) (A_run_q c')=> /#. + have ->: Pr[PRFt.IND(PRPi, PRPF_Adv(A)).main() @ &m: res] + = Pr[IND(PRPi, PRPF_Adv(A)).main() @ &m: res]. + + by byequiv=> //; sim. + have ->: Pr[PRFt.IND(PRFi, PRPF_Adv(A)).main() @ &m: res] + = Pr[IND(PRFi, PRPF_Adv(A)).main() @ &m: res]. + + by byequiv=> //; sim. + have -> //: q * ell * (q * ell - 1) = (q * ell) ^ 2 - q * ell. + rewrite (StdOrder.IntOrder.Domain.exprS _ 1) //. + rewrite StdOrder.IntOrder.Domain.expr1. + smt(). qed. end section Probability_RP_RF. section Probability_Collision. - declare module A <: RCPA_Adversary { -PRPi, -PRFi, -Compute, -QueryBounder }. + declare module A <: RCPA_Adversary { -PRPi, -PRFi, -Compute, -C }. declare axiom A_run_ll (O <: RCPA_Oracles { -A }): islossless O.enc => islossless A(O).distinguish. + declare op q : { int | 0 <= q } as ge0_q. + declare op ell : { int | 0 <= ell } as ge0_ell. + declare axiom A_run_q c: + hoare [ A(C(Compute)).distinguish: C.c = c ==> C.c <= c + q * ell ]. + local clone import Birthday as BBound with type T <- block, - op uT <- dBlock, - op q <- q * ell - proof * by smt (dBlock_uffu IntOrder.divr_ge0 gt0_q gt0_ell). - - local module Wrap(A : RCPA_Adversary,S : ASampler) = { - var qC : int + op uT <- dBlock + proof * by smt (dBlock_uffu). + local module Wrap (A : RCPA_Adversary) (S : ASampler) = { module O = { proc enc(p: block list): block list = { var i, c, s, pi; i <- 0; c <- []; - if (qC < q /\ size p <= ell) { - while (i < size p) { - pi <- nth witness p i; - s <@ S.s(); - c <- c ++ [s + pi]; - i <- i + 1; - } - s <$ dBlock; - c <- c ++ [s]; - qC <- qC + 1; - } else { - while (i <= size p) { - c <- c ++ [witness]; - i <- i + 1; - } + while (i < size p) { + pi <- nth witness p i; + s <@ S.s(); + c <- c ++ [s + pi]; + i <- i + 1; } + s <$ dBlock; + c <- c ++ [s]; return c; } } - proc a(): unit = { - qC <- 0; - A(O).distinguish(); - } + proc a() = { A(O).distinguish(); } }. - local lemma pr_PushBound_list p &m: - Pr[Exp(Bounder(Sample),Wrap(A)).main() @ &m: p Sample.l] - = Pr[Exp(Sample,Bounded(Wrap(A))).main() @ &m: p Sample.l]. + local equiv transfer_count c: + A(Wrap(A, Sample).O).distinguish ~ A(C(Compute)).distinguish: + ={glob A} /\ size Sample.l{1} - C.c{2} = c ==> size Sample.l{1} - C.c{2} = c. proof. - byequiv (: ={glob Wrap(A), glob Sample} ==> ={glob Wrap(A), glob Sample})=> //=. - by conseq (PushBound Sample (Wrap(A))). + proc (size Sample.l{1} - C.c{2} = c)=> //. + proc; inline {2} 1; cfold {2} 1; wp; rnd. + while (={i, c, p} /\ i{1} <= size p{1} /\ size Sample.l{1} - C.c{2} = c + i{1}). + + by inline *; auto=> |> /#. + by auto=> |>; smt(size_ge0). qed. lemma Bound_by_Birthday &m: - Pr[INDR_CPA_direct(Compute,QueryBounder(A)).main() @ &m: Compute.bad] - <= ((q * ell)^2)%r * mu dBlock (pred1 witness). + Pr[INDR_CPA_direct(Compute,A).main() @ &m: Compute.bad] + <= ((q * ell)^2)%r * mu1 dBlock witness. proof. - apply/(ler_trans Pr[Exp(Bounder(Sample),Wrap(A)).main() @ &m: !(uniq Sample.l)]). - + rewrite (pr_PushBound_list (fun l=> !uniq l) &m)=> /=. - byequiv (: ={glob A} ==> Compute.bad{1} => !uniq Sample.l{2})=> //. - proc; inline *; wp. - call (_: OracleBounder.qC{1} = Wrap.qC{2} - /\ 0 <= Wrap.qC{2} <= q - /\ 0 <= Bounder.c{2} <= Wrap.qC{2} * ell - /\ (Compute.bad{1} <=> !List.uniq Sample.l{2}) - /\ (forall x, mem Compute.qs{1} x <=> mem Sample.l{2} x)). - + proc; sp; if=> //. - + inline *; auto. - while ( ={c} - /\ p0{1} = p{2} - /\ i0{1} = i{2} - /\ 0 <= Wrap.qC{2} < q - /\ 0 <= i{2} <= size p{2} <= ell - /\ 0 <= Bounder.c{2} <= Wrap.qC{2} * ell + i{2} - /\ (Compute.bad{1} <=> !List.uniq Sample.l{2}) - /\ (forall x, mem Compute.qs{1} x <=> mem Sample.l{2} x)). - + rcondt{2} 3; first auto => />; smt(mulrSl). - by auto=> /> &1 &2; smt(in_fsetU in_fset1). - by auto=> />; smt(size_ge0). - by while (={i, p} /\ r{1} = c{2}); auto. - by auto; smt (in_fset0 gt0_q). - have:= BBound.pr_collision_bounded_oracles (Wrap(A)) _ &m. - + move=> S S_s_ll; proc. - call (A_run_ll (<: Wrap(A,S).O) _). - + proc; sp; if. - + auto; while (true) (size p - i). - + by move=> z; wp; call S_s_ll; auto=> /#. - by auto; rewrite -/predT; smt (dBlock_uffu). - by while (true) (size p + 1 - i); auto=> /#. - by auto. - have [] + [] _ dBlock_fu:= dBlock_uffu. - by rewrite /is_uniform=> /(_ _ _ (dBlock_fu maxu) (dBlock_fu witness)) ->. + have ->: Pr[INDR_CPA_direct(Compute, A).main() @ &m: Compute.bad] + = Pr[Exp(Sample, Wrap(A)).main() @ &m: !uniq Sample.l]. + + byequiv=> //; proc; inline {2} 2. + call (: Compute.bad{1} = !uniq Sample.l{2} + /\ (forall x, x \in Compute.qs{1} <=> x \in Sample.l{2})). + + proc; auto. + while (={c, i, p} + /\ (Compute.bad{1} = !uniq Sample.l{2}) + /\ (forall x, x \in Compute.qs{1} <=> x \in Sample.l{2})). + + inline {2} 2; auto=> |> &1 &2 qs_is_l i_lt_szp s _. + rewrite qs_is_l=> |>. + by split=> _ x; rewrite in_fsetU1 qs_is_l /#. + by auto. + by inline *; auto=> |> x; rewrite in_fset0. + have ->: mu1 dBlock witness = mu1 dBlock maxu. + + smt(dBlock_uffu). + apply: (pr_collision_q2 (Wrap(A)) _ (q * ell) _ _ &m). + + move=> S S_ll; proc; call (A_run_ll (<: Wrap(A, S).O))=> //. + proc; wp; rnd (predT); while (0 <= i <= size p) (size p - i); auto. + + by call S_ll; auto=> |> /#. + smt(dBlock_uffu size_ge0). + + smt(ge0_q ge0_ell). + proc; call (: size Sample.l = 0 ==> size Sample.l <= q * ell)=> //. + by conseq (transfer_count 0) (A_run_q 0)=> /#. qed. end section Probability_Collision. -lemma Conclusion (A <: RCPA_Adversary { -RCPA_Wrap, -PRP, -PRPi, -QueryBounder, -PRFi (* pollution *), -Compute (* pollution *) }) &m: - (forall (O <: RCPA_Oracles {-A}), islossless O.enc => islossless A(O).distinguish) => - `|Pr[INDR_CPA(IV_Wrap(CBC(PseudoRP)),QueryBounder(A)).main() @ &m: res] - - Pr[INDR_CPA(Random,QueryBounder(A)).main() @ &m: res]| - <= `|Pr[IND(PRP,PRPF_Adv(QueryBounder(A))).main() @ &m: res] - - Pr[IND(PRPi,PRPF_Adv(QueryBounder(A))).main() @ &m: res]| - + 2%r * ((q*ell)^2)%r * mu dBlock (pred1 witness). +lemma Conclusion (A <: RCPA_Adversary { -C, -RCPA_Wrap, -Count, -PRFt.Count, -PRP, -PRPi, -PRFi (* pollution *), -Compute (* pollution *) }) q ell &m: + 0 <= q + => 0 <= ell + => (forall (O <: RCPA_Oracles {-A}), islossless O.enc => islossless A(O).distinguish) + => (forall c, + hoare [A(C(D(PRPF_Adv(A, PRFi).O))).distinguish: C.c = c ==> C.c <= c + q * ell]) + => (forall c, + hoare [A(C(Compute)).distinguish: C.c = c ==> C.c <= c + q * ell]) + => `| Pr[INDR_CPA(IV_Wrap(CBC(PseudoRP)),A).main() @ &m: res] + - Pr[INDR_CPA(Random,A).main() @ &m: res]| + <= `| Pr[IND(PRP(PseudoRP),PRPF_Adv(A)).main() @ &m: res] + - Pr[IND(PRPi,PRPF_Adv(A)).main() @ &m: res]| + + 2%r * ((q*ell)^2)%r * mu dBlock (pred1 witness). proof. -move=> A_distinguish_ll. -have BA_distinguish_ll: (forall (O <: RCPA_Oracles { -QueryBounder(A) }), islossless O.enc => islossless QueryBounder(A,O).distinguish). -+ move=> O O_enc_ll; proc. - call (A_distinguish_ll (<: QueryBounder(A,O).O') _). - + proc; sp; if. - + by wp; call O_enc_ll; auto. - by while (true) (size p + 1 - i); auto=> /#. - by auto. -have:= reduction (QueryBounder(A)) &m BA_distinguish_ll. -have:= Bound_by_Birthday A A_distinguish_ll &m. -have:= Bound_by_PRP_PRF A A_distinguish_ll &m. +move=> ge0_q ge0_ell A_distinguish_ll A_cbc_distinguish_q A_prf_distinguish_q. +have:= reduction A &m A_distinguish_ll. +have:= (Bound_by_Birthday A A_distinguish_ll q ge0_q ell ge0_ell A_prf_distinguish_q &m). +have:= (Bound_by_PRP_PRF A A_distinguish_ll q ge0_q ell ge0_ell A_cbc_distinguish_q &m). have -> : (q * ell)^2 = (q * ell) * (q * ell) by ring. smt(mu_bounded). qed. diff --git a/examples/MEE-CBC/FunctionalSpec.ec b/examples/MEE-CBC/FunctionalSpec.ec index fe3a468d32..280ea88cd4 100644 --- a/examples/MEE-CBC/FunctionalSpec.ec +++ b/examples/MEE-CBC/FunctionalSpec.ec @@ -458,65 +458,75 @@ realize max_pad_n by move=> m t szm /=; rewrite size_pad -addrA ltr_add2r. (** We show that the pWhile programs on which we do the security proof fully and faithfully implement the operators used as functional specs for the C code... **) +module PRP_AES = { + proc keygen() = { + var k; + k <$ dblock; + return k; + } + + proc p(k, x) = { return AES k x; } + proc pi(k, x) = { return AESi k x; } +}. phoare mee_encrypt_correct _mk _ek _p _c: - [MEEt.MEE(MEEt.PRPc.PseudoRP,MEEt.MAC).enc: key = (_ek,_mk) /\ p = _p + [MEEt.MEE(PRP_AES,MEEt.MAC).enc: key = (_ek,_mk) /\ p = _p ==> res = _c] =(mu (dapply (fun iv => iv :: mee_enc AES hmac_sha256 _ek _mk iv _p) dblock) (pred1 _c)). proof. - have->: mu1 (dapply (fun iv=> iv :: mee_enc AES hmac_sha256 _ek _mk iv _p) dblock) _c - = mu1 (dmap dblock (fun iv=> iv :: mee_enc AES hmac_sha256 _ek _mk iv _p)) _c by move. - rewrite dmap1E /pred1 /=. - proc; inline MAC.tag PRPc.PseudoRP.f. - swap 6 -5 => //=; alias 2 iv = s. - while ( 0 <= i <= size (pad _p (hmac_sha256 _mk _p)) - /\ ek = _ek - /\ p' = pad _p (hmac_sha256 _mk _p) - /\ s = nth witness c i - /\ size c = 1 + i - /\ c = iv :: cbc_enc AES _ek iv (take i (pad _p (hmac_sha256 _mk _p)))) - (size (pad _p (hmac_sha256 _mk _p)) - i). - auto=> /> &hr le0_i _ /addzI szcbc_eq_i lti_szpadded. - split; last by smt (). - split; first by smt(). - split; last first. - split; first by rewrite size_cat /= szcbc_eq_i. - rewrite (take_nth witness) //= -cbc_enc_rcons -cats1 /=. - by rewrite size_take // lti_szpadded. - have -> /=: i{hr} + 1 <> 0 by smt (). - by rewrite cats1 nth_rcons size_cbc_enc size_take // lti_szpadded /=. - wp=> //=. - conseq (_: _ ==> s :: mee_enc AES hmac_sha256 _ek _mk s _p = _c)=> //=. - move=> &m [->>] ->> iv //=; split=> [[[le0_size _] h]|<<-]. - have -> //=:= h (iv :: mee_enc AES hmac_sha256 _ek _mk iv _p) - (size (pad _p (hmac_sha256 _mk _p))) - (nth witness (iv :: mee_enc AES hmac_sha256 _ek _mk iv _p) - (size (pad _p (hmac_sha256 _mk _p)))). - split=> //=. - split; 1:by rewrite /mee_enc /= size_cbc_enc addzC. - by rewrite take_size. - split=> [|c n s0]; 1:by split; [rewrite size_ge0|rewrite take0]. - split=> [[[le0_n le_n_size] [s0_is_nth [size_c]]] c_is_enc|]. - by rewrite StdOrder.IntOrder.ler_subl_addr add0z=> /StdOrder.IntOrder.ler_gtF. - rewrite -lezNgt=> le_size_n [[le0_n le_n_size]] [_] [_] ->. - have [_ ->] //:= eqz_leq n (size (pad _p (hmac_sha256 _mk _p))). +have->: mu1 (dapply (fun iv=> iv :: mee_enc AES hmac_sha256 _ek _mk iv _p) dblock) _c + = mu1 (dmap dblock (fun iv=> iv :: mee_enc AES hmac_sha256 _ek _mk iv _p)) _c by move. +rewrite dmap1E /pred1 /=. +proc; inline MAC.tag PRP_AES.p. +swap 6 -5 => //=; alias 2 iv = s. +while ( 0 <= i <= size (pad _p (hmac_sha256 _mk _p)) + /\ ek = _ek + /\ p' = pad _p (hmac_sha256 _mk _p) + /\ s = nth witness c i + /\ size c = 1 + i + /\ c = iv :: cbc_enc AES _ek iv (take i (pad _p (hmac_sha256 _mk _p)))) + (size (pad _p (hmac_sha256 _mk _p)) - i). +- auto=> /> &0 le0_i _ /addzI szcbc_eq_i lti_szpadded. + split; last by smt (). + split; first by smt(). + split; last first. + + split; first by rewrite size_cat /= szcbc_eq_i. + rewrite (take_nth witness) //= -cbc_enc_rcons -cats1 /=. + by rewrite size_take // lti_szpadded. + have -> /=: i{0} + 1 <> 0 by smt (). + by rewrite cats1 nth_rcons size_cbc_enc size_take // lti_szpadded /=. +wp=> //=. +conseq (_: _ ==> s :: mee_enc AES hmac_sha256 _ek _mk s _p = _c)=> //=. ++ move=> &m [->>] ->> iv //=; split=> [[[le0_size _] h]|<<-]. + + have -> //=:= h (iv :: mee_enc AES hmac_sha256 _ek _mk iv _p) + (size (pad _p (hmac_sha256 _mk _p))) + (nth witness (iv :: mee_enc AES hmac_sha256 _ek _mk iv _p) + (size (pad _p (hmac_sha256 _mk _p)))). + split=> //=. + split; 1:by rewrite /mee_enc /= size_cbc_enc addzC. by rewrite take_size. - by rnd. + split=> [|c n s0]; 1:by split; [rewrite size_ge0|rewrite take0]. + split=> [[[le0_n le_n_size] [s0_is_nth [size_c]]] c_is_enc|]. + + by rewrite StdOrder.IntOrder.ler_subl_addr add0z=> /StdOrder.IntOrder.ler_gtF. + rewrite -lezNgt=> le_size_n [[le0_n le_n_size]] [_] [_] ->. + have [_ ->] //:= eqz_leq n (size (pad _p (hmac_sha256 _mk _p))). + by rewrite take_size. +by rnd. qed. phoare mee_decrypt_correct _mk _ek _c: - [MEEt.MEE(MEEt.PRPc.PseudoRP,MEEt.MAC).dec: key = (_ek,_mk) /\ c = _c + [MEEt.MEE(PRP_AES,MEEt.MAC).dec: key = (_ek,_mk) /\ c = _c ==> res = mee_dec AESi hmac_sha256 _ek _mk (head witness _c) (behead _c)] =1%r. proof. conseq (_: true ==> true) (_: _ ==> _)=> //=. -+ proc; inline MAC.verify PRPc.PseudoRP.fi; wp. ++ proc; inline MAC.verify PRP_AES.pi; wp. while ( 0 <= i <= size c /\ ek = _ek /\ s = (if 0 < i then nth witness c (i - 1) else head witness _c) /\ size padded = i /\ padded = cbc_dec AESi _ek (head witness _c) (take i c)). - auto=> /> &hr le0_szpadded _ h lt_padded_c. + + auto=> /> &0 le0_szpadded _ h lt_padded_c. split; first by smt (). split; first by smt (size_ge0). split; first by rewrite size_cat. @@ -525,11 +535,10 @@ conseq (_: true ==> true) (_: _ ==> _)=> //=. auto=> />; split. + by rewrite size_ge0 take0. move=> p /lezNgt le_szc_p _ ge_szc_p. - rewrite (ler_asym (size p) (size (behead _c)) _); - rewrite ?ge_szc_p ?le_szc_p // take_size => p_def. + rewrite (ler_asym (size p) (size (behead _c)) _) ?ge_szc_p ?le_szc_p // take_size => p_def. split. + case: {-1}(unpad p) (eq_refl (unpad p))=> //= - [] m t. by rewrite /mee_dec /= -p_def=> -> /=. by rewrite /mee_dec -p_def /= => ->. - proc; inline *; wp; while true (size c - i); auto =>/#. +by proc; inline *; wp; while true (size c - i); auto =>/#. qed. diff --git a/examples/MEE-CBC/MAC_then_Pad_then_CBC.eca b/examples/MEE-CBC/MAC_then_Pad_then_CBC.eca index 379e672b5f..9678022f48 100644 --- a/examples/MEE-CBC/MAC_then_Pad_then_CBC.eca +++ b/examples/MEE-CBC/MAC_then_Pad_then_CBC.eca @@ -22,16 +22,34 @@ axiom bijectiveP k: (* Import definitions to consider (P,Pinv) as a weak PRP *) clone import PRP as PRPt with - type D <- block. + type D <- block. clone import WeakPRP as PRPSec. clone import PseudoRP as PRPc with - type K <- eK, - op dK <- d_eK, - op p <- P, - op pi <- Pi -proof * by smt (d_eK_uffu bijectiveP). + type K <- eK +proof *. + +module P = { + module S = { + proc keygen() = { + var k; + + k <$ d_eK; + return k; + } + + proc p(k, x) = { + return P k x; + } + + proc pi(k, y) = { + return Pi k y; + } + } + + include PRPc.PRP(S) +}. clone import RP as PRPi with op dD <- d_block @@ -141,7 +159,7 @@ module MEE (P:PseudoRP) (M:MAC_Scheme): Enc_Scheme = { i <- 0; while (i < size p') { pi <- nth witness p' i; - s <@ P.f(ek,s + pi); + s <@ P.p(ek,s + pi); c <- c ++ [s]; i <- i + 1; } @@ -161,7 +179,7 @@ module MEE (P:PseudoRP) (M:MAC_Scheme): Enc_Scheme = { i <- 0; while (i < size c) { ci <- nth witness c i; - pi <@ P.fi(ek,ci); + pi <@ P.pi(ek,ci); padded <- padded ++ [s + pi]; s <- ci; i <- i + 1; @@ -178,41 +196,22 @@ module MEE (P:PseudoRP) (M:MAC_Scheme): Enc_Scheme = { } }. -module RCPA_QueryBounder (A : RCPA_Adversary, O : RCPA_Oracles) = { +module RCPA_QueryCounter (O : RCPA_Oracles) = { var qC : int + var max_size: int - module O' = { - proc enc(p:msg): block list = { - var i; - var c <- witness; - - if (qC < q /\ size (pad (p,witness)) <= n) { - c <@ O.enc(p); - qC <- qC + 1; - } else { - c <- []; - i <- 0; - while (i <= size (pad (p,witness))) { - c <- c ++ [witness]; - i <- i + 1; - } - } - return c; - } - } - - proc distinguish(): bool = { - var b; + proc enc(p:msg): block list = { + var c <- witness; - qC <- 0; - b <@ A(O').distinguish(); - return b; + c <@ O.enc(p); + qC <- qC + 1; + max_size <- max max_size (size (pad (p, witness))); + return c; } }. (* From the MAC and a CPA adversary against MtE, we construct an adversary against the PRP *) -module Weak_PRPa (M : MAC_Scheme, A : RCPA_Adversary, P : PRP_Oracles) = { - var qC: int +module Weak_PRPa (M : MAC_Scheme) (A : RCPA_Adversary) (P : WeakPRP_Oracles) = { var mk: mK module O = { @@ -220,26 +219,16 @@ module Weak_PRPa (M : MAC_Scheme, A : RCPA_Adversary, P : PRP_Oracles) = { var i, s, t, padded, pi; var c <- witness; - if (qC < q /\ size (pad (p,witness)) <= n) { - t <@ M.tag(mk,p); - padded <- pad(p,t); - s <$ d_block; - c <- [s]; - i <- 0; - while (i < size padded) { - pi <- nth witness padded i; - s <@ P.f(s + pi); - c <- c ++ [s]; - i <- i + 1; - } - qC <- qC + 1; - } else { - c <- []; - i <- 0; - while (i <= size (pad (p,witness))) { - c <- c ++ [witness]; - i <- i + 1; - } + t <@ M.tag(mk,p); + padded <- pad(p,t); + s <$ d_block; + c <- [s]; + i <- 0; + while (i < size padded) { + pi <- nth witness padded i; + s <@ P.f(s + pi); + c <- c ++ [s]; + i <- i + 1; } return c; } @@ -248,7 +237,6 @@ module Weak_PRPa (M : MAC_Scheme, A : RCPA_Adversary, P : PRP_Oracles) = { proc distinguish(): bool = { var b; - qC <- 0; mk <@ M.keygen(); b <@ A(O).distinguish(); return b; @@ -256,13 +244,15 @@ module Weak_PRPa (M : MAC_Scheme, A : RCPA_Adversary, P : PRP_Oracles) = { }. section RCPA. - declare module A <: RCPA_Adversary { -PRPi, -PRP, -RCPA_Wrap, -RCPA_QueryBounder, -Weak_PRPa }. + declare module A <: RCPA_Adversary { -PRPi, -PRP, -RCPA_Wrap, -RCPA_QueryCounter, -Weak_PRPa }. declare axiom A_distinguish_ll (O <: RCPA_Oracles { -A }): islossless O.enc => islossless A(O).distinguish. + declare axiom A_querycount (O <: RCPA_Oracles { -A, -RCPA_QueryCounter } (* TODO (optional): refine this *)) c m: + hoare[A(RCPA_QueryCounter(O)).distinguish: + RCPA_QueryCounter.qC = c /\ RCPA_QueryCounter.max_size = m + ==> RCPA_QueryCounter.qC <= c + q /\ RCPA_QueryCounter.max_size = max m n]. local clone import CBC as CBCa with - op q <- q, - op ell <- n, type key <- eK, op dKey <- d_eK, type block <- block, @@ -272,8 +262,6 @@ section RCPA. op P <- P, op Pi <- Pi proof *. - realize gt0_q by exact/gt0_q. - realize gt0_ell by smt (gt1_n). realize dKey_uffu by smt(@Distr d_eK_uffu). realize dBlock_uffu by smt(@Distr d_block_uffu). realize add0b by exact/add0b. @@ -309,174 +297,223 @@ section RCPA. proof * by smt (dlist_ll d_block_uffu can_unpad leak_pad pad_tag). local lemma MEE_unfold &m: - Pr[INDR_CPA(MEE(PseudoRP,MAC),RCPA_QueryBounder(A)).main() @ &m: res] - = Pr[INDR_CPA(MacThenEncrypt(PadThenEncrypt(IV_Wrap(CBC(PseudoRP))),MAC),RCPA_QueryBounder(A)).main () @ &m: res]. + Pr[INDR_CPA(MEE(PseudoRP,MAC), A).main() @ &m: res] + = Pr[INDR_CPA(MacThenEncrypt(PadThenEncrypt(IV_Wrap(CBC(PseudoRP))),MAC), A).main () @ &m: res]. proof. - byequiv (: ={glob A} ==> ={res}); first last. - + done. - + done. + byequiv (: ={glob A} ==> ={res})=> //; first last. proc; inline *. - wp; call (: ={glob RCPA_QueryBounder, glob RCPA_Wrap}). - + proc; inline*; sp; if; auto; sim. + wp; call (: ={glob RCPA_Wrap}). + + proc; inline *; auto; sim. by auto. by auto. qed. (** We bound the RCPA advantage of A against MEE(P,M) **) local lemma MtE_security &m: - `|Pr[INDR_CPA(MacThenEncrypt(PadThenEncrypt(IV_Wrap(CBC(PseudoRP))),MAC),RCPA_QueryBounder(A)).main() @ &m: res] - - Pr[INDR_CPA(Ideal,RCPA_QueryBounder(A)).main() @ &m: res]| - = `|Pr[SKEa.RCPA.INDR_CPA(PadThenEncrypt(IV_Wrap(CBC(PseudoRP))),RCPA_WUF_RCPA.RCPAa(MAC,RCPA_QueryBounder(A))).main() @ &m: res] - - Pr[SKEa.RCPA.INDR_CPA(SKEa.RCPA.Ideal,RCPA_WUF_RCPA.RCPAa(MAC,RCPA_QueryBounder(A))).main() @ &m: res]|. + `| Pr[INDR_CPA(MacThenEncrypt(PadThenEncrypt(IV_Wrap(CBC(PseudoRP))),MAC), A).main() @ &m: res] + - Pr[INDR_CPA(Ideal, A).main() @ &m: res]| + = `| Pr[SKEa.RCPA.INDR_CPA(PadThenEncrypt(IV_Wrap(CBC(PseudoRP))),RCPA_WUF_RCPA.RCPAa(MAC, A)).main() @ &m: res] + - Pr[SKEa.RCPA.INDR_CPA(SKEa.RCPA.Ideal,RCPA_WUF_RCPA.RCPAa(MAC, A)).main() @ &m: res]|. proof. - (* Unfortunately, we have several copies of the modules and - alpha conversion does not work at module level, so we need - to prove that it implies semantic equality. This is easy. *) - rewrite -(RCPA_WUF_RCPA.RCPA_preservation (<: PadThenEncrypt(IV_Wrap(CBC(PseudoRP)))) MAC (<: RCPA_QueryBounder(A)) &m _ _). - by proc; rnd predT; auto=> />; smt (d_mK_uffu). - by proc. - do !congr. - by byequiv=> //=; sim. - byequiv=> //=. proc; inline *; wp; call (_: ={glob RCPA_QueryBounder}). - proc; inline *; sp; if=> //=; auto; [smt (leak_pad pad_tag)|sim]. - by auto. + (* Unfortunately, we have several copies of the modules and + alpha conversion does not work at module level, so we need + to prove that it implies semantic equality. This is easy. *) + rewrite -(RCPA_WUF_RCPA.RCPA_preservation (<: PadThenEncrypt(IV_Wrap(CBC(PseudoRP)))) MAC (<: A) &m _ _). + + by proc; rnd predT; auto=> />; smt (d_mK_uffu). + + by proc. + do !congr. + + by byequiv=> //=; sim. + byequiv=> //=. + proc; inline *; wp; call (: true). + + by proc; inline *; auto=> //; smt(leak_pad pad_tag). + by auto. qed. local lemma PtE_security &m: - `|Pr[SKEa.RCPA.INDR_CPA(PadThenEncrypt(IV_Wrap(CBC(PseudoRP))),RCPA_WUF_RCPA.RCPAa(MAC,RCPA_QueryBounder(A))).main() @ &m: res] - Pr[SKEa.RCPA.INDR_CPA(SKEa.RCPA.Ideal,RCPA_WUF_RCPA.RCPAa(MAC,RCPA_QueryBounder(A))).main() @ &m: res]| - = `|Pr[CoreDefs.RCPA.INDR_CPA(IV_Wrap(CBC(PseudoRP)),RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,RCPA_QueryBounder(A)))).main() @ &m: res] - Pr[CoreDefs.RCPA.INDR_CPA(CoreDefs.RCPA.Ideal,RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,RCPA_QueryBounder(A)))).main() @ &m: res]|. + `| Pr[SKEa.RCPA.INDR_CPA(PadThenEncrypt(IV_Wrap(CBC(PseudoRP))),RCPA_WUF_RCPA.RCPAa(MAC,A)).main() @ &m: res] + - Pr[SKEa.RCPA.INDR_CPA(SKEa.RCPA.Ideal,RCPA_WUF_RCPA.RCPAa(MAC,A)).main() @ &m: res]| + = `| Pr[CoreDefs.RCPA.INDR_CPA(IV_Wrap(CBC(PseudoRP)),RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A))).main() @ &m: res] + - Pr[CoreDefs.RCPA.INDR_CPA(CoreDefs.RCPA.Ideal,RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A))).main() @ &m: res]|. proof. - (* The same issue arises here *) - rewrite -(RCPA_preservation (<: IV_Wrap(CBC(PseudoRP))) (<: RCPA_WUF_RCPA.RCPAa(MAC,RCPA_QueryBounder(A))) &m). - do !congr. - by byequiv=> //=; sim. - byequiv=> //=; proc; inline *. - wp; call (_: ={glob RCPA_QueryBounder, glob RCPA_WUF_RCPA.RCPAa}). - by proc; inline *; sp; if=> //=; sim. - by auto. + rewrite -(RCPA_preservation (<: IV_Wrap(CBC(PseudoRP))) (<: RCPA_WUF_RCPA.RCPAa(MAC,A)) &m). + do !congr. + + by byequiv=> //=; sim. + byequiv=> //=; proc; inline *. + wp; call (: ={glob RCPA_WUF_RCPA.RCPAa}). + + by proc; inline *; auto. + by auto. qed. +(* +print RCPAa. + local module RedCount (O <: RCPA_Oracles) = { + proc distinguish() = { + var b; + + RCPA_QueryCounter.qC <- 0; + RCPA_QueryCounter.max_size <- 0; + b <@ +*) local lemma CBC_security &m: - `|Pr[CoreDefs.RCPA.INDR_CPA(IV_Wrap(CBC(PseudoRP)),RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,RCPA_QueryBounder(A)))).main () @ &m: res] - - Pr[CoreDefs.RCPA.INDR_CPA(CoreDefs.RCPA.Ideal,RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,RCPA_QueryBounder(A)))).main () @ &m: res]| - = `|Pr[CBCa.SKEa.RCPA.INDR_CPA(IV_Wrap(CBC(PseudoRP)),QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A)))).main() @ &m: res] - - Pr[CBCa.SKEa.RCPA.INDR_CPA(CBCa.SKEa.RCPA.Ideal,QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A)))).main() @ &m: res]|. - proof. - (* We have the same issue PLUS we need to move the QueryBounder around. - A much better way of doing this would be to make sure that each library - defines its own QueryCounter and QueryBounder and to make sure that - abstract security results come in both bounded and unbounded (when - possible) flavours. This is TODO when we rework the crypto libraries *) - have PushQueryBounder: forall (O <: CBCa.SKEa.RCPA.RCPA_Oracles { -A, -RCPA_QueryBounder, -OracleBounder, -RCPA_WUF_RCPA.RCPAa }), - equiv [QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A)),O).distinguish - ~ RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,RCPA_QueryBounder(A)),O).distinguish - : ={arg, glob A, glob O} ==> ={res}]. - move=> O; proc; inline *. - wp; call (_: ={glob O, glob RCPA_WUF_RCPA.RCPAa} - /\ ={qC}(OracleBounder,RCPA_QueryBounder)). - proc; inline *. - case ((RCPA_QueryBounder.qC < q /\ size (pad (p,witness)) <= n){2}). - rcondt{2} 2; 1:by auto. - rcondt{1} 8; 1:by auto; smt (pad_tag). - wp; call (_: true). - by auto. - rcondf{2} 2; 1:by auto. - rcondf{1} 8; 1:by auto; smt (pad_tag). - wp; while ( ={i, p} - /\ r{1} = c{2} - /\ p0{1} = pad (p,t){1}). - by auto; smt (pad_tag). - by auto; smt (max_pad_n pad_tag). - by auto. - have ->: Pr[CBCa.SKEa.RCPA.INDR_CPA(IV_Wrap(CBC(PseudoRP)),QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A)))).main() @ &m: res] - = Pr[CBCa.SKEa.RCPA.INDR_CPA(IV_Wrap(CBC(PseudoRP)),RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,RCPA_QueryBounder(A)))).main() @ &m: res]. - byequiv=> //=; proc. - call (PushQueryBounder (CBCa.SKEa.RCPA.RCPA_Wrap(IV_Wrap(CBC(PseudoRP))))). - by call (_: true); auto. - have ->: Pr[CBCa.SKEa.RCPA.INDR_CPA(CBCa.SKEa.RCPA.Ideal,QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A)))).main() @ &m: res] - = Pr[CBCa.SKEa.RCPA.INDR_CPA(CBCa.SKEa.RCPA.Ideal,RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,RCPA_QueryBounder(A)))).main() @ &m: res]. - byequiv=> //=; proc. - call (PushQueryBounder (CBCa.SKEa.RCPA.RCPA_Wrap(CBCa.SKEa.RCPA.Ideal))). - by call (_: true); auto. - do !congr. - by byequiv=> //=; sim. - byequiv=> //=; proc. - inline *; wp. - call (_: ={glob RCPA_QueryBounder, glob RCPA_WUF_RCPA.RCPAa} - /\ ={k}(CoreDefs.RCPA.RCPA_Wrap,CBCa.SKEa.RCPA.RCPA_Wrap)). - by proc; inline *; sp; if=> //=; sim. - by auto. - qed. + `| Pr[CoreDefs.RCPA.INDR_CPA(IV_Wrap(CBC(PseudoRP)),RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A))).main () @ &m: res] + - Pr[CoreDefs.RCPA.INDR_CPA(CoreDefs.RCPA.Ideal,RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A))).main () @ &m: res]| + = `| Pr[CBCa.SKEa.RCPA.INDR_CPA(IV_Wrap(CBC(PseudoRP)),RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A))).main() @ &m: res] + - Pr[CBCa.SKEa.RCPA.INDR_CPA(CBCa.SKEa.RCPA.Ideal,RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A))).main() @ &m: res]|. + proof. by do !congr; byequiv=> //=; sim. qed. + + local module WrapA (O : RCPA_Oracles) = A(RCPA_QueryCounter(O)). + + local module WrapRed (A : PtE.RCPA.RCPA_Adversary) (O : CoreDefs.RCPA.RCPA_Oracles) = { + proc distinguish() = { + var b; + + RCPA_QueryCounter.qC <- 0; + RCPA_QueryCounter.max_size <- 0; + b <@ RCPAa(A, O).distinguish(); + return b; + } + }. local lemma local_conclusion &m: - `|Pr[INDR_CPA(MacThenEncrypt(PadThenEncrypt(IV_Wrap(CBC(PseudoRP))),MAC),RCPA_QueryBounder(A)).main () @ &m: res] - - Pr[INDR_CPA(Ideal,RCPA_QueryBounder(A)).main() @ &m: res]| - <= `|Pr[IND(PRP, PRPF_Adv(QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A))))).main() @ &m : res] - - Pr[IND(PRPi, PRPF_Adv(QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A))))).main() @ &m : res]| + `| Pr[INDR_CPA(MacThenEncrypt(PadThenEncrypt(IV_Wrap(CBC(PseudoRP))),MAC),A).main () @ &m: res] + - Pr[INDR_CPA(Ideal,A).main() @ &m: res]| + <= `| Pr[IND(P, PRPF_Adv(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC, A)))).main() @ &m : res] + - Pr[IND(PRPi, PRPF_Adv(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC, A)))).main() @ &m : res]| + 2%r * ((q * n) ^ 2)%r * mu d_block (pred1 witness). proof. - have := Conclusion (<: RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A))) &m _. - move=> O O_enc_ll. - proc; inline *. - wp; call (_: true); 1:exact/A_distinguish_ll. - by proc; inline *; wp; call O_enc_ll; auto. - by wp; rnd predT; auto; smt (d_mK_uffu). - rewrite (MtE_security &m) (PtE_security &m) (CBC_security &m). - (* Here again, we have to tell EasyCrypt that alpha equality implies semantic equality *) - have ->: Pr[PRFt.IND(PRPr.PRP, PRPF_Adv(QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A))))).main() @ &m: res] - = Pr[IND(PRP,PRPF_Adv(QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A))))).main() @ &m: res]. - by byequiv=> //=; sim. - have ->: Pr[PRFt.IND(PRPi.PRPi, PRPF_Adv(QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A))))).main() @ &m: res] - = Pr[IND(PRPi,PRPF_Adv(QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A))))).main() @ &m: res]. - by byequiv=> //=; sim. - have ->: Pr[CBCa.SKEa.RCPA.INDR_CPA(IV_Wrap(CBC(PRPr.PseudoRP)),QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A)))).main() @ &m: res] - = Pr[CBCa.SKEa.RCPA.INDR_CPA(IV_Wrap(CBC(PseudoRP)),QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A)))).main() @ &m: res]. - by byequiv=> //=; sim. - (* And we conclude by proving the equivalence of the Random module and the Ideal module used in IND$-CPA *) - have ->: Pr[CBCa.SKEa.RCPA.INDR_CPA(Random,QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A)))).main() @ &m: res] - = Pr[CBCa.SKEa.RCPA.INDR_CPA(CBCa.SKEa.RCPA.Ideal,QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A)))).main() @ &m: res]. - byequiv=> //=; proc; inline *; wp. - call (_: ={glob OracleBounder, glob RCPA_WUF_RCPA.RCPAa}). - proc. - call (_: ={glob OracleBounder}). - call (_: ={glob OracleBounder}). - sp; if=> //=; 2:by sim. - wp; call (_: true)=> //=. - by call Random_Ideal=> //=. - by auto. - by call (_: true); auto. - by auto. - done. + have ->: Pr[IND(P, PRPF_Adv(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC, A)))).main() @ &m: res] + = Pr[RP_RF.PRPSec.IND(PRPr.PRP(PseudoRP), PRPF_Adv(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC, A)))).main() @ &m: res]. + + by byequiv=> //; sim. + have ->: Pr[IND(PRPi, PRPF_Adv(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC, A)))).main() @ &m: res] + = Pr[RP_RF.PRPSec.IND(RP_RF.PRPi.PRPi, PRPF_Adv(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC, A)))).main() @ &m: res]. + + by byequiv=> //; sim. + rewrite (MtE_security &m) (PtE_security &m) (CBC_security &m). + have <-: Pr[CBCa.SKEa.RCPA.INDR_CPA(Random,RCPAa(RCPA_WUF_RCPA.RCPAa(MAC, A))).main() @ &m: res] + = Pr[CBCa.SKEa.RCPA.INDR_CPA(CBCa.SKEa.RCPA.Ideal,RCPAa(RCPA_WUF_RCPA.RCPAa(MAC, A))).main() @ &m: res]. + + byequiv=> //=; proc; inline *; wp. + call (: ={CBCa.SKEa.RCPA.RCPA_Wrap.k, RCPA_WUF_RCPA.RCPAa.mk}). + + proc; auto; call (: ={CBCa.SKEa.RCPA.RCPA_Wrap.k, RCPA_WUF_RCPA.RCPAa.mk}). + + inline {1} 1; inline {2} 1. + by wp; call Random_Ideal; auto. + by call (: true); auto. + by auto. + (** Now this is Conclusion, up to our ability to prove that the + reduction queries no more than q * n blocks... Unfortunately, this + is the hard part. + We could fold this into the previous rewrites, but avoid doing + so for clarity. **) + have ->: Pr[CBCa.SKEa.RCPA.INDR_CPA(IV_Wrap(CBC(PseudoRP)), RCPAa(RCPA_WUF_RCPA.RCPAa(MAC, A))).main() @ &m: res] + = Pr[CBCa.SKEa.RCPA.INDR_CPA(IV_Wrap(CBC(PseudoRP)), WrapRed(RCPA_WUF_RCPA.RCPAa(MAC, WrapA))).main() @ &m: res]. + + byequiv=> //; proc; inline *. + wp; call (: ={glob RCPA_WUF_RCPA.RCPAa, glob CBCa.SKEa.RCPA.RCPA_Wrap}). + + by proc; inline *; wp; sim. + by auto. + have ->: Pr[CBCa.SKEa.RCPA.INDR_CPA(Random, RCPAa(RCPA_WUF_RCPA.RCPAa(MAC, A))).main() @ &m: res] + = Pr[CBCa.SKEa.RCPA.INDR_CPA(Random, WrapRed(RCPA_WUF_RCPA.RCPAa(MAC, WrapA))).main() @ &m: res]. + + byequiv=> //; proc; inline *. + wp; call (: ={glob RCPA_WUF_RCPA.RCPAa}). + + by proc; inline *; wp; sim. + by auto. + have ->: Pr[RP_RF.PRPSec.IND(PRPr.PRP(PseudoRP), PRPF_Adv(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC, A)))).main() @ &m: res] + = Pr[RP_RF.PRPSec.IND(PRPr.PRP(PseudoRP), PRPF_Adv(WrapRed(RCPA_WUF_RCPA.RCPAa(MAC, WrapA)))).main() @ &m: res]. + + byequiv=> //; proc; inline *. + wp; call (: ={glob RCPA_WUF_RCPA.RCPAa, glob PRPr.PRP}). + + by proc; inline *; wp; sim. + by auto. + have ->: Pr[RP_RF.PRPSec.IND(RP_RF.PRPi.PRPi, PRPF_Adv(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC, A)))).main() @ &m: res] + = Pr[RP_RF.PRPSec.IND(RP_RF.PRPi.PRPi, PRPF_Adv(WrapRed(RCPA_WUF_RCPA.RCPAa(MAC, WrapA)))).main() @ &m: res]. + + byequiv=> //; proc; inline *. + wp; call (: ={glob RCPA_WUF_RCPA.RCPAa, glob RP_RF.PRPi.PRPi}). + + by proc; inline *; wp; sim. + by auto. + apply: (Conclusion (<: WrapRed(RCPA_WUF_RCPA.RCPAa(MAC, WrapA))) q n &m _ _ _). + + smt(gt0_q). + + smt(gt1_n). + + move=> O O_enc_ll. + proc; inline *. + wp; call (_: true); 1:exact/A_distinguish_ll. + + by proc; inline *; wp; call O_enc_ll; auto. + by wp; rnd predT; auto; smt (d_mK_uffu). + + move=> c; proc; inline 3; wp. + call (: RCPA_QueryCounter.qC = 0 + /\ RCPA_QueryCounter.max_size = 0 + /\ C.c = c + ==> 0 <= RCPA_QueryCounter.qC + /\ 0 <= RCPA_QueryCounter.max_size + /\ C.c - c <= RCPA_QueryCounter.qC * RCPA_QueryCounter.max_size + /\ RCPA_QueryCounter.qC <= q + /\ RCPA_QueryCounter.max_size <= n). + + conseq (: 0 <= RCPA_QueryCounter.qC + /\ 0 <= RCPA_QueryCounter.max_size + /\ C.c - c <= RCPA_QueryCounter.qC * RCPA_QueryCounter.max_size) + (A_querycount (<: RCPA_WUF_RCPA.RCPAa(MAC, WrapA, RCPAa(RCPA_WUF_RCPA.RCPAa(MAC, WrapA), C(D(PRPF_Adv(WrapRed(RCPA_WUF_RCPA.RCPAa(MAC, WrapA)), RP_RF.RF.PRFi).O))).S).Sim) 0 0)=> //. + + smt(gt1_n). + proc ( 0 <= RCPA_QueryCounter.qC + /\ 0 <= RCPA_QueryCounter.max_size + /\ C.c - c <= RCPA_QueryCounter.qC * RCPA_QueryCounter.max_size)=> //. + + proc; inline *; wp. + while (0 <= i <= size p2). + + by auto; conseq (: true)=> //#. + auto=> |> &0 ge0_qC ge0_ms ih _ _; split. + + exact: size_ge0. + move=> i + ge0_i /lez_eqVlt - -> /=. + by rewrite (pad_tag _ (mac RCPA_WUF_RCPA.RCPAa.mk p){0} witness) /#. + by inline *; auto=> |> _ _ max_size qC c0 /#. + + move=> c; proc; inline 3; wp. + call (: RCPA_QueryCounter.qC = 0 + /\ RCPA_QueryCounter.max_size = 0 + /\ C.c = c + ==> 0 <= RCPA_QueryCounter.qC + /\ 0 <= RCPA_QueryCounter.max_size + /\ C.c - c <= RCPA_QueryCounter.qC * RCPA_QueryCounter.max_size + /\ RCPA_QueryCounter.qC <= q + /\ RCPA_QueryCounter.max_size <= n). + + conseq (: 0 <= RCPA_QueryCounter.qC + /\ 0 <= RCPA_QueryCounter.max_size + /\ C.c - c <= RCPA_QueryCounter.qC * RCPA_QueryCounter.max_size) + (A_querycount (<: RCPA_WUF_RCPA.RCPAa(MAC, WrapA, RCPAa(RCPA_WUF_RCPA.RCPAa(MAC, WrapA), C(Compute)).S).Sim) 0 0)=> //. + + smt(gt1_n). + proc ( 0 <= RCPA_QueryCounter.qC + /\ 0 <= RCPA_QueryCounter.max_size + /\ C.c - c <= RCPA_QueryCounter.qC * RCPA_QueryCounter.max_size)=> //. + + proc; inline *; auto. + while (0 <= i <= size p2). + + by auto=> //#. + auto=> |> &0 ge0_qC ge0_ms ih; split. + + exact: size_ge0. + move=> i + ge0_i /lez_eqVlt - -> /=. + by rewrite (pad_tag _ (mac RCPA_WUF_RCPA.RCPAa.mk p){0} witness) /#. + by inline *; auto=> |> _ _ max_size qC c0 /#. qed. - local lemma CleanupAdversary (P <: PRP { -A, -Weak_PRPa, -OracleBounder, -RCPA_WUF_RCPA.RCPAa }) &m: - Pr[IND(P,Weak_PRPa(MAC,A)).main() @ &m: res] - = Pr[IND(P, PRPF_Adv(QueryBounder(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A))))).main() @ &m : res]. + local lemma CleanupAdversary (P <: WeakPRP { -A, -Weak_PRPa, -RCPA_WUF_RCPA.RCPAa }) &m: + Pr[IND(P, Weak_PRPa(MAC,A)).main() @ &m: res] + = Pr[IND(P, PRPF_Adv(RCPAa(RCPA_WUF_RCPA.RCPAa(MAC,A)))).main() @ &m : res]. proof. - byequiv (_: ={glob P, glob A} ==> ={res})=> //=; proc; inline *; wp. - call (_: ={glob P} - /\ ={qC}(Weak_PRPa,OracleBounder) - /\ Weak_PRPa.mk{1} = RCPA_WUF_RCPA.RCPAa.mk{2})=> //=. - proc; inline *; sp. - if; 1:smt (max_pad_n pad_tag). - + by sim; auto. - wp; while ( ={i} - /\ size (pad (p,witness)){1} = size p0{2} - /\ c{1} = r{2}); - 1:by auto=> /#. - by auto; smt (pad_tag). - by auto; call (_: true). + byequiv (: ={glob P, glob A} ==> ={res})=> //=; proc; inline *; wp. + call (: ={glob P} + /\ Weak_PRPa.mk{1} = RCPA_WUF_RCPA.RCPAa.mk{2})=> //=. + + proc; inline *; sp. + wp; while ( ={glob P, i, s} + /\ padded{1} = p0{2} + /\ c{1} = c1{2}). + + by auto; call (: true); auto. + by auto. + by auto; call (: true). qed. lemma RCPA_security &m: - `|Pr[INDR_CPA(MEE(PseudoRP,MAC),RCPA_QueryBounder(A)).main() @ &m: res] - - Pr[INDR_CPA(Ideal,RCPA_QueryBounder(A)).main() @ &m: res]| - <= `|Pr[IND(PRP, Weak_PRPa(MAC,A)).main() @ &m : res] + `|Pr[INDR_CPA(MEE(P.S,MAC),A).main() @ &m: res] + - Pr[INDR_CPA(Ideal,A).main() @ &m: res]| + <= `|Pr[IND(P, Weak_PRPa(MAC,A)).main() @ &m : res] - Pr[IND(PRPi, Weak_PRPa(MAC,A)).main() @ &m: res]| + 2%r * ((q * n) ^ 2)%r * mu d_block (pred1 witness). proof. - rewrite (MEE_unfold &m) (CleanupAdversary PRP &m) (CleanupAdversary PRPi &m). - exact/(local_conclusion &m). + have ->: Pr[INDR_CPA(MEE(P.S, MAC), A).main() @ &m: res] + = Pr[INDR_CPA(MEE(PseudoRP, MAC), A).main() @ &m: res]. + + by byequiv=> //; sim. + rewrite (MEE_unfold &m) (CleanupAdversary P &m) (CleanupAdversary PRPi &m). + exact/(local_conclusion &m). qed. end section RCPA. @@ -496,7 +533,7 @@ module CMAa (P : PseudoRP) (A : PTXT_Adversary) (M : CMA_Oracles) = { i <- 0; while (i < size padded) { pi <- nth witness padded i; - s <@ P.f(ek,s + pi); + s <@ P.p(ek,s + pi); c <- c ++ [s]; i <- i + 1; } @@ -514,7 +551,7 @@ module CMAa (P : PseudoRP) (A : PTXT_Adversary) (M : CMA_Oracles) = { i <- 0; while (i < size c) { ci <- nth witness c i; - pi <@ P.fi(ek,ci); + pi <@ P.pi(ek,ci); padded <- padded ++ [s + pi]; s <- ci; i <- i + 1; @@ -543,8 +580,6 @@ section PTXT. (** TODO: this is not useful apart from avoiding having to define the part of the scheme that we don't care about **) local clone import CBC as CBCb (* FIXME *) with - op q <- q, - op ell <- n, type key <- eK, op dKey <- d_eK, type block <- block, @@ -554,8 +589,6 @@ section PTXT. op P <- P, op Pi <- Pi proof *. - realize gt0_q by exact/gt0_q. - realize gt0_ell by smt (gt1_n). realize dKey_uffu by smt(@Distr d_eK_uffu). realize dBlock_uffu by smt(@Distr d_block_uffu). realize add0b by exact/add0b. @@ -595,12 +628,12 @@ section PTXT. Pr[INT_PTXT(MEE(PseudoRP,MAC),A).main() @ &m: res] = Pr[INT_PTXT(MacThenEncrypt(PadThenEncrypt(IV_Wrap(CBC(PseudoRP))),MAC),A).main () @ &m: res]. proof. - byequiv (_: ={glob A} ==> ={res})=> //=; proc; inline *. - wp; call (_: ={glob PTXT_Wrap})=> //=. - by proc; inline *; sim; auto. - proc; inline *; sim. - by wp=> //=; sim. - by auto. + byequiv (_: ={glob A} ==> ={res})=> //=; proc; inline *. + wp; call (_: ={glob PTXT_Wrap})=> //=. + by proc; inline *; sim; auto. + proc; inline *; sim. + by wp=> //=; sim. + by auto. qed. (** We bound the PTXT advantage of A against MEE(P,M) **) @@ -648,11 +681,16 @@ section PTXT. qed. lemma PTXT_security &m: - Pr[INT_PTXT(MEE(PseudoRP,MAC),A).main () @ &m: res] - <= Pr[WUF_CMA(MAC,CMAa(PseudoRP,A)).main() @ &m: res]. + Pr[INT_PTXT(MEE(P.S,MAC), A).main() @ &m: res] + <= Pr[WUF_CMA(MAC,CMAa(P.S, A)).main() @ &m: res]. proof. - rewrite (MEE_unfold &m) -(CleanupAdversary &m). - exact/(local_conclusion &m). + have ->: Pr[INT_PTXT(MEE(P.S, MAC), A).main() @ &m: res] + = Pr[INT_PTXT(MEE(PseudoRP, MAC), A).main() @ &m: res]. + + by byequiv=> //; sim. + have ->: Pr[WUF_CMA(MAC,CMAa(P.S, A)).main() @ &m: res] + = Pr[WUF_CMA(MAC,CMAa(PseudoRP, A)).main() @ &m: res]. + + by byequiv=> //; sim. + rewrite (MEE_unfold &m) -(CleanupAdversary &m). + exact/(local_conclusion &m). qed. end section PTXT. - diff --git a/examples/MEE-CBC/RCPA_CMA.ec b/examples/MEE-CBC/RCPA_CMA.ec index 574dcbe099..143c172a96 100644 --- a/examples/MEE-CBC/RCPA_CMA.ec +++ b/examples/MEE-CBC/RCPA_CMA.ec @@ -41,7 +41,7 @@ theory MtE. proof * by smt. (** The black-box construction is as follows **) - module MacThenEncrypt(E:SKEa.Enc_Scheme, M:MACa.MAC_Scheme): Enc_Scheme = { + module MacThenEncrypt (E: SKEa.Enc_Scheme) (M: MACa.MAC_Scheme): Enc_Scheme = { proc keygen(): eK * mK = { var ek, mk; diff --git a/theories/crypto/Birthday.eca b/theories/crypto/Birthday.eca index df2cfb3410..b5808d63b0 100644 --- a/theories/crypto/Birthday.eca +++ b/theories/crypto/Birthday.eca @@ -10,13 +10,7 @@ type T. op uT: T distr. -(* -------------------------------------------------------------------- *) - -(** A non-negative integer q **) -op q : { int | 0 <= q } as ge0_q. - op maxu : T = mode uT. - lemma maxuP x: mu1 uT x <= mu1 uT maxu by apply mode_ge. (** A module that samples in uT on queries to s **) @@ -67,119 +61,49 @@ section. declare module A <: Adv {-Sample}. declare axiom A_ll (S <: ASampler {-A}): islossless S.s => islossless A(S).a. + declare op q : { int | 0 <= q } as ge0_q. + lemma pr_Sample_le &m: - Pr[Exp(Sample,A).main() @ &m : size Sample.l <= q /\ !uniq Sample.l] - <= (q*(q-1))%r/2%r * mu1 uT maxu. + Pr[Exp(Sample, A).main() @ &m : size Sample.l <= q /\ !uniq Sample.l] + <= (q * (q - 1))%r / 2%r * mu1 uT maxu. proof. - fel 1 (size Sample.l) (fun x, x%r * mu1 uT maxu) q (!uniq Sample.l) []=> //. - + by rewrite -Bigreal.BRA.mulr_suml Bigreal.sumidE 1:ge0_q. - + by inline*; auto. - + proc;wp; rnd (mem Sample.l); skip=> // /> &hr ???. - apply (Mu_mem.mu_mem_le_size (Sample.l{hr}) uT (mu1 uT maxu)). - by move=> x _;rewrite maxuP. - by move=> c; proc; auto=> /#. + fel 1 (size Sample.l) (fun x, x%r * mu1 uT maxu) q (!uniq Sample.l) []=> //. + + by rewrite -Bigreal.BRA.mulr_suml Bigreal.sumidE 1:ge0_q. + + by inline *; auto. + + proc; wp; rnd (mem Sample.l); skip=> // /> &hr ???. + apply: (Mu_mem.mu_mem_le_size (Sample.l{hr}) uT (mu1 uT maxu)). + by move=> x _;rewrite maxuP. + by move=> c; proc; auto=> /#. qed. lemma pr_Sample_le_q2 &m: - Pr[Exp(Sample,A).main() @ &m: size Sample.l <= q /\ !uniq Sample.l] + Pr[Exp(Sample, A).main() @ &m: size Sample.l <= q /\ !uniq Sample.l] <= (q^2)%r * mu1 uT maxu. proof. - apply (ler_trans _ _ _ (pr_Sample_le &m)). - apply ler_wpmul2r; 1: by apply ge0_mu. - have -> : q^2 = q*q by ring. - smt(ge0_q). + apply/(ler_trans _ _ _ (pr_Sample_le &m))/ler_wpmul2r; 1: by apply ge0_mu. + rewrite (IntID.exprS _ 1) // IntID.expr1. + smt(ge0_q). qed. declare axiom A_bounded: hoare [A(Sample).a : size Sample.l = 0 ==> size Sample.l <= q]. local lemma aux &m : - Pr[Exp(Sample,A).main() @ &m: !uniq Sample.l] = - Pr[Exp(Sample,A).main() @ &m: size Sample.l <= q /\ !uniq Sample.l]. + Pr[Exp(Sample,A).main() @ &m: !uniq Sample.l] + = Pr[Exp(Sample,A).main() @ &m: size Sample.l <= q /\ !uniq Sample.l]. proof. - byequiv (_: ={glob A} ==> ={Sample.l} /\ size Sample.l{2} <= q)=> //=. - conseq (_: _ ==> ={Sample.l}) _ (_: _ ==> size Sample.l <= q)=> //=;2:by sim. - by proc;call A_bounded;inline *;auto. + byequiv (_: ={glob A} ==> ={Sample.l} /\ size Sample.l{2} <= q)=> //=. + conseq (_: _ ==> ={Sample.l}) _ (_: _ ==> size Sample.l <= q)=> //=;2:by sim. + by proc;call A_bounded;inline *;auto. qed. lemma pr_collision &m: - Pr[Exp(Sample,A).main() @ &m: !uniq Sample.l] - <= (q*(q-1))%r/2%r* mu1 uT maxu. - proof. rewrite (aux &m); apply (pr_Sample_le &m). qed. + Pr[Exp(Sample,A).main() @ &m: !uniq Sample.l] + <= (q * (q - 1))%r / 2%r * mu1 uT maxu. + proof. by rewrite (aux &m); exact: (pr_Sample_le &m). qed. lemma pr_collision_q2 &m: - Pr[Exp(Sample,A).main() @ &m: !uniq Sample.l] + Pr[Exp(Sample,A).main() @ &m: !uniq Sample.l] <= (q^2)%r * mu1 uT maxu. - proof. rewrite (aux &m); apply (pr_Sample_le_q2 &m). qed. + proof. by rewrite (aux &m); exact: (pr_Sample_le_q2 &m). qed. end section. - -(*** The same result using a bounding module ***) -module Bounder(S:Sampler) = { - var c:int - - proc init(): unit = { - S.init(); - c <- 0; - } - - proc s(): T = { - var r <- witness; - - if (c < q) { - r <@ S.s(); - c <- c + 1; - } - return r; - } -}. - -module ABounder(S:ASampler) = { - proc s(): T = { - var r <- witness; - - if (Bounder.c < q) { - r <@ S.s(); - Bounder.c <- Bounder.c + 1; - } - return r; - } -}. - -module Bounded(A:Adv,S:ASampler) = { - proc a(): unit = { - Bounder.c <- 0; - A(ABounder(S)).a(); - } -}. - -equiv PushBound (S <: Sampler {-Bounder}) (A <: Adv {-S,-Bounder}): - Exp(Bounder(S),A).main ~ Exp(S,Bounded(A)).main: - ={glob A,glob S} ==> - ={glob A,glob S}. -proof. by proc; inline*; sim. qed. - -(** Forall adversary A with access to the bounded s oracle, the - probability that the same output is sampled twice is bounded by - q^2/|T| **) -section. - declare module A <: Adv {-Sample,-Bounder}. - - declare axiom A_ll (S <: ASampler {-A}): islossless S.s => islossless A(S).a. - - lemma pr_collision_bounded_oracles &m: - Pr[Exp(Bounder(Sample),A).main() @ &m: !uniq Sample.l] - <= (q^2)%r * mu1 uT maxu. - proof. - have ->: Pr[Exp(Bounder(Sample),A).main() @ &m: !uniq Sample.l] = - Pr[Exp(Sample,Bounded(A)).main() @ &m: !uniq Sample.l]. - + byequiv (PushBound Sample A) => //. - apply (pr_collision_q2 (Bounded(A)) _ _ &m). - + move=> S HS;proc;call (A_ll (ABounder(S)) _);2:by auto. - by proc;sp;if;auto;call HS. - proc; call (_: size Sample.l <= Bounder.c <= q). - + proc;sp;if=>//;inline *;auto=> /#. - auto; smt(ge0_q). - qed. - -end section. - diff --git a/theories/crypto/PRF.eca b/theories/crypto/PRF.eca index 8725b35214..8ad91dc239 100644 --- a/theories/crypto/PRF.eca +++ b/theories/crypto/PRF.eca @@ -1,24 +1,78 @@ +(*^ + +# Pseudo-Random Functions: Syntax and Security + +Given a domain type `D` and a codomain type `R`, this abstract theory +defines: +- the syntax of oracles ([`module type PRF`](#PRF), [`module type + PRF_Oracles`](#PRF_Oracles)) and distinguishers ([`module type + Distinguisher`](#Distinguisher)) for PRFs, as well as + a general indistinguishability experiment ([`module IND`](#IND)); +- lazily-sampled random functions from `D` to `R`, given a family `dR` + of lossless distributions over `R`, indexed by `D`; ([`abstract + theory RF`](#RF) and +- given an additional type `K` of keys, the syntax of PRFs from `D` to + `R` indexed by `K`, and the standard way to wrap them as oracles to + be distinguished from the random function. ([`abstract theory PseudoRF`](#PseudoRF) + +We do not assume that the PRF `keygen` can be reduced to sampling in +`K`. We do not assume that the PRF itself can be computed by a +deterministic function. Proofs that require such assumptions should +make them explicit locally, and can then reason about a concrete +instance of the pseudorandom function. +^*) + require import AllCore Distr FSet. pragma +implicits. -(** A PRF is a family of functions F from domain D to finite range R - indexed by a keyspace K equipped with a (lossless) distribution dK. *) +(*^ + +## Parameters and syntax + +This abstract theory *must* be instantiated with a domain type `D` and +a codomain type `R`, and defines oracle and adversary syntax, as well +as a somewhat generic indsitinguishability experiment. + +^*) + +(*& +Parameters: Types `D` and `R` for the domain and codomain, +respectively. They are not constrained any further at the top-level. +&*) type D, R. +(*& +In order to make the experiment generic, we consider it as +parameterized by an oracle with an initialization procedure. +&*) module type PRF = { proc init(): unit proc f(_ : D): R }. +(*& +Only the PRF oracle itself is presented to the adversary. This module +type captures this. +&*) module type PRF_Oracles = { proc f(_: D): R }. +(*& +A distinguisher, given an oracle `f(_: D): R`, is an algorithm taking +no further input and outputting a boolean. +&*) module type Distinguisher (F : PRF_Oracles) = { proc distinguish(): bool }. +(*& +Our indistinguishability experiment pits a distinguisher `D` against a +PRF oracle with initialization `F`. It simply calls `F`'s +initialization, then runs `D` with access to the PRF oracle and +outputs its result. +&*) module IND (F : PRF) (D : Distinguisher) = { proc main(): bool = { var b; @@ -29,10 +83,51 @@ module IND (F : PRF) (D : Distinguisher) = { } }. -(* -------------------------------------------------------------------- *) +(*& +We also define a counting wrapper once and for all. +&*) +module Count (F : PRF) : PRF = { + var c : int + + proc init() = { + F.init(); + c <- 0; + } + + proc f(x) = { + var r; + + r <@ F.f(x); + c <- c + 1; + return r; + } +}. + +(*^ +## Lazily-Sampled Random Function + +This abstract sub-theory defines the "random function" instantiation +of the PRF oracles with initialization, which is often used as an +"ideal" functionality. + +In typical settings, outputs are lazily sampled uniformly at random +from the codomain. However, it is useful to generalize to any family +of lossless distributions that can be parameterized by the oracle's +input. In particular, this allows us to use this type to capture any +operation whose semantics is purely probabilistic in our model. +^*) abstract theory RF. require import FMap. +(*^ +Parameter: a family `dR` of lossless distributions over `R`, indexed +by `D`. +^*) +(*^ A typical instantiation will consider the uniform distribution +`uD` over `D`, and instantiate `dR` as `fun _=> uD` - making the +distribution each output is sampled from independent of the input that +was queried. +^*) op dR: { D -> R distr | forall x, is_lossless (dR x) } as dR_ll. module RF = { @@ -53,34 +148,55 @@ module RF = { }. end RF. -(* -------------------------------------------------------------------- *) +(*^ +## Pseudorandom Function + +This abstract sub-theory defines an abstract "pseudorandom function" +instantiation of the PRF oracles with initialization. +^*) abstract theory PseudoRF. + +(*^ +Parameter: A type `K` of keys. +^*) type K. -op dK: { K distr | is_lossless dK } as dK_ll. +(*^ +The syntax of pseudorandom functions: +- a `keygen` algorithm that outputs a key; and +- an `f` algorithm that, on input a key and an element from the + domain, output an element from the codomain. -op F : K -> D -> R. +We *do not* assume that `keygen` is simply sampling from a distribution. +We *do not* assume that `f` is a mathematical function. +In practice, this means that this *could be* instantiated using +complex stateful constructions. +^*) module type PseudoRF = { proc keygen(): K - proc f(_ : K * D): R + proc f(_: K * D): R }. -module PseudoRF = { - proc keygen() = { - var k; +(*^ +A wrapper, which wraps any given concrete PRF as a PRF oracle with +initialization, as expected by the indistinguishability experiment. - k <$ dK; - return k; - } +Initialization generates a key, which is then used with the `f` +algorithm to answer PRF oracle queries. +^*) +module PRF (P : PseudoRF) = { + var k : K - proc f(k, x) = { return F k x; } -}. + proc init() = { + k <@ P.keygen(); + } -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.eca b/theories/crypto/PRP.eca index 9c3355ef2e..86a36934b8 100644 --- a/theories/crypto/PRP.eca +++ b/theories/crypto/PRP.eca @@ -1,28 +1,89 @@ +(*^ + +# Pseudo-Random Permutations: Syntax and Security + +Given a domain type `D`, this abstract theory defines: +- the syntax of oracles and distinguishers for weak + ([`abstract theory WeakPRP`](#WeakPRP)) and strong PRPs + ([`abstract theory PRP`](#PRP)), as well as indistinguishability + experiments for each; +- a lazily-sampled random permutation on `D`, given a lossless + distribution `dD` over `D`; ([`abstract theory RP`](#RP) and +- given an additional type `K` of keys, the syntax of PRPs over `D` + indexed by `K`, and the standard way to wrap them as oracles to be + distinguished from the truly random permutation. ([`abstract theory + PseudoRP`](#PseudoRP) + +We do not assume that the PRP's `keygen` can be reduced to sampling in +`K`. We do not assume that the PRP itself can be computed by a +deterministic function or that the forward and inverse directions +share state in any particular way. Proofs that require such +assumptions should make them explicit locally, and can then reason +about a concrete instance of the pseudorandom permutation. +^*) + 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. **) +(*^ + +## Parameters and syntax + +This abstract theory *must* be instantiated with a domain type `D`, +and defines oracle and adversary syntax, as well as indistinguishability +experiments for both weak and strong PRPs. + +^*) + +(*& +Parameter: Type `D` for the domain. +&*) type D. -(** Security notions **) +(*^ + +## Weak PRP Security Notion + +A weak PRP only gives the adversary access to the forward direction +of the permutation. This section defines the relevant module types +and indistinguishability experiment. +^*) (* -------------------------------------------------------------------- *) abstract theory WeakPRP. -module type PRP = { + +(*& +The PRP oracle, parameterized by an initialization procedure and +a forward evaluation procedure `f`. +&*) +module type WeakPRP = { proc init(): unit proc f(_ : D): D }. -module type PRP_Oracles = { +(*& +Only the PRP oracle itself is presented to the adversary. This +module type captures this. +&*) +module type WeakPRP_Oracles = { proc f(_ : D): D }. -module type Distinguisher (P : PRP_Oracles) = { +(*& +A distinguisher, given an oracle `f(_: D): D`, is an algorithm +taking no further input and outputting a boolean. +&*) +module type Distinguisher (P : WeakPRP_Oracles) = { proc distinguish(): bool }. -module IND (P : PRP) (D:Distinguisher) = { +(*& +Our indistinguishability experiment pits a distinguisher `D` against +a PRP oracle with initialization `P`. It simply calls `P`'s +initialization, then runs `D` with access to the weak PRP oracle and +outputs its result. +&*) +module IND (P : WeakPRP) (D:Distinguisher) = { proc main(): bool = { var b; @@ -31,25 +92,72 @@ module IND (P : PRP) (D:Distinguisher) = { return b; } }. + +(*& +We also define a single wrapper for query counting. +&*) +module Count (P : WeakPRP) : WeakPRP = { + var c : int + + proc init() = { + P.init(); + c <- 0; + } + + proc f(x) = { + var r; + + r <@ P.f(x); + c <- c + 1; + return r; + } +}. end WeakPRP. +(*^ + +## PRP Security Notion + +A (strong) PRP additionally gives the adversary access to the inverse +direction of the permutation. This section defines the relevant +module types and indistinguishability experiment. +^*) (* -------------------------------------------------------------------- *) -abstract theory StrongPRP. +abstract theory PRP. + +(*& +The strong PRP oracle, parameterized by an initialization procedure, +a forward evaluation procedure `f`, and an inverse evaluation +procedure `fi`. +&*) module type PRP = { proc init(): unit proc f(_ : D): D proc fi(_ : D): D }. -module type SPRP_Oracles = { +(*& +The strong PRP oracles presented to the adversary, providing both +the forward and inverse directions of the permutation. +&*) +module type PRP_Oracles = { proc f(_ : D): D proc fi(_ : D): D }. -module type Distinguisher (P : SPRP_Oracles) = { +(*& +A distinguisher, given both `f` and `fi` oracles, is an algorithm +taking no further input and outputting a boolean. +&*) +module type Distinguisher (P : PRP_Oracles) = { proc distinguish(): bool }. +(*& +Indistinguishability experiment for strong PRPs. Initializes the +permutation, then runs the distinguisher with access to both the +forward and inverse oracles. +&*) module IND (P : PRP) (D:Distinguisher) = { proc main(): bool = { var b; @@ -59,17 +167,74 @@ module IND (P : PRP) (D:Distinguisher) = { return b; } }. -end StrongPRP. -(** Ideal and Real functionalities **) +(*& +We also define a single wrapper for query counting. +&*) +module Count (P : PRP) : PRP = { + var c : int + var ci : int + + proc init() = { + P.init(); + c <- 0; + ci <- 0; + } + + proc f(x) = { + var r; + + r <@ P.f(x); + c <- c + 1; + return r; + } + + proc fi(y) = { + var r; + + r <@ P.fi(y); + ci <- ci + 1; + return r; + } +}. +end PRP. + +(*^ + +## Lazily-Sampled Random Permutation + +This abstract sub-theory defines the "random permutation" instantiation +of the PRP oracles with initialization, which is used as the "ideal" +functionality in PRP security proofs. + +A random permutation on `D` is lazily sampled: the first time an input +`x` is queried in the forward direction, a fresh *new* output `y` is +sampled, and the pair `(x, y)` is recorded in both the forward map `m` +and the inverse map `mi`. The inverse direction is handled +symmetrically. +^*) (* -------------------------------------------------------------------- *) abstract theory RP. require import FMap FSet. require import Dexcepted. (*---*) import StdOrder.RealOrder RField. +(*& +Parameter: a lossless distribution `dD` over `D`, from which fresh +outputs are sampled when extending the permutation. +&*) op dD: { D distr | is_lossless dD } as dD_ll. +(*& +The ideal random permutation module. Maintains two maps: +- `m` : forward map, from inputs to outputs; +- `mi` : inverse map, from outputs to inputs. + +Fresh outputs are sampled from `dD` excluding the current range of +the forward map; fresh inputs are sampled from `dD` excluding the +current range of the inverse map, ensuring the permutation property +is preserved. +&*) module RP = { var m : (D,D) fmap var mi: (D,D) fmap @@ -102,41 +267,54 @@ module RP = { } }. -(* -------------------------------------------------------------------- *) +(*^ +## Useful properties of lazily sampled random permutations +^*) + +(*& +Predicate characterizing when `m` and `mi` form a valid permutation +pair: looking up the image of `x` in `m` and then inverting it via +`mi` returns `x`, and conversely for `y` in `mi`. +&*) 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}. +hoare RP_f_is_perm: RP.f: + is_permutation RP.m RP.mi ==> is_permutation RP.m RP.mi. proof. -proc; if=> //=; auto=> |> &2 is_perm x_notin_m yL. -rewrite supp_dexcepted rngE /= negb_exists=>- [] _ /= m__neq_yL. +proc; if; auto=> |> &0 is_perm x_notin_m y /supp_dexcepted [] y_in_D. +rewrite rngE=> /= /negb_exists mX_neq_y. 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). ++ by case: (x' = x{0})=> /#. +by case: (y' = y)=> /#. +qed. + +hoare RP_fi_is_perm: RP.fi: + is_permutation RP.m RP.mi ==> is_permutation RP.m RP.mi. +proof. +proc; if; auto=> |> &0 is_perm y_notin_mi x /supp_dexcepted [] x_in_D. +rewrite rngE=> /= /negb_exists miX_neq_x. +split=> [x'|y']; rewrite !get_setE !mem_set. ++ by case: (x' = x)=> /#. +by case: (y' = y{0})=> /#. qed. (* -------------------------------------------------------------------- *) +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. +conseq (: ={glob RP, x} ==> ={glob RP, res}) RP_f_is_perm. +by sim. +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}. + ={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 ->. +conseq (: ={glob RP, y} ==> ={glob RP, res}) RP_fi_is_perm. +by sim. qed. (* -------------------------------------------------------------------- *) @@ -191,6 +369,9 @@ have ->: card (fset1 x `&` frng m) = if x \in (frng m) then 1 else 0. by move: x_notin_m; rewrite -mem_fdom; smt (leq_card_rng_dom @FSet). qed. +(*& +Losslessness lemma for `RP.f`: when `dD` is full, `RP.f` is lossless. +&*) lemma f_ll: is_full dD => islossless RP.f. proof. move=> dD_fu. @@ -209,6 +390,9 @@ by apply/mu_sub=> x ->. qed. (* -------------------------------------------------------------------- *) +(*& +Losslessness lemma for `RP.fi`: when `dD` is full, `RP.fi` is lossless. +&*) lemma fi_ll: is_full dD => islossless RP.fi. proof. move=> dD_fu. @@ -225,505 +409,57 @@ apply/(ltr_le_trans (mu dD (pred1 y0))). + by apply: dD_fu. by apply/mu_sub=> y ->. qed. +end RP. -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. +## Pseudorandom Permutation -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. +This abstract sub-theory defines an abstract "pseudorandom permutation" +instantiation of the PRP oracles with initialization. +^*) +(* -------------------------------------------------------------------- *) +abstract theory PseudoRP. -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 !get_setE=> -[z_in_m] [z'_in_m] mz_eq_mz'. - case (rng m y)=> //= y_notin_rngm. - by exists z z'; smt(). -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'; rewrite !get_setE !mem_set /#. -qed. +(*^ +Parameter: A type `K` of keys. +^*) +type K. -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 +(*& +The module type for pseudorandom permutations: key generation, +forward evaluation, and inverse evaluation. +&*) +module type PseudoRP = { + proc keygen(): K + proc p(_ : K * D): D + proc pi(_ : K * D): D }. -module Direct = { - proc sample(X:D -> bool): D = { - var r; +(*& +A wrapper, which wraps any given concrete PRP as a PRP oracle with +initialization, as expected by the indistinguishability experiment. - r <$ dD \ X; - return r; - } -}. +Initialization generates a key, which is then used with the `p` and +`pi` operations to answer forward and inverse oracle queries. +&*) +module PRP (P : PseudoRP) = { + var k : K + + proc init() = { k <@ P.keygen(); } -module Indirect = { - proc sample(X:D -> bool): D = { + proc f(x : D) = { var r; - r <$ dD; - if (X r) { - r <$ dD \ X; - } + r <@ P.p(k, x); return r; } -}. - -module PRPi'(S:Sample_t) = { - proc init = RP.init - proc f(x:D): D = { + proc fi(y : D) = { var r; - if (x \notin RP.m) { - r <@ S.sample(rng RP.m); - RP.m.[x] <- r; - } - return oget RP.m.[x]; - } -}. - -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. - -(* 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'. - by exists x{2} x'; rewrite !mem_set !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(dD_ll excepted_lossless). - by auto=> /> /#. - 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)=> //=. - proc; if; auto=> />; rewrite dD_ll //=. - move=> &0 x x' x'_neq_x x_in_m x'_in_m x_coll_x' x0_notin_m v _. - by exists x x'=> />; rewrite !mem_set x_in_m x'_in_m /= !get_set_neqE 1,2:/#. - 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. - 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'_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 - proof *. - realize ge0_q by apply ge0_q. - - (* 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, rng 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. - split; 1:smt(). - split. - + move=> v; rewrite -h2 !rngE /=; split. - + move=> [] x0; rewrite get_setE; case: (x0 = x{2})=> /> _ m_x0. - by right; exists x0. - + case=> />. - + by exists x{2}; rewrite get_set_sameE. - + move=> x0 m_x0; exists x0; rewrite get_set_neqE //. - rewrite domE in h4; rewrite -negP=> <<-. - by move: h4; rewrite m_x0. - + smt(collision_add). - by 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. - have ->: mu1 dD witness = mu1 dD maxu by apply /rnd_funi /dD_funi. - 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; + r <@ P.pi(k, y); + return r; } - - 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. diff --git a/theories/crypto/prp_prf/RP_RF.eca b/theories/crypto/prp_prf/RP_RF.eca new file mode 100644 index 0000000000..d7f72650b0 --- /dev/null +++ b/theories/crypto/prp_prf/RP_RF.eca @@ -0,0 +1,418 @@ +require import AllCore Distr List FSet FMap. +require import Dexcepted. +require (*--*) PRP. +(*---*) import RField StdOrder.RealOrder. + +require (*--*) FelTactic Mu_mem. + +(** We assume a finite domain D, equipped with a full and lossless + distribution. **) +type D. +op [lossless full] dD: D distr. + +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. + +clone import PRP as PRPt with + type D <- D +proof *. + +clone import PRP as PRPSec +proof *. + +clone import RP as PRPi with + 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 m, mi: (D, D) fmap + + proc init(): unit = { + m <- empty; + mi <- empty; + } + + proc f(x: D) = { + var y; + + if (x \notin m) { + y <$ dD; + m.[x] <- y; + mi.[y] <- x; + } + return oget m.[x]; + } + + proc fi(y: D) = { + var x; + + if (y \notin mi) { + x <$ dD; + m.[x] <- y; + mi.[y] <- x; + } + return oget mi.[y]; + } +}. + +section. + +declare module D <: Distinguisher { -PRPi, -ARP, -Count }. +declare axiom D_ll (O <: PRP_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 c: + hoare [D(Count(ARP)).distinguish: Count.c + Count.ci = c ==> Count.c + Count.ci <= 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 +}. + +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; 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; + PRPi.mi.[oget PRPi.m.[x]] <- x; + } + return oget PRPi.m.[x]; + } + + proc fi(x:D): D = { + var r; + + if (x \notin PRPi.mi) { + r <@ S.sample(rng PRPi.mi); + PRPi.mi.[x] <- r; + PRPi.m.[oget PRPi.mi.[x]] <- x; + } + return oget PRPi.mi.[x]; + } +}. + +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]; + } +}. + +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. + +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. + +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. +move=> z; rewrite /predU /pred1 /= (rngE m.[_ <- _])=> /= - [] x0. +rewrite get_setE; case: (x0 = x)=> |> _ m_x0; left; rewrite rngE /=. +by exists x0. +qed. + +local lemma frng_set_subset_rngU1 (m : ('a, 'b) fmap) (x : 'a) y: + frng m.[x <- y] \subset frng m `|` fset1 y. +proof. +by move=> z; rewrite in_fsetU1 !mem_frng=> /rng_set_subset_rngU1. +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 (: ={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. + +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. + +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. + +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. + +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. + +import StdBigop.Bigreal BRA. + +local equiv Count_ARP: + IND(Count(ARP_bad), D).main ~ IND(Count(ARP), D).main: + ={glob D, glob ARP, glob Count} ==> ={glob Count}. +proof. +proc; call (: ={glob Count, glob ARP}). ++ by proc; inline *; sp; if; auto. ++ by proc; inline *; sp; if; auto. +by inline *; auto. +qed. + +local hoare Count_ARP_bad: + IND(Count(ARP), D).main: true ==> Count.c + Count.ci <= q. +proof. by proc; call (D_count 0); inline *; auto. qed. + +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. +have ->: Pr[IND(ARP_bad, D).main() @ &m: ARP_bad.bad] + = Pr[IND(Count(ARP_bad), D).main() @ &m: ARP_bad.bad /\ Count.c + Count.ci <= q]. ++ byequiv (: ={glob D} ==> ={ARP_bad.bad} /\ (Count.c + Count.ci){2} <= q)=> //. + conseq (: _ ==> ={ARP_bad.bad}) _ (: _ ==> Count.c + Count.ci <= q)=> //. + + by conseq Count_ARP Count_ARP_bad=> [/#|]. + 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.c + Count.ci) (fun i=> i%r * hmin_dD) q + ARP_bad.bad + [] (card (frng ARP.m) <= Count.c + Count.ci /\ card (frng ARP.mi) <= Count.c + Count.ci)=> //. ++ by rewrite -mulr_suml sumidE 1:ge0_q mulrDr expr2 mulrN1. ++ by inline *; auto=> |>; rewrite frng0 fcards0. ++ exlim (Count.c + Count.ci)=> 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.c + Count.ci)=> 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 y{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. + +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. +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. diff --git a/theories/crypto/prp_prf/Strong_RP_RF.eca b/theories/crypto/prp_prf/Strong_RP_RF.eca deleted file mode 100644 index 435ecbadcf..0000000000 --- a/theories/crypto/prp_prf/Strong_RP_RF.eca +++ /dev/null @@ -1,576 +0,0 @@ -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 its uniform - distribution. **) -type D. -op uD: { D distr | is_uniform uD /\ is_lossless uD /\ is_full uD } as uD_uf_fu. - -(** and a type K equipped with a lossless distribution **) -type K. -op dK: { K distr | is_lossless dK } as dK_ll. - -clone import PRP as PRPt with - type D <- D. - -clone import StrongPRP as PRPSec. - -clone import RP as PRPi with - op dD <- uD -proof * by smt(uD_uf_fu) -rename "RP" as "PRPi". - -(* 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 - - proc init(): unit = { - m <- empty; - mi <- empty; - coll <- false; - } - - proc f(x : D) = { - var y; - - if (x \notin m) { - y <$ uD; - coll <- coll \/ rng m y; - m.[x] <- y; - mi.[y] <- x; - } - return oget m.[x]; - } - - proc fi(y : D) = { - var x; - - if (y \notin mi) { - x <$ uD; - coll <- coll \/ rng mi x; - m.[x] <- y; - mi.[y] <- x; - } - return oget mi.[y]; - } -}. - -op q : { int | 0 <= q } as ge0_q. - -(** 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 <$ uD \ X; - return r; - } -}. - -module Indirect = { - proc sample(X:D -> bool): D = { - var r; - - r <$ uD; - if (X r) { - r <$ uD \ X; - } - return r; - } -}. - -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; - PRPi.mi.[oget PRPi.m.[x]] <- x; - } - return oget PRPi.m.[x]; - } - - proc fi(x:D): D = { - var r; - if (x \notin PRPi.mi) { - r <@ S.sample(rng PRPi.mi); - PRPi.mi.[x] <- r; - PRPi.m.[oget PRPi.mi.[x]] <- x; - } - return oget PRPi.mi.[x]; - } -}. - -(* Some losslessness lemmas *) -(* FIXME: cleanup *) - -(* 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. -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. - -lemma excepted_lossless (m:(D,D) fmap): - (exists x, x \notin m) => - mu (uD \ (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. -qed. - -phoare Indirect_ll: [Indirect.sample: exists x, support uD x /\ !X x ==> true] = 1%r. -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 ->. -qed. - -lemma PRPi'_Indirect_f_ll: islossless PRPi'(Indirect).f. -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). -qed. - -lemma PRPi'_Indirect_fi_ll: islossless PRPi'(Indirect).fi. -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). -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; - - if (c < q) { - if (card (frng ARP.m) < q) { - r <@ ARP.f(x); - } - c <- c + 1; - } - return r; - } - - proc fi(x:D): D = { - var r <- witness; - - if (c < q) { - if (card (frng ARP.mi) < q) { - r <@ ARP.fi(x); - } - c <- c + 1; - } - return r; - } - } - - proc main(): bool = { - var b : bool; - - 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). -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. -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). -proof. -move=> D_ll. -by rewrite (pr_PRPi_PRPi'_Indirect (DBounder(D)) &m) (PartialConclusion D &m D_ll). -qed. diff --git a/theories/crypto/prp_prf/Weak_RP_RF.eca b/theories/crypto/prp_prf/Weak_RP_RF.eca new file mode 100644 index 0000000000..b87beedad8 --- /dev/null +++ b/theories/crypto/prp_prf/Weak_RP_RF.eca @@ -0,0 +1,297 @@ +require import AllCore Distr List FSet FMap. +require import Dexcepted. +require (*--*) PRF PRP. +(*---*) import RField StdOrder.RealOrder. + +require (*--*) FelTactic Mu_mem. + +(** 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 WeakPRP 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. + +section. + +(** The following is a proof that holds **) +(** For all lossless distinguisher D ... **) +declare module D <: PRFt.Distinguisher { -PRPi, -PRFi, -PRFt.Count, -PRPSec.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 c0: + hoare [D(Count(PRFi)).distinguish: Count.c = c0 ==> Count.c <= 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.c <= q]. ++ byequiv (: ={glob D} ==> ={PRFi'_bad.bad} /\ Count.c{2} <= q)=> //. + conseq (: _ ==> ={PRFi'_bad.bad}) _ (: _ ==> Count.c <= q)=> //. + + proc *. + proc change 1: { r <@ IND(Count(PRFi), D).main(); }. + + call (: ={glob D, Count.c} ==> ={Count.c})=> //. + proc; call (: ={Count.c} /\ PRPi.m{1} = PRFi.m{2}). + + by proc; inline *; sp; if; auto. + by inline *; auto. + call (: true ==> Count.c <= q)=> //. + by proc; call (D_count 0); inline *; auto. + proc; call (: ={PRPi.m, PRFi'_bad.bad})=> //. + + by proc; inline *; sp; if; auto. + by inline *; auto. +fel 1 (Count.c) (fun i=> i%r * hmin_dD) q + PRFi'_bad.bad + [] (card (frng PRPi.m) <= Count.c)=> //. ++ by rewrite -mulr_suml sumidE 1:ge0_q mulrDr expr2 mulrN1. ++ by inline *; auto=> |>; rewrite frng0 fcards0. ++ exlim Count.c=> 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.