search

WalletWasabi / WabiSabi

MIT License
100 stars 27 forks source link

Protocol: ACL based #16

Closed nothingmuch closed 4 years ago

nothingmuch commented 4 years ago

Mostly copypasta of #15, but with concrete signature scheme. This protocol is based on the paper: Anonymous Credentials Light (ACL) by Foteini Baldimtsi and Anna Lysyanskaya.

Amount Splitting

User has UTXO with value v and wants to split it into outputs with values v_1 and v_2 such that v = v_1 + v_2.

Input Registration

User creates n Pedersen Commitments: C_1 = C(v_1, r_1), C_2 = C(v_2, r_2), C_3 = C(v_3, r_3), C_4 = C(v_4, r_4), \dots, C_n = C(v_n, r_n,) where \forall i \in 3 \dots n: v_i = 0. The v_i terms correspond to a single attribute L_0 in an ACL signature with an empty message, with a range proofs for each.

The user also needs to prove the sum of the commitments - I think this can just be done revealing \sum_{i=1}^n r_i and letting the coordinator ensure that the combined commitment is a commitment to the public input amount with this randomness, but if this is problematic for the ACL security proof this can probably be proved in another ways.

From this protocol the user obtains n signatures for n commitments \zeta_{1.n} in a way where the following properties hold:

Output Registration

User can register a desired output for v_1 by sending the coordinator

Notice that, the first subscript of \zeta is part of the variable name in the paper, while the second one denotes the index of the amount commitment.

Amount Merging

The protocol is the same, except instead of only registering signed zero commitments at output registration, some of those commitments aren't zero, but maybe they were coming from different inputs.

Unlinkability

Since the coordinator cannot recognize the unblinded signatures at output registration, it can only tell they are valid, unlinkability is guaranteed.

Double Spend

Since the unblinded signatures are valid for single blinded commitments only, the coordinator can make sure one signature can only be used once.

nothingmuch commented 4 years ago

Variable names should correspond to Section 5 of the Anonymous Credentials Light (ACL) paper.

an open question is how to set up the tag key z - seems like we probably just want a NUMS point?

for an intuition on the way the blinding works with the tag key, see Abe's paper.

it's noteworthy that the blinding/unlinkability is based on computational hardness, so if i'm not mistaken if the coordinator has a quantum computer or the underlying curve is broken then the coordinator would be able to de-anonymize users after the fact, but this doesn't seem like a concern since that would require bitcoin users to move all their funds anyway

finally, i don't understand the security proofs of ACL yet, but in the wasabi research club call about it Jonas mentioned the log of the group order needs to be larger than the security parameter. if this is only an issue for soundness then i don't think this is a problem, since a soundness break only leads to blameless DoS, and the coinjoin security model still applies WRT theft.

nopara73 commented 4 years ago

The user also needs to prove the sum - i think this can just be done revealing \sum_{i=1}^n r_i and letting the coordinator ensure that the combined commitment is a commitment to the public input amount with this randomness, but if this is problematic for the ACL security proof this can probably proved otherwise.

AFAIK revealing the sum of the r values is enough.

nothingmuch commented 4 years ago

to prove the amount it's enough, what I'm not sure about is whether or not this might interferes with the provable security of ACL, in particular blindness/unlinkability.

during registration you can reveal some of the attributes' values instead of proving their validity in zero knowledge, so i suspect this is not an issue, and intuitively revealing a sum says nothing about the individual summands so i suspect even if the proof of blindness relies on the randomness in the \zeta_1 commitment not being revealed to the adversary, revealing the sum of several of these would be OK. (edit: i got confused about proving the sum at input and output registration time, i don't think this is a problem at input registration)

but I want to be sure.

nothingmuch commented 4 years ago

I had a mistake in the derivation of \product_{i} \zeta_{1.i} terms - since the gamma term (blinding factor) applies to all generators, but the amount only applies to generator h_0, the this would require a combination of sub-amounts that has no 0 terms to avoid cancelling out the gamma terms.

So this means that we don't get signatures over commitments that are homomorphic in the amounts as simply as in #10 or #5.

nothingmuch commented 4 years ago

I think this works: (nope, it's broken, @seresistvanandras points out: since the curve is a cyclic group of prime order q, and finding the inverse of some factor c in the scalar field Z_q is easy, this means that a malicious user can trivially claim multiples of their actual amount by correctly computing s as below, but then submitting s^{1/c} to claim c*v_out)

\zeta_{1.i} denotes the different Pedersen commitments and \sigma_i the corresponding signatures the user obtained through the signing protocol.

Let S be the the set of indices that the user want to sum in a single output and v_{\mathrm{out}} = \sum_{i \in S} v_i be the desired output amount (note that v_{\mathrm{out}} \mod q = v_{\mathrm{out}} \ll q as per the range proofs over the limited number of summands)

To prove a valid sum without revealing the summands, the coordinator needs to ensure that the the product of the commitment is commits to the right value. The user can prove this to the coordinator by producing a group element s, such that the coordinator can verify the sum:

$\prod_{i \in S} \zeta_{1.i} \stackrel{?}{=} s^{v_{\mathrm{out}}}$

The user can calculate this because she knows all of the exponents:

$\prod_{i \in S} \zeta_{1.i} = \prod_{i \in S} h_1^{\gamma_i v_i} h_0^{\gamma_i R_i} g^{\gamma_i \mathrm{rnd}_i} = \left(\prod_{i \in S} h_1^{\left(\frac{\gamma_i v_i}{v_{\mathrm{out}}}\right)} h_0^{\left(\frac{\gamma_i R_i}{v_{\mathrm{out}}}\right)} g^{\left(\frac{\gamma_i \mathrm{rnd}_i}{v_{\mathrm{out}}}\right)}\right)^{v_{\mathrm{out}}}$%5E%7Bv_%7B%5Cmathrm%7Bout%7D%7D%7D%24)

At output registration time the user submits v_{\mathrm{out}}, s and for each i \in S the pair \zeta_{1.i}, \sigma_i. The coordinator verifies the signatures individually, ensuring they haven't been used before, and then computes the product of the commitments and s^{v_{\mathrm{out}}} to verify that the sum equation holds.

nothingmuch commented 4 years ago

About the unused message m and provable security: it seems it is the opposite, in this paper it is specifically removed, keeping only the attributes, in order to prove EUF-CMA security more generally (the ACL paper only proves it WRT sequential setting, whereas this variant is proven in concurrent one).

This paper also presents the ACL protocol with this very minor modification in additive notation, which is probably more readable for bitcoin audiences, where that seems to be standard.

seresistvanandras commented 4 years ago

Hereby a fix for the coin merging protocol is suggested by @nothingmuch and me. Again, we want to prove that the following relation holds between blinded commitments and a specially crafted point on the curve, $s$. One lesson from the attack described above, that we need to constrain the user on how to select $s$, otherwise she could lie about it.

$\prod_{i \in S} \zeta_{1.i} \stackrel{?}{=} s^{v_{\mathrm{out}}}$

Specifically the blinded commitments $\zeta_{1.i}$ have the following structure: $\prod_{i \in S} \zeta_{1.i} = \prod_{i \in S} h_1^{\gamma_i v_i} h_0^{\gamma_i R_i} g^{\gamma_i \mathrm{rnd}_i}$.

Note that the user knows all the exponents present in the expression above, however user obviously does not know the discrete logarithms between the generators $g,h_0,h_1$, because then the commitment scheme would not be computationally binding. The user can therefore create the following terms separately for each $\zeta_{1.i}$: $h_1^{\gamma_i v_i}$, h_0^{\gamma_i R_i} , g^{\gamma_i \mathrm{rnd}_i}. Subsequently the user will prove that each of these terms contain $\gamma_i$ in their exponent without disclosing anything about $\gamma_i$. Put differently, user proves that the following tuple is a Diffie-Hellman tuple: $(h_1,h^{\gamma_i}_1,h_1^{v_i},h_1^{\gamma_{i}v_{i}})$.

After revealing all these elements it is easy to verify the relation we want to prove to the coordinator by checking:

$\prod_{i\in S}h_1^{v_i}=h_1^{\Sigma_{i\in S}v_i}=h_1^{v_\textit{out}}$

With this approach in place we do assume that an appropriate padding scheme is used for the values $v_i$ to have a sufficiently large message space for the values $v_i$. Otherwise coordinator could just figure out $h_1^{v_i}$ by brute-forcing the exponent.

However two crucial questions remain which are not immediate IMO:

  1. Do we harm blindness of ACL by revealing this many new elements in the Diffie-Hellman tuples?

  2. Do we really achieve soundness with this fix?

Maybe we do not harm neither 1) nor 2) but we additionally need to assume the Diffie-Hellman assumption for the soundness of the coin merging protocol and for the blindness of the ACL scheme to hold. We should try to prove blindness and soundness formally on our own and then see whether we can prove it with these modifications or not.

nothingmuch commented 4 years ago

i don't think there is a benefit to making that verification equation work on public values.

assuming soundness is addressed by these additional relations, i think the sum amount should also be done in zero knowledge, with only v_out as just a term in the relation being proved, so that the individual h_1^x as well as their product remain secret

seresistvanandras commented 4 years ago

i don't think there is a benefit to making that verification equation work on public values.

Why? The only public value used is the registered output UTXO amount. All the rest is computationally unrecoverable assuming that the Discrete Logarithm Problem is hard in the underlying group.

assuming soundness is addressed by these additional relations, i think the sum amount should also be done in zero knowledge, with only v_out as just a term in the relation being proved, so that the individual h_1^x as well as their product remain secret

I don't understand these arguments. If soundness is addressed then we are ready and don't need to work anymore. More precisely, if soundness is addressed then everything can be left unchanged in the protocol and used as it is, it would be unnecessary to hide any more elements as soundness is already achieved. If you want all the $h_i^{v_i}$ terms remain secret, then the whole coin merging protocol will be significantly more complex and I'm not yet convinced that it is necessary to hide those terms. My bet is that soundness is already achieved but not 100% sure yet.

nothingmuch commented 4 years ago

hmm, maybe i misunderstood:

After revealing all these elements it is easy to verify the relation we want to prove to the coordinator by checking:

$\prod_{i\in S}h_1^{v_i}=h_1^{\Sigma_{i\in S}v_i}=h_1^{v_\textit{out}}$

does this imply the coordinator computes the product out of individual h_1^{v_i} terms?

i understood yes (because otherwise padding the amounts would be unnecessary)

the reason i expect a single proof to be simpler is that verifying the sum should a single linear constraint on the v_i secret inputs which must be proven to be committed to anyway, whereas adding padding terms to rule out brute forcing makes the range proof relations much larger, each inner product would have an additional 128 multiplications in the inner product, and 128 multiplications checking that the bit vector components are in the subset {0, 1} \subseteq Z_q. technically the structure of the proof is as simple as the non-padded case, but the statements are much larger, and even with bulletproofs verification and proving time are still O(N)

seresistvanandras commented 4 years ago

After revealing all these elements it is easy to verify the relation we want to prove to the coordinator by checking: $\prod_{i\in S}h_1^{v_i}=h_1^{\Sigma_{i\in S}v_i}=h_1^{v_\textit{out}}$

does this imply the coordinator computes the product out of individual h_1^{v_i} terms?

i understood yes (because otherwise padding the amounts would be unnecessary)

Yes, your understanding is correct!

the reason i expect a single proof to be simpler is that verifying the sum should a single linear constraint on the v_i secret inputs which must be proven to be committed to anyway, whereas adding padding terms to rule out brute forcing makes the range proof relations much larger, each inner product would have an additional 128 multiplications in the inner product, and 128 multiplications checking that the bit vector components are in the subset {0, 1} \subseteq Z_q. technically the structure of the proof is as simple as the non-padded case, but the statements are much larger, and even with bulletproofs verification and proving time are still O(N)

As Bulletproofs are logarithmic in the range size, the added overhead is negligible IMO. For 32-bit range (without padding) we would have 5 group elements for the range proof, for a full range proof of 256-bit we would have 8 group elements.

nothingmuch commented 4 years ago

the proof size itself is negligibly larger, but constructing as well as verifying it is still O(N), it's just that the that this work is compressed to only a logarithmic sized verification equation in the end,

secondly, it feels a bit crude to me to use a computationally hiding padding scheme when we already have a perfectly hiding binding (sorry, very unfortunate brain fart) commitment scheme for the same values

i'm still stuck on the homework phase, trying to figure out how to prove the sum of values committed to by a bunch of Pedersen commitments in a sigma protocol, but my understanding is that this isn't very complex, and should naturally compose with the per-credential proofs that relates the zeta terms to the individual amounts?

seresistvanandras commented 4 years ago

the proof size itself is negligibly larger, but constructing as well as verifying it is still O(N), it's just that the that this work is compressed to only a logarithmic sized verification equation in the end,

I agree. If we can solve it without padding than we can save some dozens of exponentiations from the proof generation time. But still, I hardly doubt that this will be the protocol's bottleneck.

secondly, it feels a bit crude to me to use a computationally hiding padding scheme when we already have a perfectly binding commitment scheme for the same values

Since the commitment scheme is perfectly binding, then we cannot hope more than a computationally hiding scheme. So this is an inherent limitation we cannot circumvent.

i'm still stuck on the homework phase, trying to figure out how to prove the sum of values committed to by a bunch of Pedersen commitments in a sigma protocol, but my understanding is that this isn't very complex, and should naturally compose with the per-credential proofs that relates the zeta terms to the individual amounts?

Yeah, let's see if we can improve on this very elementary ZK proof system for coin merging. I agree that there should be a cleaner and more elegant way to achieve the same thing exploiting the nice properties of the blinded commitments.

nothingmuch commented 4 years ago

why is the commitment scheme perfectly binding? even ignoring gamma, the domain of Pedersen commitments in the attributes is Z_q^2, and the range is G of order q, and that's what we're trying to prove things about.

i agree for simple Pedersen hashing with generator h1 the domain and range are of the same order, making it computationally hiding, but at least logically i see no reason why we need to disclose those values without the additional randomness mixed in, hence my desire to not expose these values,

nothingmuch commented 4 years ago

sorry, i had a very unfortunate brainfart, meant to write "we already have a perfectly hiding commitment scheme", since attributes are a Pedersen commitment.

just to be clear, given the choice for this application we should definitely favor perfect hiding to maintain privacy in case of any future crypto break

nopara73 commented 4 years ago

I'm going through this issue sequentially, so things I'm mentioning here is probably addressed in later comments, anyway, I think everything should add up in the starting post of this issue, so I'm noting the logical problems:

From this protocol the user obtains n signatures for n blinded commitments \zeta_{1.n}, which are not linkable to the C_n commitments, but the coordinator can be sure they commit to the same values (or attributes in ACL terms.)

Shouldn't it be more like: the user acquires n blinded signatures, which it unblinds such that they will be valid for n commitments those commit to the same values?

nopara73 commented 4 years ago

https://github.com/zkSNACKs/WabiSabi/issues/30