Propositional encoding of direct and inverse round transformations in attacks on some block ciphers

We suggest an attack on block ciphers, which is based on the well-known meet-in-the-middle strategy. To solve the corresponding cryptanalysis equations, algorithms for solving the Boolean satisfiability problem (SAT) are used. The main know-how consists in the usage in the propositional encoding of the considered cipher not only information about direct round transformations, but also information about inverse round transformations. Using the suggested type of encodings, we have constructed runtime estimations of guess-and-determine attacks on several block ciphers with reduced number of rounds ($6$-round DES, $6$-round PRESENT, $6$-round and $8$-round GOST 28147-89). It turned out that in some cases these attacks are several times more effective than attacks, in which standard methods of propositional encodings are used.