Check that Distr is in scope when tagging distributions, fixing #211

[oskgo]

Check that Distr is in scope when tagging distributions. The original implementation required parts of AllCore instead, of which Distr is not a part.

This breaks code that tags distributions without requiring Distr.

Edit: note to self; #416 and #756 are similar, but different.

[fdupress]

Can you please also propose a fix for the XMSS proof? It should be as simple as importing Distr, but I'm not sure I'll have time to look into it quickly enough to not hold this back.

This is clearly a breaking change, so please do mark it as such.

[oskgo]

@fdupress Why is that repo using its own copy of the DigitalSignatures theory in the first place? Was that where it was first built? If that's the only reason, the proper fix would be to delete the copy. Otherwise, requiring Distr should suffice.

[fdupress]

Yes, that's where it came from. Thanks for checking it out. I'll try getting to that tomorrow.

[fdupress]

So it looks like the XMSS proof extends those definitions a tiny bit, with a notion of an interactive EUF-RMA adversary. @MM45, should that extension be ported over to the stdlib version of the signature-related definitiions, or is it ultra-local? (And if it is ultra-local, can you see an easy way of extending without duplicating?)

[fdupress]

My own thoughts on this: the interactive notion is the one we actually want (much more usable in proofs, since it avoids a pre-sampling argument the non-interactive notion forces), but departs from what a more traditional cryptographer would write on paper when defining security against random message attacks.

We should adopt (as a breaking change) the I-EUFRMA version as EUFRMA, rename the current EUFRMA version N-EUFRMA, and push the "almost equivalence" proof into the library. This should be discussed properly.

As a short term fix, we should just reflect the fixes made to the stdlib into the modified version in the XMSS repo so we can merge this.

I'll take comments on this until tomorrow-ish, and then we move on the plan.

[MM45]

IIRC, the interactive EUF-RMA notion was just an auxiliary intermediate notion to get an initial proof going for the Hash-then-Sign, isolating the lazy-eager argument around the EUF-RMA notion. Not sure why I even spent time including this in the library (guess that is also the reason I ended up removing it when porting to the standard library). I will take a look at fixing the failing check here in a minute.

Anyways, I don't agree on departing from the pen-and-paper definition as the default EUF-RMA notion in the library. A notion named EUF-RMA in the library should IMO match the (most conventional way of writing the) notion named EUF-RMA on paper (as long as it is possible/reasonable to do so in EC, which I think is definitely the case here). However, I do like the idea of having the (usually) more convenient notion to work with (in EC) also being part of the library with an attached equivalence proof (to the default definition).

[MM45]

Created PR with simple fix (requiring Distr, formosa-crypto/formosa-xmss#17) to formosa-xmss, security test succeeds locally. I tried for a proper fix for a while (removing local libraries where they are in the standard library), but this seems to be less trivial than expected: the dependency on ROM (instead of PROM, which the standard library versions assume) seems to be quite pervasive. Should really sit down to implement the proper fix.

[fdupress]

Short term fix applied on the external side. Rerunning jobs now.

@MM45 , let's talk about the best choice for the library Soon. But if you do the work before we talk, you get to choose how you do it :)

[strub]

Could you update the PR title? We use it for generating the ChangeLog.