Formal verification of elliptic curves. Depence on the equation form

Question

I'm doing formal verification of the group properties of elliptic curve addition in Weiertrass form. I was taking as a reference this and this articles. The first does the verification for Weiertrass form and the second does it for Curve22519, a Montgomery curve, but his approach can be generalized to Weiertrass form.

My question is, can I proof the group properties for the Weiertrass form and then translate the operation from this form to Montgomery form or Edwards form? I believe the three of them present some "equivalent" families of curves. Would this approach preserve the good properties of each family?

For instance, say I do the verification for Weiertrass form and then I "convert" the results to Edwards form. Would this be still side-channel attacks resistant?

Answer 1

For instance, say I do the verification for Weiertrass form and then I "convert" the results to Edwards form. Would this be still side-channel attacks resistant?

Well, if you have a Weierstrass form and an Edwards form of the same curve, they're actually the same group, with an easily computable isomorphism between the two, and so any group property (including things such as the difficulty of the discrete log problem) would be preserved.

However, you specifically asked about side channel resistance; that's not a group property. Instead, it is a property of the implementation (as a side channel attack listens into internals of the implementation as it computes). If you have two different implementations of the same curve (for example, a Weierstrass implementation and an Edwards form implementation), then proving that one of your implementations is resistant to a specific side channel attack says nothing about whether your other implementation is.