報告名稱: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.