Algebraic Linear Analysis for Number Theoretic Transform in Lattice-Based Cryptography
The topic of verifying postquantum cryptographic software has never been more pressing than today between the new NIST postquantum cryptosystem standards being finalized and various countries issuing directives to switch to postquantum or at least hybrid cryptography in a decade. One critical issue...
Saved in:
| Main Authors: | , , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Ruhr-Universität Bochum
2025-06-01
|
| Series: | Transactions on Cryptographic Hardware and Embedded Systems |
| Subjects: | |
| Online Access: | https://tches.iacr.org/index.php/TCHES/article/view/12230 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1849467299206004736 |
|---|---|
| author | Chun-Ming Chiu Jiaxiang Liu Ming-Hsien Tsai Xiaomu Shi Bow-Yaw Wang Bo-Yin Yang |
| author_facet | Chun-Ming Chiu Jiaxiang Liu Ming-Hsien Tsai Xiaomu Shi Bow-Yaw Wang Bo-Yin Yang |
| author_sort | Chun-Ming Chiu |
| collection | DOAJ |
| description |
The topic of verifying postquantum cryptographic software has never been more pressing than today between the new NIST postquantum cryptosystem standards being finalized and various countries issuing directives to switch to postquantum or at least hybrid cryptography in a decade. One critical issue in verifying lattice-based cryptographic software is range-checking in the finite-field arithmetic assembly code which occurs frequently in highly optimized cryptographic software. For the most part these have been handled by Satisfiability Modulo Theory (SMT) but so far they mostly are restricted to Montgomery arithmetic and 16-bit precision. We add semi-automatic range-check reasoning capability to the CryptoLine toolkit via the Integer Set Library (wrapped via the python package islpy) which makes it easier and faster to verify more arithmetic crypto code, including Barrett and Plantard finite-field arithmetic, and show experimentally that this is viable on production code.
|
| format | Article |
| id | doaj-art-9619f7dde6ae4a9d87f2831e5fa3b311 |
| institution | Kabale University |
| issn | 2569-2925 |
| language | English |
| publishDate | 2025-06-01 |
| publisher | Ruhr-Universität Bochum |
| record_format | Article |
| series | Transactions on Cryptographic Hardware and Embedded Systems |
| spelling | doaj-art-9619f7dde6ae4a9d87f2831e5fa3b3112025-08-20T03:26:16ZengRuhr-Universität BochumTransactions on Cryptographic Hardware and Embedded Systems2569-29252025-06-012025310.46586/tches.v2025.i3.668-692Algebraic Linear Analysis for Number Theoretic Transform in Lattice-Based CryptographyChun-Ming Chiu0Jiaxiang Liu1Ming-Hsien Tsai2Xiaomu Shi3Bow-Yaw Wang4Bo-Yin Yang5National Taiwan University, Taipei, TaiwanKey Laboratory of System Software (Chinese Academy of Sciences) and State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, ChinaNational Taiwan University of Science and Technology, Taipei, TaiwanKey Laboratory of System Software (Chinese Academy of Sciences) and State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, ChinaAcademia Sinica, Taipei, TaiwanAcademia Sinica, Taipei, Taiwan The topic of verifying postquantum cryptographic software has never been more pressing than today between the new NIST postquantum cryptosystem standards being finalized and various countries issuing directives to switch to postquantum or at least hybrid cryptography in a decade. One critical issue in verifying lattice-based cryptographic software is range-checking in the finite-field arithmetic assembly code which occurs frequently in highly optimized cryptographic software. For the most part these have been handled by Satisfiability Modulo Theory (SMT) but so far they mostly are restricted to Montgomery arithmetic and 16-bit precision. We add semi-automatic range-check reasoning capability to the CryptoLine toolkit via the Integer Set Library (wrapped via the python package islpy) which makes it easier and faster to verify more arithmetic crypto code, including Barrett and Plantard finite-field arithmetic, and show experimentally that this is viable on production code. https://tches.iacr.org/index.php/TCHES/article/view/12230Integer Set LibraryCryptoLineFormal VerificationAssembly Code |
| spellingShingle | Chun-Ming Chiu Jiaxiang Liu Ming-Hsien Tsai Xiaomu Shi Bow-Yaw Wang Bo-Yin Yang Algebraic Linear Analysis for Number Theoretic Transform in Lattice-Based Cryptography Transactions on Cryptographic Hardware and Embedded Systems Integer Set Library CryptoLine Formal Verification Assembly Code |
| title | Algebraic Linear Analysis for Number Theoretic Transform in Lattice-Based Cryptography |
| title_full | Algebraic Linear Analysis for Number Theoretic Transform in Lattice-Based Cryptography |
| title_fullStr | Algebraic Linear Analysis for Number Theoretic Transform in Lattice-Based Cryptography |
| title_full_unstemmed | Algebraic Linear Analysis for Number Theoretic Transform in Lattice-Based Cryptography |
| title_short | Algebraic Linear Analysis for Number Theoretic Transform in Lattice-Based Cryptography |
| title_sort | algebraic linear analysis for number theoretic transform in lattice based cryptography |
| topic | Integer Set Library CryptoLine Formal Verification Assembly Code |
| url | https://tches.iacr.org/index.php/TCHES/article/view/12230 |
| work_keys_str_mv | AT chunmingchiu algebraiclinearanalysisfornumbertheoretictransforminlatticebasedcryptography AT jiaxiangliu algebraiclinearanalysisfornumbertheoretictransforminlatticebasedcryptography AT minghsientsai algebraiclinearanalysisfornumbertheoretictransforminlatticebasedcryptography AT xiaomushi algebraiclinearanalysisfornumbertheoretictransforminlatticebasedcryptography AT bowyawwang algebraiclinearanalysisfornumbertheoretictransforminlatticebasedcryptography AT boyinyang algebraiclinearanalysisfornumbertheoretictransforminlatticebasedcryptography |