SAT-Based Cryptanalysis of Salsa20 Cipher

Abstract

Modeling through Boolean encoding is often used for the investigation of various kinds of algorithms or other computer systems. Such an approach can be used successfully to cryptanalysis of symmetric ciphers. In this case, cipher testing begins with encoding the cipher algorithm into a Boolean propositional formula. Then the randomly selected bits representing plaintext and cryptographic key are encoded as formulas too. Specially dedicated programs, called SAT solvers, which can solve an SAT problem, can then compute ciphertext values for such inputs. The final cryptanalysis is an attempt at computing a key value from plaintext and ciphertext. In this way, we perform cryptanalysis with plaintext and ciphertext. In this paper, we show how SAT techniques behave for the Salsa20 cipher which is one of a stream cipher widely used in many security systems of computer networks. In our work, we compared a number of selected SAT solvers. Some are relatively old but still very efficient and some are modern and popular.