索引演算攻击的奇偶性（XOR）推理
Parity (XOR) Reasoning for the Index Calculus Attack
摘要：
密码学问题通常可以简化为求解布尔多项式系统，其等价的逻辑公式可以使用SAT求解器来处理。考虑到问题的代数性质，逻辑XOR运算符的使用在基于SAT的密码分析中很常见。最近的工作集中在处理奇偶校验（XOR）约束的先进技术，如高斯消除技术。首先，我们提出了一个原始的XOR推理SAT求解器，名为WDSat（Weil Descent SAT求解），致力于一个特定的加密问题。其次，我们表明，在某些情况下，高斯消元SAT实例不工作，以及高斯消元代数系统。我们演示了如何在我们的求解器，这是适应于读取代数范式（ANF）的情况下，这种疏忽是固定的。最后，我们提出了一种新的预处理技术的基础上最小顶点覆盖问题的图论。这种预处理技术，在多变量布尔多项式系统的框架内，作为DLL分支选择规则，导致快速线性化的基本代数系统。我们的基准测试使用从加密实例中获得的模型，使用本文的研究结果实现了显着的加速。我们进一步解释了我们的预处理技术可以用来作为一个评估的安全性的密码系统。
英文摘要：
Cryptographic problems can often be reduced to solving Boolean polynomial systems, whose equivalent logical formulas can be treated using SAT solvers. Given the algebraic nature of the problem, the use of the logical XOR operator is common in SAT-based cryptanalysis. Recent works have focused on advanced techniques for handling parity (XOR) constraints, such as the Gaussian Elimination technique. First, we propose an original XOR-reasoning SAT solver, named WDSat (Weil Descent SAT solving), dedicated to a specific cryptographic problem. Secondly, we show that in some cases Gaussian Elimination on SAT instances does not work as well as Gaussian Elimination on algebraic systems. We demonstrate how this oversight is fixed in our solver, which is adapted to read instances in algebraic normal form (ANF). Finally, we propose a novel preprocessing technique based on the Minimal Vertex Cover Problem in graph theory. This preprocessing technique is, within the framework of multivariate Boolean polynomial systems, used as a DLL branching selection rule that leads to quick linearization of the underlying algebraic system. Our benchmarks use a model obtained from cryptographic instances for which a significant speedup is achieved using the findings in this paper. We further explain how our preprocessing technique can be used as an assessment of the security of a cryptographic system.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
