clutch.approxis.examples.ElGamal_syntactic
(* ElGamal encryption has one-time secrecy against chosen plaintext attack, in
the real/random paradigm. Following Rosulek's "The Joy of Crypto". *)
(* This is a direct port of clutch/examples/crypto/ElGamal.v. *)
(* It should be possible to derive the results of this file from the ones in
ElGamal_sem since the essential difference is that in this file, we only
assume that the adversary is syntactically rather than semantically
well-typed. Messages produced by the adversary are first filtered through
`vg_of_int` to obtain a group element. Thereafter, the semantic security
should apply. For this to work, one would reuse the standard security games,
and define a modified "safe" encryption function as
(λ pk msg, let:m msg := vg_of_int msg in enc pk msg)
*)
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 diffie_hellman ElGamal_defs.
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.
Set Default Proof Using "Type*".
Section ElGamal.
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.
(* Public key OTS-CPA*)
(* In the random game, rather than encrypting the message, "query" returns a
random ciphertext, i.e. two random group elements (B,X). *)
Definition pk_rand : expr :=
let, ("sk", "pk") := keygen #() 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: "x" := rand #n in
let, ("B", "X") := (vgval g^"b", vgval g^"x") in
("B", "X") in
("pk", "query").
(* The real game instead encrypts the message in "query". Below, we transform
pk_real into CDDH_real and CDH_rnd into pk_rnd. *)
Definition pk_real : expr :=
let, ("sk", "pk") := keygen #() in
let: "count" := ref #0 in
let: "query" := λ:"msg",
let:m "msg" := vg_of_int "msg" in
assert (!"count" = #0) ;;;
"count" <- #1 ;;
enc "pk" "msg" in
("pk", "query").
(* 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_rnd",
let, ("pk", "B", "C") := "DDH_real_or_rnd" in
let: "count" := ref #0 in
let: "query" := λ: "msg",
let:m "msg" := vg_of_int "msg" in
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",
let:m "msg" := vg_of_int "msg" in
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").
(* Finally, we connect pk_rand_tape to pk_rand. For this last step, we
want to show that multiplying the message with a random group element really
looks random, i.e. that msg⋅C = msg⋅g^c looks random, just like X = g^x. *)
(* We prove this by showing that multiplying by msg induces a bijection f on the
set fin (S n) we sampled x from: Since msg = g^k for some unique k, msg has
inverse g^(-k), i.e. we define f(c) := k+c (the inverse is obviously given
by (λ c, c-k)). Let msg⋅g^c = g^k⋅g^c = g^(k+c). Let x = f(c) be sampled along
the bijection f. Then g^x = g^f(c) = g^(c+k), as required. *)
(* Since we need to know the value of msg, we cannot combine this game-hop with
the previous one: in C_DDH_rand, c is sampled before msg is known. *)
Section LogRel.
Context `{!approxisRGS Σ}.
Context {G : clutch_group (vg:=vg) (cg:=cg)}. (* cg satisfies the group laws. *)
Context {Δ : listO (lrelC Σ)}.
#[local] Notation T := (interp τG Δ).
(* The semantic type of the Diffie-Hellman game(s). *)
Definition T_DH := Eval cbn in (interp τ_DDH Δ).
(* The semantic type of the ElGamal game(s). *)
Definition T_EG := Eval cbn in (interp τ_EG Δ).
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.
Lemma real_real_tape : ⊢ refines top 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...
rel_apply_l refines_exp_l; rel_apply_r refines_exp_r...
inv_mk (βₛ ↪ₛN (n;[]) ∗ (count ↦ #0 ∗ countₛ ↦ₛ #0) ∨ (count ↦ #1 ∗ countₛ ↦ₛ #1) )%I "#Hinv"...
rel_vals ; iIntros "!>" (??) "[%v[->->]]"...
rel_bind_l (vg_of_int _) ; rel_bind_r (vg_of_int _) ; rel_apply refines_bind.
1: iApply vg_of_int_lrel_G ; iExists _ ; eauto.
iIntros (??) "#(%_&%_'&[(->&->&->&->)|(->&->&%vmsg&->&->)])"... 1: rel_vals.
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 : ⊢ refines top 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...
rel_apply_l refines_exp_l; rel_apply_r refines_exp_r...
inv_mk (β ↪N (n;[]) ∗ (count ↦ #0 ∗ countₛ ↦ₛ #0) ∨ (count ↦ #1 ∗ countₛ ↦ₛ #1) )%I "#Hinv"...
rel_vals ; iIntros "!>" (??) "[%v[->->]]"...
rel_bind_l (vg_of_int _) ; rel_bind_r (vg_of_int _) ; rel_apply refines_bind.
1: iApply vg_of_int_lrel_G ; iExists _ ; eauto.
iIntros (??) "#(%_&%_'&[(->&->&->&->)|(->&->&%vmsg&->&->)])"... 1: rel_vals.
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 : ⊢ refines top 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.
rewrite -Nat2Z.inj_mul/eC...
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]) ∗ count ↦ #0 ∗ countₛ ↦ₛ #0)
∨ (count ↦ #1 ∗ countₛ ↦ₛ #1))%I "#Hinv".
rel_vals ; iIntros "!>" (??) "#(%msg&->&->)"...
rel_bind_l (vg_of_int _) ; rel_bind_r (vg_of_int _) ; rel_apply refines_bind.
1: iApply vg_of_int_lrel_G ; iExists _ ; eauto.
iIntros (??) "#(%_1&%_2&[(->&->&->&->)|(->&->&%vmsg&->&->)])"... 1: rel_vals.
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...
rewrite -expgM -ssrnat.multE. rel_vals.
Qed.
Lemma C_DDH_real_real_tape : ⊢ refines top 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...
ireds.
rel_apply (refines_couple_UT). 1: intuition auto ; lia.
iFrame. iIntros (b bn) "!> βₛ". iredpures.
rewrite -Nat2Z.inj_mul/eC...
rel_apply_r refines_exp_r...
rel_apply_l refines_exp_l...
rel_apply_l refines_exp_l...
rel_apply_l refines_exp_l...
inv_mk ((βₛ ↪ₛN (n;[b]) ∗ count ↦ #0 ∗ countₛ ↦ₛ #0)
∨ (count ↦ #1 ∗ countₛ ↦ₛ #1))%I "#Hinv".
rel_vals ; iIntros "!>" (??) "#(%msg&->&->)"...
rel_bind_l (vg_of_int _) ; rel_bind_r (vg_of_int _) ; rel_apply refines_bind.
1: iApply vg_of_int_lrel_G ; iExists _ ; eauto.
iIntros (??) "#(%_1&%_2&[(->&->&->&->)|(->&->&%vmsg&->&->)])"... 1: rel_vals.
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...
rewrite -expgM -ssrnat.multE. rel_vals.
Qed.
(* This assumption is too strong in this generality, since it does not mention
PPT indistinguishability and assumes a logical instead of contextual
refinement. *)
Definition DDH_ref := ⊢ refines top DDH_real DDH_rand T_DH.
(* If we do make this assumption though, we may prove the following refinement. *)
Lemma DDH_C_DDH_real_C_DDH_rand (DDH : DDH_ref) : ⊢ refines top C_DDH_real C_DDH_rand T_EG.
Proof with rel_red.
rewrite /C_DDH_real /C_DDH_rand.
rel_bind_l DDH_real. rel_bind_r DDH_rand.
rel_apply refines_app. 2: iApply DDH.
replace (T_DH → T_EG)%lrel with (interp (τ_DDH → τ_EG)%ty Δ) by auto.
iApply refines_typed. unfold eC. tychk => //.
Qed.
Lemma C_DDH_rand_rand_tape : ⊢ refines top 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_r refines_exp_r...
rel_apply_l refines_exp_l...
rel_apply_l refines_exp_l...
rel_apply_l refines_exp_l...
inv_mk ((βₛ ↪ₛN (n;[b]) ∗ γₛ ↪ₛN (n;[c]) ∗ count ↦ #0 ∗ countₛ ↦ₛ #0)
∨ (count ↦ #1 ∗ countₛ ↦ₛ #1))%I "#Hinv".
rel_vals ; iIntros "!>" (??) "#(%msg&->&->)"...
rel_bind_l (vg_of_int _) ; rel_bind_r (vg_of_int _) ; rel_apply refines_bind ;
[iApply vg_of_int_lrel_G ; iExists _ ; eauto|].
iIntros (??) "#(%_1&%_2&[(->&->&->&->)|(->&->&%vmsg&->&->)])"... 1: rel_vals.
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 : ⊢ refines top 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_r refines_exp_r... rel_apply_r refines_exp_r... rel_apply_r refines_exp_r...
rel_apply_l refines_exp_l...
inv_mk ((β ↪N (n;[b]) ∗ γ ↪N (n;[c]) ∗ count ↦ #0 ∗ countₛ ↦ₛ #0)
∨ (count ↦ #1 ∗ countₛ ↦ₛ #1))%I "#Hinv".
rel_vals ; iIntros "!>" (??) "#(%msg&->&->)"...
rel_bind_l (vg_of_int _) ; rel_bind_r (vg_of_int _) ; rel_apply refines_bind
; [iApply vg_of_int_lrel_G ; iExists _ ; eauto|].
iIntros (??) "#(%_1&%_2&[(->&->&->&->)|(->&->&%vmsg&->&->)])"... 1: rel_vals.
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.
Import ElGamal_bijection.bij_nat.
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"...
rel_apply_r refines_exp_r...
rel_apply_l refines_exp_l...
inv_mk ((β ↪N (n;[]) ∗ γ ↪N (n;[]) ∗ count ↦ #0 ∗ countₛ ↦ₛ #0)
∨ (count ↦ #1 ∗ countₛ ↦ₛ #1))%I "#Hinv".
rel_vals ; iIntros "!>" (??) "#(%msg&->&->)"...
rel_bind_l (vg_of_int _) ; rel_bind_r (vg_of_int _) ; rel_apply refines_bind
; [iApply vg_of_int_lrel_G ; iExists _ ; eauto|].
iIntros (??) "#(%_1&%_2&[(->&->&->&->)|(->&->&%vmsg&->&->)])"... 1: rel_vals.
iApply (refines_na_inv with "[-$Hinv]") => //.
iIntros "[>[(β&γ&cnt&cnt')|(cnt&cnt')] Hclose]"...
2: by (inv_cl "[-$Hclose]" ; rel_vals).
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...
rewrite -expgD -ssrnat.plusE.
rewrite /mod_plus...
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. rel_vals.
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"...
rel_apply_r refines_exp_r...
rel_apply_l refines_exp_l...
inv_mk ((βₛ ↪ₛN (n;[]) ∗ γₛ ↪ₛN (n;[]) ∗ count ↦ #0 ∗ countₛ ↦ₛ #0)
∨ (count ↦ #1 ∗ countₛ ↦ₛ #1))%I "#Hinv"...
rel_vals ; iIntros "!>" (??) "#(%msg&->&->)"...
rel_bind_l (vg_of_int _) ; rel_bind_r (vg_of_int _) ; rel_apply refines_bind
; [iApply vg_of_int_lrel_G ; iExists _ ; eauto|].
iIntros (??) "#(%_1&%_2&[(->&->&->&->)|(->&->&%vmsg&->&->)])"... 1: rel_vals.
iApply (refines_na_inv with "[-$Hinv]") => //.
iIntros "[>[(βₛ&γₛ&count&countₛ)|(count&countₛ)] Hclose]"...
2: by (inv_cl "[-$Hclose]" ; rel_vals).
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_r refines_exp_r... rel_apply_r refines_exp_r... rel_apply_r refines_mult_r...
rel_apply_l refines_exp_l... rel_apply_l refines_exp_l...
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,
i.e. integers that decode to a group element (in practice, this means that
the integer has to be smaller than the group order). *)
Lemma ElGamal_correct :
⊢ refines top
(let, ("sk", "pk") := keygen #() in
λ:"msg",
let:m "msg" := vg_of_int "msg" in
let: "c" := enc "pk" "msg" in
let: "vmsg" := dec "sk" "c" in
SOME ("vmsg"))
(λ:"msg",
let:m "vmsg" := vg_of_int "msg" in
SOME ("vmsg"))
(lrel_int → () + 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&->&->)"...
rel_bind_l (vg_of_int _) ; rel_bind_r (vg_of_int _) ; rel_apply refines_bind.
1: iApply vg_of_int_lrel_G ; iExists _ ; eauto.
iIntros (??) "#(%_1&%_2&[(->&->&->&->)|(->&->&%vmsg&->&->)])"... 1: rel_vals.
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 ctx_real_real_tape : ∅ ⊨ pk_real =ctx= pk_real_tape : τ_EG.
Proof. split ; apply (refines_sound approxisRΣ) ; intros ; [ apply: real_real_tape | apply: real_tape_real ]. Qed.
Lemma ctx_real_tape_C_DDH_real : ∅ ⊨ pk_real_tape =ctx= (fill C DDH_real) : τ_EG.
Proof. split ; apply (refines_sound approxisRΣ) ; intros ; [ apply: real_tape_C_DDH_real | apply: C_DDH_real_real_tape ]. Qed.
Lemma ctx_C_DDH_rand_rand_tape : ∅ ⊨ (fill C DDH_rand) =ctx= pk_rand_tape : τ_EG.
Proof. split ; apply (refines_sound approxisRΣ) ; intros ; [ apply: C_DDH_rand_rand_tape | apply: rand_tape_C_DDH_rand ]. Qed.
Lemma ctx_rand_tape_rand : ∅ ⊨ pk_rand_tape =ctx= pk_rand : τ_EG.
Proof. split ; apply (refines_sound approxisRΣ) ; intros ; [ apply: rand_tape_rand | apply: rand_rand_tape ]. Qed.
Lemma ctx_real_C_DDH_real : ∅ ⊨ pk_real =ctx= (fill C DDH_real) : τ_EG.
Proof. eapply ctx_equiv_transitive ; [ apply: ctx_real_real_tape | apply: ctx_real_tape_C_DDH_real ]. Qed.
Lemma ctx_C_DDH_rand_rand : ∅ ⊨ (fill C DDH_rand) =ctx= pk_rand : τ_EG.
Proof. eapply ctx_equiv_transitive ; [ apply: ctx_C_DDH_rand_rand_tape | apply: ctx_rand_tape_rand ]. Qed.
Theorem ElGamal_DH_secure :
forall (A : val), (⊢ᵥ A : (τ_EG → TBool)) ->
let AC := (λ:"v", A (fill C "v"))%E in
(advantage A pk_real pk_rand #true <= advantage AC DDH_real DDH_rand #true)%R.
Proof.
intros ? H ; 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.
- right. eapply ctx_advantage. 2: by tychk.
apply ctx_real_C_DDH_real.
- right. eapply ctx_advantage. 2: by tychk.
apply ctx_C_DDH_rand_rand.
- simpl. eapply advantage_reduction_ty. 1: apply H.
+ rewrite /eC /DDH_real /DDH_rand ; tychk => //.
+ apply DDH_real_typed.
+ apply DDH_rand_typed.
Qed.
(* The following lemmas make the unreasonably strong assumption that
DDH_real/rand are contextually equivalent when they really should only be
assumed to be computationally indistinguishable, but they illustrate how one
would combine the results in a logic with support for reasoning about
computational indistinguishability. *)
Lemma ctx_C_DDH_real_C_DDH_rand :
(∅ ⊨ DDH_real =ctx= DDH_rand : τ_DDH) →
(∅ ⊨ (fill C DDH_real) =ctx= (fill C DDH_rand) : τ_EG).
Proof.
replace (fill C _) with (fill_ctx [CTX_AppR eC] DDH_real) ; auto ;
replace (fill C _) with (fill_ctx [CTX_AppR eC] DDH_rand) => //.
intros DDH.
split.
- eapply ctx_refines_congruence.
2: apply DDH.
unfold eC. tychk => //.
- eapply ctx_refines_congruence.
2: apply DDH.
unfold eC. tychk => //.
Qed.
Lemma pk_ots_rnd_ddh (DDH : ∅ ⊨ DDH_real =ctx= DDH_rand : τ_DDH) :
(∅ ⊨ pk_real =ctx= pk_rand : τ_EG).
Proof.
eapply ctx_equiv_transitive.
- apply: ctx_real_C_DDH_real.
- eapply ctx_equiv_transitive.
+ apply: ctx_C_DDH_real_C_DDH_rand => //.
+ apply: ctx_C_DDH_rand_rand.
Qed.
End Ctx.
End ElGamal.
the real/random paradigm. Following Rosulek's "The Joy of Crypto". *)
(* This is a direct port of clutch/examples/crypto/ElGamal.v. *)
(* It should be possible to derive the results of this file from the ones in
ElGamal_sem since the essential difference is that in this file, we only
assume that the adversary is syntactically rather than semantically
well-typed. Messages produced by the adversary are first filtered through
`vg_of_int` to obtain a group element. Thereafter, the semantic security
should apply. For this to work, one would reuse the standard security games,
and define a modified "safe" encryption function as
(λ pk msg, let:m msg := vg_of_int msg in enc pk msg)
*)
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 diffie_hellman ElGamal_defs.
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.
Set Default Proof Using "Type*".
Section ElGamal.
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.
(* Public key OTS-CPA*)
(* In the random game, rather than encrypting the message, "query" returns a
random ciphertext, i.e. two random group elements (B,X). *)
Definition pk_rand : expr :=
let, ("sk", "pk") := keygen #() 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: "x" := rand #n in
let, ("B", "X") := (vgval g^"b", vgval g^"x") in
("B", "X") in
("pk", "query").
(* The real game instead encrypts the message in "query". Below, we transform
pk_real into CDDH_real and CDH_rnd into pk_rnd. *)
Definition pk_real : expr :=
let, ("sk", "pk") := keygen #() in
let: "count" := ref #0 in
let: "query" := λ:"msg",
let:m "msg" := vg_of_int "msg" in
assert (!"count" = #0) ;;;
"count" <- #1 ;;
enc "pk" "msg" in
("pk", "query").
(* 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_rnd",
let, ("pk", "B", "C") := "DDH_real_or_rnd" in
let: "count" := ref #0 in
let: "query" := λ: "msg",
let:m "msg" := vg_of_int "msg" in
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",
let:m "msg" := vg_of_int "msg" in
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").
(* Finally, we connect pk_rand_tape to pk_rand. For this last step, we
want to show that multiplying the message with a random group element really
looks random, i.e. that msg⋅C = msg⋅g^c looks random, just like X = g^x. *)
(* We prove this by showing that multiplying by msg induces a bijection f on the
set fin (S n) we sampled x from: Since msg = g^k for some unique k, msg has
inverse g^(-k), i.e. we define f(c) := k+c (the inverse is obviously given
by (λ c, c-k)). Let msg⋅g^c = g^k⋅g^c = g^(k+c). Let x = f(c) be sampled along
the bijection f. Then g^x = g^f(c) = g^(c+k), as required. *)
(* Since we need to know the value of msg, we cannot combine this game-hop with
the previous one: in C_DDH_rand, c is sampled before msg is known. *)
Section LogRel.
Context `{!approxisRGS Σ}.
Context {G : clutch_group (vg:=vg) (cg:=cg)}. (* cg satisfies the group laws. *)
Context {Δ : listO (lrelC Σ)}.
#[local] Notation T := (interp τG Δ).
(* The semantic type of the Diffie-Hellman game(s). *)
Definition T_DH := Eval cbn in (interp τ_DDH Δ).
(* The semantic type of the ElGamal game(s). *)
Definition T_EG := Eval cbn in (interp τ_EG Δ).
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.
Lemma real_real_tape : ⊢ refines top 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...
rel_apply_l refines_exp_l; rel_apply_r refines_exp_r...
inv_mk (βₛ ↪ₛN (n;[]) ∗ (count ↦ #0 ∗ countₛ ↦ₛ #0) ∨ (count ↦ #1 ∗ countₛ ↦ₛ #1) )%I "#Hinv"...
rel_vals ; iIntros "!>" (??) "[%v[->->]]"...
rel_bind_l (vg_of_int _) ; rel_bind_r (vg_of_int _) ; rel_apply refines_bind.
1: iApply vg_of_int_lrel_G ; iExists _ ; eauto.
iIntros (??) "#(%_&%_'&[(->&->&->&->)|(->&->&%vmsg&->&->)])"... 1: rel_vals.
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 : ⊢ refines top 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...
rel_apply_l refines_exp_l; rel_apply_r refines_exp_r...
inv_mk (β ↪N (n;[]) ∗ (count ↦ #0 ∗ countₛ ↦ₛ #0) ∨ (count ↦ #1 ∗ countₛ ↦ₛ #1) )%I "#Hinv"...
rel_vals ; iIntros "!>" (??) "[%v[->->]]"...
rel_bind_l (vg_of_int _) ; rel_bind_r (vg_of_int _) ; rel_apply refines_bind.
1: iApply vg_of_int_lrel_G ; iExists _ ; eauto.
iIntros (??) "#(%_&%_'&[(->&->&->&->)|(->&->&%vmsg&->&->)])"... 1: rel_vals.
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 : ⊢ refines top 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.
rewrite -Nat2Z.inj_mul/eC...
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]) ∗ count ↦ #0 ∗ countₛ ↦ₛ #0)
∨ (count ↦ #1 ∗ countₛ ↦ₛ #1))%I "#Hinv".
rel_vals ; iIntros "!>" (??) "#(%msg&->&->)"...
rel_bind_l (vg_of_int _) ; rel_bind_r (vg_of_int _) ; rel_apply refines_bind.
1: iApply vg_of_int_lrel_G ; iExists _ ; eauto.
iIntros (??) "#(%_1&%_2&[(->&->&->&->)|(->&->&%vmsg&->&->)])"... 1: rel_vals.
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...
rewrite -expgM -ssrnat.multE. rel_vals.
Qed.
Lemma C_DDH_real_real_tape : ⊢ refines top 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...
ireds.
rel_apply (refines_couple_UT). 1: intuition auto ; lia.
iFrame. iIntros (b bn) "!> βₛ". iredpures.
rewrite -Nat2Z.inj_mul/eC...
rel_apply_r refines_exp_r...
rel_apply_l refines_exp_l...
rel_apply_l refines_exp_l...
rel_apply_l refines_exp_l...
inv_mk ((βₛ ↪ₛN (n;[b]) ∗ count ↦ #0 ∗ countₛ ↦ₛ #0)
∨ (count ↦ #1 ∗ countₛ ↦ₛ #1))%I "#Hinv".
rel_vals ; iIntros "!>" (??) "#(%msg&->&->)"...
rel_bind_l (vg_of_int _) ; rel_bind_r (vg_of_int _) ; rel_apply refines_bind.
1: iApply vg_of_int_lrel_G ; iExists _ ; eauto.
iIntros (??) "#(%_1&%_2&[(->&->&->&->)|(->&->&%vmsg&->&->)])"... 1: rel_vals.
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...
rewrite -expgM -ssrnat.multE. rel_vals.
Qed.
(* This assumption is too strong in this generality, since it does not mention
PPT indistinguishability and assumes a logical instead of contextual
refinement. *)
Definition DDH_ref := ⊢ refines top DDH_real DDH_rand T_DH.
(* If we do make this assumption though, we may prove the following refinement. *)
Lemma DDH_C_DDH_real_C_DDH_rand (DDH : DDH_ref) : ⊢ refines top C_DDH_real C_DDH_rand T_EG.
Proof with rel_red.
rewrite /C_DDH_real /C_DDH_rand.
rel_bind_l DDH_real. rel_bind_r DDH_rand.
rel_apply refines_app. 2: iApply DDH.
replace (T_DH → T_EG)%lrel with (interp (τ_DDH → τ_EG)%ty Δ) by auto.
iApply refines_typed. unfold eC. tychk => //.
Qed.
Lemma C_DDH_rand_rand_tape : ⊢ refines top 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_r refines_exp_r...
rel_apply_l refines_exp_l...
rel_apply_l refines_exp_l...
rel_apply_l refines_exp_l...
inv_mk ((βₛ ↪ₛN (n;[b]) ∗ γₛ ↪ₛN (n;[c]) ∗ count ↦ #0 ∗ countₛ ↦ₛ #0)
∨ (count ↦ #1 ∗ countₛ ↦ₛ #1))%I "#Hinv".
rel_vals ; iIntros "!>" (??) "#(%msg&->&->)"...
rel_bind_l (vg_of_int _) ; rel_bind_r (vg_of_int _) ; rel_apply refines_bind ;
[iApply vg_of_int_lrel_G ; iExists _ ; eauto|].
iIntros (??) "#(%_1&%_2&[(->&->&->&->)|(->&->&%vmsg&->&->)])"... 1: rel_vals.
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 : ⊢ refines top 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_r refines_exp_r... rel_apply_r refines_exp_r... rel_apply_r refines_exp_r...
rel_apply_l refines_exp_l...
inv_mk ((β ↪N (n;[b]) ∗ γ ↪N (n;[c]) ∗ count ↦ #0 ∗ countₛ ↦ₛ #0)
∨ (count ↦ #1 ∗ countₛ ↦ₛ #1))%I "#Hinv".
rel_vals ; iIntros "!>" (??) "#(%msg&->&->)"...
rel_bind_l (vg_of_int _) ; rel_bind_r (vg_of_int _) ; rel_apply refines_bind
; [iApply vg_of_int_lrel_G ; iExists _ ; eauto|].
iIntros (??) "#(%_1&%_2&[(->&->&->&->)|(->&->&%vmsg&->&->)])"... 1: rel_vals.
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.
Import ElGamal_bijection.bij_nat.
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"...
rel_apply_r refines_exp_r...
rel_apply_l refines_exp_l...
inv_mk ((β ↪N (n;[]) ∗ γ ↪N (n;[]) ∗ count ↦ #0 ∗ countₛ ↦ₛ #0)
∨ (count ↦ #1 ∗ countₛ ↦ₛ #1))%I "#Hinv".
rel_vals ; iIntros "!>" (??) "#(%msg&->&->)"...
rel_bind_l (vg_of_int _) ; rel_bind_r (vg_of_int _) ; rel_apply refines_bind
; [iApply vg_of_int_lrel_G ; iExists _ ; eauto|].
iIntros (??) "#(%_1&%_2&[(->&->&->&->)|(->&->&%vmsg&->&->)])"... 1: rel_vals.
iApply (refines_na_inv with "[-$Hinv]") => //.
iIntros "[>[(β&γ&cnt&cnt')|(cnt&cnt')] Hclose]"...
2: by (inv_cl "[-$Hclose]" ; rel_vals).
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...
rewrite -expgD -ssrnat.plusE.
rewrite /mod_plus...
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. rel_vals.
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"...
rel_apply_r refines_exp_r...
rel_apply_l refines_exp_l...
inv_mk ((βₛ ↪ₛN (n;[]) ∗ γₛ ↪ₛN (n;[]) ∗ count ↦ #0 ∗ countₛ ↦ₛ #0)
∨ (count ↦ #1 ∗ countₛ ↦ₛ #1))%I "#Hinv"...
rel_vals ; iIntros "!>" (??) "#(%msg&->&->)"...
rel_bind_l (vg_of_int _) ; rel_bind_r (vg_of_int _) ; rel_apply refines_bind
; [iApply vg_of_int_lrel_G ; iExists _ ; eauto|].
iIntros (??) "#(%_1&%_2&[(->&->&->&->)|(->&->&%vmsg&->&->)])"... 1: rel_vals.
iApply (refines_na_inv with "[-$Hinv]") => //.
iIntros "[>[(βₛ&γₛ&count&countₛ)|(count&countₛ)] Hclose]"...
2: by (inv_cl "[-$Hclose]" ; rel_vals).
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_r refines_exp_r... rel_apply_r refines_exp_r... rel_apply_r refines_mult_r...
rel_apply_l refines_exp_l... rel_apply_l refines_exp_l...
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,
i.e. integers that decode to a group element (in practice, this means that
the integer has to be smaller than the group order). *)
Lemma ElGamal_correct :
⊢ refines top
(let, ("sk", "pk") := keygen #() in
λ:"msg",
let:m "msg" := vg_of_int "msg" in
let: "c" := enc "pk" "msg" in
let: "vmsg" := dec "sk" "c" in
SOME ("vmsg"))
(λ:"msg",
let:m "vmsg" := vg_of_int "msg" in
SOME ("vmsg"))
(lrel_int → () + 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&->&->)"...
rel_bind_l (vg_of_int _) ; rel_bind_r (vg_of_int _) ; rel_apply refines_bind.
1: iApply vg_of_int_lrel_G ; iExists _ ; eauto.
iIntros (??) "#(%_1&%_2&[(->&->&->&->)|(->&->&%vmsg&->&->)])"... 1: rel_vals.
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 ctx_real_real_tape : ∅ ⊨ pk_real =ctx= pk_real_tape : τ_EG.
Proof. split ; apply (refines_sound approxisRΣ) ; intros ; [ apply: real_real_tape | apply: real_tape_real ]. Qed.
Lemma ctx_real_tape_C_DDH_real : ∅ ⊨ pk_real_tape =ctx= (fill C DDH_real) : τ_EG.
Proof. split ; apply (refines_sound approxisRΣ) ; intros ; [ apply: real_tape_C_DDH_real | apply: C_DDH_real_real_tape ]. Qed.
Lemma ctx_C_DDH_rand_rand_tape : ∅ ⊨ (fill C DDH_rand) =ctx= pk_rand_tape : τ_EG.
Proof. split ; apply (refines_sound approxisRΣ) ; intros ; [ apply: C_DDH_rand_rand_tape | apply: rand_tape_C_DDH_rand ]. Qed.
Lemma ctx_rand_tape_rand : ∅ ⊨ pk_rand_tape =ctx= pk_rand : τ_EG.
Proof. split ; apply (refines_sound approxisRΣ) ; intros ; [ apply: rand_tape_rand | apply: rand_rand_tape ]. Qed.
Lemma ctx_real_C_DDH_real : ∅ ⊨ pk_real =ctx= (fill C DDH_real) : τ_EG.
Proof. eapply ctx_equiv_transitive ; [ apply: ctx_real_real_tape | apply: ctx_real_tape_C_DDH_real ]. Qed.
Lemma ctx_C_DDH_rand_rand : ∅ ⊨ (fill C DDH_rand) =ctx= pk_rand : τ_EG.
Proof. eapply ctx_equiv_transitive ; [ apply: ctx_C_DDH_rand_rand_tape | apply: ctx_rand_tape_rand ]. Qed.
Theorem ElGamal_DH_secure :
forall (A : val), (⊢ᵥ A : (τ_EG → TBool)) ->
let AC := (λ:"v", A (fill C "v"))%E in
(advantage A pk_real pk_rand #true <= advantage AC DDH_real DDH_rand #true)%R.
Proof.
intros ? H ; 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.
- right. eapply ctx_advantage. 2: by tychk.
apply ctx_real_C_DDH_real.
- right. eapply ctx_advantage. 2: by tychk.
apply ctx_C_DDH_rand_rand.
- simpl. eapply advantage_reduction_ty. 1: apply H.
+ rewrite /eC /DDH_real /DDH_rand ; tychk => //.
+ apply DDH_real_typed.
+ apply DDH_rand_typed.
Qed.
(* The following lemmas make the unreasonably strong assumption that
DDH_real/rand are contextually equivalent when they really should only be
assumed to be computationally indistinguishable, but they illustrate how one
would combine the results in a logic with support for reasoning about
computational indistinguishability. *)
Lemma ctx_C_DDH_real_C_DDH_rand :
(∅ ⊨ DDH_real =ctx= DDH_rand : τ_DDH) →
(∅ ⊨ (fill C DDH_real) =ctx= (fill C DDH_rand) : τ_EG).
Proof.
replace (fill C _) with (fill_ctx [CTX_AppR eC] DDH_real) ; auto ;
replace (fill C _) with (fill_ctx [CTX_AppR eC] DDH_rand) => //.
intros DDH.
split.
- eapply ctx_refines_congruence.
2: apply DDH.
unfold eC. tychk => //.
- eapply ctx_refines_congruence.
2: apply DDH.
unfold eC. tychk => //.
Qed.
Lemma pk_ots_rnd_ddh (DDH : ∅ ⊨ DDH_real =ctx= DDH_rand : τ_DDH) :
(∅ ⊨ pk_real =ctx= pk_rand : τ_EG).
Proof.
eapply ctx_equiv_transitive.
- apply: ctx_real_C_DDH_real.
- eapply ctx_equiv_transitive.
+ apply: ctx_C_DDH_real_C_DDH_rand => //.
+ apply: ctx_C_DDH_rand_rand.
Qed.
End Ctx.
End ElGamal.