An efficient SAT-based algorithm for finding short cycles in cryptographic algorithms
An efficient SAT-based algorithm for finding short cycles in cryptographic algorithms
复制标题
一种基于 SAT 的高效算法，用于查找密码算法中的短周期
DOI：
10.1109/hst.2018.8383892
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
M. Teslenko
中科院分区：
文献类型：
--
作者：
E. Dubrova;M. Teslenko
对于迭代的密码算法来说，没有短循环是一个理想的属性。此外，正如A5的密码分析所证明的那样，可以利用短周期来降低攻击的复杂性。我们提出了一个算法，它使用基于SAT的有界模型检查找到所有短周期的给定长度。现有的布尔决策图（BDD）的基础上寻找循环的算法有有限的容量，由于过多的存储器需求的BDD。基于仿真的算法可以应用于更大的问题实例，但是，它们不能保证检测到给定长度的所有循环。这同样适用于通用的基于SAT的模型检查器。该算法可以处理具有非常大的状态空间的密码算法，包括重要的密码，如Trivium和Grain-128。我们发现，这些密码包含短周期的存在，据我们所知，以前是未知的。这可能为密码分析开辟新的可能性。
The absence of short cycles is a desirable property for cryptographic algorithms that are iterated. Furthermore, as demonstrated by the cryptanalysis of A5, short cycles can be exploited to reduce the complexity of an attack. We present an algorithm which uses a SAT-based bounded model checking for finding all short cycles of a given length. The existing Boolean Decision Diagram (BDD) based algorithms for finding cycles have limited capacity due to the excessive memory requirements of BDDs. The simulation-based algorithms can be applied to larger problem instances, however, they cannot guarantee the detection of all cycles of a given length. The same holds for general-purpose SAT-based model checkers. The presented algorithm can handle cryptographic algorithms with very large state spaces, including important ciphers such as Trivium and Grain-128. We found that these ciphers contain short cycles whose existence, to our best knowledge, was previously unknown. This potentially opens new possibilities for cryptanalysis.