密码学报（中英文）2025，Vol.12Issue(4)：894-910,17.DOI:10.13868/j.cnki.jcr.000800
顺序编码方法优化与SAT搜索应用
Optimization of Sequential Encoding Method and SAT Search Application
摘要
Abstract
Automated search techniques are becoming increasingly important in cryptanalysis.SAT search techniques are among the commonly used methods.To better apply SAT search methods in the field of cryptanalysis and improve search efficiency,this study proposes a new method for constructing SAT models.First,a new k-input XOR model is proposed,which reduces the number of variables to 「(k-3)/2(」)·n while generating 4·(k-1)·n clauses.Second,improvements are made to the sequential encoding method for constraint objective functions,introducing two new sequential encoding methods.The auxiliary variables introduced by these two methods are reduced to(n-k-1/2)·k and(n-k)·k,respectively.Furthermore,based on the new sequential encoding methods,a new bounding condition encoding method is proposed,incorporating Matsui's bounding condition into the SAT model to accelerate the search.Finally,the new SAT model construction methods are applied to the search for the minimum active S-boxes in reduced-round ciphers of algorithms such as FBC,SMS4,and PRESENT,providing the minimum number of active S-boxes for these reduced-round ciphers.关键词
分组密码/差分分析/自动搜索/SAT方法Key words
block cipher/differential analysis/automatic search/SAT method分类
信息技术与安全科学引用本文复制引用
颜国华,张凤荣,崔笑,韦永壮,王保仓..顺序编码方法优化与SAT搜索应用[J].密码学报（中英文）,2025,12(4):894-910,17.基金项目
国家自然科学基金面上项目(62372346) （62372346）
陕西高校青年创新团队 General Program of National Natural Science Foundation of China(62372346) （62372346）
Youth Innovation Team of Shaanxi Universities （）
