proposition: Theorem PKE_security : ∀ LA A, ValidPackage LA PKE_CCA_out A_export A → fdisjoint LA PKE_CCA_loc → fdisjoint LA Aux_loc → Advantage (PKE_CCA KEM_DEM) A <= Advantage KEM_CCA (A ∘ (MOD_CCA KEM_DEM) ∘ par (ID KEM_out) (DEM true)) + Advantage DEM_CCA (A ∘ (MOD_CCA KEM_DEM) ∘ par (KEM false) (ID DEM_out)) + Advantage KEM_CCA (A ∘ (MOD_CCA KEM_DEM) ∘ par (ID KEM_out) (DEM false)).
proof: Proof. intros LA A hA hA' hd. rewrite Advantage_E. ssprove triangle (PKE_CCA KEM_DEM false) [:: (MOD_CCA KEM_DEM) ∘ par (KEM true) (DEM false) ∘ KEY ; (MOD_CCA KEM_DEM) ∘ par (KEM true) (DEM true) ∘ KEY ] (PKE_CCA KEM_DEM true) A as ineq. eapply le_trans. 1: exact ineq. clear ineq. rewrite PKE_CCA_perf. 2,3: auto. rewrite PKE_CCA_perf_true. 2,3: auto. rewrite GRing.addr0. rewrite GRing.add0r. eapply le_trans. - rewrite Advantage_sym. rewrite -Advantage_link. eapply single_key_b with (CK₁ := (KEM false).(pack)). 7,8,11,12: ssprove_valid. 1-2: ssprove_valid. 5-8: unfold KEM, DEM. 5-8: cbn - [mkdef mkfmap]. 5-8: ssprove_valid. all: unfold Parable. all: rewrite domm_ID_fset. 3,4: rewrite fdisjointC. all: eapply fdisjoint_trans ; [ eapply domm_trimmed ; unfold KEM, DEM ; cbn - [mkdef mkfmap] ; ssprove_valid |]. all: simpl. all: unfold idents, KEM_out, DEM_out. all: rewrite imfset_fset. all: simpl. all: rewrite fdisjointC. all: fdisjoint_auto. - rewrite !Advantage_E. unfold KEM_CCA. unfold KEM_CCA_pkg. unfold DEM_CCA. unfold DEM_CCA_pkg. change ({locpackage ?p }.(pack)) with p. change ({package ?p }.(pack)) with p. apply eq_ler. rewrite !link_assoc. f_equal. all: rewrite Advantage_sym. 2: reflexivity. f_equal. rewrite Advantage_sym. f_equal. all: f_equal. all: apply par_commut. all: unfold Parable. all: rewrite domm_ID_fset. all: rewrite fdisjointC. all: eapply fdisjoint_trans ; [ eapply domm_trimmed ; unfold KEM, DEM ; cbn - [mkdef mkfmap] ; ssprove_valid |]. all: simpl. all: unfold idents, DEM_out. all: rewrite imfset_fset. all: simpl. all: rewrite fdisjointC. all: fdisjoint_auto. Qed.
imports: Relational(OrderEnrichedCategory GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr fingroup.fingroup realsum ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq) Crypt(Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb UniformStateProb Package Prelude pkg_composition) Coq(Utf8 Lia) extructures(ord fset fmap) Equations(Equations)