clutch.approxis.examples.kemdem_hybrid_cpa_instance_otp
From Ltac2 Require Import Ltac2.
Set Default Proof Mode "Classic".
From clutch.prob_lang Require Import advantage typing.tychk.
From clutch.approxis Require Import map reltac2 approxis option.
From clutch.clutch.examples.crypto Require ElGamal_bijection.
From clutch.approxis.examples Require Import
valgroup diffie_hellman security_aux option xor
ElGamal_defs bounded_oracle pubkey advantage_laws iterable_expression.
From clutch.approxis.examples Require symmetric_init kemdem_hybrid_cpa_generic
one_time_pad kemdem_hybrid_cpa_instance_rf.
From mathcomp Require Import ssrbool.
From mathcomp Require fingroup.fingroup.
Set Default Proof Using "All".
Import ElGamal_bijection.bij_nat.
Import valgroup_notation.
Import map.
Section Hybrid_scheme.
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 *)
Let N := S n''.
Let SymKey := n''.
Let Input := n''.
Let SymOutput := n''.
Variable xor_struct : XOR (Key := SymOutput) (Support := SymOutput).
Section logrel.
Context `{!approxisRGS Σ}.
Context {G : clutch_group (vg:=vg) (cg:=cg)}.
Context {Δ : listO (lrelC Σ)}.
Definition lrel_sym_key : lrel Σ := lrel_int_bounded 0 SymKey.
Definition lrel_key : lrel Σ := lrel_G.
Definition lrel_output : lrel Σ := lrel_int_bounded 0 SymOutput.
Definition lrel_input : lrel Σ := lrel_int_bounded 0 Input.
Variable xor_spec : XOR_spec.
Local Tactic Notation "rel_bind" open_constr(pat) :=
rel_bind_l pat; rel_bind_r pat.
Local Ltac refines_until tac :=
repeat (rel_pure_l; rel_pure_r; try (rel_apply tac)).
Axiom G_Z_img : list Z.
Axiom vg_of_int_dom : ∀ n, n ∈ G_Z_img
→ ∃ x, vg_of_int_sem n = Some x.
Axiom int_of_vg_img : ∀ x, int_of_vg_sem x ∈ G_Z_img.
Axiom len_G_Z_img : length G_Z_img = N.
Axiom nodup_G_Z_img : NoDup G_Z_img.
Fixpoint val_of_list {X} (l : list X) (f : X → val) : val := match l with
| [] => #()
| h :: t => (f h, val_of_list t f)
end.
Definition find : val :=
rec: "find" "l" "x" :=
if: "l" = #() then #()
else if: (Fst "l") = "x" then #0
else #1 + ("find" (Snd "l") "x").
Definition lookup_expr : val :=
rec: "lookup" "l" "i" :=
if: "l" = #() then #()
else if: "i" = #0 then (Fst "l")
else "lookup" (Snd "l") ("i" - #1).
Definition index_of : val :=
rec: "index_of" "l" "x" :=
if: "l" = #() then #()
else if: (Fst "l") = "x" then #0
else #1 + "index_of" (Snd "l") "x".
Definition vg_of_symkey : val :=
λ: "key",
match: vg_of_int (lookup_expr (val_of_list G_Z_img (λ n, #n)) "key") with
| NONE => #()
| SOME "x" => "x"
end.
Definition symkey_of_vg : val :=
λ: "kg",
index_of (val_of_list G_Z_img (λ n, #n)) (int_of_vg "kg").
Fixpoint list_index_of (l : list Z) (n : Z) : nat := match l with
| [] => 0
| h :: t => if (h =? n)%Z then 0 else 1 + list_index_of t n
end.
Lemma list_index_of_lt (l : list Z) (n : Z) :
n ∈ l → list_index_of l n < length l.
Proof. induction l as [|h t IHt]; intros H.
- inversion H.
- simpl. destruct (h =? n)%Z eqn:eqhead.
+ lia.
+ apply Z.eqb_neq in eqhead.
rewrite <- Nat.succ_lt_mono.
apply IHt.
apply elem_of_cons in H; destruct H as [H|H]; last assumption.
exfalso; apply eqhead; lia.
Qed.
Lemma index_of_list_lt_l (l : list Z) :
∀ x, x ∈ l →
∀ K e E A,
refines E (fill K (Val #(list_index_of l x))) e A
⊢ refines E (fill K (index_of (val_of_list l (λ n, #n)) #x)) e A
.
Proof with rel_pures_l.
iInduction l as [|h t] "IH".
- iIntros (x H); inversion H.
- iIntros (x H K e E A) "Hrel".
rewrite /index_of...
destruct (bool_decide (#h = #x)) eqn:eqhead.
+ apply bool_decide_eq_true in eqhead...
injection eqhead; clear eqhead; intros eqhead.
simpl. rewrite eqhead. rewrite Z.eqb_refl.
replace (Z.of_nat 0) with 0%Z by lia. iAssumption.
+ rel_pure_l. rel_pure_l.
apply bool_decide_eq_false in eqhead.
rel_apply "IH".
* rewrite elem_of_cons in H. destruct H as [H|H].
{ exfalso; apply eqhead; f_equal. symmetry. f_equal. assumption. }
iPureIntro; assumption.
* simpl.
assert (Hbool : (h =? x)%Z = false).
{ apply Z.eqb_neq. intro contra; apply eqhead; rewrite contra; reflexivity. }
rewrite Hbool; clear Hbool...
replace (Z.of_nat (S (list_index_of t x))) with
(1 + Z.of_nat (list_index_of t x))%Z by lia.
rel_apply "Hrel".
Qed.
Lemma index_of_list_lt_r (l : list Z) :
∀ x, x ∈ l →
∀ K e E A,
refines E e (fill K (Val #(list_index_of l x))) A
⊢ refines E e (fill K (index_of (val_of_list l (λ n, #n)) #x)) A
.
Proof with rel_pures_r.
iInduction l as [|h t] "IH".
- iIntros (x H); inversion H.
- iIntros (x H K e E A) "Hrel".
rewrite /index_of...
destruct (bool_decide (#h = #x)) eqn:eqhead.
+ apply bool_decide_eq_true in eqhead...
injection eqhead; clear eqhead; intros eqhead.
simpl. rewrite eqhead. rewrite Z.eqb_refl.
replace (Z.of_nat 0) with 0%Z by lia. iAssumption.
+ rel_pure_r. rel_pure_r.
apply bool_decide_eq_false in eqhead.
rel_apply "IH".
* rewrite elem_of_cons in H. destruct H as [H|H].
{ exfalso; apply eqhead; f_equal. symmetry. f_equal. assumption. }
iPureIntro; assumption.
* simpl.
assert (Hbool : (h =? x)%Z = false).
{ apply Z.eqb_neq. intro contra; apply eqhead; rewrite contra; reflexivity. }
rewrite Hbool; clear Hbool...
replace (Z.of_nat (S (list_index_of t x))) with
(1 + Z.of_nat (list_index_of t x))%Z by lia.
rel_apply "Hrel".
Qed.
Lemma lookup_list_lt_l {X} (l : list X) (to_val : X → val) :
∀ n, n < length l →
∃ x, (l !! n) = Some x
∧ ∀ K e E A,
refines E (fill K (Val (to_val x))) e A
⊢ refines E (fill K (lookup_expr (val_of_list l to_val) #n)) e A.
Proof with (rel_pures_l; rel_pures_r). intros * Hlt.
apply lookup_lt_is_Some_2 in Hlt as Hsome.
destruct Hsome as [x Hsome]. exists x. split; first assumption.
iIntros (K e E A) "Hrel".
iInduction l as [|h t] "IH" forall (n Hlt Hsome).
- inversion Hlt.
- rewrite /lookup_expr...
destruct (bool_decide (#n = #0)) eqn:eqn0.
+ apply bool_decide_eq_true in eqn0. injection eqn0.
replace 0%Z with (Z.of_nat 0) by lia.
clear eqn0; intros eqn0.
apply Nat2Z.inj in eqn0.
rewrite eqn0 in Hsome. simpl in Hsome.
injection Hsome. intros eqx; rewrite eqx...
iAssumption.
+ rel_pure_l. rel_pure_l. rel_pure_l.
apply bool_decide_eq_false in eqn0.
destruct n as [|n']; first (exfalso; apply eqn0; f_equal).
replace (Z.of_nat (S n') - 1)%Z with (Z.of_nat n')%Z by lia.
rel_apply_l "IH"; last iAssumption; iPureIntro.
* simpl in Hlt. lia.
* simpl in Hsome. apply Hsome.
Qed.
Lemma lookup_list_lt_r {X} (l : list X) (to_val : X → val) :
∀ n, n < length l →
∃ x, (l !! n) = Some x
∧ ∀ K e E A,
refines E e (fill K (Val (to_val x))) A
⊢ refines E e (fill K (lookup_expr (val_of_list l to_val) #n)) A
.
Proof with (rel_pures_l; rel_pures_r). intros * Hlt.
apply lookup_lt_is_Some_2 in Hlt as Hsome.
destruct Hsome as [x Hsome]. exists x. split; first assumption.
iIntros (K e E A) "Hrel".
iInduction l as [|h t] "IH" forall (n Hlt Hsome).
- inversion Hlt.
- rewrite /lookup_expr...
destruct (bool_decide (#n = #0)) eqn:eqn0.
+ apply bool_decide_eq_true in eqn0. injection eqn0.
replace 0%Z with (Z.of_nat 0) by lia.
clear eqn0; intros eqn0.
apply Nat2Z.inj in eqn0.
rewrite eqn0 in Hsome. simpl in Hsome.
injection Hsome. intros eqx; rewrite eqx...
iAssumption.
+ rel_pure_r. rel_pure_r. rel_pure_r.
apply bool_decide_eq_false in eqn0.
destruct n as [|n']; first (exfalso; apply eqn0; f_equal).
replace (Z.of_nat (S n') - 1)%Z with (Z.of_nat n')%Z by lia.
rel_apply_l "IH"; last iAssumption; iPureIntro.
* simpl in Hlt. lia.
* simpl in Hsome. apply Hsome.
Qed.
Lemma vg_of_symkey_sem_typed :
⊢ (lrel_car (lrel_sym_key → lrel_G)) vg_of_symkey vg_of_symkey.
Proof with rel_pures_l; rel_pures_r. rewrite /vg_of_symkey.
iIntros (v1 v2 [k [eq1 [eq2 Hkbound]]]); subst.
iModIntro...
rel_bind (lookup_expr _ _).
rewrite -(Z2Nat.id k); last lia.
pose proof (lookup_list_lt_l G_Z_img (λ n : Z, #n) (Z.to_nat k)) as H'.
rewrite len_G_Z_img in H'.
rewrite /SymKey in Hkbound.
assert (H : Z.to_nat k < N) by lia.
apply H' in H as Hrel.
destruct Hrel as [x [eqx Hrel]].
iPoseProof (Hrel) as "Hrel".
rel_apply "Hrel".
clear H' H Hrel.
pose proof (lookup_list_lt_r G_Z_img (λ n : Z, #n) (Z.to_nat k)) as H'.
rewrite len_G_Z_img in H'.
rewrite /SymKey in Hkbound.
assert (H : Z.to_nat k < N) by lia.
apply H' in H.
destruct H as [y [eqy Hrel]].
iClear "Hrel".
iPoseProof (Hrel) as "Hrel".
rel_apply "Hrel".
clear H' Hrel. iClear "Hrel".
rewrite eqx in eqy. injection eqy.
intros eqxy. rewrite eqxy.
rel_apply_l vg_of_int_correct; last
rel_apply_r vg_of_int_correct;
try (iSplit;
first (rewrite /to_val_type_rel;
iIntros (n); iExists _; done);
rewrite /to_val_type_rel;
iIntros ([xg|]);
iExists _, _; iPureIntro;
try (right; repeat split;
eexists; split; by done);
(left; repeat split;
eexists; split; done)).
pose proof (vg_of_int_dom y) as H'.
rewrite eqy in eqx.
apply list_elem_of_lookup_2 in eqx.
apply H' in eqx as H; clear H'.
destruct H as [xg eqvgy].
rewrite eqvgy...
rel_vals.
Qed.
Lemma symkey_of_vg_sem_typed :
⊢ (lrel_car (lrel_G → lrel_sym_key)) symkey_of_vg symkey_of_vg.
Proof with rel_pures_l; rel_pures_r. rewrite /symkey_of_vg.
iIntros (v1 v2 [xg [eq1 eq2]]); subst.
iModIntro...
rel_apply_l int_of_vg_correct; last
rel_apply_r int_of_vg_correct;
try (rewrite /to_val_type_rel; iSplit;
iIntros (x); iExists _; iPureIntro; done).
rel_apply index_of_list_lt_l; last
rel_apply index_of_list_lt_r;
try (apply int_of_vg_img).
rel_vals.
iExists _. iPureIntro; repeat split; try done;
rewrite /SymKey.
- lia.
- apply Nat2Z.inj_le.
apply PeanoNat.lt_n_Sm_le.
rewrite -/N.
rewrite -len_G_Z_img.
apply list_index_of_lt.
apply int_of_vg_img.
Qed.
Definition otp_enc : val := one_time_pad.otp_enc n'' xor_struct.
Definition otp_dec : val := one_time_pad.otp_dec n'' xor_struct.
(* The four following definition are very similar.
The only difference is that otp_... takes a value as input within
the language, whereas senc and sdec take a list of locations
at the meta-level (as a crocq function )*)
Definition otp_enc_vg : val :=
(λ: "key",
otp_enc (symkey_of_vg "key"))%V.
Definition otp_dec_vg : val :=
(λ: "key",
otp_dec (symkey_of_vg "key"))%V.
Definition senc (ls : list loc) : val := otp_enc_vg.
Definition sdec (ls : list loc) : val := otp_dec_vg.
Definition otp_scheme_vg : expr :=
(Val (senc []), Val (sdec [])).
#[local] Instance otp_SYM_param : symmetric_init.SYM_init_params :=
one_time_pad.SYM_otp_param N.
#[local] Instance sym_otp_scheme_inst : symmetric_init.SYM_init := {|
symmetric_init.keygen := λ: <>, vg_of_symkey (one_time_pad.otp_keygen SymKey #())
; symmetric_init.enc_scheme := otp_scheme_vg
; symmetric_init.rand_cipher := one_time_pad.otp_rand_cipher n''
|}.
#[local] Instance elgamal_params : pubkey_class.ASYM_params :=
kemdem_hybrid_cpa_generic.asym_params N N N.
#[local] Instance elgamal_scheme : pubkey_class.ASYM := {|
pubkey_class.keygen := keygen
; pubkey_class.enc := enc
; pubkey_class.dec := dec
; pubkey_class.rand_cipher := (λ: <>, let: "a" := rand #N in let: "b" := rand #N in (vgval g^"a", vgval g^"b"))
|}.
Ltac simpl_exp := try (rel_apply refines_exp_l; rel_pures_l);
try (rel_apply refines_exp_r; rel_pures_r).
Ltac simpl_mult := try (rel_apply refines_mult_l; rel_pures_l);
try (rel_apply refines_mult_r; rel_pures_r).
Definition init_scheme (e : expr) : expr :=
let: "scheme" := symmetric_init.get_enc_scheme symmetric_init.sym_scheme
#() in
e "scheme".
(* ASSUMPTIONS ON THE SYMMETRIC SCHEME FOR CORRECTNESS *)
Lemma lrel_input_refl : forall v v', lrel_input v v' -∗ lrel_input v v.
Proof. intros v v'. iIntros ([x [eq1 [eq2 Hbound]]]).
iExists x. iPureIntro; done.
Qed.
Definition P0l (lls : list loc) : iProp Σ := match lls with
| [] => True%I
| _ => False%I
end.
Definition P0r (rls : list loc) : iProp Σ := match rls with
| [] => True%I
| _ => False%I
end.
Definition Pl (lls : list loc) : iProp Σ := match lls with
| [] => True%I
| _ => False%I
end.
Definition Pr (rls : list loc) : iProp Σ := match rls with
| [] => True%I
| _ => False%I
end.
Definition Plr (lls rls : list loc) : iProp Σ := match lls, rls with
| [], [] => True%I
| _, _ => False%I
end.
#[local] Instance initializable_sym_scheme_defs_otp :
(@kemdem_hybrid_cpa_generic.initializable_sym_scheme_defs Σ).
Proof. unshelve econstructor.
- exact senc.
- exact sdec.
- exact P0l.
- exact P0r.
- exact Pl.
- exact Pr.
- exact Plr.
Defined.
Lemma otp_enc_sem_typed :
∀ lls rls (𝒩 : namespace) (P : iProp Σ),
(∃ (Q : iProp Σ),
P ⊣⊢
(Q
∗ Plr lls rls)
) →
na_invP 𝒩 P
⊢ refines top (senc lls)
(senc rls) (lrel_key → lrel_input → lrel_output).
Proof with (rel_pures_l; rel_pures_r).
intros lls rls 𝒩 P [Q H].
apply bi.equiv_entails in H.
destruct H as [H1 H2].
iIntros "#Inv".
rewrite /senc.
rel_arrow_val.
iIntros (v1 v2 [kg [eq1 eq2]]); subst.
rewrite /otp_enc_vg/otp_enc/one_time_pad.otp_enc.
destruct lls as [|mapref [|tmp lls]];
destruct rls as [|mapref' [|tmp' rls]];
try (simpl in H1;
rel_apply refines_na_inv; iSplitL; first iAssumption;
iIntros "[HP _]"; rel_pures_l; rel_pures_r;
iExFalso;
iPoseProof (H1 with "HP") as "[_ contra]";
iAssumption)...
rel_bind (symkey_of_vg _); rel_apply refines_bind...
{ rel_apply refines_app; rel_vals;
first iApply symkey_of_vg_sem_typed; iExists _; done. }
iIntros (v1 v2 [k [eq1 [eq2 Hkbounds]]]); subst...
rel_arrow_val.
iIntros (v1 v2 [msg [eq1 [eq2 Hmsgbounds]]]); subst...
rewrite -(Z2Nat.id k); last lia.
rel_apply xor_correct_l; try lia.
rel_apply xor_correct_r; try lia.
rel_vals.
iExists _. iPureIntro; repeat split; try lia.
epose proof (xor_dom (Z.to_nat msg) _ (Z.to_nat k)).
lia.
Unshelve.
lia.
Qed.
Lemma P0_P_l : ∀ lls, P0l lls -∗ Pl lls.
Proof. rewrite /P0l/Pl.
intros [|ll [|tmp lls]]; iIntros "H"; iAssumption.
Qed.
Lemma P0_P_r : ∀ rls, P0r rls -∗ Pr rls.
Proof. rewrite /P0l/Pl.
intros [|ll [|tmp lls]]; iIntros "H"; iAssumption.
Qed.
Lemma P0lr_Plr : ∀ lls rls, P0l lls -∗ P0r rls -∗ Plr lls rls.
Proof. rewrite /P0l/P0r/Plr. intros [|ll [|tmp lls]] [|rl [|tmp' rls]];
iIntros "Hl Hr"; iAssumption.
Qed.
Lemma refines_init_otp_scheme_l : forall K e E A,
(∀ lls,
P0l lls -∗
refines E
(fill K (senc lls, sdec lls))
e A)
⊢ refines E
(fill K (symmetric_init.get_enc_scheme symmetric_init.sym_scheme #()))
e A.
Proof. intros *. iIntros "H".
rewrite /symmetric_init.get_enc_scheme.
rewrite /symmetric_init.sym_scheme.
rel_pure_l.
rel_pure_l.
rel_pure_l.
rel_pure_l.
rel_pure_l.
rewrite /otp_scheme_vg.
rel_apply "H".
done.
Qed.
Lemma refines_init_otp_scheme_r : forall K e E A,
(∀ lls,
P0r lls -∗
refines E
e
(fill K (senc lls, sdec lls))
A)
⊢ refines E
e
(fill K (symmetric_init.get_enc_scheme symmetric_init.sym_scheme #()))
A.
Proof. intros *. iIntros "H".
rewrite /symmetric_init.get_enc_scheme.
rewrite /symmetric_init.sym_scheme.
rel_pure_r.
rel_pure_r.
rel_pure_r.
rel_pure_r.
rel_pure_r.
rewrite /otp_scheme_vg.
rel_apply "H".
done.
Qed.
Lemma refines_otp_keygen_couple :forall K K' E A,
(∀ key,
(lrel_car lrel_key) key key -∗
refines E
(fill K (Val key))
(fill K' (Val key))
A)
⊢ refines E
(fill K (symmetric_init.keygen #()))
(fill K' (symmetric_init.keygen #()))
A.
Proof with (rel_pures_l; rel_pures_r).
intros *. iIntros "Hrelkey".
rewrite /symmetric_init.keygen/sym_otp_scheme_inst...
rewrite /one_time_pad.otp_keygen...
rel_apply refines_couple_UU; first done.
iModIntro; iIntros (k Hkbound).
rewrite /vg_of_symkey.
pose proof (lookup_list_lt_l G_Z_img (λ n : Z, #n) k).
rewrite /SymKey in Hkbound.
apply PeanoNat.le_lt_n_Sm in Hkbound.
rewrite -/N in Hkbound.
rewrite -len_G_Z_img in Hkbound.
apply H in Hkbound as Hrel; clear H.
destruct Hrel as [x [Hlookup Hrel]].
iPoseProof Hrel as "Hrel". clear Hrel...
rel_apply "Hrel". iClear "Hrel".
pose proof (lookup_list_lt_r G_Z_img (λ n : Z, #n) k).
apply H in Hkbound as Hrel; clear H.
destruct Hrel as [y [Hlookup' Hrel]].
iPoseProof Hrel as "Hrel". clear Hrel.
rel_apply "Hrel". iClear "Hrel".
rewrite Hlookup' in Hlookup.
injection Hlookup; clear Hlookup; intros eqxy; subst.
rel_apply_l vg_of_int_correct; last
rel_apply_r vg_of_int_correct; last first.
- apply list_elem_of_lookup_2 in Hlookup'.
pose proof (vg_of_int_dom x Hlookup') as [xg eqvg]; rewrite eqvg...
rel_apply "Hrelkey". iExists _. iPureIntro; split; done.
- clear Hlookup' x. rewrite /to_val_type_rel. iSplit.
+ iIntros (x). iExists x. done.
+ iIntros (ox). destruct ox as [x|]; iPureIntro.
* eexists. eexists. right. repeat split.
eexists. done.
* eexists. eexists. left. repeat split.
- clear Hlookup' x. rewrite /to_val_type_rel. iSplit.
+ iIntros (x). iExists x. done.
+ iIntros (ox). destruct ox as [x|]; iPureIntro.
* eexists. eexists. right. repeat split.
eexists. done.
* eexists. eexists. left. repeat split.
Qed.
Lemma refines_otp_keygen_l : forall K e E A,
(∀ key,
kemdem_hybrid_cpa_generic.left_lrel lrel_key key -∗
refines E
(fill K (Val key))
e A)
⊢ refines E
(fill K (symmetric_init.keygen #()))
e A.
Proof with rel_pures_l. intros *. iIntros "Hrelkey".
rewrite /symmetric_init.keygen... simpl.
rewrite /one_time_pad.otp_keygen...
rel_apply refines_randU_l.
iIntros (k Hkbound).
rewrite /vg_of_symkey.
pose proof (lookup_list_lt_l G_Z_img (λ n : Z, #n) k).
rewrite /SymKey in Hkbound.
apply PeanoNat.le_lt_n_Sm in Hkbound.
rewrite -/N in Hkbound.
rewrite -len_G_Z_img in Hkbound.
apply H in Hkbound as Hrel; clear H.
destruct Hrel as [x [Hlookup Hrel]].
iPoseProof Hrel as "Hrel". clear Hrel...
rel_apply "Hrel". iClear "Hrel".
rel_apply_l vg_of_int_correct; last first.
- apply list_elem_of_lookup_2 in Hlookup.
pose proof (vg_of_int_dom x Hlookup) as [xg eqvg]; rewrite eqvg...
rel_apply "Hrelkey". iExists _, _. iPureIntro; split; done.
- clear Hlookup x. rewrite /to_val_type_rel. iSplit.
+ iIntros (x). iExists x. done.
+ iIntros (ox). destruct ox as [x|]; iPureIntro.
* eexists. eexists. right. repeat split.
eexists. done.
* eexists. eexists. left. repeat split.
Qed.
Lemma refines_otp_keygen_r : forall K e E A,
(∀ key,
kemdem_hybrid_cpa_generic.right_lrel lrel_key key -∗
refines E
e
(fill K (Val key))
A)
⊢ refines E
e
(fill K (symmetric_init.keygen #()))
A.
Proof with rel_pures_r. intros *. iIntros "Hrelkey".
rewrite /symmetric_init.keygen... simpl.
rewrite /one_time_pad.otp_keygen...
rel_apply refines_randU_r.
iIntros (k Hkbound).
rewrite /vg_of_symkey.
pose proof (lookup_list_lt_r G_Z_img (λ n : Z, #n) k).
rewrite /SymKey in Hkbound.
apply PeanoNat.le_lt_n_Sm in Hkbound.
rewrite -/N in Hkbound.
rewrite -len_G_Z_img in Hkbound.
apply H in Hkbound as Hrel; clear H.
destruct Hrel as [x [Hlookup Hrel]].
iPoseProof Hrel as "Hrel". clear Hrel...
rel_apply "Hrel". iClear "Hrel".
rel_apply_r vg_of_int_correct; last first.
- apply list_elem_of_lookup_2 in Hlookup.
pose proof (vg_of_int_dom x Hlookup) as [xg eqvg]; rewrite eqvg...
rel_apply "Hrelkey". iExists _, _. iPureIntro; split; done.
- clear Hlookup x. rewrite /to_val_type_rel. iSplit.
+ iIntros (x). iExists x. done.
+ iIntros (ox). destruct ox as [x|]; iPureIntro.
* eexists. eexists. right. repeat split.
eexists. done.
* eexists. eexists. left. repeat split.
Qed.
Lemma refines_otp_senc_l :
∀ (lls : list loc) (msg : val) (k : val) K e E A,
kemdem_hybrid_cpa_generic.left_lrel lrel_key k ∗
kemdem_hybrid_cpa_generic.left_lrel lrel_input msg ∗ Pl lls ⊢
((∀ (c : val),
@kemdem_hybrid_cpa_generic.sym_is_cipher_l _ _ _ lls msg c k
-∗ refines E
(fill K (Val c))
e A)
-∗ refines E
(fill K (senc lls k msg))
e A).
Proof with rel_pures_l.
iIntros (lls vmsg k K e E A) "[[%vk' %Hrelk] [[%msg' [%msg [%eq [%eq2 %Hmsgbound]]]] HP]] H".
rewrite /senc/otp_enc_vg/otp_enc/one_time_pad.otp_enc.
destruct lls as [|mapref [|tmp lls]]; try (iExFalso; done)...
destruct Hrelk as [kg [eqkg _]]; subst.
rewrite /symkey_of_vg...
rel_apply_l int_of_vg_correct...
{
rewrite /to_val_type_rel. iSplit.
- iIntros (x). iExists _. iPureIntro. split; done.
- iIntros (x). iExists _. iPureIntro; split; done.
}
rel_apply index_of_list_lt_l; first apply int_of_vg_img...
rewrite -(Z2Nat.id (list_index_of G_Z_img (int_of_vg_sem kg))); last lia.
rel_apply xor_correct_l; try rewrite Nat2Z.id; try lia.
{ rewrite /SymOutput. rewrite -/N.
rewrite -len_G_Z_img. apply list_index_of_lt.
apply int_of_vg_img. }
rel_apply "H".
rewrite /kemdem_hybrid_cpa_generic.sym_is_cipher_l.
clear K e E A.
iIntros (K e E A) "H".
iPoseProof ("H" with "HP") as "H".
rewrite /kemdem_hybrid_cpa_generic.sdec... simpl.
rewrite /sdec/otp_dec_vg/otp_dec/one_time_pad.otp_dec...
rewrite /symkey_of_vg...
rel_apply int_of_vg_correct.
{
rewrite /to_val_type_rel. iSplit.
- iIntros (x). iExists _. iPureIntro. split; done.
- iIntros (x). iExists _. iPureIntro; split; done.
}
rel_apply index_of_list_lt_l; first apply int_of_vg_img...
rel_apply xor_correct_l; try lia.
- rewrite /SymOutput.
rewrite Nat2Z.id.
apply xor_dom; try lia.
rewrite -/N.
rewrite -len_G_Z_img. apply list_index_of_lt.
apply int_of_vg_img.
- rewrite -/N.
rewrite -len_G_Z_img. apply list_index_of_lt.
apply int_of_vg_img.
- rewrite Nat2Z.id.
rewrite xor_sem_inverse_r; try lia; last first.
{ rewrite -/N.
rewrite -len_G_Z_img. apply list_index_of_lt.
apply int_of_vg_img. }
rewrite Z2Nat.id; last lia.
rel_apply "H".
Qed.
Definition sdec_not_vg : list loc → val := λ _, otp_dec.
Lemma refines_couple_otp_sdec : ∀ K K' E (A : lrel Σ) k k' c c' lls rls,
Plr lls rls
-∗ (lrel_int_bounded 0 SymOutput) k k'
-∗ lrel_output c c'
-∗
((∀ decr decr', lrel_input decr decr' -∗ Plr lls rls -∗
(REL fill K (Val decr) << fill K' (Val decr') @ E : A))
-∗ REL fill K (sdec_not_vg lls k c) << fill K' (sdec_not_vg rls k' c') @ E : A).
Proof with rel_pures_l; rel_pures_r.
iIntros (K K' E A kv kv' cv cv' lls rls) "HP [%k [%eqk1 [%eqk2 %Hkbound]]] [%c [%eqc1 [%eqc2 %Hcbound]]] Hrel"; subst.
rewrite /sdec_not_vg/otp_dec/one_time_pad.otp_dec...
rewrite -(Z2Nat.id k); last lia.
rel_apply xor_correct_l; try lia.
rel_apply xor_correct_r; try lia.
rel_apply "Hrel"; last iAssumption.
iExists (xor_sem (Z.to_nat c) (Z.to_nat k)).
iPureIntro; repeat split; try lia.
apply inj_le. rewrite /Input.
apply PeanoNat.lt_n_Sm_le.
apply xor_dom; lia.
Qed.
#[local] Instance otp_enc_lrel : @kemdem_hybrid_cpa_generic.lrel_sym_scheme Σ.
Proof. unshelve econstructor.
- exact lrel_input.
- exact lrel_output.
- exact lrel_key.
Defined.
#[local] Instance elgamal_lrel : @kemdem_hybrid_cpa_generic.lrel_asym_scheme Σ.
Proof. unshelve econstructor.
- exact lrel_G.
- exact (lrel_G * lrel_G)%lrel.
- exact kemdem_hybrid_cpa_instance_rf.lrel_sk.
- exact kemdem_hybrid_cpa_instance_rf.lrel_pk.
Defined.
#[local] Instance elgamal_is_key : @kemdem_hybrid_cpa_generic.is_asym_key Σ.
Proof. unshelve econstructor.
- exact kemdem_hybrid_cpa_instance_rf.elgamal_is_asym_key_l.
- exact kemdem_hybrid_cpa_instance_rf.elgamal_is_asym_key_r.
- exact kemdem_hybrid_cpa_instance_rf.elgamal_is_asym_key_lr.
Defined.
#[local] Instance otp_enc_props :
kemdem_hybrid_cpa_generic.initializable_sym_scheme_props.
Proof with rel_pures_l; rel_pures_r. unshelve econstructor.
- rewrite /kemdem_hybrid_cpa_generic.lrel_key. simpl.
iIntros (v v') "H". rewrite /lrel_key. iAssumption.
- simpl. apply P0_P_l.
- simpl. apply P0_P_r.
- simpl. apply P0lr_Plr.
- simpl. iIntros (K e E A) "H".
rewrite /symmetric_init.get_enc_scheme/symmetric_init.sym_scheme.
rel_pure_l. rel_pure_l. rel_pure_l. rel_pure_l.
rel_pure_l. rewrite /otp_scheme_vg. rel_apply "H".
done.
- simpl. iIntros (K e E A) "H".
rewrite /symmetric_init.get_enc_scheme/symmetric_init.sym_scheme.
rel_pure_r. rel_pure_r. rel_pure_r. rel_pure_r.
rel_pure_r. rewrite /otp_scheme_vg. rel_apply "H".
done.
- simpl. apply refines_otp_keygen_l.
- simpl. apply refines_otp_keygen_r.
- simpl. apply refines_otp_keygen_couple.
- simpl. apply refines_otp_senc_l.
- simpl. apply otp_enc_sem_typed.
Defined.
Lemma is_asym_key_lrel `{!approxisRGS Σ} :
∀ sk pk, kemdem_hybrid_cpa_instance_rf.elgamal_is_asym_key_lr sk pk ⊢
((lrel_car kemdem_hybrid_cpa_instance_rf.lrel_pk) pk pk).
Proof.
iIntros (sk pk) "[%k [[%eq1 %Hkbound] %eq2]]".
rewrite /kemdem_hybrid_cpa_instance_rf.lrel_pk.
iExists _. iPureIntro; split; done.
Qed.
(* ASSUMPTIONS ON THE ASYMMETRIC SCHEME *)
Lemma elgamal_refines_akeygen_l : forall K e E A,
(∀ sk pk,
kemdem_hybrid_cpa_instance_rf.elgamal_is_asym_key_l sk pk -∗
refines E
(fill K (Val (sk, pk)))
e A)
⊢ refines E
(fill K (keygen #()))
e A.
Proof with rel_pures_l. iIntros (K e E A) "H".
rewrite /keygen...
rel_apply refines_randU_l.
iIntros (sk Hskbound)...
rel_apply refines_exp_l...
rel_apply "H".
rewrite /kemdem_hybrid_cpa_instance_rf.elgamal_is_asym_key_l.
iExists _, _, _. iPureIntro. repeat split; try lia.
rewrite Nat2Z.id. reflexivity.
Qed.
Lemma elgamal_refines_akeygen_r : forall K e E A,
(∀ sk pk,
kemdem_hybrid_cpa_instance_rf.elgamal_is_asym_key_r sk pk -∗
refines E
e
(fill K (Val (sk, pk)))
A)
⊢ refines E
e
(fill K (keygen #()))
A.
Proof with rel_pures_r. iIntros (K e E A) "H".
rewrite /keygen...
rel_apply refines_randU_r.
iIntros (sk Hskbound)...
rel_apply refines_exp_r...
rel_apply "H".
rewrite /kemdem_hybrid_cpa_instance_rf.elgamal_is_asym_key_r.
iExists _, _, _. iPureIntro. repeat split; try lia.
rewrite Nat2Z.id. reflexivity.
Qed.
Lemma elgamal_refines_akeygen_couple : forall K K' E A,
(∀ sk pk,
kemdem_hybrid_cpa_instance_rf.elgamal_is_asym_key_lr sk pk -∗
refines E
(fill K (Val (sk, pk)))
(fill K' (Val (sk, pk)))
A)
⊢ refines E
(fill K (keygen #()))
(fill K' (keygen #()))
A.
Proof with (rel_pures_l; rel_pures_r). iIntros (K e E A) "H".
rewrite /keygen...
rel_apply refines_couple_UU; first done.
iIntros (sk Hskbound); iModIntro...
rel_apply refines_exp_l.
rel_apply refines_exp_r...
rel_apply "H".
rewrite /kemdem_hybrid_cpa_instance_rf.elgamal_is_asym_key_lr.
iExists _. iPureIntro. repeat split; try lia.
rewrite Nat2Z.id. reflexivity.
Qed.
Definition elgamal_asym_is_cipher_l (msg c pk : val) : iProp Σ :=
∀ K e E A sk,
kemdem_hybrid_cpa_instance_rf.elgamal_is_asym_key_l sk pk
-∗ refines E
(fill K (Val msg))
e A
-∗ refines E
(fill K (dec sk c))
e A.
Lemma elgamal_refines_aenc_l :
∀ (msg pk sk : val) K e E A,
kemdem_hybrid_cpa_generic.left_lrel lrel_G msg ∗ kemdem_hybrid_cpa_instance_rf.elgamal_is_asym_key_l sk pk ⊢
((∀ (c : val),
@elgamal_asym_is_cipher_l msg c pk
-∗ refines E
(fill K (Val c))
e A)
-∗ refines E
(fill K (enc pk msg))
e A).
Proof with (rel_pures_l; rel_pures_r).
iIntros (msg pk sk K e E A)
"[[%v [%msg_g [%eqmsg1 %eqmsg2]]] [%sk' [%pk' [%n_sk [[%eqsk [%eqsk' %Hskbound]] [%eqpk %eqpk']]]]]] H"; subst.
rewrite /enc...
rel_apply refines_randU_l.
iIntros (b Hbbound)...
rel_apply refines_exp_l...
rewrite /kemdem_hybrid_cpa_instance_rf.elgamal_is_asym_key_l.
rel_apply refines_exp_l...
rel_apply refines_mult_l...
rel_apply "H".
rewrite /elgamal_asym_is_cipher_l.
clear K e E A.
iIntros (K e E A sk) "[%sk' [%pk' [%n_sk' [[%eqsk [%eqsk' %Hskbound']] [%eqpk %eqpk']]]]]"; subst.
iIntros "H".
rewrite /dec...
rewrite -(Z2Nat.id n_sk'); last lia.
rel_apply refines_exp_l.
rel_apply refines_inv_l.
rel_apply refines_mult_l.
rewrite -?expgM.
Admitted.
Let lrel_asym_output := (lrel_G * lrel_G)%lrel.
Lemma aenc_sem_typed :
⊢ refines top enc enc (kemdem_hybrid_cpa_instance_rf.lrel_pk → lrel_G → lrel_asym_output).
Proof with (rel_pures_l; rel_pures_r).
rewrite /pubkey_class.enc...
rewrite /elgamal_scheme...
rewrite /enc...
rel_arrow_val.
iIntros (v1 v2 [pk [eq1 eq2]]); subst...
rel_arrow_val.
iIntros (msg1 msg2 [msg [eq1 eq2]]); subst...
rel_apply refines_couple_UU; first done.
iModIntro; iIntros (n Hnbound)...
rel_apply refines_exp_l.
rel_apply refines_exp_r...
rel_apply refines_exp_l.
rel_apply refines_exp_r...
rel_apply refines_mult_l.
rel_apply refines_mult_r...
rel_vals; iExists _; done.
Qed.
Lemma asym_rand_cipher_couple :
∀ (v v' : val) K K' E A,
(∀ r r', lrel_asym_output r r' -∗
refines E (fill K (Val r)) (fill K' (Val r')) A)
⊢ refines E (fill K (pubkey_class.rand_cipher v))
(fill K' (pubkey_class.rand_cipher v')) A.
Proof with (rel_pures_l; rel_pures_r).
iIntros (v v' K K' E A) "H".
rewrite /pubkey_class.rand_cipher...
rewrite /elgamal_scheme...
rel_apply refines_couple_UU; first done.
iModIntro; iIntros (n Hnbound)...
rel_apply refines_couple_UU; first done.
iModIntro; iIntros (b Hbbound)...
rel_apply refines_exp_l;
rel_apply refines_exp_r;
rel_apply refines_exp_l;
rel_apply refines_exp_r...
rel_apply "H".
iExists _, _, _, _.
iSplit; last iSplit; [done|done|].
iSplit; iExists _; done.
Qed.
Lemma rand_cipher_sem_typed :
⊢ refines top symmetric_init.rand_cipher
symmetric_init.rand_cipher (kemdem_hybrid_cpa_generic.lrel_trivial → lrel_output).
Proof with (rel_pures_l; rel_pures_r).
rewrite /symmetric_init.rand_cipher... simpl.
rewrite /one_time_pad.otp_rand_cipher...
rel_arrow_val.
iIntros (v1 v2) "_"...
rel_apply refines_couple_UU; first done.
iIntros (i Hibound); iModIntro... rel_vals.
iExists i; iPureIntro; repeat split; lia.
Qed.
#[warnings="-notation-incompatible-prefix"]
Import fingroup.
Lemma asym_key_lr_l_r :
∀ sk pk, (@kemdem_hybrid_cpa_instance_rf.elgamal_is_asym_key_lr _ _ Σ) sk pk
-∗ kemdem_hybrid_cpa_instance_rf.elgamal_is_asym_key_l sk pk ∗ kemdem_hybrid_cpa_instance_rf.elgamal_is_asym_key_r sk pk.
Proof. rewrite /Persistent.
iIntros (sk pk) "#H". iSplit;
last rewrite /kemdem_hybrid_cpa_instance_rf.elgamal_is_asym_key_r; rewrite /kemdem_hybrid_cpa_instance_rf.elgamal_is_asym_key_l/kemdem_hybrid_cpa_instance_rf.elgamal_is_asym_key_lr;
iDestruct "H" as "[%k [[%eqsk %Hkbound] %eqpk]]"; subst.
- iExists #k, (vgval (g ^+ (Z.to_nat k))), k. iPureIntro; repeat split; lia.
- iExists #k, (vgval (g ^+ (Z.to_nat k))), k. iPureIntro; repeat split; lia.
Qed.
#[local] Instance elgamal_props :
@kemdem_hybrid_cpa_generic.asym_scheme_props _ _ _ _ _ _ _ _ _ _ _.
Proof. unshelve econstructor.
- eapply is_asym_key_lrel.
- eapply asym_key_lr_l_r.
- eapply elgamal_refines_akeygen_l.
- eapply elgamal_refines_akeygen_r.
- eapply elgamal_refines_akeygen_couple.
- eapply elgamal_refines_aenc_l.
- eapply aenc_sem_typed.
- eapply asym_rand_cipher_couple.
- eapply rand_cipher_sem_typed.
Defined.
Lemma is_asym_key_l_persistent : ∀ sk pk, Persistent ((@kemdem_hybrid_cpa_instance_rf.elgamal_is_asym_key_l _ _ Σ) sk pk).
Proof. rewrite /Persistent.
iIntros (sk pk) "#H". iAssumption.
Qed.
Lemma is_asym_key_r_persistent : ∀ sk pk, Persistent ((@kemdem_hybrid_cpa_instance_rf.elgamal_is_asym_key_r _ _ Σ) sk pk).
Proof. rewrite /Persistent.
iIntros (sk pk) "#H". iAssumption.
Qed.
Lemma is_asym_key_lr_persistent : ∀ sk pk, Persistent ((@kemdem_hybrid_cpa_instance_rf.elgamal_is_asym_key_lr _ _ Σ) sk pk).
Proof. rewrite /Persistent.
iIntros (sk pk) "#H". iAssumption.
Qed.
Section Correctness.
Import mathcomp.fingroup.fingroup.
Let dec_hyb := @kemdem_hybrid_cpa_generic.dec_hyb _ _ _ elgamal_scheme.
Let enc_hyb := @kemdem_hybrid_cpa_generic.enc_hyb otp_SYM_param sym_otp_scheme_inst _ _ _ elgamal_scheme.
Lemma hybrid_scheme_correct :
⊢ refines top
(kemdem_hybrid_cpa_generic.init_scheme (λ: "scheme", (let, ("sk", "pk") := pubkey_class.keygen #() in
λ:"msg", dec_hyb "scheme" "sk"
(enc_hyb "scheme" "pk" "msg"))))
(λ: "msg", "msg")%V
(lrel_input → lrel_input).
Proof.
rewrite /dec_hyb/enc_hyb.
iStartProof.
iPoseProof kemdem_hybrid_cpa_generic.hybrid_scheme_correct as "H".
- exact SymKey.
- exact SymKey.
- exact SymOutput.
- exact Δ.
- rewrite /kemdem_hybrid_cpa_generic.is_asym_key_l. simpl.
exact is_asym_key_l_persistent.
- rewrite /kemdem_hybrid_cpa_generic.is_asym_key_l. simpl.
exact is_asym_key_r_persistent.
- rewrite /kemdem_hybrid_cpa_generic.is_asym_key_l. simpl.
exact is_asym_key_lr_persistent.
- rewrite /SymKey/SymOutput. simpl.
rel_apply "H".
Qed.
End Correctness.
Let lrel_kemdem_output : lrel Σ := lrel_output * lrel_asym_output.
Let pk_real := @kemdem_hybrid_cpa_generic.pk_real _ _ _ _ _ elgamal_scheme.
Lemma rf_pk_real_adv :
⊢ refines top (kemdem_hybrid_cpa_generic.init_scheme
(kemdem_hybrid_cpa_generic.pk_real N N
N))
(kemdem_hybrid_cpa_generic.init_scheme
kemdem_hybrid_cpa_generic.adv_pk_real
pubkey_class.CPA_OTS_real) (kemdem_hybrid_cpa_generic.lrel_pk *
(kemdem_hybrid_cpa_generic.lrel_input
→ () +
kemdem_hybrid_cpa_generic.lrel_output *
kemdem_hybrid_cpa_generic.lrel_asym_output))%lrel.
Proof.
eapply (kemdem_hybrid_cpa_generic.pk_real_adv SymKey SymKey SymOutput).
- exact Δ.
- rewrite /kemdem_hybrid_cpa_generic.is_asym_key_l. simpl.
exact is_asym_key_l_persistent.
- rewrite /kemdem_hybrid_cpa_generic.is_asym_key_l. simpl.
exact is_asym_key_r_persistent.
- rewrite /kemdem_hybrid_cpa_generic.is_asym_key_l. simpl.
exact is_asym_key_lr_persistent.
- exact _.
- exact _.
Qed.
(* here we use the DDH assumption: we replace CDDHreal by CDDHrand *)
Lemma rf_adv__pk_real_arand :
⊢ refines top
(kemdem_hybrid_cpa_generic.init_scheme
kemdem_hybrid_cpa_generic.adv_pk_real pubkey_class.CPA_OTS_rand)
(kemdem_hybrid_cpa_generic.init_scheme
(@kemdem_hybrid_cpa_generic.pk_real_arand _ _ _ _ _ elgamal_scheme))
(kemdem_hybrid_cpa_generic.lrel_pk *
(kemdem_hybrid_cpa_generic.lrel_input →
() + kemdem_hybrid_cpa_generic.lrel_output * kemdem_hybrid_cpa_generic.lrel_asym_output))%lrel.
Proof. eapply kemdem_hybrid_cpa_generic.adv__pk_real_arand.
- exact SymKey.
- exact SymKey.
- exact SymOutput.
- exact Δ.
- rewrite /kemdem_hybrid_cpa_generic.is_asym_key_l. simpl.
exact is_asym_key_l_persistent.
- rewrite /kemdem_hybrid_cpa_generic.is_asym_key_l. simpl.
exact is_asym_key_r_persistent.
- rewrite /kemdem_hybrid_cpa_generic.is_asym_key_l. simpl.
exact is_asym_key_lr_persistent.
- exact _.
- exact _.
Qed.
Lemma rf_pk_real_arand_perm__adv :
⊢ refines top (kemdem_hybrid_cpa_generic.init_scheme
(@kemdem_hybrid_cpa_generic.pk_real_arand_permute _ _ _ _ _ elgamal_scheme))
(kemdem_hybrid_cpa_generic.OTS #true
(@kemdem_hybrid_cpa_generic.adv_pk_real_arand_permute _ _ _ elgamal_scheme) symmetric_init.sym_scheme)
(kemdem_hybrid_cpa_generic.lrel_pk *
(kemdem_hybrid_cpa_generic.lrel_input → () +
kemdem_hybrid_cpa_generic.lrel_output * kemdem_hybrid_cpa_generic.lrel_asym_output))%lrel.
Proof. eapply kemdem_hybrid_cpa_generic.pk_real_arand_perm__adv.
- exact SymKey.
- exact SymKey.
- exact SymOutput.
- exact Δ.
- rewrite /kemdem_hybrid_cpa_generic.is_asym_key_l. simpl.
exact is_asym_key_l_persistent.
- rewrite /kemdem_hybrid_cpa_generic.is_asym_key_l. simpl.
exact is_asym_key_r_persistent.
- rewrite /kemdem_hybrid_cpa_generic.is_asym_key_l. simpl.
exact is_asym_key_lr_persistent.
- exact _.
- exact _.
Qed.
Lemma rf_adv__pk_rand_srand :
⊢ refines top
(kemdem_hybrid_cpa_generic.OTS #false
(@kemdem_hybrid_cpa_generic.adv_pk_real_arand_permute _ _ _ elgamal_scheme)
symmetric_init.sym_scheme)
(@kemdem_hybrid_cpa_generic.pk_rand_srand _ _ _ _ _ elgamal_scheme)
(kemdem_hybrid_cpa_generic.lrel_pk *
(kemdem_hybrid_cpa_generic.lrel_input → () +
kemdem_hybrid_cpa_generic.lrel_output * kemdem_hybrid_cpa_generic.lrel_asym_output))%lrel.
Proof. eapply kemdem_hybrid_cpa_generic.adv__pk_rand_srand.
- exact SymKey.
- exact SymKey.
- exact SymOutput.
- exact Δ.
- rewrite /kemdem_hybrid_cpa_generic.is_asym_key_l. simpl.
exact is_asym_key_l_persistent.
- rewrite /kemdem_hybrid_cpa_generic.is_asym_key_l. simpl.
exact is_asym_key_r_persistent.
- rewrite /kemdem_hybrid_cpa_generic.is_asym_key_l. simpl.
exact is_asym_key_lr_persistent.
- exact _.
- exact _.
Qed.
Lemma rf_pk_rand_srand__rand :
⊢ refines top (@kemdem_hybrid_cpa_generic.pk_rand_srand _ _ _ _ _ elgamal_scheme)
(@kemdem_hybrid_cpa_generic.pk_rand _ _ _ _ _ elgamal_scheme)
(kemdem_hybrid_cpa_generic.lrel_pk *
(kemdem_hybrid_cpa_generic.lrel_input → () +
kemdem_hybrid_cpa_generic.lrel_output * kemdem_hybrid_cpa_generic.lrel_asym_output)).
Proof. eapply kemdem_hybrid_cpa_generic.pk_rand_srand__rand.
- exact SymKey.
- exact SymKey.
- exact SymOutput.
- exact Δ.
- rewrite /kemdem_hybrid_cpa_generic.is_asym_key_l. simpl.
exact is_asym_key_l_persistent.
- rewrite /kemdem_hybrid_cpa_generic.is_asym_key_l. simpl.
exact is_asym_key_r_persistent.
- rewrite /kemdem_hybrid_cpa_generic.is_asym_key_l. simpl.
exact is_asym_key_lr_persistent.
- exact _.
- exact _.
Qed.
End logrel.
End Hybrid_scheme.
Set Default Proof Mode "Classic".
From clutch.prob_lang Require Import advantage typing.tychk.
From clutch.approxis Require Import map reltac2 approxis option.
From clutch.clutch.examples.crypto Require ElGamal_bijection.
From clutch.approxis.examples Require Import
valgroup diffie_hellman security_aux option xor
ElGamal_defs bounded_oracle pubkey advantage_laws iterable_expression.
From clutch.approxis.examples Require symmetric_init kemdem_hybrid_cpa_generic
one_time_pad kemdem_hybrid_cpa_instance_rf.
From mathcomp Require Import ssrbool.
From mathcomp Require fingroup.fingroup.
Set Default Proof Using "All".
Import ElGamal_bijection.bij_nat.
Import valgroup_notation.
Import map.
Section Hybrid_scheme.
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 *)
Let N := S n''.
Let SymKey := n''.
Let Input := n''.
Let SymOutput := n''.
Variable xor_struct : XOR (Key := SymOutput) (Support := SymOutput).
Section logrel.
Context `{!approxisRGS Σ}.
Context {G : clutch_group (vg:=vg) (cg:=cg)}.
Context {Δ : listO (lrelC Σ)}.
Definition lrel_sym_key : lrel Σ := lrel_int_bounded 0 SymKey.
Definition lrel_key : lrel Σ := lrel_G.
Definition lrel_output : lrel Σ := lrel_int_bounded 0 SymOutput.
Definition lrel_input : lrel Σ := lrel_int_bounded 0 Input.
Variable xor_spec : XOR_spec.
Local Tactic Notation "rel_bind" open_constr(pat) :=
rel_bind_l pat; rel_bind_r pat.
Local Ltac refines_until tac :=
repeat (rel_pure_l; rel_pure_r; try (rel_apply tac)).
Axiom G_Z_img : list Z.
Axiom vg_of_int_dom : ∀ n, n ∈ G_Z_img
→ ∃ x, vg_of_int_sem n = Some x.
Axiom int_of_vg_img : ∀ x, int_of_vg_sem x ∈ G_Z_img.
Axiom len_G_Z_img : length G_Z_img = N.
Axiom nodup_G_Z_img : NoDup G_Z_img.
Fixpoint val_of_list {X} (l : list X) (f : X → val) : val := match l with
| [] => #()
| h :: t => (f h, val_of_list t f)
end.
Definition find : val :=
rec: "find" "l" "x" :=
if: "l" = #() then #()
else if: (Fst "l") = "x" then #0
else #1 + ("find" (Snd "l") "x").
Definition lookup_expr : val :=
rec: "lookup" "l" "i" :=
if: "l" = #() then #()
else if: "i" = #0 then (Fst "l")
else "lookup" (Snd "l") ("i" - #1).
Definition index_of : val :=
rec: "index_of" "l" "x" :=
if: "l" = #() then #()
else if: (Fst "l") = "x" then #0
else #1 + "index_of" (Snd "l") "x".
Definition vg_of_symkey : val :=
λ: "key",
match: vg_of_int (lookup_expr (val_of_list G_Z_img (λ n, #n)) "key") with
| NONE => #()
| SOME "x" => "x"
end.
Definition symkey_of_vg : val :=
λ: "kg",
index_of (val_of_list G_Z_img (λ n, #n)) (int_of_vg "kg").
Fixpoint list_index_of (l : list Z) (n : Z) : nat := match l with
| [] => 0
| h :: t => if (h =? n)%Z then 0 else 1 + list_index_of t n
end.
Lemma list_index_of_lt (l : list Z) (n : Z) :
n ∈ l → list_index_of l n < length l.
Proof. induction l as [|h t IHt]; intros H.
- inversion H.
- simpl. destruct (h =? n)%Z eqn:eqhead.
+ lia.
+ apply Z.eqb_neq in eqhead.
rewrite <- Nat.succ_lt_mono.
apply IHt.
apply elem_of_cons in H; destruct H as [H|H]; last assumption.
exfalso; apply eqhead; lia.
Qed.
Lemma index_of_list_lt_l (l : list Z) :
∀ x, x ∈ l →
∀ K e E A,
refines E (fill K (Val #(list_index_of l x))) e A
⊢ refines E (fill K (index_of (val_of_list l (λ n, #n)) #x)) e A
.
Proof with rel_pures_l.
iInduction l as [|h t] "IH".
- iIntros (x H); inversion H.
- iIntros (x H K e E A) "Hrel".
rewrite /index_of...
destruct (bool_decide (#h = #x)) eqn:eqhead.
+ apply bool_decide_eq_true in eqhead...
injection eqhead; clear eqhead; intros eqhead.
simpl. rewrite eqhead. rewrite Z.eqb_refl.
replace (Z.of_nat 0) with 0%Z by lia. iAssumption.
+ rel_pure_l. rel_pure_l.
apply bool_decide_eq_false in eqhead.
rel_apply "IH".
* rewrite elem_of_cons in H. destruct H as [H|H].
{ exfalso; apply eqhead; f_equal. symmetry. f_equal. assumption. }
iPureIntro; assumption.
* simpl.
assert (Hbool : (h =? x)%Z = false).
{ apply Z.eqb_neq. intro contra; apply eqhead; rewrite contra; reflexivity. }
rewrite Hbool; clear Hbool...
replace (Z.of_nat (S (list_index_of t x))) with
(1 + Z.of_nat (list_index_of t x))%Z by lia.
rel_apply "Hrel".
Qed.
Lemma index_of_list_lt_r (l : list Z) :
∀ x, x ∈ l →
∀ K e E A,
refines E e (fill K (Val #(list_index_of l x))) A
⊢ refines E e (fill K (index_of (val_of_list l (λ n, #n)) #x)) A
.
Proof with rel_pures_r.
iInduction l as [|h t] "IH".
- iIntros (x H); inversion H.
- iIntros (x H K e E A) "Hrel".
rewrite /index_of...
destruct (bool_decide (#h = #x)) eqn:eqhead.
+ apply bool_decide_eq_true in eqhead...
injection eqhead; clear eqhead; intros eqhead.
simpl. rewrite eqhead. rewrite Z.eqb_refl.
replace (Z.of_nat 0) with 0%Z by lia. iAssumption.
+ rel_pure_r. rel_pure_r.
apply bool_decide_eq_false in eqhead.
rel_apply "IH".
* rewrite elem_of_cons in H. destruct H as [H|H].
{ exfalso; apply eqhead; f_equal. symmetry. f_equal. assumption. }
iPureIntro; assumption.
* simpl.
assert (Hbool : (h =? x)%Z = false).
{ apply Z.eqb_neq. intro contra; apply eqhead; rewrite contra; reflexivity. }
rewrite Hbool; clear Hbool...
replace (Z.of_nat (S (list_index_of t x))) with
(1 + Z.of_nat (list_index_of t x))%Z by lia.
rel_apply "Hrel".
Qed.
Lemma lookup_list_lt_l {X} (l : list X) (to_val : X → val) :
∀ n, n < length l →
∃ x, (l !! n) = Some x
∧ ∀ K e E A,
refines E (fill K (Val (to_val x))) e A
⊢ refines E (fill K (lookup_expr (val_of_list l to_val) #n)) e A.
Proof with (rel_pures_l; rel_pures_r). intros * Hlt.
apply lookup_lt_is_Some_2 in Hlt as Hsome.
destruct Hsome as [x Hsome]. exists x. split; first assumption.
iIntros (K e E A) "Hrel".
iInduction l as [|h t] "IH" forall (n Hlt Hsome).
- inversion Hlt.
- rewrite /lookup_expr...
destruct (bool_decide (#n = #0)) eqn:eqn0.
+ apply bool_decide_eq_true in eqn0. injection eqn0.
replace 0%Z with (Z.of_nat 0) by lia.
clear eqn0; intros eqn0.
apply Nat2Z.inj in eqn0.
rewrite eqn0 in Hsome. simpl in Hsome.
injection Hsome. intros eqx; rewrite eqx...
iAssumption.
+ rel_pure_l. rel_pure_l. rel_pure_l.
apply bool_decide_eq_false in eqn0.
destruct n as [|n']; first (exfalso; apply eqn0; f_equal).
replace (Z.of_nat (S n') - 1)%Z with (Z.of_nat n')%Z by lia.
rel_apply_l "IH"; last iAssumption; iPureIntro.
* simpl in Hlt. lia.
* simpl in Hsome. apply Hsome.
Qed.
Lemma lookup_list_lt_r {X} (l : list X) (to_val : X → val) :
∀ n, n < length l →
∃ x, (l !! n) = Some x
∧ ∀ K e E A,
refines E e (fill K (Val (to_val x))) A
⊢ refines E e (fill K (lookup_expr (val_of_list l to_val) #n)) A
.
Proof with (rel_pures_l; rel_pures_r). intros * Hlt.
apply lookup_lt_is_Some_2 in Hlt as Hsome.
destruct Hsome as [x Hsome]. exists x. split; first assumption.
iIntros (K e E A) "Hrel".
iInduction l as [|h t] "IH" forall (n Hlt Hsome).
- inversion Hlt.
- rewrite /lookup_expr...
destruct (bool_decide (#n = #0)) eqn:eqn0.
+ apply bool_decide_eq_true in eqn0. injection eqn0.
replace 0%Z with (Z.of_nat 0) by lia.
clear eqn0; intros eqn0.
apply Nat2Z.inj in eqn0.
rewrite eqn0 in Hsome. simpl in Hsome.
injection Hsome. intros eqx; rewrite eqx...
iAssumption.
+ rel_pure_r. rel_pure_r. rel_pure_r.
apply bool_decide_eq_false in eqn0.
destruct n as [|n']; first (exfalso; apply eqn0; f_equal).
replace (Z.of_nat (S n') - 1)%Z with (Z.of_nat n')%Z by lia.
rel_apply_l "IH"; last iAssumption; iPureIntro.
* simpl in Hlt. lia.
* simpl in Hsome. apply Hsome.
Qed.
Lemma vg_of_symkey_sem_typed :
⊢ (lrel_car (lrel_sym_key → lrel_G)) vg_of_symkey vg_of_symkey.
Proof with rel_pures_l; rel_pures_r. rewrite /vg_of_symkey.
iIntros (v1 v2 [k [eq1 [eq2 Hkbound]]]); subst.
iModIntro...
rel_bind (lookup_expr _ _).
rewrite -(Z2Nat.id k); last lia.
pose proof (lookup_list_lt_l G_Z_img (λ n : Z, #n) (Z.to_nat k)) as H'.
rewrite len_G_Z_img in H'.
rewrite /SymKey in Hkbound.
assert (H : Z.to_nat k < N) by lia.
apply H' in H as Hrel.
destruct Hrel as [x [eqx Hrel]].
iPoseProof (Hrel) as "Hrel".
rel_apply "Hrel".
clear H' H Hrel.
pose proof (lookup_list_lt_r G_Z_img (λ n : Z, #n) (Z.to_nat k)) as H'.
rewrite len_G_Z_img in H'.
rewrite /SymKey in Hkbound.
assert (H : Z.to_nat k < N) by lia.
apply H' in H.
destruct H as [y [eqy Hrel]].
iClear "Hrel".
iPoseProof (Hrel) as "Hrel".
rel_apply "Hrel".
clear H' Hrel. iClear "Hrel".
rewrite eqx in eqy. injection eqy.
intros eqxy. rewrite eqxy.
rel_apply_l vg_of_int_correct; last
rel_apply_r vg_of_int_correct;
try (iSplit;
first (rewrite /to_val_type_rel;
iIntros (n); iExists _; done);
rewrite /to_val_type_rel;
iIntros ([xg|]);
iExists _, _; iPureIntro;
try (right; repeat split;
eexists; split; by done);
(left; repeat split;
eexists; split; done)).
pose proof (vg_of_int_dom y) as H'.
rewrite eqy in eqx.
apply list_elem_of_lookup_2 in eqx.
apply H' in eqx as H; clear H'.
destruct H as [xg eqvgy].
rewrite eqvgy...
rel_vals.
Qed.
Lemma symkey_of_vg_sem_typed :
⊢ (lrel_car (lrel_G → lrel_sym_key)) symkey_of_vg symkey_of_vg.
Proof with rel_pures_l; rel_pures_r. rewrite /symkey_of_vg.
iIntros (v1 v2 [xg [eq1 eq2]]); subst.
iModIntro...
rel_apply_l int_of_vg_correct; last
rel_apply_r int_of_vg_correct;
try (rewrite /to_val_type_rel; iSplit;
iIntros (x); iExists _; iPureIntro; done).
rel_apply index_of_list_lt_l; last
rel_apply index_of_list_lt_r;
try (apply int_of_vg_img).
rel_vals.
iExists _. iPureIntro; repeat split; try done;
rewrite /SymKey.
- lia.
- apply Nat2Z.inj_le.
apply PeanoNat.lt_n_Sm_le.
rewrite -/N.
rewrite -len_G_Z_img.
apply list_index_of_lt.
apply int_of_vg_img.
Qed.
Definition otp_enc : val := one_time_pad.otp_enc n'' xor_struct.
Definition otp_dec : val := one_time_pad.otp_dec n'' xor_struct.
(* The four following definition are very similar.
The only difference is that otp_... takes a value as input within
the language, whereas senc and sdec take a list of locations
at the meta-level (as a crocq function )*)
Definition otp_enc_vg : val :=
(λ: "key",
otp_enc (symkey_of_vg "key"))%V.
Definition otp_dec_vg : val :=
(λ: "key",
otp_dec (symkey_of_vg "key"))%V.
Definition senc (ls : list loc) : val := otp_enc_vg.
Definition sdec (ls : list loc) : val := otp_dec_vg.
Definition otp_scheme_vg : expr :=
(Val (senc []), Val (sdec [])).
#[local] Instance otp_SYM_param : symmetric_init.SYM_init_params :=
one_time_pad.SYM_otp_param N.
#[local] Instance sym_otp_scheme_inst : symmetric_init.SYM_init := {|
symmetric_init.keygen := λ: <>, vg_of_symkey (one_time_pad.otp_keygen SymKey #())
; symmetric_init.enc_scheme := otp_scheme_vg
; symmetric_init.rand_cipher := one_time_pad.otp_rand_cipher n''
|}.
#[local] Instance elgamal_params : pubkey_class.ASYM_params :=
kemdem_hybrid_cpa_generic.asym_params N N N.
#[local] Instance elgamal_scheme : pubkey_class.ASYM := {|
pubkey_class.keygen := keygen
; pubkey_class.enc := enc
; pubkey_class.dec := dec
; pubkey_class.rand_cipher := (λ: <>, let: "a" := rand #N in let: "b" := rand #N in (vgval g^"a", vgval g^"b"))
|}.
Ltac simpl_exp := try (rel_apply refines_exp_l; rel_pures_l);
try (rel_apply refines_exp_r; rel_pures_r).
Ltac simpl_mult := try (rel_apply refines_mult_l; rel_pures_l);
try (rel_apply refines_mult_r; rel_pures_r).
Definition init_scheme (e : expr) : expr :=
let: "scheme" := symmetric_init.get_enc_scheme symmetric_init.sym_scheme
#() in
e "scheme".
(* ASSUMPTIONS ON THE SYMMETRIC SCHEME FOR CORRECTNESS *)
Lemma lrel_input_refl : forall v v', lrel_input v v' -∗ lrel_input v v.
Proof. intros v v'. iIntros ([x [eq1 [eq2 Hbound]]]).
iExists x. iPureIntro; done.
Qed.
Definition P0l (lls : list loc) : iProp Σ := match lls with
| [] => True%I
| _ => False%I
end.
Definition P0r (rls : list loc) : iProp Σ := match rls with
| [] => True%I
| _ => False%I
end.
Definition Pl (lls : list loc) : iProp Σ := match lls with
| [] => True%I
| _ => False%I
end.
Definition Pr (rls : list loc) : iProp Σ := match rls with
| [] => True%I
| _ => False%I
end.
Definition Plr (lls rls : list loc) : iProp Σ := match lls, rls with
| [], [] => True%I
| _, _ => False%I
end.
#[local] Instance initializable_sym_scheme_defs_otp :
(@kemdem_hybrid_cpa_generic.initializable_sym_scheme_defs Σ).
Proof. unshelve econstructor.
- exact senc.
- exact sdec.
- exact P0l.
- exact P0r.
- exact Pl.
- exact Pr.
- exact Plr.
Defined.
Lemma otp_enc_sem_typed :
∀ lls rls (𝒩 : namespace) (P : iProp Σ),
(∃ (Q : iProp Σ),
P ⊣⊢
(Q
∗ Plr lls rls)
) →
na_invP 𝒩 P
⊢ refines top (senc lls)
(senc rls) (lrel_key → lrel_input → lrel_output).
Proof with (rel_pures_l; rel_pures_r).
intros lls rls 𝒩 P [Q H].
apply bi.equiv_entails in H.
destruct H as [H1 H2].
iIntros "#Inv".
rewrite /senc.
rel_arrow_val.
iIntros (v1 v2 [kg [eq1 eq2]]); subst.
rewrite /otp_enc_vg/otp_enc/one_time_pad.otp_enc.
destruct lls as [|mapref [|tmp lls]];
destruct rls as [|mapref' [|tmp' rls]];
try (simpl in H1;
rel_apply refines_na_inv; iSplitL; first iAssumption;
iIntros "[HP _]"; rel_pures_l; rel_pures_r;
iExFalso;
iPoseProof (H1 with "HP") as "[_ contra]";
iAssumption)...
rel_bind (symkey_of_vg _); rel_apply refines_bind...
{ rel_apply refines_app; rel_vals;
first iApply symkey_of_vg_sem_typed; iExists _; done. }
iIntros (v1 v2 [k [eq1 [eq2 Hkbounds]]]); subst...
rel_arrow_val.
iIntros (v1 v2 [msg [eq1 [eq2 Hmsgbounds]]]); subst...
rewrite -(Z2Nat.id k); last lia.
rel_apply xor_correct_l; try lia.
rel_apply xor_correct_r; try lia.
rel_vals.
iExists _. iPureIntro; repeat split; try lia.
epose proof (xor_dom (Z.to_nat msg) _ (Z.to_nat k)).
lia.
Unshelve.
lia.
Qed.
Lemma P0_P_l : ∀ lls, P0l lls -∗ Pl lls.
Proof. rewrite /P0l/Pl.
intros [|ll [|tmp lls]]; iIntros "H"; iAssumption.
Qed.
Lemma P0_P_r : ∀ rls, P0r rls -∗ Pr rls.
Proof. rewrite /P0l/Pl.
intros [|ll [|tmp lls]]; iIntros "H"; iAssumption.
Qed.
Lemma P0lr_Plr : ∀ lls rls, P0l lls -∗ P0r rls -∗ Plr lls rls.
Proof. rewrite /P0l/P0r/Plr. intros [|ll [|tmp lls]] [|rl [|tmp' rls]];
iIntros "Hl Hr"; iAssumption.
Qed.
Lemma refines_init_otp_scheme_l : forall K e E A,
(∀ lls,
P0l lls -∗
refines E
(fill K (senc lls, sdec lls))
e A)
⊢ refines E
(fill K (symmetric_init.get_enc_scheme symmetric_init.sym_scheme #()))
e A.
Proof. intros *. iIntros "H".
rewrite /symmetric_init.get_enc_scheme.
rewrite /symmetric_init.sym_scheme.
rel_pure_l.
rel_pure_l.
rel_pure_l.
rel_pure_l.
rel_pure_l.
rewrite /otp_scheme_vg.
rel_apply "H".
done.
Qed.
Lemma refines_init_otp_scheme_r : forall K e E A,
(∀ lls,
P0r lls -∗
refines E
e
(fill K (senc lls, sdec lls))
A)
⊢ refines E
e
(fill K (symmetric_init.get_enc_scheme symmetric_init.sym_scheme #()))
A.
Proof. intros *. iIntros "H".
rewrite /symmetric_init.get_enc_scheme.
rewrite /symmetric_init.sym_scheme.
rel_pure_r.
rel_pure_r.
rel_pure_r.
rel_pure_r.
rel_pure_r.
rewrite /otp_scheme_vg.
rel_apply "H".
done.
Qed.
Lemma refines_otp_keygen_couple :forall K K' E A,
(∀ key,
(lrel_car lrel_key) key key -∗
refines E
(fill K (Val key))
(fill K' (Val key))
A)
⊢ refines E
(fill K (symmetric_init.keygen #()))
(fill K' (symmetric_init.keygen #()))
A.
Proof with (rel_pures_l; rel_pures_r).
intros *. iIntros "Hrelkey".
rewrite /symmetric_init.keygen/sym_otp_scheme_inst...
rewrite /one_time_pad.otp_keygen...
rel_apply refines_couple_UU; first done.
iModIntro; iIntros (k Hkbound).
rewrite /vg_of_symkey.
pose proof (lookup_list_lt_l G_Z_img (λ n : Z, #n) k).
rewrite /SymKey in Hkbound.
apply PeanoNat.le_lt_n_Sm in Hkbound.
rewrite -/N in Hkbound.
rewrite -len_G_Z_img in Hkbound.
apply H in Hkbound as Hrel; clear H.
destruct Hrel as [x [Hlookup Hrel]].
iPoseProof Hrel as "Hrel". clear Hrel...
rel_apply "Hrel". iClear "Hrel".
pose proof (lookup_list_lt_r G_Z_img (λ n : Z, #n) k).
apply H in Hkbound as Hrel; clear H.
destruct Hrel as [y [Hlookup' Hrel]].
iPoseProof Hrel as "Hrel". clear Hrel.
rel_apply "Hrel". iClear "Hrel".
rewrite Hlookup' in Hlookup.
injection Hlookup; clear Hlookup; intros eqxy; subst.
rel_apply_l vg_of_int_correct; last
rel_apply_r vg_of_int_correct; last first.
- apply list_elem_of_lookup_2 in Hlookup'.
pose proof (vg_of_int_dom x Hlookup') as [xg eqvg]; rewrite eqvg...
rel_apply "Hrelkey". iExists _. iPureIntro; split; done.
- clear Hlookup' x. rewrite /to_val_type_rel. iSplit.
+ iIntros (x). iExists x. done.
+ iIntros (ox). destruct ox as [x|]; iPureIntro.
* eexists. eexists. right. repeat split.
eexists. done.
* eexists. eexists. left. repeat split.
- clear Hlookup' x. rewrite /to_val_type_rel. iSplit.
+ iIntros (x). iExists x. done.
+ iIntros (ox). destruct ox as [x|]; iPureIntro.
* eexists. eexists. right. repeat split.
eexists. done.
* eexists. eexists. left. repeat split.
Qed.
Lemma refines_otp_keygen_l : forall K e E A,
(∀ key,
kemdem_hybrid_cpa_generic.left_lrel lrel_key key -∗
refines E
(fill K (Val key))
e A)
⊢ refines E
(fill K (symmetric_init.keygen #()))
e A.
Proof with rel_pures_l. intros *. iIntros "Hrelkey".
rewrite /symmetric_init.keygen... simpl.
rewrite /one_time_pad.otp_keygen...
rel_apply refines_randU_l.
iIntros (k Hkbound).
rewrite /vg_of_symkey.
pose proof (lookup_list_lt_l G_Z_img (λ n : Z, #n) k).
rewrite /SymKey in Hkbound.
apply PeanoNat.le_lt_n_Sm in Hkbound.
rewrite -/N in Hkbound.
rewrite -len_G_Z_img in Hkbound.
apply H in Hkbound as Hrel; clear H.
destruct Hrel as [x [Hlookup Hrel]].
iPoseProof Hrel as "Hrel". clear Hrel...
rel_apply "Hrel". iClear "Hrel".
rel_apply_l vg_of_int_correct; last first.
- apply list_elem_of_lookup_2 in Hlookup.
pose proof (vg_of_int_dom x Hlookup) as [xg eqvg]; rewrite eqvg...
rel_apply "Hrelkey". iExists _, _. iPureIntro; split; done.
- clear Hlookup x. rewrite /to_val_type_rel. iSplit.
+ iIntros (x). iExists x. done.
+ iIntros (ox). destruct ox as [x|]; iPureIntro.
* eexists. eexists. right. repeat split.
eexists. done.
* eexists. eexists. left. repeat split.
Qed.
Lemma refines_otp_keygen_r : forall K e E A,
(∀ key,
kemdem_hybrid_cpa_generic.right_lrel lrel_key key -∗
refines E
e
(fill K (Val key))
A)
⊢ refines E
e
(fill K (symmetric_init.keygen #()))
A.
Proof with rel_pures_r. intros *. iIntros "Hrelkey".
rewrite /symmetric_init.keygen... simpl.
rewrite /one_time_pad.otp_keygen...
rel_apply refines_randU_r.
iIntros (k Hkbound).
rewrite /vg_of_symkey.
pose proof (lookup_list_lt_r G_Z_img (λ n : Z, #n) k).
rewrite /SymKey in Hkbound.
apply PeanoNat.le_lt_n_Sm in Hkbound.
rewrite -/N in Hkbound.
rewrite -len_G_Z_img in Hkbound.
apply H in Hkbound as Hrel; clear H.
destruct Hrel as [x [Hlookup Hrel]].
iPoseProof Hrel as "Hrel". clear Hrel...
rel_apply "Hrel". iClear "Hrel".
rel_apply_r vg_of_int_correct; last first.
- apply list_elem_of_lookup_2 in Hlookup.
pose proof (vg_of_int_dom x Hlookup) as [xg eqvg]; rewrite eqvg...
rel_apply "Hrelkey". iExists _, _. iPureIntro; split; done.
- clear Hlookup x. rewrite /to_val_type_rel. iSplit.
+ iIntros (x). iExists x. done.
+ iIntros (ox). destruct ox as [x|]; iPureIntro.
* eexists. eexists. right. repeat split.
eexists. done.
* eexists. eexists. left. repeat split.
Qed.
Lemma refines_otp_senc_l :
∀ (lls : list loc) (msg : val) (k : val) K e E A,
kemdem_hybrid_cpa_generic.left_lrel lrel_key k ∗
kemdem_hybrid_cpa_generic.left_lrel lrel_input msg ∗ Pl lls ⊢
((∀ (c : val),
@kemdem_hybrid_cpa_generic.sym_is_cipher_l _ _ _ lls msg c k
-∗ refines E
(fill K (Val c))
e A)
-∗ refines E
(fill K (senc lls k msg))
e A).
Proof with rel_pures_l.
iIntros (lls vmsg k K e E A) "[[%vk' %Hrelk] [[%msg' [%msg [%eq [%eq2 %Hmsgbound]]]] HP]] H".
rewrite /senc/otp_enc_vg/otp_enc/one_time_pad.otp_enc.
destruct lls as [|mapref [|tmp lls]]; try (iExFalso; done)...
destruct Hrelk as [kg [eqkg _]]; subst.
rewrite /symkey_of_vg...
rel_apply_l int_of_vg_correct...
{
rewrite /to_val_type_rel. iSplit.
- iIntros (x). iExists _. iPureIntro. split; done.
- iIntros (x). iExists _. iPureIntro; split; done.
}
rel_apply index_of_list_lt_l; first apply int_of_vg_img...
rewrite -(Z2Nat.id (list_index_of G_Z_img (int_of_vg_sem kg))); last lia.
rel_apply xor_correct_l; try rewrite Nat2Z.id; try lia.
{ rewrite /SymOutput. rewrite -/N.
rewrite -len_G_Z_img. apply list_index_of_lt.
apply int_of_vg_img. }
rel_apply "H".
rewrite /kemdem_hybrid_cpa_generic.sym_is_cipher_l.
clear K e E A.
iIntros (K e E A) "H".
iPoseProof ("H" with "HP") as "H".
rewrite /kemdem_hybrid_cpa_generic.sdec... simpl.
rewrite /sdec/otp_dec_vg/otp_dec/one_time_pad.otp_dec...
rewrite /symkey_of_vg...
rel_apply int_of_vg_correct.
{
rewrite /to_val_type_rel. iSplit.
- iIntros (x). iExists _. iPureIntro. split; done.
- iIntros (x). iExists _. iPureIntro; split; done.
}
rel_apply index_of_list_lt_l; first apply int_of_vg_img...
rel_apply xor_correct_l; try lia.
- rewrite /SymOutput.
rewrite Nat2Z.id.
apply xor_dom; try lia.
rewrite -/N.
rewrite -len_G_Z_img. apply list_index_of_lt.
apply int_of_vg_img.
- rewrite -/N.
rewrite -len_G_Z_img. apply list_index_of_lt.
apply int_of_vg_img.
- rewrite Nat2Z.id.
rewrite xor_sem_inverse_r; try lia; last first.
{ rewrite -/N.
rewrite -len_G_Z_img. apply list_index_of_lt.
apply int_of_vg_img. }
rewrite Z2Nat.id; last lia.
rel_apply "H".
Qed.
Definition sdec_not_vg : list loc → val := λ _, otp_dec.
Lemma refines_couple_otp_sdec : ∀ K K' E (A : lrel Σ) k k' c c' lls rls,
Plr lls rls
-∗ (lrel_int_bounded 0 SymOutput) k k'
-∗ lrel_output c c'
-∗
((∀ decr decr', lrel_input decr decr' -∗ Plr lls rls -∗
(REL fill K (Val decr) << fill K' (Val decr') @ E : A))
-∗ REL fill K (sdec_not_vg lls k c) << fill K' (sdec_not_vg rls k' c') @ E : A).
Proof with rel_pures_l; rel_pures_r.
iIntros (K K' E A kv kv' cv cv' lls rls) "HP [%k [%eqk1 [%eqk2 %Hkbound]]] [%c [%eqc1 [%eqc2 %Hcbound]]] Hrel"; subst.
rewrite /sdec_not_vg/otp_dec/one_time_pad.otp_dec...
rewrite -(Z2Nat.id k); last lia.
rel_apply xor_correct_l; try lia.
rel_apply xor_correct_r; try lia.
rel_apply "Hrel"; last iAssumption.
iExists (xor_sem (Z.to_nat c) (Z.to_nat k)).
iPureIntro; repeat split; try lia.
apply inj_le. rewrite /Input.
apply PeanoNat.lt_n_Sm_le.
apply xor_dom; lia.
Qed.
#[local] Instance otp_enc_lrel : @kemdem_hybrid_cpa_generic.lrel_sym_scheme Σ.
Proof. unshelve econstructor.
- exact lrel_input.
- exact lrel_output.
- exact lrel_key.
Defined.
#[local] Instance elgamal_lrel : @kemdem_hybrid_cpa_generic.lrel_asym_scheme Σ.
Proof. unshelve econstructor.
- exact lrel_G.
- exact (lrel_G * lrel_G)%lrel.
- exact kemdem_hybrid_cpa_instance_rf.lrel_sk.
- exact kemdem_hybrid_cpa_instance_rf.lrel_pk.
Defined.
#[local] Instance elgamal_is_key : @kemdem_hybrid_cpa_generic.is_asym_key Σ.
Proof. unshelve econstructor.
- exact kemdem_hybrid_cpa_instance_rf.elgamal_is_asym_key_l.
- exact kemdem_hybrid_cpa_instance_rf.elgamal_is_asym_key_r.
- exact kemdem_hybrid_cpa_instance_rf.elgamal_is_asym_key_lr.
Defined.
#[local] Instance otp_enc_props :
kemdem_hybrid_cpa_generic.initializable_sym_scheme_props.
Proof with rel_pures_l; rel_pures_r. unshelve econstructor.
- rewrite /kemdem_hybrid_cpa_generic.lrel_key. simpl.
iIntros (v v') "H". rewrite /lrel_key. iAssumption.
- simpl. apply P0_P_l.
- simpl. apply P0_P_r.
- simpl. apply P0lr_Plr.
- simpl. iIntros (K e E A) "H".
rewrite /symmetric_init.get_enc_scheme/symmetric_init.sym_scheme.
rel_pure_l. rel_pure_l. rel_pure_l. rel_pure_l.
rel_pure_l. rewrite /otp_scheme_vg. rel_apply "H".
done.
- simpl. iIntros (K e E A) "H".
rewrite /symmetric_init.get_enc_scheme/symmetric_init.sym_scheme.
rel_pure_r. rel_pure_r. rel_pure_r. rel_pure_r.
rel_pure_r. rewrite /otp_scheme_vg. rel_apply "H".
done.
- simpl. apply refines_otp_keygen_l.
- simpl. apply refines_otp_keygen_r.
- simpl. apply refines_otp_keygen_couple.
- simpl. apply refines_otp_senc_l.
- simpl. apply otp_enc_sem_typed.
Defined.
Lemma is_asym_key_lrel `{!approxisRGS Σ} :
∀ sk pk, kemdem_hybrid_cpa_instance_rf.elgamal_is_asym_key_lr sk pk ⊢
((lrel_car kemdem_hybrid_cpa_instance_rf.lrel_pk) pk pk).
Proof.
iIntros (sk pk) "[%k [[%eq1 %Hkbound] %eq2]]".
rewrite /kemdem_hybrid_cpa_instance_rf.lrel_pk.
iExists _. iPureIntro; split; done.
Qed.
(* ASSUMPTIONS ON THE ASYMMETRIC SCHEME *)
Lemma elgamal_refines_akeygen_l : forall K e E A,
(∀ sk pk,
kemdem_hybrid_cpa_instance_rf.elgamal_is_asym_key_l sk pk -∗
refines E
(fill K (Val (sk, pk)))
e A)
⊢ refines E
(fill K (keygen #()))
e A.
Proof with rel_pures_l. iIntros (K e E A) "H".
rewrite /keygen...
rel_apply refines_randU_l.
iIntros (sk Hskbound)...
rel_apply refines_exp_l...
rel_apply "H".
rewrite /kemdem_hybrid_cpa_instance_rf.elgamal_is_asym_key_l.
iExists _, _, _. iPureIntro. repeat split; try lia.
rewrite Nat2Z.id. reflexivity.
Qed.
Lemma elgamal_refines_akeygen_r : forall K e E A,
(∀ sk pk,
kemdem_hybrid_cpa_instance_rf.elgamal_is_asym_key_r sk pk -∗
refines E
e
(fill K (Val (sk, pk)))
A)
⊢ refines E
e
(fill K (keygen #()))
A.
Proof with rel_pures_r. iIntros (K e E A) "H".
rewrite /keygen...
rel_apply refines_randU_r.
iIntros (sk Hskbound)...
rel_apply refines_exp_r...
rel_apply "H".
rewrite /kemdem_hybrid_cpa_instance_rf.elgamal_is_asym_key_r.
iExists _, _, _. iPureIntro. repeat split; try lia.
rewrite Nat2Z.id. reflexivity.
Qed.
Lemma elgamal_refines_akeygen_couple : forall K K' E A,
(∀ sk pk,
kemdem_hybrid_cpa_instance_rf.elgamal_is_asym_key_lr sk pk -∗
refines E
(fill K (Val (sk, pk)))
(fill K' (Val (sk, pk)))
A)
⊢ refines E
(fill K (keygen #()))
(fill K' (keygen #()))
A.
Proof with (rel_pures_l; rel_pures_r). iIntros (K e E A) "H".
rewrite /keygen...
rel_apply refines_couple_UU; first done.
iIntros (sk Hskbound); iModIntro...
rel_apply refines_exp_l.
rel_apply refines_exp_r...
rel_apply "H".
rewrite /kemdem_hybrid_cpa_instance_rf.elgamal_is_asym_key_lr.
iExists _. iPureIntro. repeat split; try lia.
rewrite Nat2Z.id. reflexivity.
Qed.
Definition elgamal_asym_is_cipher_l (msg c pk : val) : iProp Σ :=
∀ K e E A sk,
kemdem_hybrid_cpa_instance_rf.elgamal_is_asym_key_l sk pk
-∗ refines E
(fill K (Val msg))
e A
-∗ refines E
(fill K (dec sk c))
e A.
Lemma elgamal_refines_aenc_l :
∀ (msg pk sk : val) K e E A,
kemdem_hybrid_cpa_generic.left_lrel lrel_G msg ∗ kemdem_hybrid_cpa_instance_rf.elgamal_is_asym_key_l sk pk ⊢
((∀ (c : val),
@elgamal_asym_is_cipher_l msg c pk
-∗ refines E
(fill K (Val c))
e A)
-∗ refines E
(fill K (enc pk msg))
e A).
Proof with (rel_pures_l; rel_pures_r).
iIntros (msg pk sk K e E A)
"[[%v [%msg_g [%eqmsg1 %eqmsg2]]] [%sk' [%pk' [%n_sk [[%eqsk [%eqsk' %Hskbound]] [%eqpk %eqpk']]]]]] H"; subst.
rewrite /enc...
rel_apply refines_randU_l.
iIntros (b Hbbound)...
rel_apply refines_exp_l...
rewrite /kemdem_hybrid_cpa_instance_rf.elgamal_is_asym_key_l.
rel_apply refines_exp_l...
rel_apply refines_mult_l...
rel_apply "H".
rewrite /elgamal_asym_is_cipher_l.
clear K e E A.
iIntros (K e E A sk) "[%sk' [%pk' [%n_sk' [[%eqsk [%eqsk' %Hskbound']] [%eqpk %eqpk']]]]]"; subst.
iIntros "H".
rewrite /dec...
rewrite -(Z2Nat.id n_sk'); last lia.
rel_apply refines_exp_l.
rel_apply refines_inv_l.
rel_apply refines_mult_l.
rewrite -?expgM.
Admitted.
Let lrel_asym_output := (lrel_G * lrel_G)%lrel.
Lemma aenc_sem_typed :
⊢ refines top enc enc (kemdem_hybrid_cpa_instance_rf.lrel_pk → lrel_G → lrel_asym_output).
Proof with (rel_pures_l; rel_pures_r).
rewrite /pubkey_class.enc...
rewrite /elgamal_scheme...
rewrite /enc...
rel_arrow_val.
iIntros (v1 v2 [pk [eq1 eq2]]); subst...
rel_arrow_val.
iIntros (msg1 msg2 [msg [eq1 eq2]]); subst...
rel_apply refines_couple_UU; first done.
iModIntro; iIntros (n Hnbound)...
rel_apply refines_exp_l.
rel_apply refines_exp_r...
rel_apply refines_exp_l.
rel_apply refines_exp_r...
rel_apply refines_mult_l.
rel_apply refines_mult_r...
rel_vals; iExists _; done.
Qed.
Lemma asym_rand_cipher_couple :
∀ (v v' : val) K K' E A,
(∀ r r', lrel_asym_output r r' -∗
refines E (fill K (Val r)) (fill K' (Val r')) A)
⊢ refines E (fill K (pubkey_class.rand_cipher v))
(fill K' (pubkey_class.rand_cipher v')) A.
Proof with (rel_pures_l; rel_pures_r).
iIntros (v v' K K' E A) "H".
rewrite /pubkey_class.rand_cipher...
rewrite /elgamal_scheme...
rel_apply refines_couple_UU; first done.
iModIntro; iIntros (n Hnbound)...
rel_apply refines_couple_UU; first done.
iModIntro; iIntros (b Hbbound)...
rel_apply refines_exp_l;
rel_apply refines_exp_r;
rel_apply refines_exp_l;
rel_apply refines_exp_r...
rel_apply "H".
iExists _, _, _, _.
iSplit; last iSplit; [done|done|].
iSplit; iExists _; done.
Qed.
Lemma rand_cipher_sem_typed :
⊢ refines top symmetric_init.rand_cipher
symmetric_init.rand_cipher (kemdem_hybrid_cpa_generic.lrel_trivial → lrel_output).
Proof with (rel_pures_l; rel_pures_r).
rewrite /symmetric_init.rand_cipher... simpl.
rewrite /one_time_pad.otp_rand_cipher...
rel_arrow_val.
iIntros (v1 v2) "_"...
rel_apply refines_couple_UU; first done.
iIntros (i Hibound); iModIntro... rel_vals.
iExists i; iPureIntro; repeat split; lia.
Qed.
#[warnings="-notation-incompatible-prefix"]
Import fingroup.
Lemma asym_key_lr_l_r :
∀ sk pk, (@kemdem_hybrid_cpa_instance_rf.elgamal_is_asym_key_lr _ _ Σ) sk pk
-∗ kemdem_hybrid_cpa_instance_rf.elgamal_is_asym_key_l sk pk ∗ kemdem_hybrid_cpa_instance_rf.elgamal_is_asym_key_r sk pk.
Proof. rewrite /Persistent.
iIntros (sk pk) "#H". iSplit;
last rewrite /kemdem_hybrid_cpa_instance_rf.elgamal_is_asym_key_r; rewrite /kemdem_hybrid_cpa_instance_rf.elgamal_is_asym_key_l/kemdem_hybrid_cpa_instance_rf.elgamal_is_asym_key_lr;
iDestruct "H" as "[%k [[%eqsk %Hkbound] %eqpk]]"; subst.
- iExists #k, (vgval (g ^+ (Z.to_nat k))), k. iPureIntro; repeat split; lia.
- iExists #k, (vgval (g ^+ (Z.to_nat k))), k. iPureIntro; repeat split; lia.
Qed.
#[local] Instance elgamal_props :
@kemdem_hybrid_cpa_generic.asym_scheme_props _ _ _ _ _ _ _ _ _ _ _.
Proof. unshelve econstructor.
- eapply is_asym_key_lrel.
- eapply asym_key_lr_l_r.
- eapply elgamal_refines_akeygen_l.
- eapply elgamal_refines_akeygen_r.
- eapply elgamal_refines_akeygen_couple.
- eapply elgamal_refines_aenc_l.
- eapply aenc_sem_typed.
- eapply asym_rand_cipher_couple.
- eapply rand_cipher_sem_typed.
Defined.
Lemma is_asym_key_l_persistent : ∀ sk pk, Persistent ((@kemdem_hybrid_cpa_instance_rf.elgamal_is_asym_key_l _ _ Σ) sk pk).
Proof. rewrite /Persistent.
iIntros (sk pk) "#H". iAssumption.
Qed.
Lemma is_asym_key_r_persistent : ∀ sk pk, Persistent ((@kemdem_hybrid_cpa_instance_rf.elgamal_is_asym_key_r _ _ Σ) sk pk).
Proof. rewrite /Persistent.
iIntros (sk pk) "#H". iAssumption.
Qed.
Lemma is_asym_key_lr_persistent : ∀ sk pk, Persistent ((@kemdem_hybrid_cpa_instance_rf.elgamal_is_asym_key_lr _ _ Σ) sk pk).
Proof. rewrite /Persistent.
iIntros (sk pk) "#H". iAssumption.
Qed.
Section Correctness.
Import mathcomp.fingroup.fingroup.
Let dec_hyb := @kemdem_hybrid_cpa_generic.dec_hyb _ _ _ elgamal_scheme.
Let enc_hyb := @kemdem_hybrid_cpa_generic.enc_hyb otp_SYM_param sym_otp_scheme_inst _ _ _ elgamal_scheme.
Lemma hybrid_scheme_correct :
⊢ refines top
(kemdem_hybrid_cpa_generic.init_scheme (λ: "scheme", (let, ("sk", "pk") := pubkey_class.keygen #() in
λ:"msg", dec_hyb "scheme" "sk"
(enc_hyb "scheme" "pk" "msg"))))
(λ: "msg", "msg")%V
(lrel_input → lrel_input).
Proof.
rewrite /dec_hyb/enc_hyb.
iStartProof.
iPoseProof kemdem_hybrid_cpa_generic.hybrid_scheme_correct as "H".
- exact SymKey.
- exact SymKey.
- exact SymOutput.
- exact Δ.
- rewrite /kemdem_hybrid_cpa_generic.is_asym_key_l. simpl.
exact is_asym_key_l_persistent.
- rewrite /kemdem_hybrid_cpa_generic.is_asym_key_l. simpl.
exact is_asym_key_r_persistent.
- rewrite /kemdem_hybrid_cpa_generic.is_asym_key_l. simpl.
exact is_asym_key_lr_persistent.
- rewrite /SymKey/SymOutput. simpl.
rel_apply "H".
Qed.
End Correctness.
Let lrel_kemdem_output : lrel Σ := lrel_output * lrel_asym_output.
Let pk_real := @kemdem_hybrid_cpa_generic.pk_real _ _ _ _ _ elgamal_scheme.
Lemma rf_pk_real_adv :
⊢ refines top (kemdem_hybrid_cpa_generic.init_scheme
(kemdem_hybrid_cpa_generic.pk_real N N
N))
(kemdem_hybrid_cpa_generic.init_scheme
kemdem_hybrid_cpa_generic.adv_pk_real
pubkey_class.CPA_OTS_real) (kemdem_hybrid_cpa_generic.lrel_pk *
(kemdem_hybrid_cpa_generic.lrel_input
→ () +
kemdem_hybrid_cpa_generic.lrel_output *
kemdem_hybrid_cpa_generic.lrel_asym_output))%lrel.
Proof.
eapply (kemdem_hybrid_cpa_generic.pk_real_adv SymKey SymKey SymOutput).
- exact Δ.
- rewrite /kemdem_hybrid_cpa_generic.is_asym_key_l. simpl.
exact is_asym_key_l_persistent.
- rewrite /kemdem_hybrid_cpa_generic.is_asym_key_l. simpl.
exact is_asym_key_r_persistent.
- rewrite /kemdem_hybrid_cpa_generic.is_asym_key_l. simpl.
exact is_asym_key_lr_persistent.
- exact _.
- exact _.
Qed.
(* here we use the DDH assumption: we replace CDDHreal by CDDHrand *)
Lemma rf_adv__pk_real_arand :
⊢ refines top
(kemdem_hybrid_cpa_generic.init_scheme
kemdem_hybrid_cpa_generic.adv_pk_real pubkey_class.CPA_OTS_rand)
(kemdem_hybrid_cpa_generic.init_scheme
(@kemdem_hybrid_cpa_generic.pk_real_arand _ _ _ _ _ elgamal_scheme))
(kemdem_hybrid_cpa_generic.lrel_pk *
(kemdem_hybrid_cpa_generic.lrel_input →
() + kemdem_hybrid_cpa_generic.lrel_output * kemdem_hybrid_cpa_generic.lrel_asym_output))%lrel.
Proof. eapply kemdem_hybrid_cpa_generic.adv__pk_real_arand.
- exact SymKey.
- exact SymKey.
- exact SymOutput.
- exact Δ.
- rewrite /kemdem_hybrid_cpa_generic.is_asym_key_l. simpl.
exact is_asym_key_l_persistent.
- rewrite /kemdem_hybrid_cpa_generic.is_asym_key_l. simpl.
exact is_asym_key_r_persistent.
- rewrite /kemdem_hybrid_cpa_generic.is_asym_key_l. simpl.
exact is_asym_key_lr_persistent.
- exact _.
- exact _.
Qed.
Lemma rf_pk_real_arand_perm__adv :
⊢ refines top (kemdem_hybrid_cpa_generic.init_scheme
(@kemdem_hybrid_cpa_generic.pk_real_arand_permute _ _ _ _ _ elgamal_scheme))
(kemdem_hybrid_cpa_generic.OTS #true
(@kemdem_hybrid_cpa_generic.adv_pk_real_arand_permute _ _ _ elgamal_scheme) symmetric_init.sym_scheme)
(kemdem_hybrid_cpa_generic.lrel_pk *
(kemdem_hybrid_cpa_generic.lrel_input → () +
kemdem_hybrid_cpa_generic.lrel_output * kemdem_hybrid_cpa_generic.lrel_asym_output))%lrel.
Proof. eapply kemdem_hybrid_cpa_generic.pk_real_arand_perm__adv.
- exact SymKey.
- exact SymKey.
- exact SymOutput.
- exact Δ.
- rewrite /kemdem_hybrid_cpa_generic.is_asym_key_l. simpl.
exact is_asym_key_l_persistent.
- rewrite /kemdem_hybrid_cpa_generic.is_asym_key_l. simpl.
exact is_asym_key_r_persistent.
- rewrite /kemdem_hybrid_cpa_generic.is_asym_key_l. simpl.
exact is_asym_key_lr_persistent.
- exact _.
- exact _.
Qed.
Lemma rf_adv__pk_rand_srand :
⊢ refines top
(kemdem_hybrid_cpa_generic.OTS #false
(@kemdem_hybrid_cpa_generic.adv_pk_real_arand_permute _ _ _ elgamal_scheme)
symmetric_init.sym_scheme)
(@kemdem_hybrid_cpa_generic.pk_rand_srand _ _ _ _ _ elgamal_scheme)
(kemdem_hybrid_cpa_generic.lrel_pk *
(kemdem_hybrid_cpa_generic.lrel_input → () +
kemdem_hybrid_cpa_generic.lrel_output * kemdem_hybrid_cpa_generic.lrel_asym_output))%lrel.
Proof. eapply kemdem_hybrid_cpa_generic.adv__pk_rand_srand.
- exact SymKey.
- exact SymKey.
- exact SymOutput.
- exact Δ.
- rewrite /kemdem_hybrid_cpa_generic.is_asym_key_l. simpl.
exact is_asym_key_l_persistent.
- rewrite /kemdem_hybrid_cpa_generic.is_asym_key_l. simpl.
exact is_asym_key_r_persistent.
- rewrite /kemdem_hybrid_cpa_generic.is_asym_key_l. simpl.
exact is_asym_key_lr_persistent.
- exact _.
- exact _.
Qed.
Lemma rf_pk_rand_srand__rand :
⊢ refines top (@kemdem_hybrid_cpa_generic.pk_rand_srand _ _ _ _ _ elgamal_scheme)
(@kemdem_hybrid_cpa_generic.pk_rand _ _ _ _ _ elgamal_scheme)
(kemdem_hybrid_cpa_generic.lrel_pk *
(kemdem_hybrid_cpa_generic.lrel_input → () +
kemdem_hybrid_cpa_generic.lrel_output * kemdem_hybrid_cpa_generic.lrel_asym_output)).
Proof. eapply kemdem_hybrid_cpa_generic.pk_rand_srand__rand.
- exact SymKey.
- exact SymKey.
- exact SymOutput.
- exact Δ.
- rewrite /kemdem_hybrid_cpa_generic.is_asym_key_l. simpl.
exact is_asym_key_l_persistent.
- rewrite /kemdem_hybrid_cpa_generic.is_asym_key_l. simpl.
exact is_asym_key_r_persistent.
- rewrite /kemdem_hybrid_cpa_generic.is_asym_key_l. simpl.
exact is_asym_key_lr_persistent.
- exact _.
- exact _.
Qed.
End logrel.
End Hybrid_scheme.