Differential cryptanalysis against ARX block ciphers using SAT solvers

Humanity is living during these days critical and unprecedented changes introduced by the fourth industrial revolution. In fact, this fourth major industrial era characterized by the fusion of information technologies and the blur of lines between physical and cyber spaces is changing, the way we live, work, and communicate; and reshape government, education, health care, and almost every aspect of society. However, having all those new technologies impacting human lives, abilities and even values, information systems security needs to move beyond more than ever in order to protect data confidentiality and ensure digital privacy, authenticity, integrity, and availability. Indeed, sensitive data leakage or exposure to unintended hands would affect someone’s professional or personal life, be the source of losing billions of dollars, or even more threaten the existence of a multinational company and=or the national security of some country. Thus, ensuring information systems’ and networks’ security becomes a necessity nowadays. Generally, information security refers to tools designed and deployed to protect information from modification, disruption, destruction and inspection. Cryptography is considered as one of the most fundamental of these tools. It is mainly composed of a set of algorithms used to provide cryptographic services such as integrity, authenticity and confidentiality of information. Confidentiality is a service used to keep the content of information from all but those authorized to have it. Integrity is a service which addresses the unauthorized alteration of data. Authenticity is the fact of surely determining the origin of information. To achieve confidentiality, encryption algorithms are used. An encryption algorithm is a method that uses a parameter called the encryption key to transform plaintext to an unreadable form for those who do not possess the corresponding decryption key. The result of this transformation is called ciphertext. To find the plaintext, another method, called the decryption algorithm, is applied to the ciphertext using a parameter called decryption key. There are two types of encryption, symmetric encryption, and asymmetric encryption. Symmetric encryption consists of using the same key for encryption and decryption. Asymmetric encryption consists of using one key for encryption and another key for decryption. In practice, a huge amount of data is often encrypted. However, the asymmetric encryption is slow compared to the symmetric encryption because it requires much more computing power . As it is much faster and requires less computational power, symmetric encryption is widely used to protect the information in many modern computer systems. Conversely, asymmetric encryption is applied especially when speed and computing power are not primary concerns.

While the security of asymmetric encryption algorithms is based on hard problems such as integer factorization and discrete logarithms, the security of symmetric encryption algorithms comes from their exposure to public scrutiny: if no attack is exposed after years of analysis by the research community, the algorithm is considered valid for deployment. For this reason, this study focuses on the security of symmetric encryption algorithms. Symmetric encryption algorithms include two classes, stream ciphers and block ciphers. While a stream cipher is applied to plaintext of arbitrary length and encrypts a single data digit at time, a block cipher is applied to a plaintext of fixed length and encrypts the whole block of data at once. Block ciphers represent an important component in many cryptographic systems. Indeed, they are used in the design of pseudo random number generators, stream ciphers and hash functions. Therefore, they have a main role in message authentication techniques, data integrity mechanisms and entity authentication protocols. This study will first and foremost focus on ARX block ciphers which are block ciphers composed mainly of three operations: modular addition, bit rotation, and bitwise Xor. ARX block ciphers have been widely adopted for many years now[5], due to their rapidity and efficiency in both software and hardware environments. Indeed, they are based on lightweight mathematical operations known for their desirable cryptographic proprieties such as modular addition which provides non-linearity, bit rotation which offers single word diffusion, and XOR which affords both inter-words diffusion and linearity. However, no concrete understanding of their security properties has been developed until those days[10]. Although ARX block ciphers have been developed for a long time, their security analysis has not been yet well studied. Their

popularity comes from the conviction that they are both efficient and secure at

the same time[11]. Furthermore, it is believed that the use of a large number of

rounds enhances their security[12].

Differential cryptanalysis is one of the most powerful techniques used to evaluate the security of symmetric key primitives in general and block ciphers in

particular[12][13]. It has been used in the cryptanalysis of various symmetric

block ciphers. Except for Dinu et al.’ attempt in[14], there are no proven security bounds for ARX block ciphers against differential cryptanalysis.

To study the differentiability of ARX block ciphers I will use SAT solvers. Their

appearance allows solving many real-world problems related to different domains

such as planning software, hardware verification and cryptography[15]. In cryptography particularly, the propositional logic, on which they are based, strikes a

good balance for the formal verification of cryptographic primitives since many

cryptographic properties can be expressed as instances of the Boolean satisfia-

2

bility problem[3]. Indeed, SAT solvers have already been proved useful in the

automatic analysis of symmetric key primitives and used on several occasions for

cryptanalysis[16]. Applying SAT solvers in cryptanalysis consists in expressing

the relation between the input and output bits of a cryptographic algorithm as

a Boolean satisfiability problem (SAT), then involve a solver to find the secret

bits[17]. In[17] SAT solvers were used to find weak keys for block ciphers and

preimages in hash functions. In the context of algebraic attacks, Jovanovic and

Kreuzer applied them in[18] to solve polynomial systems over F2. They were

also used in[12] as a tool to search for an optimal differential characteristic to

an ARX cipher with the application to the Salsa20 stream cipher.

Although several works have demonstrated the utility of SAT solver in cryptanalysis, there is a lack of practical software tools for this purpose[3]. One of

the candidates for this task is Cryptosat. It is a free software tool that allows cryptographers unfamiliar with Boolean satisfiability to verify properties

of symmetric key primitives using SAT-solvers[3].

In its current version, Cryptosat cannot be easily used for differential and linear

cryptanalysis. Therefore, I will adapt this tool in studying the differential cryptanalysis of ARX block ciphers. For that, the main contribution of my PhD will

be to build an automatic method to find the good differential characteristic in

ARX block cipher. Besides, a similar method will be produced for an AND-RX

block cipher which is a block that uses bit rotation, XOR operation and the

bitwise AND as a source of non-linearity. These methods will be integrated into

the CryptoSAT tool by ensuring their accessibility.