Моделирование и анализ информационных систем

Расширенный поиск

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

Ключевые слова

MSC2020: 004.052.42:004.056.55

Об авторах

M. Anikeev
Southern Federal University, Taganrog, Russia

F. Madlener
Technische Universitat Darmstadt, Germany

A. Schlosser
Technische Universitat Darmstadt, Germany

S. Huss
Technische Universitat Darmstadt, Germany

C. Walther
Technische Universitat Darmstadt, Germany

Список литературы

1. R. S. Boyer and J. S. Moore. Proof checking the RSA public key encryption algorithm. American Mathematical Monthly, 91(3):181-189, 1984.

2. J. Duan, J. Hurd, G. Li, S. Owens, K. Slind, and J. Zhang. Functional correctness proofs of encryption algorithms. In G. Sutcliffe and A. Voronkov, editors, LPAR, volume 3835 of Lecture Notes in Computer Science, pages 519-533. Springer, 2005.

3. D. Hankerson, A. Menezes, and S. Vanstone. Guide to Elliptic Curve Cryptography. Springer-Verlag, 2004.

4. J. Hurd, M. Gordon, and A. Fox. Formalized elliptic curve cryptography. High Confidence Software and Systems: HCSS 2006.

5. N. Koblitz. Elliptic curve cryptosytems. Mathematics of Computation, 48(177):203- 209, 1987.

6. A. K. Lenstra and E. R. Verheul. The XTR public key system. Lecture Notes in Computer Science, 1880:1-19, 2000.

7. V. S. Miller. Use of elliptic curves in cryptography. In H. C. Williams, editor, CRYPTO85, volume 218 of Lecture Notes in Computer Science, pages 417-426, 1985.

8. A. Riazanov and A. Voronkov. The Design and Implementation of VAMPIRE. AI Communications, 15(2):91-110, 2002.

9. R. L. Rivest, A. Shamir, and L. Adleman. A method of obtaining digital signaturtes and public-key cryptosystems. Communications of the ACM, 21:120-126, Feb. 1978.

10. S. Schulz. System Abstract: E 0.81. In D. Basin and M. Rusinowitch, editors, 2nd International Joint Conference on Automated Reasoning (IJCAR), volume 3097 of Lecture Notes in Artificial Intelligence, pages 223-228. Springer-Verlag, July 2004.

11. L. Thery. Proving the group law for elliptic curves formally. Technical Report 0330, INRIA, Sophia Antipolis, 2007.

12. C. Walther, M. Aderhold, and A. Schlosser. The L 1.0 Primer. Technical Report VFR 06/01, Programmiermethodik, Technische Universit¨at Darmstadt, Germany, Apr. 2006.

13. C. Walther et al. XeriFun: A verifier for functional programs, 2006.

14. C. Walther and S. Schweitzer. A machine supported proof of the unique prime factorization theorem. In D. Haneberg, G. Schellhorn, and W. Reif, editors, Proc. of the 5th Workshop on Tools for System Design and Verification (FM-TOOLS 2002), volume 2002-11, pages 39-45, Augsburg, 2002. Institut f¨ur Informatik, Universit¨at Augsburg.


Для цитирования:

., ., ., ., . . Моделирование и анализ информационных систем. 2010;17(4):7-16.

For citation:

Anikeev M..., Madlener F..., Schlosser A..., Huss S.A., Walther C... Automated Correctness Proof of Algorithm Variants in Elliptic Curve Cryptography. Modeling and Analysis of Information Systems. 2010;17(4):7-16. (In Russ.)

Просмотров: 288

Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.

ISSN 1818-1015 (Print)
ISSN 2313-5417 (Online)