A Bit-Vector Differential Model for the Modular Addition by a Constant

Seyyed Arash Azimi; Adrián Ranea; Mahmoud Salmasizadeh; Javad Mohajeri; Mohammad Reza Aref; Vincent Rijmen

Paper 2020/1025

A Bit-Vector Differential Model for the Modular Addition by a Constant

Seyyed Arash Azimi, Adrián Ranea, Mahmoud Salmasizadeh, Javad Mohajeri, Mohammad Reza Aref, and Vincent Rijmen

Abstract

ARX algorithms are a class of symmetric-key algorithms constructed by Addition, Rotation, and XOR, which achieve the best software performances in low-end microcontrollers. To evaluate the resistance of an ARX cipher against differential cryptanalysis and its variants, the recent automated methods employ constraint satisfaction solvers, such as SMT solvers, to search for optimal characteristics. The main difficulty to formulate this search as a constraint satisfaction problem is obtaining the differential models of the non-linear operations, that is, the constraints describing the differential probability of each non-linear operation of the cipher. While an efficient bit-vector differential model was obtained for the modular addition with two variable inputs, no differential model for the modular addition by a constant has been proposed so far, preventing ARX ciphers including this operation from being evaluated with automated methods. In this paper, we present the first bit-vector differential model for the n-bit modular addition by a constant input. Our model contains O(log_2(n)) basic bit-vector constraints and describes the binary logarithm of the differential probability. We also represent an SMT-based automated method to look for differential characteristics of ARX, including constant additions, and we provide an open-source tool ArxPy to find ARX differential characteristics in a fully automated way. To provide some examples, we have searched for related-key differential characteristics of TEA, XTEA, HIGHT, and LEA, obtaining better results than previous works. Our differential model and our automated tool allow cipher designers to select the best constant inputs for modular additions and cryptanalysts to evaluate the resistance of ARX ciphers against differential attacks.

Note: Fixed Table 10.

Metadata

Available format(s): PDF
Category: Secret-key cryptography
Publication info: A minor revision of an IACR publication in ASIACRYPT 2020
DOI: 10.1007/978-3-030-64837-4_13
Keywords: modular addition by a constant differential probability ARX SMT automated search bit-vector theory
Contact author(s): arash_azimi @ ee sharif edu
adrian ranea @ esat kuleuven be
History: 2022-04-28: revised; 2020-08-27: received; See all versions
Short URL: https://ia.cr/2020/1025
License: CC BY

BibTeX

@misc{cryptoeprint:2020/1025,
      author = {Seyyed Arash Azimi and Adrián Ranea and Mahmoud Salmasizadeh and Javad Mohajeri and Mohammad Reza Aref and Vincent Rijmen},
      title = {A Bit-Vector Differential Model for the Modular Addition by a Constant},
      howpublished = {Cryptology {ePrint} Archive, Paper 2020/1025},
      year = {2020},
      doi = {10.1007/978-3-030-64837-4_13},
      url = {https://eprint.iacr.org/2020/1025}
}