Sebastian Ertel (Apr 17 2023 at 08:15): Sebastian Ertel (Apr 17 2023 at 08:15):Dear SSProvers,
thanks a lot for building the SSProve framework and also for creating this stream, i.e., taking your time to answer questions.
(I apologize for the length of this question which comes primarily from the code itself.)
We would like to formally verify the security properties of well-established protocols and our extensions thereof. SSProve seems like interesting fit for us.
To better understand SSProve, we tried to formalize a first protocol (details below). What we realized so far:
the hard work for the developer using SSProve comes from r_uniform_bij lemma/uniform rule in the paper. It associates both sides, more specifically monadic sample uniform calls, via a function f that is required to be bijective.
Either this seems to have profound implications on the code or there is a pattern to apply this rule that I have not understood yet (probably the latter).
Any help on this would be greatly appreciated.
Here is the example as (mostly) consecutive code for better copy-pasting. The example is Diffie-Hellmann (DH) which is also in the repo but does not have a security proof. (It is redefined in ElGamal.vbut the proof is different because it uses an auxiliary package.) Our definition is almost identical to your, modulo minor changes. That is why I skip the imports.
Module Type DHParams.
Parameter gT : finGroupType.
Definition ζ : {set gT} := [set : gT].
Parameter g : gT.
Parameter g_gen : ζ = <[g]>.
Parameter prime_order : prime #[g].
End DHParams.
Module Type DHAux (DHP : DHParams).
Import DHP.
#[local] Open Scope package_scope.
Definition GroupSpace : finType := FinGroup.arg_finType gT.
#[local] Instance GroupSpace_pos : Positive #|GroupSpace|.
Proof. apply /card_gt0P; by exists g. Defined.
Definition chGroup : choice_type := 'fin #|GroupSpace|.
Notation " 'group " := (chGroup) (in custom pack_type at level 2).
Definition p := #[g].
Lemma p_gt1 : (1 < p)%N.
Proof. apply (prime_gt1 prime_order). Qed.
#[export] Instance p_pos : Positive p.
Proof. rewrite /p/Positive. move: p_gt1; rewrite /p //=. Defined.
Definition chPElem : choice_type := 'fin p.
End DHAux.
Module DiffieHellman (DHP : DHParams) (DHAux : DHAux DHP)
Import DHP.
Import DHAux.
Definition DDH : nat := 0.
Definition sk_A : Location := (chPElem ; 0%N).
Definition sk_B : Location := (chPElem ; 1%N).
Definition fk : Location := (chPElem ; 2%N).
Definition L__0 := fset [:: sk_A ; sk_B].
Definition L__1 := L__0 :|: fset [:: fk].
#[local] Open Scope package_scope.
Definition Game__Import : Interface := [interface].
Definition Game__Export : Interface := [interface #val #[ DDH ] : 'unit → 'group × 'group × 'group].
Definition DH__real: package L__0 Game__Import Game__Export
:=
[package
#def #[ DDH ] (_ : 'unit) : 'group × 'group × 'group
{
sk_alice ← sample uniform p ;;
sk_bob ← sample uniform p ;;
#put sk_A := sk_alice ;;
#put sk_B := sk_bob ;;
sk_alice' ← get sk_A ;;
let e_a := (g^+ sk_alice') in
sk_bob' ← get sk_B ;;
let e_b := (g^+ sk_bob') in
let e_a_at_bob := e_a in
let e_b_at_alice := e_b in
let fk_alice := (e_b_at_alice^+ sk_alice') in
let fk_bob := (e_a_at_bob^+ sk_bob') in
ret (fto e_a , (fto e_b, fto fk_alice))
}
].
Lemma sk_A_in_L__1: sk_A \in L__1. Admitted.
Lemma sk_B_in_L__1: sk_B \in L__1. Admitted.
Lemma fk_in_L__1: fk \in L__1. Admitted.
Definition DH__ideal: package L__1 Game__Import Game__Export.
refine(
[package
#def #[ DDH ] (_ : 'unit) : 'group × 'group × 'group
{
a ← sample uniform p ;;
b ← sample uniform p ;;
c ← sample uniform p ;;
#put sk_A := a ;;
#put sk_B := b ;;
#put fk := c ;;
ret (fto (g^+ a), (fto (g^+ b), fto (g^+ c)))
}
]).
ssprove_valid.
- apply sk_A_in_L__1.
- apply sk_B_in_L__1.
- apply fk_in_L__1 .
Defined.
Definition ɛ__DH A := AdvantageE DH__real DH__ideal A.
(I have proofs for the admitted lemmas, of course.) Note that we essentially calculate g^+b^+c instead of g^+ (b*c). But
Check expgM.
(* expgM
: ∀ (T : baseFinGroupType) (x : FinGroup.arg_sort T) (n m : nat), x ^+ (n * m) = x ^+ n ^+ m *)
Conceptually, the real code has 2 sampling calls while the ideal has 3. We would therefore like to teach Coq/SSProve that the real computation of fk_alice provides the same information to the attacker as sampling c and computing g^+c. Hence, the proof needs to actually encapsulate the computation performed in the real code as a bijective functionf. I did that and proved the following lemma:
Lemma mul_inv : forall (a b : 'Z_q),
prime q -> b != 0 -> (Zp_mul (Zp_mul a b) (Zp_inv b)) = a.
Hence, my "setup" is done.
Here is the SSProve proof so far:
Theorem DDH__security : ∀ L__A A,
ValidPackage L__0 Game__Import Game__Export DH__real →
ValidPackage L__1 Game__Import Game__Export DH__ideal →
ValidPackage L__A Game__Export A_export A →
fdisjoint L__A L__0 →
fdisjoint L__A L__1 →
ɛ__DH A = 0.
Proof.
intros.
eapply eq_rel_perf_ind_ignore.
- exact H.
- exact H0.
- apply ignored_is_subset.
- simplify_eq_rel x.
ssprove_code_simpl_more.
ssprove_sync. intros.
(* Take care of the put/get combos. *)
ssprove_swap_lhs 0%N.
ssprove_swap_lhs 2%N.
ssprove_swap_lhs 1%N.
ssprove_contract_put_get_lhs.
ssprove_swap_rhs 1%N.
ssprove_swap_rhs 0%N.
ssprove_sync.
Now I need to turn the two sampling calls in the ideal code into a single one to continue matching side-by-side:
eapply r_transR.
1: { eapply r_uniform_prod. intros. eapply rreflexivity_rule. }
simpl.
Now I'm ready to apply r_uniform_bij:
eapply r_uniform_bij.
But function f now naturally needs to be:
Axiom Aritp_Zp : Arit (uniform p) -> 'Z_p.
Axiom Zp_Aritp : 'Z_p -> Arit (uniform p).
Definition f (a : Arit (uniform p)): Arit (uniform p) -> Arit (uniform (p * p)) :=
fun b =>
let c := f' p (Aritp_Zp a) (Aritp_Zp b) in
prod2ch (b, Zp_Aritp c).
(I also implemented the conversions and have bijectivity proofs for them.)
But function f cannot be bijective because it uses b twice. Once it by-passes b but it also uses b to compute the second value of the return tuple.
More specifically, I can define either:
Definition f_inv (a : Arit (uniform p)) : Arit (uniform (p * p)) → Arit (uniform p) :=
fun x => let '(b,_) := ch2prod x in b.
or
Definition f_inv (a : Arit (uniform p)) : Arit (uniform (p * p)) → Arit (uniform p) :=
fun x => let '(_,c) := ch2prod x in Zp_Aritp (f_inv' p (Aritp_Zp a) (Aritp_Zp c)).
In both cases I can prove cancel f f_inv but never cancel f_inv f.
But the type of the bijective function is dictated by the code itself.
What is the proper way of dealing with this situation in SSProve?
Benjamin Salling Hvass (Apr 18 2023 at 07:58):Thanks for the question. What are f' and f_inv' in the definitions of f and f_inv? Are they related to f' from ElGamal.v?
Sebastian Ertel (Apr 18 2023 at 08:07):Thanks @Benjamin Salling Hvass for having a look at this.
Ah sorry :(
Definition f' {q: nat} (a : 'Z_q) : 'Z_q -> 'Z_q := fun b => Zp_mul b a.
Definition f_inv' {q: nat} (a : 'Z_q) : 'Z_q -> 'Z_q := fun c => Zp_mul c (Zp_inv a).
For which I have proven:
Lemma f_bij {q:nat} : forall (a : 'Z_q),
prime q ->
(0 != a) ->
bijective (f' a).
Note that I left out the second requirement 0!=a from the code so far.
I plan to just add this requirement as an assertion to the real and ideal code as follows:
a ← sample uniform p ;;
#assert (0 != Aritp_Zp a) ;;
Hm, I'm not entirely sure what the solution is, but note that applying r_uniform_bij can never work, since the two types that you are sampling from have different sizes (p vs. p * p).
Sebastian Ertel (Apr 18 2023 at 09:36):That I do not understand.
Sampling is in the same space uniform p but uniform (p * p) samples a tuple.
That is, it samples two values instead of single one. That is also what the r_uniform_prod rule says (if I'm not mistaken).
Benjamin Salling Hvass (Apr 18 2023 at 09:38):Sorry I wasn't being clear: The proof goal when you apply r_uniform_bij is
{ ... }
a <- sample uniform p ;; ...
\equiv
b <- sample uniform (p * p) ;; ...
{ ... }
r_uniform_bij cannot solve such a goal, since p and p * p are not the same size (thus no bijection can exist).
Sebastian Ertel (Apr 18 2023 at 09:43):Sorry, I do not understand what you mean by size here.
If you refer to (p * p) then I thought that saying
ab <- sample uniform (p * p) ;;
let '(a,b) = ch2prod ab in c
is the same as saying:
a <- sample uniform p ;;
b <- sample uniform p ;;
c
That is also what the r_uniform_prod rule states.
Am I mistaken here?
Benjamin Salling Hvass (Apr 18 2023 at 09:44):No, that is correct, but when I go through the proof you sent, I get to a goal where you sample from p on the LHS and p * p on RHS, right?
Sebastian Ertel (Apr 18 2023 at 09:58):That is correct.
Benjamin Salling Hvass (Apr 18 2023 at 09:59):In that case r_uniform_bij does not apply, since it requires there is a bijection from fin p to fin (p * p).
Sebastian Ertel (Apr 18 2023 at 10:06):That is my problem, yes. But that is not the case in general.
I could certainly define such a function:
Definition f : Arit (uniform p) -> Arit (uniform (p * p)) := fun b => (b,b).
And this function would be bijective.
So it is not a general observation that there is no bijective function f for the type Arit (uniform p) -> Arit (uniform (p * p)).
Sebastian Ertel (Apr 18 2023 at 10:08):That is why my question is:
Is there a SSProve proof for my DH code or would I have to write my code differently?
Benjamin Salling Hvass (Apr 18 2023 at 10:16):Sebastian Ertel said:
That is why my question is:
Is there a SSProve proof for my DH code or would I have to write my code differently?
I believe there is, one following the same strategy as in ElGamal.v.
Benjamin Salling Hvass (Apr 18 2023 at 10:16):Sebastian Ertel said:
That is my problem, yes. But that is not the case in general.
I could certainly define such a function:Definition f : Arit (uniform p) -> Arit (uniform (p * p)) := fun b => (b,b).And this function would be bijective.
So it is not a general observation that there is no bijective functionffor the typeArit (uniform p) -> Arit (uniform (p * p)).
What is the inverse of this function?
Théo Winterhalter (Apr 18 2023 at 11:01):I think Benjamin means cardinality when he says size. An invariant of bijections.
Théo Winterhalter (Apr 18 2023 at 11:02):But it's possible that you would like to use a rule that we have not yet implemented.
Sebastian Ertel (Apr 18 2023 at 11:46):@Benjamin Salling Hvass , there is an inverse to the function I defined above but I cannot prove surjectivity.
Thanks @Théo Winterhalter for the clarification on the cardinality. That makes sense to me now.
The ElGamal.v version is really quite different.
It shows perfect indistinguishability of DH_real and Asymmetric encryption (real). It does the same for the ideal cases and then uses both facts in a triangle inequality proof.
So I guess the answer to my question is then:
For now, I will have to find out how to perform this proof using the same triangle inequality.
Is that correct?
What would be the new rule?
Théo Winterhalter (Apr 18 2023 at 11:52):I'm not sure what rule you actually need, I just wanted to point out that not everything that is provable has a corresponding rule, we basically only proved those we needed, but it might be there is a more general rule than bijection which applies. I personally lack intuition about couplings…
Sebastian Ertel (Apr 18 2023 at 11:53):Ah I see.
Last updated: Oct 13 2024 at 01:02 UTC