A bit-vector differential model for the modular addition by a constant and its applications to differential and...

Area of Science:

• Cryptography and Information Security
• Computer Science
• Applied Mathematics

Background:

• Automated cryptanalysis of ARX (Addition, Rotation, XOR) ciphers relies on constraint satisfaction solvers.
• Evaluating ARX ciphers against differential and impossible-differential cryptanalysis requires differential models for non-linear operations.
• A key limitation was the lack of a bit-vector differential model for modular addition by a constant.

Purpose of the Study:

• To introduce the first bit-vector differential model for n-bit modular addition by a constant.
• To develop SMT-based automated methods for searching differential characteristics and impossible differentials in ARX ciphers with constant additions.
• To implement these methods in an open-source tool for practical application.

Main Methods:

• Developed a novel bit-vector differential model for n-bit modular addition by a constant, detailing binary logarithm of differential probability.
• Designed an SMT-based automated method incorporating the new model to find differential characteristics.
• Introduced a new SMT-based automated method for discovering impossible differentials by searching the entire difference space.

Main Results:

• Successfully modeled n-bit modular addition by a constant using bit-vector constraints.
• Implemented automated methods in the open-source tool ArxPy for finding differential characteristics and impossible differentials.
• Achieved improved results in finding related-key impossible differentials and differential characteristics for ciphers like TEA, XTEA, HIGHT, LEA, SHACAL-1, and SHACAL-2.

Conclusions:

• The proposed bit-vector differential model and automated SMT-based methods significantly advance the cryptanalysis of ARX ciphers containing constant additions.
• ArxPy provides a practical, fully automated solution for discovering differential characteristics and impossible differentials.
• The findings enable more comprehensive security evaluations of various ARX-based cryptographic algorithms.