Malicious strong universal exclusive ownership; Message bound security

[mikedilger]

Sorry if this issue ends up being noise, as I'm not a cryptographer.

This is in regard to this paper from 2020:

The Provable Security of Ed25519: Theory and Practice

They claim to have proven security properties of Ed25519 but that not all implementations have all the security properties, and in particular

• All implementations are existentially unforgeable under chosen message attacks (an adversary cannot construct a signature for a message that the key owner did not sign previously)
• All implementations resist key substitution attacks (strong universal exclusive ownership) but not a malicious variant of such.
• The original Bernstein's paper source code does not provide Strong Unforgeability as S < 2^b-1 does not prevent signature malleability (and IETF and your verify_strict() corrects this by testing S is in 0..L-1).
• Only the libsodium implementation also provides provable resilience against malicious strong universal exclusive ownership (M-S-UEO in the paper) and also provides provable Message Based Security (a signature verifies a unique message, even for malicious keys) by checking that |R|>=L ^ |A| >=L

Is this extra verification step check that libsodium does even compatible with checking [8][S]B = [8]R + [8][k]A' (as the IETF implementation requires) and is it possible (or useful) to do this check?

If this makes no sense, refer to the paper.

Thanks.

[mikedilger]

I've now skimmed https://eprint.iacr.org/2020/1244.pdf and in particular I ran their test vectors against current dalek and it appears to properly reject everything except vector 3 (mixed point, expensive to reject). So maybe you are checking R and A both are canonical, and rejecting small order components (which only libsodium used to do I believe). Is that right?