密码学SAT入门文献1——Algebraic and Logic Solving Methods for Cryptanalysis

Algebraic solving of polynomial systems and satisfiability of propositional logic formulas are not two completely separate research areas, as it may appear at first sight. In fact, many problems coming from cryptanalysis, such as algebraic fault attacks, can be rephrased as solving a set of Boolean polynomials or as deciding the satisfiability of a propositional logic formula.

译文：事实上，许多来自密码分析的问题，如代数错误攻击，可以重新表述为解决一组布尔多项式或确定命题逻辑公式的可满足性。

Thus one can analyze the security of cryptosystems by applying standard solving methods from computer algebra and SAT solving.

译文：因此，人们可以通过应用计算机代数和SAT求解的标准求解方法来分析密码系统的安全性。

This doctoral thesis is dedicated to studying solvers that are based on logic and algebra separately as well as integrating them into one such that the combined solvers become more powerful tools for cryptanalysis.

译文：这篇博士论文致力于研究分别基于逻辑和代数的求解器，以及将它们集成到一起，使组合求解器成为密码分析的更强大的工具。

This disseration is divided into three parts. In this first part, we recall some theory and basic techniques for algebraic and logic solving. We focus mainly on DPLL-based SAT solving and techniques that are related to border bases and Gröbner bases.

译文：本文共分为三个部分。在第一部分中，我们回顾了代数和逻辑求解的一些理论和基本技术。我们主要关注基于dpll的SAT求解和与边界基地和Gröbner基地相关的技术。

In particular, we describe in detail the Border Basis Algorithm and discuss its specialized version for Boolean polynomials called the Boolean Border Basis Algorithm. In the second part of the thesis, we deal with connecting solvers based on algebra and logic. 特别地，我们详细描述了边界基算法，并讨论了布尔多项式的专门版本，称为布尔边界基算法。在论文的第二部分，我们处理基于代数和逻辑的连接求解器。

The ultimate goal is to combine the strength of different solvers into one. Namely, we fuse the XOR reasoning from algebraic solvers with the light, efficient design of SAT solvers. As a first step in this direction, we design various conversions from sets of clauses to sets of Boolean polynomials, and vice versa, such that solutions and models are preserved via the conversions.最终目标是将不同解算器的力量合而为一。也就是说，我们将代数解算器中的异或推理与SAT解算器的轻、高效设计融合在一起。作为这个方向的第一步，我们设计了从子句集到布尔多项式集的各种转换，反之亦然，这样通过转换可以保留解和模型。

In particular, based on a block-building mechanism, we design a new blockwise algorithm for the CNF to ANF conversion which is geared towards producing fewer and lower degree polynomials. 特别地，基于块构建机制，我们设计了一种新的基于块的CNF到ANF转换算法，该算法旨在产生更少、更低阶的多项式。

The above conversions allow usto integrate both solvers via a communication interface. To reach an even tighter integration, we consider proof systems that combine resolution and polynomial calculus, i.e. the two most used proof systems in logic and algebraic solving.

译文：上述转换允许我们通过通信接口集成两个求解器。为了达到更紧密的集成，我们考虑了结合分辨率和多项式演算的证明系统，即逻辑和代数求解中最常用的两个证明系统

Based on such a proof system, which we call SRES, we introduce new types of solving algorithms that demostrate the synergy between Gröbner-like and DPLL-like solving. At the end of the second part of the dissertation, we provide some experiments based on a new benchmark which illustrate that the our new method based on DPLL has the potential to outperform CDCL SAT solvers.

译文：基于这样一个我们称为SRES的证明系统，我们引入了新的求解算法类型，演示了Gröbner-like和类dpll求解之间的协同作用。在论文第二部分的最后，我们提供了一些基于新的基准的实验，这些实验表明，我们的基于DPLL的新方法具有超越CDCL SAT求解器的潜力。

In the third part of the thesis, we focus on practical attacks on various cryptograhic primitives. For instance, we apply SAT solvers in the case of algebraic fault attacks on the symmetric ciphers LED and derivatives of the block cipher AES. 在论文的第三部分，我们重点讨论了对各种密码原语的实际攻击。例如，我们将SAT求解器应用于对称密码LED和分组密码AES的导数上的代数故障攻击。

The main goal there is to derive so-called fault equations automatically from the hardware description of the cryptosystem and thus automatizate the attack. 主要目标是从密码系统的硬件描述中自动推导出所谓的故障方程，从而实现攻击的自动化。

To give some extra power to a SAT solver that inverts the hash functions SHA-1 and SHA-2, we describe how to tweak the SAT solver using a programmatic interface such that the propagation of the solver and thus the attack itself is improved. 为了给反转散列函数SHA-1和SHA-2的SAT求解器提供一些额外的功能，我们描述了如何使用编程接口来调整SAT求解器，以便改进求解器的传播，从而改进攻击本身。