proposition: Lemma forward_secrecy_based_on_prg LA A: ValidPackage LA [interface #val #[attack]: 'seq 'word → ('seq 'word) × 'word ] A_export A -> Advantage ATTACK A <= prg_epsilon (A ∘ ATTACK_GEN_pkg) + cpa_epsilon (A ∘ ATTACK_CTXT_pkg).
proof: Proof. move=> vA. rewrite Advantage_E Advantage_sym. ssprove triangle (ATTACK true) [:: ATTACK_GEN_pkg ∘ GEN_STRETCH true ; ATTACK_GEN_pkg ∘ GEN_STRETCH false ; pack ATTACK_HYB_pkg ; ATTACK_CTXT_pkg ∘ CTXT true ; ATTACK_CTXT_pkg ∘ CTXT false ] (ATTACK false) A as ineq. apply: le_trans. 1: by apply: ineq. rewrite ATTACK_equiv_true ?fdisjointUr ?fdisjoints0 // GRing.add0r. rewrite ATTACK_HYB_equiv_1 ?fdisjointUr ?fdisjoints0 // GRing.addr0. rewrite ATTACK_HYB_equiv_2 ?fdisjointUr ?fdisjoints0 // GRing.addr0. rewrite ATTACK_equiv_false ?fdisjointUr ?fdisjoints0 // GRing.addr0. rewrite /prg_epsilon /cpa_epsilon !Advantage_E -!Advantage_link. by rewrite (Advantage_sym (GEN_STRETCH true)) (Advantage_sym (CTXT 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)