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/

[1] R. S. Boyer, J. S. Moore, “Proof checking the RSA public key encryption algorithm”, American Mathematical Monthly, 91:3 (1984), 181–189 | DOI | MR | Zbl

[2] J. Duan, J. Hurd, G. Li, S. Owens, K. Slind, J. Zhang, “Functional Correctness Proofs of Encryption Algorithms”, LPAR, LNCS, 3835, eds. G. Sutcliffe, A. Voronkov, Springer, 2005, 519–533 | Zbl

[3] D. Hankerson, A. Menezes, S. Vanstone, Guide to Elliptic Curve Cryptography, Springer-Verlag, 2004, 311 pp. | MR | Zbl

[4] J. Hurd, M. Gordon, A. Fox, Formalized Elliptic Curve Cryptography, High Confidence Software and Systems: HCSS, 2006

[5] N. Koblitz, “Elliptic Curve Cryptosytems”, Mathematics of Computation, 48:177 (1987), 203–209 | DOI | MR | Zbl

[6] A. K. Lenstra, E. R. Verheul, “The XTR Public Key System”, CRYPTO 2000, Lecture Notes in Computer Science, 1880, 2000, 1–19 | MR | Zbl

[7] V. S. Miller, “Use of elliptic curves in cryptography”, CRYPTO85, Lecture Notes in Computer Science, 218, ed. H. C. Williams, 1985, 417–426 | MR

[8] A. Riazanov, A. Voronkov, “The Design and Implementation of VAMPIRE”, AI Communications, 15, no. 2, IOS Press, 2002, 91–110 | Zbl

[9] R. L. Rivest, A. Shamir, L. Adleman, “A Method of Obtaining Digital Signaturtes and Public-Key Cryptosystems”, Communications of the ACM, 21 (1978), 120–126 | DOI | MR | Zbl

[10] S. Schulz, “System Abstract: E 0.81”, 2nd International Joint Conference on Automated Reasoning (IJCAR), Lecture Notes in Artificial Intelligence, 3097, jul., eds. D. Basin, M. Rusinowitch, Springer-Verlag, 2004, 223–228 | MR | Zbl

[11] C. Walther, M. Aderhold, A. Schlosser, The $\mathcal{L}$ 1.0 Primer, Technical Report VFR 06/01, Programmiermethodik, Technische Universität Darmstadt, Germany, Apr. 2006

[12] C. Walther and others, VeriFun: A Verifier for Functional Programs, 2006

[13] C. Walther, S. Schweitzer, “A Machine Supported Proof of the Unique Prime Factorization Theorem”, Proc. of the 5th Workshop on Tools for System Design and Verification (FM-TOOLS 2002), 2002-11, eds. D. Haneberg, G. Schellhorn, W. Reif, Institut für Informatik, Universität Augsburg, Augsburg, 2002, 39–45

[14] L. Théry, Proving the group law for elliptic curves formally INRIA, Technical Report 0330, Sophia Antipolis, 2007