Geodesic
Automated correctness proof of algorithm variants in elliptic curve cryptography
Modelirovanie i analiz informacionnyh sistem, Tome 17 (2010) no. 4, pp. 7-16

Voir la notice de l'article provenant de la source Math-Net.Ru

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.
Keywords: verification, cryptography, elliptic curves. 
@article{MAIS_2010_17_4_a1,
     author = {M. Anikeev and F. Madlener and A. Schlosser and S. A. Huss and C. Walther},
     title = {Automated correctness proof of algorithm variants in elliptic curve cryptography},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {7--16},
     publisher = {mathdoc},
     volume = {17},
     number = {4},
     year = {2010},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2010_17_4_a1/}
}
TY  - JOUR
AU  - M. Anikeev
AU  - F. Madlener
AU  - A. Schlosser
AU  - S. A. Huss
AU  - C. Walther
TI  - Automated correctness proof of algorithm variants in elliptic curve cryptography
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2010
SP  - 7
EP  - 16
VL  - 17
IS  - 4
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2010_17_4_a1/
LA  - en
ID  - MAIS_2010_17_4_a1
ER  - 
%0 Journal Article
%A M. Anikeev
%A F. Madlener
%A A. Schlosser
%A S. A. Huss
%A C. Walther
%T Automated correctness proof of algorithm variants in elliptic curve cryptography
%J Modelirovanie i analiz informacionnyh sistem
%D 2010
%P 7-16
%V 17
%N 4
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2010_17_4_a1/
%G en
%F MAIS_2010_17_4_a1
M. Anikeev; F. Madlener; A. Schlosser; S. A. Huss; C. Walther. Automated correctness proof of algorithm variants in elliptic curve cryptography. Modelirovanie i analiz informacionnyh sistem, Tome 17 (2010) no. 4, pp. 7-16. http://geodesic.mathdoc.fr/item/MAIS_2010_17_4_a1/