clutch.clutch.examples.DH_assumptions
From clutch Require Import clutch.
From clutch.prob_lang Require Import advantage.
From clutch.prob_lang.typing Require Import tychk.
From clutch.clutch.examples.crypto Require Import valgroup advantage_laws.
From clutch.clutch.examples.crypto Require ElGamal_bijection.
From mathcomp Require ssrnat.
#[warning="-notation-incompatible-prefix"]
From mathcomp Require Import zmodp finset ssrbool fingroup.fingroup solvable.cyclic.
Import valgroup_notation.
From clutch.clutch.examples.crypto Require Import ElGamal.
Set Default Proof Using "Type*".
Section DH_assumptions.
Context {vg : val_group}. (* A group on a subset of values. *)
Context {cg : clutch_group_struct}. (* Implementations of the vg group operations *)
Context {vgg : @val_group_generator vg}. (* G is generated by g. *)
Context {cgg : @clutch_group_generator vg cg vgg}. (* g is well-typed *)
#[local] Notation n := (S n'').
#[local] Definition rnd t := (rand(t) #n)%E.
(* decisional DH game *)
Definition DH_decisional_real : expr := DH_real.
Definition DH_decisional_rand : expr := DH_rand.
(* computational DH game *)
Definition DH_computational : expr :=
let: "a" := rnd #() in
let: "b" := rnd #() in
(g^"a", g^"b").
(* Discrete Logarithm game *)
Definition DL : expr :=
let: "a" := rnd #() in g^"a".
(* reduction DL ≥ DH computational*)
Definition eC_toDL : val :=
(λ: "DHcomp",
let, ("A", "B") := "DHcomp" in
"A" ).
Definition C_toDL : list ectx_item := [AppRCtx eC_toDL].
Definition C_toDL_DHcomp : expr := fill C_toDL DH_computational.
Definition τ_comp_to_dl := τG%ty.
(* reduction DH computational ≥ DH_decisional *)
Definition eC_toDHcomp : expr :=
(λ: "DHdec",
let, ("A", "B", "X") := "DHdec" in
("A", "B")).
Definition C_toDHcomp : list ectx_item := [AppRCtx eC_toDHcomp].
Definition C_toDHcomp_DHdecreal : expr := fill C_toDHcomp DH_decisional_real.
Definition C_toDHcomp_DHdecrand : expr := fill C_toDHcomp DH_decisional_rand.
Definition τ_dec_to_comp := (τG * τG)%ty.
Section LogRel.
Context `{!clutchRGS Σ}.
Context {G : clutch_group (vg:=vg) (cg:=cg)}. (* cg satisfies the group laws. *)
Context {Δ : listO (lrelC Σ)}.
Import valgroup_tactics.
Ltac rel_red :=
iStartProof ;
repeat (iredrs ; try first [rel_exp_r | rel_mult_r | rel_inv_r]) ;
repeat (iredls ; try first [rel_exp_l | rel_mult_l | rel_inv_l]).
Definition pkN := nroot.@"pks".
Local Tactic Notation "inv_prove" :=
iSplitL ; [ by (repeat (iExists _) ; (by iFrame) || (iLeft ; by iFrame) || (iRight ; by iFrame)) |].
Local Tactic Notation "inv_mk" constr(Pinv) constr(h) :=
iApply (refines_na_alloc Pinv pkN) ; inv_prove ; iIntros h.
Local Tactic Notation "inv_cl" constr(h) :=
iApply (refines_na_close with h) ; inv_prove.
(* The semantic type of the game. *)
Definition T_comp_to_dl := Eval cbn in (interp τ_comp_to_dl Δ).
Definition T_dec_to_comp := Eval cbn in (interp τ_dec_to_comp Δ).
(* proof of logrel for the reduction reduction DL ≥ DH_computational *)
Lemma DL_C_toDL_DHcomp : ⊢ refines top DL C_toDL_DHcomp T_comp_to_dl.
Proof. iStartProof. rewrite /DL; rewrite /C_toDL_DHcomp.
simpl. unfold eC_toDL. rewrite /DH_computational.
rewrite /rnd.
rel_couple_UU.
rel_pures_l. rel_pures_r.
rel_apply refines_randU_r. iIntros (b).
rel_pures_r. rel_pures. unfold T_comp_to_dl. unfold τ_comp_to_dl.
rel_apply_l refines_exp_l.
rel_apply_r refines_exp_r. rel_apply_r refines_exp_r.
rel_pures_r.
rel_vals.
Qed.
Lemma C_toDL_DHcomp_DL : ⊢ refines top C_toDL_DHcomp DL T_comp_to_dl.
Proof. iStartProof. rewrite /DL. rewrite /C_toDL_DHcomp.
simpl. rewrite /eC_toDL. rewrite /DH_computational.
rewrite /rnd.
rel_couple_UU.
rel_pures_l. rel_pures_r.
rel_apply refines_randU_l. iIntros (b).
rel_pures_l. rel_pures. unfold T_comp_to_dl. unfold τ_comp_to_dl.
rel_apply_l refines_exp_l. rel_apply_l refines_exp_l.
rel_apply_r refines_exp_r. rel_pures.
rel_vals.
Qed.
(* proof of logrel for the reduction DL ≥ DH_computational *)
Lemma DHcomp_C_toDHcomp_DHdecreal :
⊢ refines top DH_computational C_toDHcomp_DHdecreal T_dec_to_comp.
Proof. rewrite /DH_computational. rewrite /C_toDHcomp_DHdecreal.
simpl. rewrite /eC_toDHcomp. rewrite /DH_decisional_real. rewrite /DH_real.
rewrite /rnd. rewrite /ElGamal.rnd.
rel_couple_UU.
rel_pures_l. rel_pures_r.
rel_couple_UU.
rel_pures_l. rel_pures_r.
rewrite -Nat2Z.inj_mul. rel_pures.
rel_pures_l.
rel_apply_l refines_exp_l. rel_apply_l refines_exp_l.
rel_apply_r refines_exp_r. rel_apply_r refines_exp_r. rel_apply_r refines_exp_r. rel_pures.
rel_vals.
Qed.
Lemma C_toDHcomp_DHdecreal_DHcomp :
⊢ refines top C_toDHcomp_DHdecreal DH_computational T_dec_to_comp.
Proof. rewrite /DH_computational. rewrite /C_toDHcomp_DHdecreal.
simpl. rewrite /eC_toDHcomp. rewrite /DH_decisional_real. rewrite /DH_real.
rewrite /rnd. rewrite /ElGamal.rnd.
rel_couple_UU.
rel_pures_l. rel_pures_r.
rel_couple_UU.
rel_pures_l. rel_pures_r. ireds.
rewrite -Nat2Z.inj_mul. rel_pures.
rel_pures_l.
rel_apply_r refines_exp_r. rel_apply_r refines_exp_r.
rel_apply_l refines_exp_l. rel_apply_l refines_exp_l. rel_apply_l refines_exp_l. rel_pures.
rel_vals.
Qed.
Lemma DHcomp_C_toDHcomp_DHdecrand :
⊢ refines top DH_computational C_toDHcomp_DHdecrand T_dec_to_comp.
Proof. rewrite /DH_computational. rewrite /C_toDHcomp_DHdecrand.
simpl. rewrite /eC_toDHcomp. rewrite /DH_decisional_rand. rewrite /DH_rand.
rewrite /rnd. rewrite /ElGamal.rnd.
rel_couple_UU.
rel_pures_l. rel_pures_r.
rel_couple_UU.
rel_pures_l. rel_pures_r.
rel_apply refines_randU_r. iIntros (c).
rel_pures_r. rel_pures.
rel_apply_l refines_exp_l. rel_apply_l refines_exp_l.
rel_apply_r refines_exp_r. rel_apply_r refines_exp_r. rel_apply_r refines_exp_r. rel_pures.
rel_vals.
Qed.
Lemma C_toDHcomp_DHdecrand_DHcomp :
⊢ refines top C_toDHcomp_DHdecrand DH_computational T_dec_to_comp.
Proof. rewrite /DH_computational. rewrite /C_toDHcomp_DHdecrand.
simpl. rewrite /eC_toDHcomp. rewrite /DH_decisional_rand. rewrite /DH_rand.
rewrite /rnd. rewrite /ElGamal.rnd.
rel_couple_UU.
rel_pures_l. rel_pures_r.
rel_couple_UU.
rel_pures_l. rel_pures_r.
rel_apply refines_randU_l. iIntros (c).
rel_pures_r. rel_pures.
rel_apply_r refines_exp_r. rel_apply_r refines_exp_r.
rel_apply_l refines_exp_l. rel_apply_l refines_exp_l. rel_apply_l refines_exp_l. rel_pures.
rel_vals.
Qed.
End LogRel.
Section Ctx.
Context {G : forall `{!clutchRGS Σ}, clutch_group (vg:=vg) (cg:=cg)}.
(* reduction DL ≥ DH computational *)
Lemma ctx_DL_C_toDL_DHcomp : ∅ ⊨ DL =ctx= C_toDL_DHcomp : τ_comp_to_dl.
Proof. split.
- apply (refines_sound clutchRΣ). intros. apply DL_C_toDL_DHcomp.
- apply (refines_sound clutchRΣ). intros. apply C_toDL_DHcomp_DL.
Qed.
(* reduction DH computational ≥ DH decisional *)
Lemma ctx_DHcomp_C_toDHcomp_DHdecreal : ∅ ⊨ DH_computational =ctx= C_toDHcomp_DHdecreal : τ_dec_to_comp.
Proof. split.
- apply (refines_sound clutchRΣ). intros. apply DHcomp_C_toDHcomp_DHdecreal.
- apply (refines_sound clutchRΣ). intros. apply C_toDHcomp_DHdecreal_DHcomp.
Qed.
Lemma ctx_DHcomp_C_toDHcomp_DHdecrand : ∅ ⊨ DH_computational =ctx= C_toDHcomp_DHdecrand : τ_dec_to_comp.
Proof. split.
- apply (refines_sound clutchRΣ). intros. apply DHcomp_C_toDHcomp_DHdecrand.
- apply (refines_sound clutchRΣ). intros. apply C_toDHcomp_DHdecrand_DHcomp.
Qed.
(*
Theorem ElGamal_DH_secure :
forall (A : val), (⊢ᵥ A : (τ_EG → TBool)) ->
let AC := (λ:"v", A (fill C "v"))R.
Proof.
intros ; eapply (advantage_triangle _ _ (fill C DH_real) _ _ 0).
3: right ; rewrite Rplus_0_l ; eauto.
2: eapply (advantage_triangle _ _ (fill C DH_rand) _ _ _ 0) ; first last.
2: rewrite Rplus_0_r ; right ; eauto.
- right. eapply ctx_advantage. 2: by tychk.
apply ctx_real_C_DH_real.
- right. eapply ctx_advantage. 2: by tychk.
apply ctx_C_DH_rand_rand.
- simpl. eapply advantage_reduction_ty ; rewrite /eC /DH_real /DH_rand ; tychk => //.
all: rewrite /rnd ; apply Subsume_int_nat ; tychk.
Qed.*)
(* TODO maybe add advantage inequality (as in `ElGamal.v`) *)
End Ctx.
End DH_assumptions.
From clutch.prob_lang Require Import advantage.
From clutch.prob_lang.typing Require Import tychk.
From clutch.clutch.examples.crypto Require Import valgroup advantage_laws.
From clutch.clutch.examples.crypto Require ElGamal_bijection.
From mathcomp Require ssrnat.
#[warning="-notation-incompatible-prefix"]
From mathcomp Require Import zmodp finset ssrbool fingroup.fingroup solvable.cyclic.
Import valgroup_notation.
From clutch.clutch.examples.crypto Require Import ElGamal.
Set Default Proof Using "Type*".
Section DH_assumptions.
Context {vg : val_group}. (* A group on a subset of values. *)
Context {cg : clutch_group_struct}. (* Implementations of the vg group operations *)
Context {vgg : @val_group_generator vg}. (* G is generated by g. *)
Context {cgg : @clutch_group_generator vg cg vgg}. (* g is well-typed *)
#[local] Notation n := (S n'').
#[local] Definition rnd t := (rand(t) #n)%E.
(* decisional DH game *)
Definition DH_decisional_real : expr := DH_real.
Definition DH_decisional_rand : expr := DH_rand.
(* computational DH game *)
Definition DH_computational : expr :=
let: "a" := rnd #() in
let: "b" := rnd #() in
(g^"a", g^"b").
(* Discrete Logarithm game *)
Definition DL : expr :=
let: "a" := rnd #() in g^"a".
(* reduction DL ≥ DH computational*)
Definition eC_toDL : val :=
(λ: "DHcomp",
let, ("A", "B") := "DHcomp" in
"A" ).
Definition C_toDL : list ectx_item := [AppRCtx eC_toDL].
Definition C_toDL_DHcomp : expr := fill C_toDL DH_computational.
Definition τ_comp_to_dl := τG%ty.
(* reduction DH computational ≥ DH_decisional *)
Definition eC_toDHcomp : expr :=
(λ: "DHdec",
let, ("A", "B", "X") := "DHdec" in
("A", "B")).
Definition C_toDHcomp : list ectx_item := [AppRCtx eC_toDHcomp].
Definition C_toDHcomp_DHdecreal : expr := fill C_toDHcomp DH_decisional_real.
Definition C_toDHcomp_DHdecrand : expr := fill C_toDHcomp DH_decisional_rand.
Definition τ_dec_to_comp := (τG * τG)%ty.
Section LogRel.
Context `{!clutchRGS Σ}.
Context {G : clutch_group (vg:=vg) (cg:=cg)}. (* cg satisfies the group laws. *)
Context {Δ : listO (lrelC Σ)}.
Import valgroup_tactics.
Ltac rel_red :=
iStartProof ;
repeat (iredrs ; try first [rel_exp_r | rel_mult_r | rel_inv_r]) ;
repeat (iredls ; try first [rel_exp_l | rel_mult_l | rel_inv_l]).
Definition pkN := nroot.@"pks".
Local Tactic Notation "inv_prove" :=
iSplitL ; [ by (repeat (iExists _) ; (by iFrame) || (iLeft ; by iFrame) || (iRight ; by iFrame)) |].
Local Tactic Notation "inv_mk" constr(Pinv) constr(h) :=
iApply (refines_na_alloc Pinv pkN) ; inv_prove ; iIntros h.
Local Tactic Notation "inv_cl" constr(h) :=
iApply (refines_na_close with h) ; inv_prove.
(* The semantic type of the game. *)
Definition T_comp_to_dl := Eval cbn in (interp τ_comp_to_dl Δ).
Definition T_dec_to_comp := Eval cbn in (interp τ_dec_to_comp Δ).
(* proof of logrel for the reduction reduction DL ≥ DH_computational *)
Lemma DL_C_toDL_DHcomp : ⊢ refines top DL C_toDL_DHcomp T_comp_to_dl.
Proof. iStartProof. rewrite /DL; rewrite /C_toDL_DHcomp.
simpl. unfold eC_toDL. rewrite /DH_computational.
rewrite /rnd.
rel_couple_UU.
rel_pures_l. rel_pures_r.
rel_apply refines_randU_r. iIntros (b).
rel_pures_r. rel_pures. unfold T_comp_to_dl. unfold τ_comp_to_dl.
rel_apply_l refines_exp_l.
rel_apply_r refines_exp_r. rel_apply_r refines_exp_r.
rel_pures_r.
rel_vals.
Qed.
Lemma C_toDL_DHcomp_DL : ⊢ refines top C_toDL_DHcomp DL T_comp_to_dl.
Proof. iStartProof. rewrite /DL. rewrite /C_toDL_DHcomp.
simpl. rewrite /eC_toDL. rewrite /DH_computational.
rewrite /rnd.
rel_couple_UU.
rel_pures_l. rel_pures_r.
rel_apply refines_randU_l. iIntros (b).
rel_pures_l. rel_pures. unfold T_comp_to_dl. unfold τ_comp_to_dl.
rel_apply_l refines_exp_l. rel_apply_l refines_exp_l.
rel_apply_r refines_exp_r. rel_pures.
rel_vals.
Qed.
(* proof of logrel for the reduction DL ≥ DH_computational *)
Lemma DHcomp_C_toDHcomp_DHdecreal :
⊢ refines top DH_computational C_toDHcomp_DHdecreal T_dec_to_comp.
Proof. rewrite /DH_computational. rewrite /C_toDHcomp_DHdecreal.
simpl. rewrite /eC_toDHcomp. rewrite /DH_decisional_real. rewrite /DH_real.
rewrite /rnd. rewrite /ElGamal.rnd.
rel_couple_UU.
rel_pures_l. rel_pures_r.
rel_couple_UU.
rel_pures_l. rel_pures_r.
rewrite -Nat2Z.inj_mul. rel_pures.
rel_pures_l.
rel_apply_l refines_exp_l. rel_apply_l refines_exp_l.
rel_apply_r refines_exp_r. rel_apply_r refines_exp_r. rel_apply_r refines_exp_r. rel_pures.
rel_vals.
Qed.
Lemma C_toDHcomp_DHdecreal_DHcomp :
⊢ refines top C_toDHcomp_DHdecreal DH_computational T_dec_to_comp.
Proof. rewrite /DH_computational. rewrite /C_toDHcomp_DHdecreal.
simpl. rewrite /eC_toDHcomp. rewrite /DH_decisional_real. rewrite /DH_real.
rewrite /rnd. rewrite /ElGamal.rnd.
rel_couple_UU.
rel_pures_l. rel_pures_r.
rel_couple_UU.
rel_pures_l. rel_pures_r. ireds.
rewrite -Nat2Z.inj_mul. rel_pures.
rel_pures_l.
rel_apply_r refines_exp_r. rel_apply_r refines_exp_r.
rel_apply_l refines_exp_l. rel_apply_l refines_exp_l. rel_apply_l refines_exp_l. rel_pures.
rel_vals.
Qed.
Lemma DHcomp_C_toDHcomp_DHdecrand :
⊢ refines top DH_computational C_toDHcomp_DHdecrand T_dec_to_comp.
Proof. rewrite /DH_computational. rewrite /C_toDHcomp_DHdecrand.
simpl. rewrite /eC_toDHcomp. rewrite /DH_decisional_rand. rewrite /DH_rand.
rewrite /rnd. rewrite /ElGamal.rnd.
rel_couple_UU.
rel_pures_l. rel_pures_r.
rel_couple_UU.
rel_pures_l. rel_pures_r.
rel_apply refines_randU_r. iIntros (c).
rel_pures_r. rel_pures.
rel_apply_l refines_exp_l. rel_apply_l refines_exp_l.
rel_apply_r refines_exp_r. rel_apply_r refines_exp_r. rel_apply_r refines_exp_r. rel_pures.
rel_vals.
Qed.
Lemma C_toDHcomp_DHdecrand_DHcomp :
⊢ refines top C_toDHcomp_DHdecrand DH_computational T_dec_to_comp.
Proof. rewrite /DH_computational. rewrite /C_toDHcomp_DHdecrand.
simpl. rewrite /eC_toDHcomp. rewrite /DH_decisional_rand. rewrite /DH_rand.
rewrite /rnd. rewrite /ElGamal.rnd.
rel_couple_UU.
rel_pures_l. rel_pures_r.
rel_couple_UU.
rel_pures_l. rel_pures_r.
rel_apply refines_randU_l. iIntros (c).
rel_pures_r. rel_pures.
rel_apply_r refines_exp_r. rel_apply_r refines_exp_r.
rel_apply_l refines_exp_l. rel_apply_l refines_exp_l. rel_apply_l refines_exp_l. rel_pures.
rel_vals.
Qed.
End LogRel.
Section Ctx.
Context {G : forall `{!clutchRGS Σ}, clutch_group (vg:=vg) (cg:=cg)}.
(* reduction DL ≥ DH computational *)
Lemma ctx_DL_C_toDL_DHcomp : ∅ ⊨ DL =ctx= C_toDL_DHcomp : τ_comp_to_dl.
Proof. split.
- apply (refines_sound clutchRΣ). intros. apply DL_C_toDL_DHcomp.
- apply (refines_sound clutchRΣ). intros. apply C_toDL_DHcomp_DL.
Qed.
(* reduction DH computational ≥ DH decisional *)
Lemma ctx_DHcomp_C_toDHcomp_DHdecreal : ∅ ⊨ DH_computational =ctx= C_toDHcomp_DHdecreal : τ_dec_to_comp.
Proof. split.
- apply (refines_sound clutchRΣ). intros. apply DHcomp_C_toDHcomp_DHdecreal.
- apply (refines_sound clutchRΣ). intros. apply C_toDHcomp_DHdecreal_DHcomp.
Qed.
Lemma ctx_DHcomp_C_toDHcomp_DHdecrand : ∅ ⊨ DH_computational =ctx= C_toDHcomp_DHdecrand : τ_dec_to_comp.
Proof. split.
- apply (refines_sound clutchRΣ). intros. apply DHcomp_C_toDHcomp_DHdecrand.
- apply (refines_sound clutchRΣ). intros. apply C_toDHcomp_DHdecrand_DHcomp.
Qed.
(*
Theorem ElGamal_DH_secure :
forall (A : val), (⊢ᵥ A : (τ_EG → TBool)) ->
let AC := (λ:"v", A (fill C "v"))R.
Proof.
intros ; eapply (advantage_triangle _ _ (fill C DH_real) _ _ 0).
3: right ; rewrite Rplus_0_l ; eauto.
2: eapply (advantage_triangle _ _ (fill C DH_rand) _ _ _ 0) ; first last.
2: rewrite Rplus_0_r ; right ; eauto.
- right. eapply ctx_advantage. 2: by tychk.
apply ctx_real_C_DH_real.
- right. eapply ctx_advantage. 2: by tychk.
apply ctx_C_DH_rand_rand.
- simpl. eapply advantage_reduction_ty ; rewrite /eC /DH_real /DH_rand ; tychk => //.
all: rewrite /rnd ; apply Subsume_int_nat ; tychk.
Qed.*)
(* TODO maybe add advantage inequality (as in `ElGamal.v`) *)
End Ctx.
End DH_assumptions.