Towards Parallel Direct SAT-Based Cryptanalysis

Abstract

In this paper we show a new approach of parallelised and optimised direct SAT-based cryptanalysis for symmetric block ciphers. It is shown how one can code directly in SAT each bit of the plaintext together with its ’route’ through the enciphering algorithm steps, code the round key schedule and S-boxes, and eliminate all simple Boolean equivalences and redundancies. We show Boolean coding directly from the analysed cipher’s source code, with no intermediate step of generating any auxiliary system of multivariate low-degree equations, as it was the case in SAT-enhanced algebraic cryptanalysis of [4]. This contributes to the results in much shorter formulae. Another speed-up effect we get by parallelising the cryptanalytic effort to some 2ⁿ available processing cores. We report some experimental results on two basic well known symmetric ciphers.