报告名称：CNF Characterization of Sets over Z_2^n and Its Applications in Cryptography

报告专家：冯秀涛

专家单位：中国科学院数学与系统科学研究院

报告时间：2023年5月26日15：00-17：00

报告地点：数统院201会议室

专家简介： 

   冯秀涛，博士，中国科学院数学与系统科学研究院副研究员，博士生导师。长期从事序列密码设计理论和分析方法研究。作为祖冲之序列密码设计者之一， 曾参与 4G 通信加密标准祖冲之序列密码算法的标准制定和国际标准化推进工作，并主持轻量级分组密码 FBC 研制，该算法获得全国密码算法竞赛三等奖。主持或作为核心成员参加了国家重点研发计划、国家 863 计划、国家自然科学重点基金、国家自然科学面上基金等多项项目的研发，最近获得中科院稳定支持基础研究领域青年团队计划支持; 荣获包括中科院关肇直青年研究奖，国家科技发明二等奖，全国密码竞赛三等奖，全国密码数学竞赛二等奖，全国密码竞赛命题优秀奖等在内的多项奖项。发表科研论文近 40 篇，其中在 IEEE IT，DCC，FFTA，JoC，ASIACRYPTO，FSE，SETA 等国际顶级期刊和顶级会议上发表十余篇科研论文; 申请 14 项国家/国际专利。在密码破译方面，曾彻底破解了包括 A2U2、SABLIER、FASER128/FASER256、PANDA-S 等在内的一系列密码算法。

报告摘要：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, 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.