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
XeriFun.

Ключ. слова



УДК: 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.)

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

Обратные ссылки

  • Обратные ссылки не определены.


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


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