proposition: Theorem security_based_on_prp LA A: ValidPackage LA [interface #val #[ctxt]: 'word → 'ciph ; #val #[decrypt]: 'ciph → 'word ] A_export A -> fdisjoint LA ( EVAL_locs_tt :|: EVAL_locs_ff :|: CTXT_locs :|: CTXT_EVAL_locs :|: CTXT_EVAL_SAMP_locs :|: CTXT_HYB_locs_1 :|: CTXT_HYB_locs_2 ) -> Advantage CTXT A <= prp_epsilon (A ∘ CTXT_EVAL_pkg_tt) + statistical_gap A + prp_epsilon (A ∘ CTXT_EVAL_pkg_ff).
proof: Proof. move=> vA H. rewrite Advantage_E Advantage_sym. ssprove triangle (CTXT true) [:: CTXT_EVAL_pkg_tt ∘ EVAL true ; CTXT_EVAL_pkg_tt ∘ EVAL false ; CTXT_EVAL_SAMP_pkg ∘ EVAL_SAMP false ; CTXT_EVAL_SAMP_pkg ∘ EVAL_SAMP true ; CTXT_HYB_pkg_1 ∘ SAMP Key_N false ; CTXT_HYB_pkg_1 ∘ SAMP Key_N true ; pack CTXT_HYB_pkg_2 ; pack CTXT_HYB_pkg_3 ; pack CTXT_HYB_pkg_4 ; pack CTXT_HYB_pkg_5 ; CTXT_EVAL_pkg_ff ∘ EVAL_SAMP_pkg ∘ SAMP Ciph_N true ; CTXT_EVAL_pkg_ff ∘ EVAL_SAMP_pkg ∘ SAMP Ciph_N false ; CTXT_EVAL_pkg_ff ∘ EVAL false ; CTXT_EVAL_pkg_ff ∘ EVAL true ] (CTXT false) A as ineq. apply: le_trans. 1: by apply: ineq. rewrite !fdisjointUr in H. move: H => /andP [/andP [/andP [/andP [/andP [/andP [H1 H2] H3] H4] H5] H6] H7]. move: {ineq H1 H2 H3 H4 H5 H6 H7} (H1, H2, H3, H4, H5, H6, H7, fdisjoints0) => H. rewrite CTXT_equiv_true ?fdisjointUr ?H // GRing.add0r. rewrite CTXT_EVAL_equiv_true ?fdisjointUr ?H // GRing.addr0. rewrite CTXT_HYB_equiv_1 ?fdisjointUr ?H // GRing.addr0. rewrite CTXT_HYB_equiv_2 ?fdisjointUr ?H // GRing.addr0. rewrite CTXT_HYB_equiv_3 ?fdisjointUr ?H // GRing.addr0. rewrite CTXT_HYB_equiv_4 ?fdisjointUr ?H // GRing.addr0. rewrite CTXT_HYB_equiv_5 ?fdisjointUr ?H // GRing.addr0. rewrite CTXT_HYB_equiv_6 ?fdisjointUr ?H // GRing.addr0. rewrite CTXT_EVAL_equiv_false ?fdisjointUr ?H // GRing.addr0. rewrite CTXT_equiv_false ?fdisjointUr ?H // GRing.addr0. rewrite /prp_epsilon /statistical_gap !Advantage_E !GRing.addrA. rewrite -!Advantage_link !link_assoc. by rewrite (Advantage_sym (EVAL true)) (Advantage_sym (SAMP Ciph_N true)). Qed.
imports: Relational(OrderEnrichedCategory GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr realsum ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq) Mon(SPropBase) Crypt(Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb pkg_core_definition choice_type pkg_composition pkg_rhl Package Prelude) extructures(ord fset fmap) Equations(Equations)