A SAT-Based Algorithm for Finding Short Cycles in Shift Register Based Stream Ciphers
A SAT-Based Algorithm for Finding Short Cycles in Shift Register Based Stream Ciphers
复制标题
一种基于 SAT 的移位寄存器流密码中短周期查找算法
DOI：
--
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
M. Teslenko
中科院分区：
文献类型：
--
作者：
E. Dubrova;M. Teslenko
本文研究了基于移位寄存器的流密码在内部状态空间中寻找短周期的问题。现有的基于布尔决策图（BDD）的循环查找算法由于BDD对内存的需求过大而容量有限。基于仿真的算法可以应用于更大的实例，但是，它们不能保证检测给定长度的所有循环。这同样适用于通用的基于sat的模型检查器。提出了一种基于sat的算法，该算法可以在具有非常大状态空间的实际密码系统中找到所有短周期。通过分析流密码的Trivium、Bivium和Grain族，对该算法进行了评价。分析表明，Trivium、Bivium、Grain-80和Grain-128含有短周期，据我们所知，它们的存在以前是未知的。我们描述了理论上如何使用短周期进行故障攻击，从而导致完整的密钥恢复。
This paper addresses the problem of finding short cycles in the internal state space of shift register based stream ciphers.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 instances, however, they cannot guarantee the detection of all cycles of a given length. The same holds for general-purpose SAT-based model checkers. We present a SAT-based algorithm which can find all short cycles in real cryptographic systems with very large state spaces. The algorithm is evaluated by analyzing Trivium, Bivium, and Grain family of stream ciphers. The analysis shows that Trivium, Bivium, Grain-80 and Grain-128 contain short cycles whose existence, to our best knowledge, was previously unknown. We describe how short cycles can theoretically be used to mount a fault attack which results in a full secret key recovery.