基于SAT方法进一步加速差分特征的搜索

摘要

回顾了孙等使用Matsui边界条件加速差分特征搜索的方法,为了进一步提高搜索效率,改进了Matsui边界条件以及利用Matsui边界条件加速差分特征自动化搜索的方法,并提出了一种改进的方法来搜索分组密码的最优差分特征。研究了线程数和询问条件的加速效果并提出了选择线程数以及询问条件的策略。使用STP和CryptoMiniSat分别搜索概率为2^(-24)、2^(-25)、2^(-26)的8轮SPECK96差分特征以及概率为2^(-39)的11轮HIGHT差分特征,并比较了在不同线程数和询问条件下求解SAT/SMT问题的耗时。研究发现线程数对搜索差分特征的耗时影响较大,而询问条件对搜索差分特征的耗时影响较小,从而提出了一种如何选择线程数和询问条件的策略。根据所提策略,使用改进的边界条件和方法搜索HIGHT的11轮最优差分特征,并首次获得了HIGHT的11轮最优差分特征的紧致概率,即2^(-45)。现有的11轮HIGHT最优差分特征概率的最紧致边界是P_(Opt)^(11)≥2^(-45)。这就意味着,利用现有11轮HIGHT最优差分特征概率的最紧致边界无法给出11轮HIGHT抗差分分析安全性的精确评估。因此,所提策略的结果是目前已知的最优结果。