Add new assumptions and move the DDH #81
Conversation
ErVinuelas
requested review from
4ever2 and
cmester0
and removed request for
4ever2 and
cmester0
|
I like the idea. Could you add some minimal documentation? A README in the directory with an explanation of the abbreviations, although they are fairly standard... |
|
I have added the README, let me know what you think @spitters. |
| ### Overview | ||
|
|
||
| The t-Strong Diffie-Hellman assumption posits that given a randomly chosen \( α \in \mathbb{Z}_p^*\) | ||
| and a \((t + 1)\)-tuple \((g, g^α, g^{α^2}, ..., g^{α^t})\in \mathbb{G}^{t+1} \), it is computationally infeasible for an adversary to find a \( c \in \mathbb{Z}_p - \{-α \}\) such that \( g^{1/(α + c)}\). |
There was a problem hiding this comment.
The math in the readme doesn't render correctly. You can fix this by adding $ around the equations instead of "\( \)".
There was a problem hiding this comment.
such that ( g^{1/(α + c)}).
This is not a proposition. Something seems to be missing here.
| @@ -0,0 +1,158 @@ | |||
| From SSProve.Relational Require Import OrderEnrichedCategory GenericRulesSimple. | |||
There was a problem hiding this comment.
A small header in each file would be good. It doesn't have to be super detailed since you added the README, but it would be good to at least mention in the header what the file formalizes.
| Definition tSDH b : game tSDH_E := | ||
| if b then tSDH_tt else tSDH_ff. | ||
|
|
||
| Definition ϵ_tSDH := Advantage tSDH. |
There was a problem hiding this comment.
The indentation is off here.
|
I made some minor suggestions. |
| Parameter positive_order : Positive #[g]. | ||
| Parameter order_gr_two : (#[g] > 2)%N. | ||
|
|
||
| Parameter t : nat. |
There was a problem hiding this comment.
These parameters look odd to me. From the other assumptions it is provable that #[g] > 1 like here in Schnorr.v where it is also used to work with inverse exponents. It looks like you are also trying to do that here, unless I am missing something?
positive_order is also provable from the other assumptions and t seems like it belongs as a separate parameter in tSDH.
|
|
||
| #def #[ guess ] (y: 'group) : 'bool | ||
| { | ||
| x ← get secret_loc ;; |
There was a problem hiding this comment.
Watch out for the implicit initialization of locations. secret_loc is initialized with a known value (0), so an adversary that calls guess with y^0 before calling set_up will distinguish DL_real and DL_ideal.
You can compare to my definition here, which prevents this by using an option value:
https://github.com/MarkusKL/nominal-ssprove/blob/dev-std/theories/Std/Assumptions/DL.v#L38
There was a problem hiding this comment.
The tSDH definition has the same problem.
|
Overall this looks good. Thanks. This may not be for you to solve now, but I wanted to note that at this point many files define their own |
Added some assumptions needed for the polynomial/KZG commitments. Moved all the assumptions I am aware of to a new folder.