clutch.approxis.examples.ElGamal_semantic
(* One-time indistinguishability from random for ElGamal encryption.
The main difference with the Clutch version is that we use the "standard"
one-time security games for public key encryption defined in pubkey.v.
Another difference (including w.r.t. the ElGamal ported to Approxis) is that
pubkey.v relies on semantically well-typed adversaries instead of
syntactically typed ones, so we can drop the well-formedness check for
messages from the adversary. In the Clutch version of ElGamal, we explicitly
checked if the message was a valid group element. *)
From Ltac2 Require Import Ltac2.
Set Default Proof Mode "Classic".
From clutch.prob_lang Require Import advantage typing.tychk.
From clutch.approxis Require Import reltac2 approxis option.
From clutch.clutch.examples.crypto Require ElGamal_bijection.
From clutch.approxis.examples Require Import
valgroup diffie_hellman ElGamal_defs bounded_oracle pubkey advantage_laws.
From mathcomp Require Import ssrbool.
From mathcomp Require fingroup.fingroup.
Set Default Proof Using "All".
Import ElGamal_bijection.bij_nat.
Import valgroup_notation.
Section ElGamal_sem.
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'').
Definition pk_real := CPA_OTS_real keygen enc.
Definition pk_rand := CPA_OTS_rand keygen rand_cipher.
(* Unfold definitions and label the flips. We need to label the flip in
"query" since it occurs in a closure, and we want to relate it to an
eager sampling in the set-up phase in order to make DDH_real appear as a
sub-expression. *)
Definition pk_real_tape : expr :=
let: "β" := alloc #n in
let: "sk" := rand #n in
let: "pk" := vgval g^"sk" in
let: "count" := ref #0 in
let: "query" := λ:"msg",
(* let:m "msg" := vg_of_int "msg" in *)
assert (!"count" = #0) ;;;
"count" <- #1 ;;
let: "b" := rand("β") #n in
let: "B" := vgval g^"b" in
let: "C" := "pk"^"b" in
let: "X" := "msg" · "C" in
("B", "X") in
("pk", "query").
(* Pull out DDH_real/rand. This requires moving the sampling of "b" from "query"
to the initialisation. Only equivalent because "query" gets called only
once: only one message is encrypted, so only one nonce "b" is required, and
we can pre-sample it in the setup. *)
Definition eC : val :=
(λ: "DDH_real_or_rand",
let, ("pk", "B", "C") := "DDH_real_or_rand" in
let: "count" := ref #0 in
let: "query" := λ: "msg",
assert (!"count" = #0) ;;;
"count" <- #1 ;;
let: "X" := "msg" · "C" in
("B", "X") in
("pk", "query")).
Definition C : list ectx_item := [AppRCtx eC].
Definition C_DDH_real : expr := fill C DDH_real.
Definition C_DDH_rand : expr := fill C DDH_rand.
(* Inline DDH_rand and push the two random samplings not required for the key
generation back down (using tapes β and γ). *)
Definition pk_rand_tape : expr :=
let: "β" := alloc #n in
let: "γ" := alloc #n in
let: "sk" := rand #n in
let: "pk" := vgval g^"sk" in
let: "count" := ref #0 in
let: "query" := λ:"msg",
assert (!"count" = #0) ;;;
"count" <- #1 ;;
let: "b" := rand("β") #n in
let: "c" := rand("γ") #n in
let: "B" := vgval g^"b" in
let: "C" := vgval g^"c" in
let: "X" := "msg" · "C" in
("B", "X") in
("pk", "query").
Section LogRel.
Context `{!approxisRGS Σ}.
Context {G : clutch_group (vg:=vg) (cg:=cg)}. (* cg satisfies the group laws. *)
Context {Δ : listO (lrelC Σ)}.
Import valgroup_tactics.
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.
Lemma eC_sem_typed : ⊢ REL eC << eC : (T_DDH → T_EG).
Proof with rel_red.
rewrite /eC.
rel_arrow_val ; iIntros (??) "#h" ; ireds.
rewrite /T_DDH.
iDestruct "h" as "(%&%&%&%&->&->&h&h')".
iDestruct "h" as "(%&%&%&%&->&->&h&h'')".
iDestruct "h" as "(%&->&->)".
iDestruct "h'" as "(%&->&->)".
iDestruct "h''" as "(%&->&->)"...
inv_mk ((count ↦ #0 ∗ countₛ ↦ₛ #0) ∨ (count ↦ #1 ∗ countₛ ↦ₛ #1) )%I "#Hinv"...
rel_vals => //.
iIntros (??) "!> #(%vmsg&->&->)"...
iApply (refines_na_inv with "[-$Hinv]") => //.
iIntros "[>[(count&countₛ)|(count&countₛ)] Hclose]"...
all: (inv_cl "[-$Hclose]").
2 : rel_vals.
rel_apply_l (refines_mult_l); rel_pures_l.
rel_apply_r (refines_mult_r); rel_pures_r.
rel_vals.
Qed.
Lemma real_real_tape : ⊢ REL pk_real << pk_real_tape : T_EG.
Proof with rel_red.
rel_red. rewrite /keygen... rel_apply (refines_couple_UU n). 1: intuition auto ; lia.
iIntros "!> %sk %le_sk_n".
idtac...
rewrite /q_calls_poly...
rel_apply_l (refines_exp_l); rel_apply_r (refines_exp_r)...
inv_mk (βₛ ↪ₛN (n;[]) ∗ (counter ↦ #0 ∗ countₛ ↦ₛ #0) ∨ (counter ↦ #1 ∗ countₛ ↦ₛ #1) )%I "#Hinv"...
rel_vals ; iIntros "!>".
iIntros (??) "#(%msg&->&->)"...
iApply (refines_na_inv with "[-$Hinv]"); [done|].
iIntros "[>[(β&c&c')|(c&c')] Hclose]"...
2: inv_cl "[- $Hclose]" ; rel_vals.
rewrite /enc...
rel_apply (refines_couple_UT). 1: intuition auto ; lia.
iFrame. iIntros (b bn) "!> β". iredpures.
rel_rand_r. iIntros (_)...
inv_cl "[- $Hclose]"...
rel_apply_l (refines_exp_l); rel_apply_r (refines_exp_r)...
rel_apply_l (refines_exp_l); rel_apply_r (refines_exp_r)...
rel_apply_l (refines_mult_l); rel_apply_r (refines_mult_r)...
rel_vals.
Qed.
Lemma real_tape_real : ⊢ REL pk_real_tape << pk_real : T_EG.
Proof with rel_red.
rel_red. rewrite /keygen... rel_apply (refines_couple_UU n). 1: intuition auto ; lia.
iIntros "!> %sk %le_sk_n".
idtac...
rewrite /q_calls_poly...
rel_apply_l (refines_exp_l); rel_apply_r (refines_exp_r)...
inv_mk (β ↪N (n;[]) ∗ (count ↦ #0 ∗ counterₛ ↦ₛ #0) ∨ (count ↦ #1 ∗ counterₛ ↦ₛ #1) )%I "#Hinv"...
rel_vals ; iIntros "!>" (??) "#(%msg&->&->)"...
iApply (refines_na_inv with "[-$Hinv]"); [done|].
iIntros "[>[(β&c&c')|(c&c')] Hclose]"...
2: inv_cl "[- $Hclose]" ; rel_vals.
rewrite /enc...
rel_apply (refines_couple_TU n). 1: intuition auto ; lia.
iFrame. iIntros (b bn) "β". iredpures.
rel_rand_l. iIntros (_)...
inv_cl "[- $Hclose]".
rel_apply_l (refines_exp_l); rel_apply_r (refines_exp_r)...
rel_apply_l (refines_exp_l); rel_apply_r (refines_exp_r)...
rel_apply_l (refines_mult_l); rel_apply_r (refines_mult_r)...
rel_vals.
Qed.
Lemma real_tape_C_DDH_real : ⊢ REL pk_real_tape << C_DDH_real : T_EG.
Proof with rel_red.
rewrite /C_DDH_real /=. rel_red.
rel_apply (refines_couple_UU n). 1: intuition auto ; lia.
iIntros "!> %sk %le_sk_n".
idtac...
rel_apply (refines_couple_TU n). 1: intuition auto ; lia.
iFrame. iIntros (b bn) "β". iredpures.
rel_apply_l (refines_exp_l)...
rewrite -Nat2Z.inj_mul/eC...
do 3 (rel_apply_r (refines_exp_r))...
inv_mk ((β ↪N (n;[b]) ∗ count ↦ #0 ∗ countₛ ↦ₛ #0)
∨ (count ↦ #1 ∗ countₛ ↦ₛ #1))%I "#Hinv".
rel_vals ; iIntros "!>" (??) "#(%msg&->&->)"...
iApply (refines_na_inv with "[$Hinv]"); [done|].
iIntros "[>[(β&cnt&cnt')|(c&c')] Hclose]".
2: by (ireds ; inv_cl "[- $Hclose]" ; rel_vals).
do 6 iredl.
iredl. iIntros (_).
rel_load_r...
inv_cl "[- $Hclose]"...
rel_apply_l (refines_exp_l)...
rel_apply_l (refines_exp_l)...
rel_apply_l (refines_mult_l)...
rel_apply_r (refines_mult_r)...
rel_vals.
iExists _.
iSplit; [done|]. iPureIntro.
f_equal. f_equal.
rewrite ssrnat.multE.
(* TODO: Why is the coercion not inferred??? *)
rewrite (@fingroup.expgM (fingroup.FinGroup.Exports.fingroup_FinGroup__to__monoid_Monoid vgG) g).
done.
Qed.
Lemma C_DDH_real_real_tape : ⊢ REL C_DDH_real << pk_real_tape : T_EG.
Proof with rel_red.
rewrite /C_DDH_real /=. rel_red.
rel_apply (refines_couple_UU n). 1: intuition auto ; lia.
iIntros "!> %sk %le_sk_n".
idtac...
rewrite /q_calls_poly...
ireds.
rel_apply (refines_couple_UT). 1: intuition auto ; lia.
iFrame. iIntros (b bn) "!> βₛ". iredpures.
rewrite -Nat2Z.inj_mul/eC...
rel_apply_l (refines_exp_l)... rel_apply_l (refines_exp_l)... rel_apply_l (refines_exp_l)...
rel_apply_r (refines_exp_r)...
inv_mk ((βₛ ↪ₛN (n;[b]) ∗ count ↦ #0 ∗ countₛ ↦ₛ #0)
∨ (count ↦ #1 ∗ countₛ ↦ₛ #1))%I "#Hinv".
rel_vals ; iIntros "!>" (??) "#(%msg&->&->)"...
iApply (refines_na_inv with "[$Hinv]"); [done|].
iIntros "[[(β&cnt&cnt')|(c&c')] Hclose]"...
2: (rel_load_r ; rel_red ; inv_cl "[- $Hclose]" ; rel_vals).
rel_load_r. do 6 iredr. iIntros (_). rel_red.
inv_cl "[- $Hclose]"...
rel_apply_l (refines_mult_l)...
rel_apply_r (refines_exp_r)... rel_apply_r (refines_exp_r)...
rel_apply_r (refines_mult_r)...
rel_vals. iExists _. iSplit; [done|]. iPureIntro.
f_equal. f_equal.
rewrite ssrnat.multE.
(* TODO: Why is the coercion not inferred??? *)
rewrite (@fingroup.expgM (fingroup.FinGroup.Exports.fingroup_FinGroup__to__monoid_Monoid vgG) g).
done.
Qed.
Lemma C_DDH_rand_rand_tape : ⊢ REL C_DDH_rand << pk_rand_tape : T_EG.
Proof with rel_red.
rewrite /C_DDH_rand/C/eC /=. rel_red.
rel_apply (refines_couple_UU n). 1: intuition auto ; lia.
iIntros "!> %sk %le_sk_n".
idtac...
rel_apply (refines_couple_UT). 1: intuition auto ; lia.
iFrame "βₛ". iIntros (b bn) "!> βₛ". iredpures.
rel_apply (refines_couple_UT). 1: intuition auto ; lia.
iFrame "γₛ". iIntros (c cn) "!> γₛ". iredpures...
rel_apply_l (refines_exp_l)... rel_apply_l (refines_exp_l)... rel_apply_l (refines_exp_l)...
rel_apply_r (refines_exp_r)...
inv_mk ((βₛ ↪ₛN (n;[b]) ∗ γₛ ↪ₛN (n;[c]) ∗ count ↦ #0 ∗ countₛ ↦ₛ #0)
∨ (count ↦ #1 ∗ countₛ ↦ₛ #1))%I "#Hinv".
rel_vals ; iIntros "!>" (??) "#(%msg&->&->)"...
iApply (refines_na_inv with "[$Hinv]") => //.
iIntros "[>[(β'&γ'&cnt&cnt')|(cnt&cnt')] Hclose]". 2: idtac...
2: inv_cl "[- $Hclose]" ; rel_vals.
rel_load_l ; rel_load_r. iredpures. rel_store_r. rel_store_l.
iredpures. rel_randT_r. iIntros (_). do 3 iredr. iIntros (_).
rel_red.
inv_cl "[- $Hclose]".
rel_apply_l (refines_mult_l)...
rel_apply_r (refines_exp_r)... rel_apply_r (refines_exp_r)...
rel_apply_r (refines_mult_r)...
rel_vals.
Qed.
Lemma rand_tape_C_DDH_rand : ⊢ REL pk_rand_tape << C_DDH_rand : T_EG.
Proof with rel_red.
rewrite /C_DDH_rand/C/eC /=. rel_red.
rel_apply (refines_couple_UU n). 1: intuition auto ; lia.
iIntros "!> %sk %le_sk_n"...
rel_apply (refines_couple_TU n). 1: intuition auto ; lia.
iFrame "β". iIntros (b bn) "β"...
rel_apply (refines_couple_TU n). 1: intuition auto ; lia.
iFrame "γ". iIntros (c cn) "γ"...
rel_apply_l (refines_exp_l)...
rel_apply_r (refines_exp_r)... rel_apply_r (refines_exp_r)... rel_apply_r (refines_exp_r)...
inv_mk ((β ↪N (n;[b]) ∗ γ ↪N (n;[c]) ∗ count ↦ #0 ∗ countₛ ↦ₛ #0)
∨ (count ↦ #1 ∗ countₛ ↦ₛ #1))%I "#Hinv".
rel_vals ; iIntros "!>" (??) "#(%msg&->&->)"...
iApply (refines_na_inv with "[$Hinv]") => //.
iIntros "[>[(β'&γ'&cnt&cnt')|(cnt&cnt')] Hclose]" ; rel_load_l ; rel_load_r.
2: inv_cl "[- $Hclose]" ; rel_red ; rel_vals.
do 6 iredl. iIntros (_). rel_pures_r. rel_store_r. rel_pures_l. iredl. iIntros (_)...
inv_cl "[- $Hclose]" ; rel_red.
rel_apply_l (refines_exp_l)... rel_apply_l (refines_exp_l)... rel_apply_l (refines_mult_l)...
rel_apply_r (refines_mult_r)...
rel_vals.
Qed.
#[warnings="-notation-incompatible-prefix"]
Import mathcomp.fingroup.fingroup.
Lemma rand_tape_rand : ⊢ refines top pk_rand_tape pk_rand T_EG.
Proof with rel_red.
rel_red. rewrite /keygen...
rel_apply (refines_couple_UU n). 1: intuition auto ; lia.
iIntros "!> %sk %le_sk_n"...
rewrite /q_calls_poly...
rel_apply_l (refines_exp_l)...
rel_apply_r (refines_exp_r)...
inv_mk ((β ↪N (n;[]) ∗ γ ↪N (n;[]) ∗ count ↦ #0 ∗ counterₛ ↦ₛ #0)
∨ (count ↦ #1 ∗ counterₛ ↦ₛ #1))%I "#Hinv".
rel_vals ; iIntros "!>" (??) "#(%vmsg&->&->)"...
iApply (refines_na_inv with "[-$Hinv]") => //.
iIntros "[>[(β&γ&cnt&cnt')|(cnt&cnt')] Hclose]"...
2: by (inv_cl "[-$Hclose]" ; rel_vals).
rewrite /rand_cipher...
rel_apply (refines_couple_TU n). 1: intuition auto ; lia.
iFrame "β". iIntros (b bn) "β".
rel_pures_r.
(* Rewrite msg into g^k_msg for some k_msg. *)
destruct (log_g vmsg) as [k_msg ->].
(* Sample c on the left, and ((k_msg + c) mod (S n)) on the right. *)
rel_apply (refines_couple_TU n (mod_plus _ k_msg)).
1: apply mod_plus_lt.
iFrame "γ". iIntros (x xn) "γ". rel_rand_l. iIntros (_). rel_rand_l. iIntros (_)...
inv_cl "[- $Hclose]"...
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_mult_l)... rel_vals.
rewrite -fingroup.expgD -ssrnat.plusE.
assert ((g ^+ (k_msg + x)) = (g ^+ mod_plus _ k_msg x))%g as heq.
{ clear -xn.
rewrite /mod_plus.
destruct (x <? S n) eqn:h.
2:{ exfalso. eapply Nat.ltb_nlt. 1: eauto. apply PeanoNat.le_lt_n_Sm. done. }
pose proof (e := eq_sym (expg_mod_order g (k_msg+x))).
rewrite g_nontriv in e.
exact e.
}
rewrite -heq. eauto.
Qed.
Lemma rand_rand_tape : ⊢ refines top pk_rand pk_rand_tape T_EG.
Proof with rel_red.
rel_red. rewrite /keygen...
rel_apply (refines_couple_UU n). 1: intuition auto ; lia.
iIntros "!> %sk %le_sk_n"...
rewrite /q_calls_poly...
rel_apply_l (refines_exp_l)...
rel_apply_r (refines_exp_r)...
inv_mk ((βₛ ↪ₛN (n;[]) ∗ γₛ ↪ₛN (n;[]) ∗ counter ↦ #0 ∗ countₛ ↦ₛ #0)
∨ (counter ↦ #1 ∗ countₛ ↦ₛ #1))%I "#Hinv"...
rel_vals ; iIntros "!>" (??) "#(%vmsg&->&->)"...
iApply (refines_na_inv with "[-$Hinv]") => //.
iIntros "[>[(βₛ&γₛ&count&countₛ)|(count&countₛ)] Hclose]"...
2: by (inv_cl "[-$Hclose]" ; rel_vals).
rewrite /rand_cipher...
rel_apply (refines_couple_UT n). 1: intuition auto ; lia.
iFrame "βₛ". iIntros "!>" (b bn) "βₛ". rel_pures_l.
(* Rewrite msg into g^k_msg for some k_msg. *)
destruct (log_g vmsg) as [k_msg ->].
(* Sample x on the left, and ((-x + k_msg) mod (S n)) on the right. *)
rel_apply (refines_couple_UT n (mod_minus _ k_msg)). 1: apply mod_minus_lt.
iFrame "γₛ". iIntros "!>" (x xn) "γₛ". rel_rand_r. iIntros (_).
rel_pures_r. rel_rand_r. iIntros (le_gx_n)...
inv_cl "[- $Hclose]"...
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_mult_r)...
rewrite -expgD -ssrnat.plusE.
assert ((g ^+ x) = (g ^+ (k_msg + mod_minus _ k_msg x)))%g as heq.
{
clear -xn le_gx_n.
rewrite /mod_minus.
destruct (x <? S n) eqn:h.
2:{ exfalso. eapply Nat.ltb_nlt. 1: eauto. apply PeanoNat.le_lt_n_Sm. done. }
pose proof (e := (expg_mod_order g)).
rewrite g_nontriv in e.
rewrite -[in LHS]e -{}[in RHS]e.
f_equal.
rewrite !ssrnat.plusE !ssrnat.minusE.
rewrite div.modnDmr.
rewrite ssrnat.addnC.
rewrite -ssrnat.addnA.
rewrite [ssrnat.addn x _]ssrnat.addnC ssrnat.addnA.
rewrite ssrnat.subnK.
- rewrite div.modnDl. reflexivity.
- apply /ssrnat.leP. move : (fin_to_nat_lt k_msg). lia.
}
rewrite -heq. rel_vals.
Qed.
(* Decryption is left inverse to encryption. We only consider valid messages. *)
Lemma ElGamal_correct :
⊢ refines top
(let, ("sk", "pk") := keygen #() in
λ:"msg", dec "sk" (enc "pk" "msg"))
(λ:"msg", "msg")
(lrel_G → lrel_G).
Proof with rel_red.
rewrite /keygen...
rel_apply_l refines_randU_l ; iIntros...
rel_apply_l (refines_exp_l)...
rel_arrow_val ; iIntros (??) "#(%msg&->&->)"...
rewrite /enc/dec... rel_apply_l refines_randU_l ; iIntros...
rel_apply_l (refines_exp_l)... rel_apply_l (refines_exp_l)...
rel_apply_l (refines_mult_l)... rel_apply_l (refines_exp_l)...
rel_apply_l (refines_inv_l)... rel_apply_l (refines_mult_l)...
rewrite -?expgM -ssrnat.multE -mulgA Nat.mul_comm mulgV mulg1.
rel_vals.
Qed.
End LogRel.
Section Ctx.
Context {G : forall `{!approxisRGS Σ}, clutch_group (vg:=vg) (cg:=cg)}.
Lemma A_real_real_tape `{!approxisRGS Σ}
(A : val)
(A_sem_typed : ⊢ REL A << A : (T_EG → lrel_bool))
: ⊢ REL (A pk_real) << (A pk_real_tape) : lrel_bool.
Proof. iApply refines_app. 1: iAssumption. iApply (real_real_tape (Δ:=[])). Qed.
Lemma A_real_tape_real `{!approxisRGS Σ}
(A : val)
(A_sem_typed : ⊢ REL A << A : (T_EG → lrel_bool))
: ⊢ REL (A pk_real_tape) << (A pk_real) : lrel_bool.
Proof. iApply refines_app. 1: iAssumption. iApply (real_tape_real (Δ:=[])). Qed.
Lemma ctx_real_real_tape (A : val)
(A_sem_typed : ∀ `{!approxisRGS Σ}, ⊢ REL A << A : (T_EG → lrel_bool))
: ∅ ⊨ A pk_real =ctx= A pk_real_tape : TBool.
Proof.
split ; apply (refines_sound approxisRΣ) ; intros.
- by apply A_real_real_tape.
- by apply A_real_tape_real.
Qed.
Lemma ctx_real_tape_C_DDH_real
(A : val) (A_sem_typed : ∀ `{!approxisRGS Σ}, ⊢ REL A << A : (T_EG → lrel_bool)) :
∅ ⊨ A pk_real_tape =ctx= A (fill C DDH_real) : TBool.
Proof. split ; apply (refines_sound approxisRΣ) ; intros.
- iApply refines_app. 1: iApply A_sem_typed. iApply (real_tape_C_DDH_real (Δ:=[])).
- iApply refines_app. 1: iApply A_sem_typed. iApply (C_DDH_real_real_tape (Δ:=[])).
Qed.
Lemma ctx_C_DDH_rand_rand_tape
(A : val) (A_sem_typed : ∀ `{!approxisRGS Σ}, ⊢ REL A << A : (T_EG → lrel_bool)) :
∅ ⊨ A (fill C DDH_rand) =ctx= A pk_rand_tape : TBool.
Proof. split ; apply (refines_sound approxisRΣ) ; intros.
- iApply refines_app. 1: iApply A_sem_typed. iApply (C_DDH_rand_rand_tape (Δ:=[])).
- iApply refines_app. 1: iApply A_sem_typed. iApply (rand_tape_C_DDH_rand (Δ:=[])).
Qed.
Lemma ctx_rand_tape_rand
(A : val) (A_sem_typed : ∀ `{!approxisRGS Σ}, ⊢ REL A << A : (T_EG → lrel_bool)) :
∅ ⊨ A pk_rand_tape =ctx= A pk_rand : TBool.
Proof. split ; apply (refines_sound approxisRΣ) ; intros.
- iApply refines_app. 1: iApply A_sem_typed. iApply (rand_tape_rand (Δ:=[])).
- iApply refines_app. 1: iApply A_sem_typed. iApply (rand_rand_tape (Δ:=[])).
Qed.
Lemma ctx_real_C_DDH_real
(A : val) (A_sem_typed : ∀ `{!approxisRGS Σ}, ⊢ REL A << A : (T_EG → lrel_bool)) :
∅ ⊨ A pk_real =ctx= A (fill C DDH_real) : TBool.
Proof. eapply ctx_equiv_transitive ; [ apply: ctx_real_real_tape | apply: ctx_real_tape_C_DDH_real ] => //. Qed.
Lemma ctx_C_DDH_rand_rand
(A : val) (A_sem_typed : ∀ `{!approxisRGS Σ}, ⊢ REL A << A : (T_EG → lrel_bool)) :
∅ ⊨ A (fill C DDH_rand) =ctx= A pk_rand : TBool.
Proof. eapply ctx_equiv_transitive ; [ apply: ctx_C_DDH_rand_rand_tape | apply: ctx_rand_tape_rand ] => //. Qed.
Theorem ElGamal_DDH_secure :
forall (A : val) (b : bool) (A_sem_typed : ∀ `{!approxisRGS Σ}, ⊢ REL A << A : (T_EG → lrel_bool)),
let AC := (λ:"v", A (fill C "v"))%V in
(advantage A pk_real pk_rand #b <= advantage AC DDH_real DDH_rand #b)%R.
Proof.
intros ; eapply (advantage_triangle _ _ (fill C DDH_real) _ _ 0).
3: right ; rewrite Rplus_0_l ; eauto.
2: eapply (advantage_triangle _ _ (fill C DDH_rand) _ _ _ 0) ; first last.
2: rewrite Rplus_0_r ; right ; eauto.
- eapply ctx_advantage_alt.
apply ctx_real_C_DDH_real => //.
- eapply ctx_advantage_alt.
apply ctx_C_DDH_rand_rand => //.
- simpl fill. rewrite /AC. eapply advantage_reduction_lr.
intros. eexists T_DDH, T_EG. intuition auto.
+ eapply eC_sem_typed.
+ eapply DDH_real_sem_typed.
+ eapply DDH_rand_sem_typed.
Unshelve. all: exact [].
Qed.
Let hybrid_EG := hybrid enc rand_cipher.
Let CPA_real_EG := CPA_real keygen enc.
Let CPA_rand_EG := CPA_rand keygen rand_cipher.
Definition advantage_hyb_EG_DDH Q A b k :=
(advantage (λ:"v", (λ:"v", A (hybrid_EG k Q "v"))%V (eC "v"))%V DDH_real DDH_rand #b).
Definition hybrid_advantages (Q : nat) (A : val) (b : bool) : R → Prop :=
λ ε, ∃ (k : Z), nonneg (advantage_hyb_EG_DDH Q A b k) = ε.
Definition ε_DDH_hyb_ub (Q : nat) (A : val) (b : bool) : R.
Proof.
eapply (completeness (hybrid_advantages Q A b)).
- exists 1. intros x. rewrite /hybrid_advantages. intros (k & <-).
apply advantage_bound_1.
- exists (advantage_hyb_EG_DDH Q A b 0).
rewrite /hybrid_advantages. exists 0. done.
Defined.
Fact ε_DDH_hyb_is_ub (Q : nat) (A : val) (b : bool) :
∀ (k : Z), (advantage_hyb_EG_DDH Q A b k <= ε_DDH_hyb_ub Q A b)%R.
Proof.
intros. rewrite /ε_DDH_hyb_ub.
destruct completeness as [x [ub lub]] => /=.
apply ub.
rewrite /hybrid_advantages. exists k. rewrite /advantage_hyb_EG_DDH. simpl. done.
Qed.
Lemma ElGamal_DDH_CPA_bound (Q : nat) (b : bool) :
∀ (A : val)
(A_sem_typed : ∀ `{!approxisRGS Σ}, ⊢ REL A << A : (T_EG → lrel_bool))
(ε_DDH : R)
(H_ε : ∀ (k : Z), (advantage_hyb_EG_DDH Q A b k <= ε_DDH)%R),
(advantage A (CPA_real_EG Q) (CPA_rand_EG Q) #b <= Q * ε_DDH)%R.
Proof.
intros.
eapply Claim_15_5.
1: iIntros ; iApply keygen_sem_typed.
1: iIntros ; iApply enc_sem_typed.
1: iIntros ; iApply rand_cipher_sem_typed.
1: iIntros ; iApply A_sem_typed.
rewrite /ε_OTS.
rewrite -/pk_real -/pk_rand.
etrans. 2: apply (H_ε k).
opose proof (ElGamal_DDH_secure (λ: "v", A (hybrid_EG k Q "v")) b) as h.
cbn -[advantage] in h. rewrite /advantage_hyb_EG_DDH.
apply h.
iIntros.
rel_arrow_val ; iIntros (??) "#h". rel_pures_r. rel_pures_l.
iApply refines_app. 1: iApply A_sem_typed. rewrite /hybrid_EG.
iApply refines_app. 2: valgroup_tactics.rel_vals.
iApply hybrid_typed.
1: iIntros ; iApply keygen_sem_typed.
1: iIntros ; iApply enc_sem_typed.
1: iIntros ; iApply rand_cipher_sem_typed.
Unshelve. all: exact [].
Qed.
Theorem ElGamal_DDH_CPA (Q : nat) (b : bool) :
∀ (A : val) (A_sem_typed : ∀ `{!approxisRGS Σ}, ⊢ REL A << A : (T_EG → lrel_bool)),
(advantage A (CPA_real_EG Q) (CPA_rand_EG Q) #b <= Q * ε_DDH_hyb_ub Q A b)%R.
Proof.
intros.
eapply ElGamal_DDH_CPA_bound => //.
apply ε_DDH_hyb_is_ub.
Qed.
End Ctx.
End ElGamal_sem.
The main difference with the Clutch version is that we use the "standard"
one-time security games for public key encryption defined in pubkey.v.
Another difference (including w.r.t. the ElGamal ported to Approxis) is that
pubkey.v relies on semantically well-typed adversaries instead of
syntactically typed ones, so we can drop the well-formedness check for
messages from the adversary. In the Clutch version of ElGamal, we explicitly
checked if the message was a valid group element. *)
From Ltac2 Require Import Ltac2.
Set Default Proof Mode "Classic".
From clutch.prob_lang Require Import advantage typing.tychk.
From clutch.approxis Require Import reltac2 approxis option.
From clutch.clutch.examples.crypto Require ElGamal_bijection.
From clutch.approxis.examples Require Import
valgroup diffie_hellman ElGamal_defs bounded_oracle pubkey advantage_laws.
From mathcomp Require Import ssrbool.
From mathcomp Require fingroup.fingroup.
Set Default Proof Using "All".
Import ElGamal_bijection.bij_nat.
Import valgroup_notation.
Section ElGamal_sem.
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'').
Definition pk_real := CPA_OTS_real keygen enc.
Definition pk_rand := CPA_OTS_rand keygen rand_cipher.
(* Unfold definitions and label the flips. We need to label the flip in
"query" since it occurs in a closure, and we want to relate it to an
eager sampling in the set-up phase in order to make DDH_real appear as a
sub-expression. *)
Definition pk_real_tape : expr :=
let: "β" := alloc #n in
let: "sk" := rand #n in
let: "pk" := vgval g^"sk" in
let: "count" := ref #0 in
let: "query" := λ:"msg",
(* let:m "msg" := vg_of_int "msg" in *)
assert (!"count" = #0) ;;;
"count" <- #1 ;;
let: "b" := rand("β") #n in
let: "B" := vgval g^"b" in
let: "C" := "pk"^"b" in
let: "X" := "msg" · "C" in
("B", "X") in
("pk", "query").
(* Pull out DDH_real/rand. This requires moving the sampling of "b" from "query"
to the initialisation. Only equivalent because "query" gets called only
once: only one message is encrypted, so only one nonce "b" is required, and
we can pre-sample it in the setup. *)
Definition eC : val :=
(λ: "DDH_real_or_rand",
let, ("pk", "B", "C") := "DDH_real_or_rand" in
let: "count" := ref #0 in
let: "query" := λ: "msg",
assert (!"count" = #0) ;;;
"count" <- #1 ;;
let: "X" := "msg" · "C" in
("B", "X") in
("pk", "query")).
Definition C : list ectx_item := [AppRCtx eC].
Definition C_DDH_real : expr := fill C DDH_real.
Definition C_DDH_rand : expr := fill C DDH_rand.
(* Inline DDH_rand and push the two random samplings not required for the key
generation back down (using tapes β and γ). *)
Definition pk_rand_tape : expr :=
let: "β" := alloc #n in
let: "γ" := alloc #n in
let: "sk" := rand #n in
let: "pk" := vgval g^"sk" in
let: "count" := ref #0 in
let: "query" := λ:"msg",
assert (!"count" = #0) ;;;
"count" <- #1 ;;
let: "b" := rand("β") #n in
let: "c" := rand("γ") #n in
let: "B" := vgval g^"b" in
let: "C" := vgval g^"c" in
let: "X" := "msg" · "C" in
("B", "X") in
("pk", "query").
Section LogRel.
Context `{!approxisRGS Σ}.
Context {G : clutch_group (vg:=vg) (cg:=cg)}. (* cg satisfies the group laws. *)
Context {Δ : listO (lrelC Σ)}.
Import valgroup_tactics.
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.
Lemma eC_sem_typed : ⊢ REL eC << eC : (T_DDH → T_EG).
Proof with rel_red.
rewrite /eC.
rel_arrow_val ; iIntros (??) "#h" ; ireds.
rewrite /T_DDH.
iDestruct "h" as "(%&%&%&%&->&->&h&h')".
iDestruct "h" as "(%&%&%&%&->&->&h&h'')".
iDestruct "h" as "(%&->&->)".
iDestruct "h'" as "(%&->&->)".
iDestruct "h''" as "(%&->&->)"...
inv_mk ((count ↦ #0 ∗ countₛ ↦ₛ #0) ∨ (count ↦ #1 ∗ countₛ ↦ₛ #1) )%I "#Hinv"...
rel_vals => //.
iIntros (??) "!> #(%vmsg&->&->)"...
iApply (refines_na_inv with "[-$Hinv]") => //.
iIntros "[>[(count&countₛ)|(count&countₛ)] Hclose]"...
all: (inv_cl "[-$Hclose]").
2 : rel_vals.
rel_apply_l (refines_mult_l); rel_pures_l.
rel_apply_r (refines_mult_r); rel_pures_r.
rel_vals.
Qed.
Lemma real_real_tape : ⊢ REL pk_real << pk_real_tape : T_EG.
Proof with rel_red.
rel_red. rewrite /keygen... rel_apply (refines_couple_UU n). 1: intuition auto ; lia.
iIntros "!> %sk %le_sk_n".
idtac...
rewrite /q_calls_poly...
rel_apply_l (refines_exp_l); rel_apply_r (refines_exp_r)...
inv_mk (βₛ ↪ₛN (n;[]) ∗ (counter ↦ #0 ∗ countₛ ↦ₛ #0) ∨ (counter ↦ #1 ∗ countₛ ↦ₛ #1) )%I "#Hinv"...
rel_vals ; iIntros "!>".
iIntros (??) "#(%msg&->&->)"...
iApply (refines_na_inv with "[-$Hinv]"); [done|].
iIntros "[>[(β&c&c')|(c&c')] Hclose]"...
2: inv_cl "[- $Hclose]" ; rel_vals.
rewrite /enc...
rel_apply (refines_couple_UT). 1: intuition auto ; lia.
iFrame. iIntros (b bn) "!> β". iredpures.
rel_rand_r. iIntros (_)...
inv_cl "[- $Hclose]"...
rel_apply_l (refines_exp_l); rel_apply_r (refines_exp_r)...
rel_apply_l (refines_exp_l); rel_apply_r (refines_exp_r)...
rel_apply_l (refines_mult_l); rel_apply_r (refines_mult_r)...
rel_vals.
Qed.
Lemma real_tape_real : ⊢ REL pk_real_tape << pk_real : T_EG.
Proof with rel_red.
rel_red. rewrite /keygen... rel_apply (refines_couple_UU n). 1: intuition auto ; lia.
iIntros "!> %sk %le_sk_n".
idtac...
rewrite /q_calls_poly...
rel_apply_l (refines_exp_l); rel_apply_r (refines_exp_r)...
inv_mk (β ↪N (n;[]) ∗ (count ↦ #0 ∗ counterₛ ↦ₛ #0) ∨ (count ↦ #1 ∗ counterₛ ↦ₛ #1) )%I "#Hinv"...
rel_vals ; iIntros "!>" (??) "#(%msg&->&->)"...
iApply (refines_na_inv with "[-$Hinv]"); [done|].
iIntros "[>[(β&c&c')|(c&c')] Hclose]"...
2: inv_cl "[- $Hclose]" ; rel_vals.
rewrite /enc...
rel_apply (refines_couple_TU n). 1: intuition auto ; lia.
iFrame. iIntros (b bn) "β". iredpures.
rel_rand_l. iIntros (_)...
inv_cl "[- $Hclose]".
rel_apply_l (refines_exp_l); rel_apply_r (refines_exp_r)...
rel_apply_l (refines_exp_l); rel_apply_r (refines_exp_r)...
rel_apply_l (refines_mult_l); rel_apply_r (refines_mult_r)...
rel_vals.
Qed.
Lemma real_tape_C_DDH_real : ⊢ REL pk_real_tape << C_DDH_real : T_EG.
Proof with rel_red.
rewrite /C_DDH_real /=. rel_red.
rel_apply (refines_couple_UU n). 1: intuition auto ; lia.
iIntros "!> %sk %le_sk_n".
idtac...
rel_apply (refines_couple_TU n). 1: intuition auto ; lia.
iFrame. iIntros (b bn) "β". iredpures.
rel_apply_l (refines_exp_l)...
rewrite -Nat2Z.inj_mul/eC...
do 3 (rel_apply_r (refines_exp_r))...
inv_mk ((β ↪N (n;[b]) ∗ count ↦ #0 ∗ countₛ ↦ₛ #0)
∨ (count ↦ #1 ∗ countₛ ↦ₛ #1))%I "#Hinv".
rel_vals ; iIntros "!>" (??) "#(%msg&->&->)"...
iApply (refines_na_inv with "[$Hinv]"); [done|].
iIntros "[>[(β&cnt&cnt')|(c&c')] Hclose]".
2: by (ireds ; inv_cl "[- $Hclose]" ; rel_vals).
do 6 iredl.
iredl. iIntros (_).
rel_load_r...
inv_cl "[- $Hclose]"...
rel_apply_l (refines_exp_l)...
rel_apply_l (refines_exp_l)...
rel_apply_l (refines_mult_l)...
rel_apply_r (refines_mult_r)...
rel_vals.
iExists _.
iSplit; [done|]. iPureIntro.
f_equal. f_equal.
rewrite ssrnat.multE.
(* TODO: Why is the coercion not inferred??? *)
rewrite (@fingroup.expgM (fingroup.FinGroup.Exports.fingroup_FinGroup__to__monoid_Monoid vgG) g).
done.
Qed.
Lemma C_DDH_real_real_tape : ⊢ REL C_DDH_real << pk_real_tape : T_EG.
Proof with rel_red.
rewrite /C_DDH_real /=. rel_red.
rel_apply (refines_couple_UU n). 1: intuition auto ; lia.
iIntros "!> %sk %le_sk_n".
idtac...
rewrite /q_calls_poly...
ireds.
rel_apply (refines_couple_UT). 1: intuition auto ; lia.
iFrame. iIntros (b bn) "!> βₛ". iredpures.
rewrite -Nat2Z.inj_mul/eC...
rel_apply_l (refines_exp_l)... rel_apply_l (refines_exp_l)... rel_apply_l (refines_exp_l)...
rel_apply_r (refines_exp_r)...
inv_mk ((βₛ ↪ₛN (n;[b]) ∗ count ↦ #0 ∗ countₛ ↦ₛ #0)
∨ (count ↦ #1 ∗ countₛ ↦ₛ #1))%I "#Hinv".
rel_vals ; iIntros "!>" (??) "#(%msg&->&->)"...
iApply (refines_na_inv with "[$Hinv]"); [done|].
iIntros "[[(β&cnt&cnt')|(c&c')] Hclose]"...
2: (rel_load_r ; rel_red ; inv_cl "[- $Hclose]" ; rel_vals).
rel_load_r. do 6 iredr. iIntros (_). rel_red.
inv_cl "[- $Hclose]"...
rel_apply_l (refines_mult_l)...
rel_apply_r (refines_exp_r)... rel_apply_r (refines_exp_r)...
rel_apply_r (refines_mult_r)...
rel_vals. iExists _. iSplit; [done|]. iPureIntro.
f_equal. f_equal.
rewrite ssrnat.multE.
(* TODO: Why is the coercion not inferred??? *)
rewrite (@fingroup.expgM (fingroup.FinGroup.Exports.fingroup_FinGroup__to__monoid_Monoid vgG) g).
done.
Qed.
Lemma C_DDH_rand_rand_tape : ⊢ REL C_DDH_rand << pk_rand_tape : T_EG.
Proof with rel_red.
rewrite /C_DDH_rand/C/eC /=. rel_red.
rel_apply (refines_couple_UU n). 1: intuition auto ; lia.
iIntros "!> %sk %le_sk_n".
idtac...
rel_apply (refines_couple_UT). 1: intuition auto ; lia.
iFrame "βₛ". iIntros (b bn) "!> βₛ". iredpures.
rel_apply (refines_couple_UT). 1: intuition auto ; lia.
iFrame "γₛ". iIntros (c cn) "!> γₛ". iredpures...
rel_apply_l (refines_exp_l)... rel_apply_l (refines_exp_l)... rel_apply_l (refines_exp_l)...
rel_apply_r (refines_exp_r)...
inv_mk ((βₛ ↪ₛN (n;[b]) ∗ γₛ ↪ₛN (n;[c]) ∗ count ↦ #0 ∗ countₛ ↦ₛ #0)
∨ (count ↦ #1 ∗ countₛ ↦ₛ #1))%I "#Hinv".
rel_vals ; iIntros "!>" (??) "#(%msg&->&->)"...
iApply (refines_na_inv with "[$Hinv]") => //.
iIntros "[>[(β'&γ'&cnt&cnt')|(cnt&cnt')] Hclose]". 2: idtac...
2: inv_cl "[- $Hclose]" ; rel_vals.
rel_load_l ; rel_load_r. iredpures. rel_store_r. rel_store_l.
iredpures. rel_randT_r. iIntros (_). do 3 iredr. iIntros (_).
rel_red.
inv_cl "[- $Hclose]".
rel_apply_l (refines_mult_l)...
rel_apply_r (refines_exp_r)... rel_apply_r (refines_exp_r)...
rel_apply_r (refines_mult_r)...
rel_vals.
Qed.
Lemma rand_tape_C_DDH_rand : ⊢ REL pk_rand_tape << C_DDH_rand : T_EG.
Proof with rel_red.
rewrite /C_DDH_rand/C/eC /=. rel_red.
rel_apply (refines_couple_UU n). 1: intuition auto ; lia.
iIntros "!> %sk %le_sk_n"...
rel_apply (refines_couple_TU n). 1: intuition auto ; lia.
iFrame "β". iIntros (b bn) "β"...
rel_apply (refines_couple_TU n). 1: intuition auto ; lia.
iFrame "γ". iIntros (c cn) "γ"...
rel_apply_l (refines_exp_l)...
rel_apply_r (refines_exp_r)... rel_apply_r (refines_exp_r)... rel_apply_r (refines_exp_r)...
inv_mk ((β ↪N (n;[b]) ∗ γ ↪N (n;[c]) ∗ count ↦ #0 ∗ countₛ ↦ₛ #0)
∨ (count ↦ #1 ∗ countₛ ↦ₛ #1))%I "#Hinv".
rel_vals ; iIntros "!>" (??) "#(%msg&->&->)"...
iApply (refines_na_inv with "[$Hinv]") => //.
iIntros "[>[(β'&γ'&cnt&cnt')|(cnt&cnt')] Hclose]" ; rel_load_l ; rel_load_r.
2: inv_cl "[- $Hclose]" ; rel_red ; rel_vals.
do 6 iredl. iIntros (_). rel_pures_r. rel_store_r. rel_pures_l. iredl. iIntros (_)...
inv_cl "[- $Hclose]" ; rel_red.
rel_apply_l (refines_exp_l)... rel_apply_l (refines_exp_l)... rel_apply_l (refines_mult_l)...
rel_apply_r (refines_mult_r)...
rel_vals.
Qed.
#[warnings="-notation-incompatible-prefix"]
Import mathcomp.fingroup.fingroup.
Lemma rand_tape_rand : ⊢ refines top pk_rand_tape pk_rand T_EG.
Proof with rel_red.
rel_red. rewrite /keygen...
rel_apply (refines_couple_UU n). 1: intuition auto ; lia.
iIntros "!> %sk %le_sk_n"...
rewrite /q_calls_poly...
rel_apply_l (refines_exp_l)...
rel_apply_r (refines_exp_r)...
inv_mk ((β ↪N (n;[]) ∗ γ ↪N (n;[]) ∗ count ↦ #0 ∗ counterₛ ↦ₛ #0)
∨ (count ↦ #1 ∗ counterₛ ↦ₛ #1))%I "#Hinv".
rel_vals ; iIntros "!>" (??) "#(%vmsg&->&->)"...
iApply (refines_na_inv with "[-$Hinv]") => //.
iIntros "[>[(β&γ&cnt&cnt')|(cnt&cnt')] Hclose]"...
2: by (inv_cl "[-$Hclose]" ; rel_vals).
rewrite /rand_cipher...
rel_apply (refines_couple_TU n). 1: intuition auto ; lia.
iFrame "β". iIntros (b bn) "β".
rel_pures_r.
(* Rewrite msg into g^k_msg for some k_msg. *)
destruct (log_g vmsg) as [k_msg ->].
(* Sample c on the left, and ((k_msg + c) mod (S n)) on the right. *)
rel_apply (refines_couple_TU n (mod_plus _ k_msg)).
1: apply mod_plus_lt.
iFrame "γ". iIntros (x xn) "γ". rel_rand_l. iIntros (_). rel_rand_l. iIntros (_)...
inv_cl "[- $Hclose]"...
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_mult_l)... rel_vals.
rewrite -fingroup.expgD -ssrnat.plusE.
assert ((g ^+ (k_msg + x)) = (g ^+ mod_plus _ k_msg x))%g as heq.
{ clear -xn.
rewrite /mod_plus.
destruct (x <? S n) eqn:h.
2:{ exfalso. eapply Nat.ltb_nlt. 1: eauto. apply PeanoNat.le_lt_n_Sm. done. }
pose proof (e := eq_sym (expg_mod_order g (k_msg+x))).
rewrite g_nontriv in e.
exact e.
}
rewrite -heq. eauto.
Qed.
Lemma rand_rand_tape : ⊢ refines top pk_rand pk_rand_tape T_EG.
Proof with rel_red.
rel_red. rewrite /keygen...
rel_apply (refines_couple_UU n). 1: intuition auto ; lia.
iIntros "!> %sk %le_sk_n"...
rewrite /q_calls_poly...
rel_apply_l (refines_exp_l)...
rel_apply_r (refines_exp_r)...
inv_mk ((βₛ ↪ₛN (n;[]) ∗ γₛ ↪ₛN (n;[]) ∗ counter ↦ #0 ∗ countₛ ↦ₛ #0)
∨ (counter ↦ #1 ∗ countₛ ↦ₛ #1))%I "#Hinv"...
rel_vals ; iIntros "!>" (??) "#(%vmsg&->&->)"...
iApply (refines_na_inv with "[-$Hinv]") => //.
iIntros "[>[(βₛ&γₛ&count&countₛ)|(count&countₛ)] Hclose]"...
2: by (inv_cl "[-$Hclose]" ; rel_vals).
rewrite /rand_cipher...
rel_apply (refines_couple_UT n). 1: intuition auto ; lia.
iFrame "βₛ". iIntros "!>" (b bn) "βₛ". rel_pures_l.
(* Rewrite msg into g^k_msg for some k_msg. *)
destruct (log_g vmsg) as [k_msg ->].
(* Sample x on the left, and ((-x + k_msg) mod (S n)) on the right. *)
rel_apply (refines_couple_UT n (mod_minus _ k_msg)). 1: apply mod_minus_lt.
iFrame "γₛ". iIntros "!>" (x xn) "γₛ". rel_rand_r. iIntros (_).
rel_pures_r. rel_rand_r. iIntros (le_gx_n)...
inv_cl "[- $Hclose]"...
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_mult_r)...
rewrite -expgD -ssrnat.plusE.
assert ((g ^+ x) = (g ^+ (k_msg + mod_minus _ k_msg x)))%g as heq.
{
clear -xn le_gx_n.
rewrite /mod_minus.
destruct (x <? S n) eqn:h.
2:{ exfalso. eapply Nat.ltb_nlt. 1: eauto. apply PeanoNat.le_lt_n_Sm. done. }
pose proof (e := (expg_mod_order g)).
rewrite g_nontriv in e.
rewrite -[in LHS]e -{}[in RHS]e.
f_equal.
rewrite !ssrnat.plusE !ssrnat.minusE.
rewrite div.modnDmr.
rewrite ssrnat.addnC.
rewrite -ssrnat.addnA.
rewrite [ssrnat.addn x _]ssrnat.addnC ssrnat.addnA.
rewrite ssrnat.subnK.
- rewrite div.modnDl. reflexivity.
- apply /ssrnat.leP. move : (fin_to_nat_lt k_msg). lia.
}
rewrite -heq. rel_vals.
Qed.
(* Decryption is left inverse to encryption. We only consider valid messages. *)
Lemma ElGamal_correct :
⊢ refines top
(let, ("sk", "pk") := keygen #() in
λ:"msg", dec "sk" (enc "pk" "msg"))
(λ:"msg", "msg")
(lrel_G → lrel_G).
Proof with rel_red.
rewrite /keygen...
rel_apply_l refines_randU_l ; iIntros...
rel_apply_l (refines_exp_l)...
rel_arrow_val ; iIntros (??) "#(%msg&->&->)"...
rewrite /enc/dec... rel_apply_l refines_randU_l ; iIntros...
rel_apply_l (refines_exp_l)... rel_apply_l (refines_exp_l)...
rel_apply_l (refines_mult_l)... rel_apply_l (refines_exp_l)...
rel_apply_l (refines_inv_l)... rel_apply_l (refines_mult_l)...
rewrite -?expgM -ssrnat.multE -mulgA Nat.mul_comm mulgV mulg1.
rel_vals.
Qed.
End LogRel.
Section Ctx.
Context {G : forall `{!approxisRGS Σ}, clutch_group (vg:=vg) (cg:=cg)}.
Lemma A_real_real_tape `{!approxisRGS Σ}
(A : val)
(A_sem_typed : ⊢ REL A << A : (T_EG → lrel_bool))
: ⊢ REL (A pk_real) << (A pk_real_tape) : lrel_bool.
Proof. iApply refines_app. 1: iAssumption. iApply (real_real_tape (Δ:=[])). Qed.
Lemma A_real_tape_real `{!approxisRGS Σ}
(A : val)
(A_sem_typed : ⊢ REL A << A : (T_EG → lrel_bool))
: ⊢ REL (A pk_real_tape) << (A pk_real) : lrel_bool.
Proof. iApply refines_app. 1: iAssumption. iApply (real_tape_real (Δ:=[])). Qed.
Lemma ctx_real_real_tape (A : val)
(A_sem_typed : ∀ `{!approxisRGS Σ}, ⊢ REL A << A : (T_EG → lrel_bool))
: ∅ ⊨ A pk_real =ctx= A pk_real_tape : TBool.
Proof.
split ; apply (refines_sound approxisRΣ) ; intros.
- by apply A_real_real_tape.
- by apply A_real_tape_real.
Qed.
Lemma ctx_real_tape_C_DDH_real
(A : val) (A_sem_typed : ∀ `{!approxisRGS Σ}, ⊢ REL A << A : (T_EG → lrel_bool)) :
∅ ⊨ A pk_real_tape =ctx= A (fill C DDH_real) : TBool.
Proof. split ; apply (refines_sound approxisRΣ) ; intros.
- iApply refines_app. 1: iApply A_sem_typed. iApply (real_tape_C_DDH_real (Δ:=[])).
- iApply refines_app. 1: iApply A_sem_typed. iApply (C_DDH_real_real_tape (Δ:=[])).
Qed.
Lemma ctx_C_DDH_rand_rand_tape
(A : val) (A_sem_typed : ∀ `{!approxisRGS Σ}, ⊢ REL A << A : (T_EG → lrel_bool)) :
∅ ⊨ A (fill C DDH_rand) =ctx= A pk_rand_tape : TBool.
Proof. split ; apply (refines_sound approxisRΣ) ; intros.
- iApply refines_app. 1: iApply A_sem_typed. iApply (C_DDH_rand_rand_tape (Δ:=[])).
- iApply refines_app. 1: iApply A_sem_typed. iApply (rand_tape_C_DDH_rand (Δ:=[])).
Qed.
Lemma ctx_rand_tape_rand
(A : val) (A_sem_typed : ∀ `{!approxisRGS Σ}, ⊢ REL A << A : (T_EG → lrel_bool)) :
∅ ⊨ A pk_rand_tape =ctx= A pk_rand : TBool.
Proof. split ; apply (refines_sound approxisRΣ) ; intros.
- iApply refines_app. 1: iApply A_sem_typed. iApply (rand_tape_rand (Δ:=[])).
- iApply refines_app. 1: iApply A_sem_typed. iApply (rand_rand_tape (Δ:=[])).
Qed.
Lemma ctx_real_C_DDH_real
(A : val) (A_sem_typed : ∀ `{!approxisRGS Σ}, ⊢ REL A << A : (T_EG → lrel_bool)) :
∅ ⊨ A pk_real =ctx= A (fill C DDH_real) : TBool.
Proof. eapply ctx_equiv_transitive ; [ apply: ctx_real_real_tape | apply: ctx_real_tape_C_DDH_real ] => //. Qed.
Lemma ctx_C_DDH_rand_rand
(A : val) (A_sem_typed : ∀ `{!approxisRGS Σ}, ⊢ REL A << A : (T_EG → lrel_bool)) :
∅ ⊨ A (fill C DDH_rand) =ctx= A pk_rand : TBool.
Proof. eapply ctx_equiv_transitive ; [ apply: ctx_C_DDH_rand_rand_tape | apply: ctx_rand_tape_rand ] => //. Qed.
Theorem ElGamal_DDH_secure :
forall (A : val) (b : bool) (A_sem_typed : ∀ `{!approxisRGS Σ}, ⊢ REL A << A : (T_EG → lrel_bool)),
let AC := (λ:"v", A (fill C "v"))%V in
(advantage A pk_real pk_rand #b <= advantage AC DDH_real DDH_rand #b)%R.
Proof.
intros ; eapply (advantage_triangle _ _ (fill C DDH_real) _ _ 0).
3: right ; rewrite Rplus_0_l ; eauto.
2: eapply (advantage_triangle _ _ (fill C DDH_rand) _ _ _ 0) ; first last.
2: rewrite Rplus_0_r ; right ; eauto.
- eapply ctx_advantage_alt.
apply ctx_real_C_DDH_real => //.
- eapply ctx_advantage_alt.
apply ctx_C_DDH_rand_rand => //.
- simpl fill. rewrite /AC. eapply advantage_reduction_lr.
intros. eexists T_DDH, T_EG. intuition auto.
+ eapply eC_sem_typed.
+ eapply DDH_real_sem_typed.
+ eapply DDH_rand_sem_typed.
Unshelve. all: exact [].
Qed.
Let hybrid_EG := hybrid enc rand_cipher.
Let CPA_real_EG := CPA_real keygen enc.
Let CPA_rand_EG := CPA_rand keygen rand_cipher.
Definition advantage_hyb_EG_DDH Q A b k :=
(advantage (λ:"v", (λ:"v", A (hybrid_EG k Q "v"))%V (eC "v"))%V DDH_real DDH_rand #b).
Definition hybrid_advantages (Q : nat) (A : val) (b : bool) : R → Prop :=
λ ε, ∃ (k : Z), nonneg (advantage_hyb_EG_DDH Q A b k) = ε.
Definition ε_DDH_hyb_ub (Q : nat) (A : val) (b : bool) : R.
Proof.
eapply (completeness (hybrid_advantages Q A b)).
- exists 1. intros x. rewrite /hybrid_advantages. intros (k & <-).
apply advantage_bound_1.
- exists (advantage_hyb_EG_DDH Q A b 0).
rewrite /hybrid_advantages. exists 0. done.
Defined.
Fact ε_DDH_hyb_is_ub (Q : nat) (A : val) (b : bool) :
∀ (k : Z), (advantage_hyb_EG_DDH Q A b k <= ε_DDH_hyb_ub Q A b)%R.
Proof.
intros. rewrite /ε_DDH_hyb_ub.
destruct completeness as [x [ub lub]] => /=.
apply ub.
rewrite /hybrid_advantages. exists k. rewrite /advantage_hyb_EG_DDH. simpl. done.
Qed.
Lemma ElGamal_DDH_CPA_bound (Q : nat) (b : bool) :
∀ (A : val)
(A_sem_typed : ∀ `{!approxisRGS Σ}, ⊢ REL A << A : (T_EG → lrel_bool))
(ε_DDH : R)
(H_ε : ∀ (k : Z), (advantage_hyb_EG_DDH Q A b k <= ε_DDH)%R),
(advantage A (CPA_real_EG Q) (CPA_rand_EG Q) #b <= Q * ε_DDH)%R.
Proof.
intros.
eapply Claim_15_5.
1: iIntros ; iApply keygen_sem_typed.
1: iIntros ; iApply enc_sem_typed.
1: iIntros ; iApply rand_cipher_sem_typed.
1: iIntros ; iApply A_sem_typed.
rewrite /ε_OTS.
rewrite -/pk_real -/pk_rand.
etrans. 2: apply (H_ε k).
opose proof (ElGamal_DDH_secure (λ: "v", A (hybrid_EG k Q "v")) b) as h.
cbn -[advantage] in h. rewrite /advantage_hyb_EG_DDH.
apply h.
iIntros.
rel_arrow_val ; iIntros (??) "#h". rel_pures_r. rel_pures_l.
iApply refines_app. 1: iApply A_sem_typed. rewrite /hybrid_EG.
iApply refines_app. 2: valgroup_tactics.rel_vals.
iApply hybrid_typed.
1: iIntros ; iApply keygen_sem_typed.
1: iIntros ; iApply enc_sem_typed.
1: iIntros ; iApply rand_cipher_sem_typed.
Unshelve. all: exact [].
Qed.
Theorem ElGamal_DDH_CPA (Q : nat) (b : bool) :
∀ (A : val) (A_sem_typed : ∀ `{!approxisRGS Σ}, ⊢ REL A << A : (T_EG → lrel_bool)),
(advantage A (CPA_real_EG Q) (CPA_rand_EG Q) #b <= Q * ε_DDH_hyb_ub Q A b)%R.
Proof.
intros.
eapply ElGamal_DDH_CPA_bound => //.
apply ε_DDH_hyb_is_ub.
Qed.
End Ctx.
End ElGamal_sem.