Automated correctness proof of algorithm variants in elliptic curve cryptography

The Elliptic Curve Cryptography (ECC) is widely known as secure and reliable cryptographic scheme. In many situations the original cryptographic algorithm is modified to improve its efficiency in terms like power consumption or memory consumption which were not in the focus of the original algorithm. For all this modification it is crucial that the functionality and correctness of the original algorithm is preserved. In particular, various projective coordinate systems are applied in order to reduce the computational complexity of elliptic curve encryption by avoiding division in finite fields. This work investigates the possibilities of automated proofs on the correctness of different algorithmic variants. We introduce the theorems which are required to prove the correctness of a modified algorithm variant and the lemmas and definitions which are necessary to prove these goals. The correctness proof of the projective coordinate system transformation has practically been performed with the help of the an interactive formal verification system $\Large\checkmark\hskip-2.4mm$eriFun.