STP models of optimal differential and linear trail for S-box based ciphers  

作　　者：Yu LIU Huicong LIANG Muzhou LI Luning HUANG Kai HU Chenhe YANG Meiqin WANG 

机构地区：[1]Key Laboratory of Cryptologic Technology and Information Security,Ministry of Education,Shandong Uniuersity,Jinan 250100,China [2]School of Computer Engineering,Weifang University,Weifang 261061,China

出　　处：《Science China(Information Sciences)》2021年第5期217-219,共3页中国科学（信息科学）（英文版）

基　　金：supported by National Cryptography Development Fund(Grant No.MMJJ20170102);National Natural Science Foundation of China(Grant Nos.61572293,61502276,61692276);Natural Science Foundation of Shandong Province(Grant No.ZR2016FM22);Major Scientific and Technological Innovation Projects of Shandong Province,China(Grant No.2017CXGC0704)。

摘　　要：Dear editor,SAT solvers,based on heuristic algorithms,are used to solve Boolean satisfiability(SAT)problems.Satisfiability modulo theories(SMT)problem is a decision problem concerned with the satisfiability of a logical formula;it is expressed as a combination of first-order theories.

关 键 词：problems. TRAIL OPTIMAL 

分 类 号：TN918.1[电子电信—通信与信息系统]