[Resource Topic] 2023/300: CNF Characterization of Sets over $\mathbb{Z}_2^n$ and Its Applications in Cryptography

Welcome to the resource topic for 2023/300

CNF Characterization of Sets over \mathbb{Z}_2^n and Its Applications in Cryptography

Authors: Hu Xiaobo, Xu Shengyuan, Tu Yinzi, Feng Xiutao


In recent years, the automatic search has been widely used to search differential characteristics and linear approximations with high probability/correlation. Among these methods, the automatic search with the Boolean Satisfiability Problem (SAT, in short) gradually becomes a powerful cryptanalysis tool in symmetric ciphers. A key problem in the 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 find a sufficient and necessary condition for characterizing a plain set. Based on the properties of plain sets, we further provide an algorithm for solving a FCC problem with S, which can generate all the minimal plain closures of S and produce a best FCC theoretically. We also apply our algorithm to S-boxes used in block ciphers to characterize their differential distribution tables and linear approximation tables. All of our FCCs are the best-known results at present.

ePrint: https://eprint.iacr.org/2023/300

See all topics related to this paper.

Feel free to post resources that are related to this paper below.

Example resources include: implementations, explanation materials, talks, slides, links to previous discussions on other websites.

For more information, see the rules for Resource Topics .