clutch.approxis.examples.ElGamal_defs
(* Definitions for ElGamal encryption. *)
From clutch.prob_lang Require Import notation advantage.
From clutch.prob_lang.typing Require Import types tychk.
From clutch.approxis.examples Require Import valgroup.
From clutch.approxis Require approxis option.
Set Default Proof Using "Type*".
Section ElGamal.
Import valgroup_notation.
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'').
(* ElGamal public key encryption *)
Definition keygen : val :=
λ:<>, let: "sk" := rand #n in
let: "pk" := vgval g ^ "sk" in
("sk", "pk").
Definition enc : val :=
λ: "pk", λ: "msg",
let: "b" := rand #n in
let: "B" := vgval g ^ "b" in
let: "X" := "msg" · ("pk"^"b") in
("B", "X").
Definition dec : val :=
λ:"sk" "BX",
let, ("B", "X") := "BX" in
"X" · ("B"^-"sk").
Definition rand_cipher : val :=
λ:"msg",
let: "b" := rand #n in
let: "x" := rand #n in
let, ("B", "X") := (vgval g ^ "b", vgval g ^ "x") in
("B", "X").
(* The syntactic type of the ElGamal game(s). *)
Definition τ_EG := (τG * (TInt → () + τG * τG))%ty.
Lemma keygen_typed : ⊢ᵥ keygen : (() → TInt * τG).
Proof. rewrite /keygen. type_val 2. 2: apply Subsume_int_nat. all: tychk => //. Qed.
Lemma enc_typed : ⊢ᵥ enc : (τG → τG → τG * τG).
Proof. rewrite /enc. type_val 3. 2: apply Subsume_int_nat. all: tychk => //. Qed.
Lemma rand_cipher_typed : ⊢ᵥ rand_cipher : (τG → τG * τG).
Proof.
rewrite /rand_cipher. type_val 2. 2: apply Subsume_int_nat. 2: tychk.
type_expr 2. 2: apply Subsume_int_nat. all: tychk=> //.
Qed.
Section semantic.
Import clutch.approxis.approxis.
Context `{!approxisRGS Σ}.
Context {G : clutch_group (vg:=vg) (cg:=cg)}. (* cg satisfies the group laws. *)
Definition EG_pkey := lrel_G.
Definition EG_skey := @lrel_int Σ.
Definition EG_msg := lrel_G.
Definition EG_cipher := (lrel_G * lrel_G)%lrel.
Definition T_EG := (EG_pkey * (EG_msg → option.lrel_option EG_cipher))%lrel.
Import valgroup_tactics.
Lemma keygen_sem_typed :
⊢ REL keygen << keygen : () → EG_skey * EG_pkey.
Proof with rel_red.
rewrite /EG_skey /EG_pkey.
rewrite /keygen.
rel_arrow_val ; iIntros (??) "_"...
rel_apply (refines_couple_UU n). 1: intuition auto ; lia.
iIntros "!> %sk %le_sk_n".
rel_pures_l.
rel_apply_l refines_exp_l; rel_pures_l.
rel_pures_r.
rel_apply_r refines_exp_r; rel_pures_r.
rel_vals.
Qed.
Lemma enc_sem_typed :
⊢ REL enc << enc : EG_pkey → EG_msg → EG_cipher.
Proof with rel_red.
rewrite /enc...
rel_arrow_val ; iIntros (??) "(%&->&->)"...
rel_arrow_val ; iIntros (??) "(%&->&->)"...
rel_apply (refines_couple_UU n). 1: intuition auto ; lia.
iIntros "!> %b %le_b_n"...
rel_pures_l.
rel_apply_l refines_exp_l; rel_pures_l.
rel_apply_l refines_exp_l; rel_pures_l.
rel_apply_l refines_mult_l; rel_pures_l.
rel_pures_r.
rel_apply_r refines_exp_r; rel_pures_r.
rel_apply_r refines_exp_r; rel_pures_r.
rel_apply_r refines_mult_r; rel_pures_r.
rel_pures_r.
rel_vals.
Qed.
Lemma rand_cipher_sem_typed :
⊢ REL rand_cipher << rand_cipher : EG_msg → EG_cipher.
Proof with rel_red.
rewrite /rand_cipher.
rel_arrow_val ; iIntros (??) "(%&->&->)"...
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 "!> %x %le_x_n"...
rel_pures_l.
rel_apply_l refines_exp_l; rel_pures_l.
rel_apply_l refines_exp_l; rel_pures_l.
rel_pures_r.
rel_apply_r refines_exp_r; rel_pures_r.
rel_apply_r refines_exp_r; rel_pures_r.
rel_vals.
Qed.
End semantic.
End ElGamal.
From clutch.prob_lang Require Import notation advantage.
From clutch.prob_lang.typing Require Import types tychk.
From clutch.approxis.examples Require Import valgroup.
From clutch.approxis Require approxis option.
Set Default Proof Using "Type*".
Section ElGamal.
Import valgroup_notation.
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'').
(* ElGamal public key encryption *)
Definition keygen : val :=
λ:<>, let: "sk" := rand #n in
let: "pk" := vgval g ^ "sk" in
("sk", "pk").
Definition enc : val :=
λ: "pk", λ: "msg",
let: "b" := rand #n in
let: "B" := vgval g ^ "b" in
let: "X" := "msg" · ("pk"^"b") in
("B", "X").
Definition dec : val :=
λ:"sk" "BX",
let, ("B", "X") := "BX" in
"X" · ("B"^-"sk").
Definition rand_cipher : val :=
λ:"msg",
let: "b" := rand #n in
let: "x" := rand #n in
let, ("B", "X") := (vgval g ^ "b", vgval g ^ "x") in
("B", "X").
(* The syntactic type of the ElGamal game(s). *)
Definition τ_EG := (τG * (TInt → () + τG * τG))%ty.
Lemma keygen_typed : ⊢ᵥ keygen : (() → TInt * τG).
Proof. rewrite /keygen. type_val 2. 2: apply Subsume_int_nat. all: tychk => //. Qed.
Lemma enc_typed : ⊢ᵥ enc : (τG → τG → τG * τG).
Proof. rewrite /enc. type_val 3. 2: apply Subsume_int_nat. all: tychk => //. Qed.
Lemma rand_cipher_typed : ⊢ᵥ rand_cipher : (τG → τG * τG).
Proof.
rewrite /rand_cipher. type_val 2. 2: apply Subsume_int_nat. 2: tychk.
type_expr 2. 2: apply Subsume_int_nat. all: tychk=> //.
Qed.
Section semantic.
Import clutch.approxis.approxis.
Context `{!approxisRGS Σ}.
Context {G : clutch_group (vg:=vg) (cg:=cg)}. (* cg satisfies the group laws. *)
Definition EG_pkey := lrel_G.
Definition EG_skey := @lrel_int Σ.
Definition EG_msg := lrel_G.
Definition EG_cipher := (lrel_G * lrel_G)%lrel.
Definition T_EG := (EG_pkey * (EG_msg → option.lrel_option EG_cipher))%lrel.
Import valgroup_tactics.
Lemma keygen_sem_typed :
⊢ REL keygen << keygen : () → EG_skey * EG_pkey.
Proof with rel_red.
rewrite /EG_skey /EG_pkey.
rewrite /keygen.
rel_arrow_val ; iIntros (??) "_"...
rel_apply (refines_couple_UU n). 1: intuition auto ; lia.
iIntros "!> %sk %le_sk_n".
rel_pures_l.
rel_apply_l refines_exp_l; rel_pures_l.
rel_pures_r.
rel_apply_r refines_exp_r; rel_pures_r.
rel_vals.
Qed.
Lemma enc_sem_typed :
⊢ REL enc << enc : EG_pkey → EG_msg → EG_cipher.
Proof with rel_red.
rewrite /enc...
rel_arrow_val ; iIntros (??) "(%&->&->)"...
rel_arrow_val ; iIntros (??) "(%&->&->)"...
rel_apply (refines_couple_UU n). 1: intuition auto ; lia.
iIntros "!> %b %le_b_n"...
rel_pures_l.
rel_apply_l refines_exp_l; rel_pures_l.
rel_apply_l refines_exp_l; rel_pures_l.
rel_apply_l refines_mult_l; rel_pures_l.
rel_pures_r.
rel_apply_r refines_exp_r; rel_pures_r.
rel_apply_r refines_exp_r; rel_pures_r.
rel_apply_r refines_mult_r; rel_pures_r.
rel_pures_r.
rel_vals.
Qed.
Lemma rand_cipher_sem_typed :
⊢ REL rand_cipher << rand_cipher : EG_msg → EG_cipher.
Proof with rel_red.
rewrite /rand_cipher.
rel_arrow_val ; iIntros (??) "(%&->&->)"...
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 "!> %x %le_x_n"...
rel_pures_l.
rel_apply_l refines_exp_l; rel_pures_l.
rel_apply_l refines_exp_l; rel_pures_l.
rel_pures_r.
rel_apply_r refines_exp_r; rel_pures_r.
rel_apply_r refines_exp_r; rel_pures_r.
rel_vals.
Qed.
End semantic.
End ElGamal.