proposition: Theorem security_based_on_prf : ∀ LA A, ValidPackage LA [interface #val #[i1] : 'word → 'word × 'word ] A_export A → fdisjoint LA (IND_CPA false).(locs) → fdisjoint LA (IND_CPA true).(locs) → Advantage IND_CPA A <= prf_epsilon (A ∘ MOD_CPA_ff_pkg) + statistical_gap A + prf_epsilon (A ∘ MOD_CPA_tt_pkg).
proof: Proof. intros LA A vA hd₀ hd₁. unfold prf_epsilon, statistical_gap. rewrite !Advantage_E. ssprove triangle (IND_CPA false) [:: MOD_CPA_ff_pkg ∘ EVAL true ; MOD_CPA_ff_pkg ∘ EVAL false ; MOD_CPA_tt_pkg ∘ EVAL false ; MOD_CPA_tt_pkg ∘ EVAL true ] (IND_CPA true) A as ineq. eapply le_trans. 1: exact ineq. clear ineq. erewrite IND_CPA_equiv_false. all: eauto. 2:{ simpl. unfold MOD_CPA_location. rewrite fset0U. auto. } erewrite IND_CPA_equiv_true. all: eauto. 2:{ simpl. unfold MOD_CPA_location. rewrite fset0U. auto. } rewrite GRing.add0r GRing.addr0. rewrite !Advantage_link. rewrite Advantage_sym. auto. 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) Coq(Utf8) extructures(ord fset fmap) Equations(Equations)