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...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■{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,the authors establish a complete theory to solve a best solution of an FCC problem.Specifically,the authors start from plain sets,which can be characterized by exactly one clause.By exploring mergeable sets,the authors give a sufficient and necessary condition for characterizing a plain set.Based on the properties of plain sets,the authors further provide an algorithm of solving an 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,the authors apply the proposed 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.展开更多
基金supported by the National Key Research and Development Project under Grant No.2018YFA0704705CAS Project for Young Scientists in Basic Research under Grant No.YSBR-035。
文摘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■{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,the authors establish a complete theory to solve a best solution of an FCC problem.Specifically,the authors start from plain sets,which can be characterized by exactly one clause.By exploring mergeable sets,the authors give a sufficient and necessary condition for characterizing a plain set.Based on the properties of plain sets,the authors further provide an algorithm of solving an 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,the authors apply the proposed 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.
