Secure comparator is broken

[Sc00bz]

The attack is send g2a or g2b as the zero point "(0, 2^255-19+1)"

unsigned char zero[32] = {0xee, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff,
                          0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff,
                          0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff,
                          0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0x7f};

These won't match this zero point: https://github.com/cossacklabs/themis/blob/50fd35d987c5fcde55954e2ccc645bca721be50c/src/themis/secure_comparator.c#L168 and https://github.com/cossacklabs/themis/blob/50fd35d987c5fcde55954e2ccc645bca721be50c/src/themis/secure_comparator.c#L241

[Sc00bz]

Oh that's funny https://github.com/cossacklabs/themis/issues/83.

P.S. You should also test after scalar point multiplication for the zero point or "8*input == zero" because I can give you a point of order 8 for g2a or g2b and achieve the same as a zero point. I pretty sure Ed25519 only has points that are of order 1, 2, 4, 8, and 2^252+27742317777372353535851937790883648493.

[ignatk]

Thank you for pointing this out. We are considering it as part of #83 . Maybe it doesn't make sense to verify g2a or g2b at all, but rather to check the final g2. What do you think?

[Sc00bz]

That is what I was suggesting. Well g2, g3, Rab, and R but I don't think checking g3, Rab, and R{a,b} is necessary. But I'm too drunk to understand what you are even doing... besides a PAKE algorithm.

Have you heard of SPAKE2 (or SPAKE2-EE)? There's also the client-server augmentation: PAKE2+ and PAKE2+EE. Both are much faster and have security proofs.

[ignatk]

Actually, we were considering it for other use-cases we are having from the industry. So far these are more like handling personal data than PAKE or authentication. This is just a building block we want to try out and see whether it will fit their needs. So it is not a full-featured protocol but rather a potential piece in a bigger security structure/protocol.

[Sc00bz]

... So you don't want to use an algorithm that's better and faster because it covers more use cases? 0_o

[gene-eu-zz]

Thank you for your feedback and attention to detail. Shortly, my colleague will return after investigation and you will be able to get back to technical detail.

I can answer about general choice and reasoning, however don't think github issue is the right place to discuss such things and my discourse is going to be obvious and boring :) If password auth and speed were the only considerations, there would be much better choices than either SC or PAKE. SC's threat model is seen around 'no possible leakage' both in transport and on verifier side - for some use cases we need mutual authentication, which by design has nothing to leak even to dishonest party (this is the main use case for us, password authentication is just something that came along the way and could be developed from current SC state).

When we were planning SC a year ago as a part of larger research, we were not aware of ECC-based SPAKE implementation, and I am still not aware of publicly available security proofs (although seeing work of Mike Hamburg makes me think he knows what to do, @secumod might comment better on that). Moreover, at that point, non-EE SPAKE2 is discrete log problem class with obvious future repercussions to that.

We're quite lazy, and remember Schneier's law well, so if there was an instrument, which would fit us - we'd implement it in the first place.

[ignatk]

tl;dr We would like to choose an algorithm for our particular use-cases. It doesn’t make much sense to hammer nails with a screwdriver. Regarding SPAKE “better” is very questionable. The basic description does not recommend any choice of specific fields (even size of the field), so implementations might end-up having “simple common DH params”. We know where it goes: https://weakdh.org/imperfect-forward-secrecy-ccs15.pdf . Also, as noted in above paper, it feels that proposing non-ECC protocols today is similar to advertising video tapes in today’s world of digital online media. On the other hand, unfortunately, today’s choice of an algorithm is determined not only by security or speed, but potential applicability and adoption as well. If I see SPAKE-EE description, it mentions NIST curves. Even if one does not consider http://safecurves.cr.yp.to/rigid.html , just enabling such ECC in a new protocol might cause a lot of patent trouble. Many argue that basic ECC is not patented, but unfortunately most efficient computations are. So you may end up using only “basic schoolbook scalar multiplier” to avoid any patent fuzz and loose all your speed benefits and introduce a timing attack. That’s why you still don’t see much ECC around, except for TLS, which was considered safe from patents because of “explicit Certicom royalte free grant”: https://www.certicom.com/pdfs/FAQ-TheNSAECCLicenseAgreement.pdf. However, even TLS is not safe anymore: http://www.theregister.co.uk/2015/12/01/cryptopeak_sues_/ . That’s why many big enterprises are known to explicitly avoid ECC-based crypto, because the risks are too high, unless they are sure they can safely adopt it. Also, that’s why even today many new security technologies still prefer RSA.

P.S. We pushed a fix to the problem you pointed out and would greatly appreciate your comments.

[TethysSvensson]

I assume you are referring to a54f2fe.

I think it is still exploitable, however it depends on internals of how ed25519 is implemented, and I have not looked much at that yet.

The check for Qa == Qb is useless, because an attacker might make Qa - Qb an element that simply has order 8, which would still make rand3 * R == 0. Alternatively an attacker could choose Ra to be of low order, so rand3 * Ra == 0.

The bottom line is that Rab could still be zero and the check does nothing to prevent that.

This would not be a problem in itself, if not for another problem: I think it should be possible to make Pa - Pb == 0 without having Pa == Pb. It would at least be possible for curve25519 by choosing Pb = (-Pa) | 2 ** 255

My advice:

• Either remove the check for Pa == Pb or replace it with a check for Pa - Pb == 0.
• Either remove the check for Qa == Qb or replace it with a check for rand3 * (Qa - Qb) == 0.
• Insert a check for Rab == 0.

I think that the last one would be sufficient to make the implementation secure against these kinds of attacks however there is not much lost by doing all of them.

P.S. You should probably make ge_is_zero constant-time.

[TethysSvensson]

Hmmm. There are more attacks, which libotr protects against, but this implementation does not. One attack is to try and make Ra = base and Pa_Pb == g3a. I do not think that this is possible in the current implementation, but only a slight change would make it possible.

[ignatk]

Thanks for your valuable feedback. Good catch for ge_is_zero: somehow I had g2a in mind, but then moved check to g2 which should be done in constant-time. As for the rest, I will try to expand test cases to test all of the above: we would still like to try to minimize the checks, especially ones with point-scalar multiply. Or we might replace rand3 * (Qa - Qb) == 0 with 8 * (Qa - Qb) == 0 and check it with point addition instead.

[TethysSvensson]

Well, you are already computing Ra = rand3 * (Qa - Qb), so why do the extra point multiplication?

In any case: Consider the case where Bob sends Rb == base and Pb == g3a - Pa in step 4. This would make Rab == rand3 * base == g3a and Pa_Pb == g3a, so the authentication would succeed.

You have no way of detecting this, that would not simply be adding a lot of special-cases everywhere. I would think that there are more similar attacks possible, which would mean you would require many such special-cases.

The way OTR solves this is by having every value include a ZK-proof that it is valid. For instance g2a is checked using a Schnorr signature.

[ignatk]

Hmm. After more detailed look I see they use Schnorr signatures everywhere as ZK-proofs. Since ed25519 is a EC variant of Schnorr signature maybe we should just reuse their approach. Will take a look in that direction.

[TethysSvensson]

You will need to design a few primitives yourself, as they also use ZK-proofs for e.g. "I know a y such that g3a = y * base and Ra = y * R".

But yes, I think it should be doable. If you haven't already, I would suggest reading the first 8 pages of https://www.win.tue.nl/~berry/papers/dam.pdf

[ignatk]

I've ported all ZK-proofs from OTR to ed25519. If you have time, would really appreciate your feedback for #89

[TethysSvensson]

These lines are broken:

    if (!ge_cmp(&(comp_ctx->Pp), &(comp_ctx->P)))

[TethysSvensson]

More generally:

There are only three types of checks in the OTR implementation and in the original paper:

• That a send value is valid. In ECC terms this would mean, 1 <= n < SM_ORDER and x is a valid point different from 0.
• That a ZK-proof is valid.
• That the final result is correct.

So almost all of the ge_cmps are superfluous, if we assume that the other checks are inserted correct.

It turns out that they are not. For instance signature[63] & 224 is insufficient to check if signature[32:64] is a valid.

I have not yet verified whether that check is actually necessary, but I think it is. In any case: Either the check should be there and be done correctly, or it should be removed to reduce complexity.

[ignatk]

So far I removed some of the checks which are probably indeed excessive. The idea behind that is the following:

• we initially check two DH values g2, g3 are non-zero
• we rely on ZK-proofs for other parameter validations, since they are derived using g2, g3 and base point which are all points with high order
• we explicitly prohibit Rab to be zero. This makes the match possible only for real case or g2 being zero, but we checked that before

Would appreciate your comments on #92

[ignatk]

Closed by #92 (hopefully...)