ChaCha20 Cipher Cryptanalysis through SAT Problem Solving

Boolean encoding is a prominent method for analyzing various algorithms and computer systems, including the cryptanalysis of symmetric ciphers. This approach begins with encoding the cipher algorithm into a Boolean propositional formula, followed by encoding randomly selected bits representing plaintext and cryptographic key as formulas. Specialized programs known as SAT solvers, which solve SAT problems, can then compute ciphertext values for these inputs. The final stage of cryptanalysis involves attempting to compute a key value from the plaintext and ciphertext, effectively performing cryptanalysis with plaintext and ciphertext. In this paper, we demonstrate how SAT techniques apply to the ChaCha20 cipher, a widely used stream cipher in many computer network security systems. We present an extensive analysis and experimental results of SAT-based direct cryptanalysis of the ChaCha20 cipher. Our research involves creating a propositional logical formula representing the entire ChaCha20 algorithm, generating plaintext and key randomly, and computing the corresponding ciphertext. Subsequently, we use SAT solvers to analyze the cipher. To achieve the best results, we compare several SAT solvers, including both relatively old but efficient ones and modern, popular ones. Additionally, we explore the behavior of SAT techniques with ChaCha20, examining its properties through cryptanalysis of both its standard and potentially weaker configurations.