The prime testing program PRIMO documentation specifies the ECPP criterion thus (in the primo.html file included within the downloadable archive with the program):
Assuming $M = SR$, with $S > 0$, $R$ prime and $R > (N^{1/4} + 1)^2$, if there exists a non-singular elliptic curve $E$ given by $y^2 ≡ x^3 + ax + b$ (mod $N$) with order $M$ and a point $p = (x_p,y_p)$ on this curve such that $p\times S \ne$ Identity and $(p\times S)\times R =$ Identity then $N$ is prime.
The Wikipedia article (https://en.wikipedia.org/wiki/Elliptic_curve_primality#Elliptic_curve_primality_proving) section "Proposition" states the ECPP criterion almost equivalently (with different letters), however, it doesn't seem to include the condition that the curve has order $M$ (which Wikipedia refers to as $m$), it only gives conditions surrounding the point $p$.
The question is, if one is to verify an ECPP certificate, is it necessary to explicitly verify that the curve $E$ has order $M$ by counting points on the curve etc? Or does it follow by merely verifying the conditions listed in the Wikipedia article?
Ideally one would read the paper by Atkin and Morain (Elliptic curves and primality proving, 1993) rather than a secondary source.
Page 10, theorem 5.2:
Page 10, Corollary 5.1:
Crandall and Pomerance 2005, theorem 7.6.1 is, in my reading, similar.
The Wikipedia text is a special case where $s$ is prime, so $s=q$. This is the way most programs implement the algorithm (including Primo), and most verifiers do it this way.
For verification of Primo certificates, see the
verifier-f4.txtfile included with Primo that describes the conditions to verify. There are two open source programs I'm aware of that will also verify Primo certificates. I wrote mine using the conditions I understood from the paper rather than from Primo, which mostly map to what he is doing. There are additional steps of mapping and verification for the variables and transformations Primo uses.You don't need to count the points. You just need to verify the conditions of the theorems. It is a much faster process than the proof itself, with almost all the time spent doing the EC multiplications.