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.