HU Xiaobo, XU Shengyuan, TU Yinzi, FENG Xiutao, ZHANG Weihan
Journal of Systems Science and Complexity.
Accepted: 2023-08-28
In recent years, automatic search has been widely used to search differential characteristics and linear approximations with high probability/correlation in symmetric-key cryptanalyses. Among these methods, the automatic search with the Boolean Satisfiability Problem (SAT, in short) gradually becomes a powerful cryptanalysis tool. A key problem in the SAT-based automatic search method is how to fully characterize a set $S \subseteq \{0,1\}^n$ with as few Conjunctive Normal Form (CNF, in short) clauses as possible, which is called a full CNF characterization (FCC, in short) problem. In this work, we establish a complete theory to solve a best solution of a FCC problem. Specifically, we start from plain sets, which can be characterized by exactly one clause. By exploring mergeable sets, we give a sufficient and necessary condition for characterizing a plain set. Based on the properties of plain sets, we further provide an algorithm of solving a FCC problem for a given set $S$, which can generate all the minimal plain closures of $S$ and produce a best FCC theoretically. As application, we apply our algorithm to many common S-boxes used in block ciphers to characterize their differential distribution tables and linear approximation tables and get their FCCs, all of which are the best-known results at present.