clutch.approxis.examples.diffie_hellman
From clutch.approxis Require Import reltac2 approxis.
From clutch.prob_lang Require Import advantage.
From clutch.prob_lang.typing Require Import tychk.
From clutch.approxis.examples Require Import valgroup advantage_laws.
Import valgroup_notation.
Set Default Proof Using "Type*".
Section DH.
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. *)
#[local] Notation n := (S n'').
(* The syntactic type of the Decisional Diffie-Hellman game(s). *)
Definition τ_DDH := (τG * τG * τG)%ty.
(* The Decisional Diffie Hellman assumption says the following two programs are
PPT(n) indistinguishable. *)
Definition DDH_real : expr :=
let: "a" := rand #n in
let: "b" := rand #n in
(vgval g^"a", vgval g^"b", vgval g^("a"*"b")).
Definition DDH_rand : expr :=
let: "a" := rand #n in
let: "b" := rand #n in
let: "c" := rand #n in
(vgval g^"a", vgval g^"b", vgval g^"c").
Context {cgg : @clutch_group_generator vg cg vgg}. (* g is well-typed *)
Lemma DDH_real_typed : ∅ ⊢ₜ DDH_real : τ_DDH.
Proof with tychk.
rewrite /DDH_real.
type_expr 1. 2: apply Subsume_int_nat...
type_expr 2. 2: apply Subsume_int_nat...
tychk => //.
Qed.
Lemma DDH_rand_typed : ∅ ⊢ₜ DDH_rand : τ_DDH.
Proof with tychk.
rewrite /DDH_rand.
type_expr 1. 2: apply Subsume_int_nat...
type_expr 2. 2: apply Subsume_int_nat...
type_expr 2. 2: apply Subsume_int_nat...
tychk => //.
Qed.
Section semantic.
Context `{!approxisRGS Σ}.
Context {G : clutch_group (vg:=vg) (cg:=cg)}. (* cg satisfies the group laws. *)
Context {Δ : listO (lrelC Σ)}.
(* The semantic type of the Diffie-Hellman game(s). *)
Definition T_DDH : lrel _ := lrel_G * lrel_G * lrel_G.
Import valgroup_tactics.
Lemma DDH_real_sem_typed : ⊢ REL DDH_real << DDH_real : T_DDH.
Proof with rel_red.
rewrite /DDH_real...
rel_apply (refines_couple_UU n). 1: intuition auto ; lia.
iIntros "!> %a %le_a_n"...
rel_apply (refines_couple_UU n). 1: intuition auto ; lia.
iIntros "!> %b %le_b_n"...
replace (Z.of_nat a * Z.of_nat b)%Z with (Z.of_nat (a * b)) by lia...
rel_pures_l.
do 3 (rel_apply_l refines_exp_l; rel_pures_l).
rel_pures_r.
do 3 (rel_apply_r refines_exp_r; rel_pures_r).
rel_vals.
Qed.
Lemma DDH_rand_sem_typed : ⊢ REL DDH_rand << DDH_rand : T_DDH.
Proof with rel_red.
rewrite /DDH_real...
rel_apply (refines_couple_UU n). 1: intuition auto ; lia.
iIntros "!> %a %le_a_n"...
rel_apply (refines_couple_UU n). 1: intuition auto ; lia.
iIntros "!> %b %le_b_n"...
rel_apply (refines_couple_UU n). 1: intuition auto ; lia.
iIntros "!> %c %le_c_n"...
rel_pures_l.
do 3 (rel_apply_l refines_exp_l; rel_pures_l).
rel_pures_r.
do 3 (rel_apply_r refines_exp_r; rel_pures_r).
rel_vals.
Qed.
End semantic.
End DH.
From clutch.prob_lang Require Import advantage.
From clutch.prob_lang.typing Require Import tychk.
From clutch.approxis.examples Require Import valgroup advantage_laws.
Import valgroup_notation.
Set Default Proof Using "Type*".
Section DH.
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. *)
#[local] Notation n := (S n'').
(* The syntactic type of the Decisional Diffie-Hellman game(s). *)
Definition τ_DDH := (τG * τG * τG)%ty.
(* The Decisional Diffie Hellman assumption says the following two programs are
PPT(n) indistinguishable. *)
Definition DDH_real : expr :=
let: "a" := rand #n in
let: "b" := rand #n in
(vgval g^"a", vgval g^"b", vgval g^("a"*"b")).
Definition DDH_rand : expr :=
let: "a" := rand #n in
let: "b" := rand #n in
let: "c" := rand #n in
(vgval g^"a", vgval g^"b", vgval g^"c").
Context {cgg : @clutch_group_generator vg cg vgg}. (* g is well-typed *)
Lemma DDH_real_typed : ∅ ⊢ₜ DDH_real : τ_DDH.
Proof with tychk.
rewrite /DDH_real.
type_expr 1. 2: apply Subsume_int_nat...
type_expr 2. 2: apply Subsume_int_nat...
tychk => //.
Qed.
Lemma DDH_rand_typed : ∅ ⊢ₜ DDH_rand : τ_DDH.
Proof with tychk.
rewrite /DDH_rand.
type_expr 1. 2: apply Subsume_int_nat...
type_expr 2. 2: apply Subsume_int_nat...
type_expr 2. 2: apply Subsume_int_nat...
tychk => //.
Qed.
Section semantic.
Context `{!approxisRGS Σ}.
Context {G : clutch_group (vg:=vg) (cg:=cg)}. (* cg satisfies the group laws. *)
Context {Δ : listO (lrelC Σ)}.
(* The semantic type of the Diffie-Hellman game(s). *)
Definition T_DDH : lrel _ := lrel_G * lrel_G * lrel_G.
Import valgroup_tactics.
Lemma DDH_real_sem_typed : ⊢ REL DDH_real << DDH_real : T_DDH.
Proof with rel_red.
rewrite /DDH_real...
rel_apply (refines_couple_UU n). 1: intuition auto ; lia.
iIntros "!> %a %le_a_n"...
rel_apply (refines_couple_UU n). 1: intuition auto ; lia.
iIntros "!> %b %le_b_n"...
replace (Z.of_nat a * Z.of_nat b)%Z with (Z.of_nat (a * b)) by lia...
rel_pures_l.
do 3 (rel_apply_l refines_exp_l; rel_pures_l).
rel_pures_r.
do 3 (rel_apply_r refines_exp_r; rel_pures_r).
rel_vals.
Qed.
Lemma DDH_rand_sem_typed : ⊢ REL DDH_rand << DDH_rand : T_DDH.
Proof with rel_red.
rewrite /DDH_real...
rel_apply (refines_couple_UU n). 1: intuition auto ; lia.
iIntros "!> %a %le_a_n"...
rel_apply (refines_couple_UU n). 1: intuition auto ; lia.
iIntros "!> %b %le_b_n"...
rel_apply (refines_couple_UU n). 1: intuition auto ; lia.
iIntros "!> %c %le_c_n"...
rel_pures_l.
do 3 (rel_apply_l refines_exp_l; rel_pures_l).
rel_pures_r.
do 3 (rel_apply_r refines_exp_r; rel_pures_r).
rel_vals.
Qed.
End semantic.
End DH.