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...
| Main Authors: | , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Yaroslavl State University
2010-12-01
|
| Series: | Моделирование и анализ информационных систем |
| Subjects: | |
| Online Access: | https://www.mais-journal.ru/jour/article/view/1047 |
| _version_ | 1826559046609534976 |
|---|---|
| author | M. . Anikeev F. . Madlener A. . Schlosser S. A. Huss C. . Walther |
| author_facet | M. . Anikeev F. . Madlener A. . Schlosser S. A. Huss C. . Walther |
| author_sort | M. . Anikeev |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-10T02:25:12Z |
| format | Article |
| id | doaj.art-a9cb4510dcfb45549c87263fc4649663 |
| institution | Directory Open Access Journal |
| issn | 1818-1015 2313-5417 |
| language | English |
| last_indexed | 2025-03-14T08:54:10Z |
| publishDate | 2010-12-01 |
| publisher | Yaroslavl State University |
| record_format | Article |
| series | Моделирование и анализ информационных систем |
| spelling | doaj.art-a9cb4510dcfb45549c87263fc46496632025-03-02T12:46:53ZengYaroslavl State UniversityМоделирование и анализ информационных систем1818-10152313-54172010-12-01174716788Automated Correctness Proof of Algorithm Variants in Elliptic Curve CryptographyM. . Anikeev0F. . Madlener1A. . Schlosser2S. A. Huss3C. . Walther4Southern Federal University, Taganrog, RussiaTechnische Universitat Darmstadt, GermanyTechnische Universitat Darmstadt, GermanyTechnische Universitat Darmstadt, GermanyTechnische Universitat Darmstadt, GermanyThe 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.https://www.mais-journal.ru/jour/article/view/1047verificationcryptographyelliptic curves |
| spellingShingle | M. . Anikeev F. . Madlener A. . Schlosser S. A. Huss C. . Walther Automated Correctness Proof of Algorithm Variants in Elliptic Curve Cryptography Моделирование и анализ информационных систем verification cryptography elliptic curves |
| title | Automated Correctness Proof of Algorithm Variants in Elliptic Curve Cryptography |
| title_full | Automated Correctness Proof of Algorithm Variants in Elliptic Curve Cryptography |
| title_fullStr | Automated Correctness Proof of Algorithm Variants in Elliptic Curve Cryptography |
| title_full_unstemmed | Automated Correctness Proof of Algorithm Variants in Elliptic Curve Cryptography |
| title_short | Automated Correctness Proof of Algorithm Variants in Elliptic Curve Cryptography |
| title_sort | automated correctness proof of algorithm variants in elliptic curve cryptography |
| topic | verification cryptography elliptic curves |
| url | https://www.mais-journal.ru/jour/article/view/1047 |
| work_keys_str_mv | AT manikeev automatedcorrectnessproofofalgorithmvariantsinellipticcurvecryptography AT fmadlener automatedcorrectnessproofofalgorithmvariantsinellipticcurvecryptography AT aschlosser automatedcorrectnessproofofalgorithmvariantsinellipticcurvecryptography AT sahuss automatedcorrectnessproofofalgorithmvariantsinellipticcurvecryptography AT cwalther automatedcorrectnessproofofalgorithmvariantsinellipticcurvecryptography |