SAT vs. Substitution Boxes of DES like Ciphers
Sylwia Stachowiak, Mirosław Kurkowski, Artur Soboń · 2021
One of the applied methods of symmetric ciphers investigations is cryptanalysis that uses the SAT problem. In this case, cipher testing starts with encoding the cipher's algorithm into a propositional Boolean formula. Then chosen randomly plaintext and cryptographic key are also encoded as formulas. Specialized to solve the SAT problem programs called SAT solvers can count the values of encrypted text for such input data. The final cipher analysis consists of providing the SAT solver with encoding formulas: plaintext and ciphertext. With such data, the SAT solver calculates the key value, i.e. performs cryptanalysis of the cipher with plaintext and ciphertext. In this work, we examine how SAT techniques behave for certain limited versions of the DES cipher and various types of S-boxes. To get the best result, we compared many, selected SAT solvers.