一句话：提出将离散函数算法描述归约为 SAT 的技术与 Transalg 工具，用于代数密码分析并构造攻击。
论文面向代数密码分析中如何将密码函数与攻击场景自然归约为 SAT 的问题。作者提出一套将离散函数算法描述翻译为 SAT 的技术，并在理论上论证对一大类密码学常用函数进行通用 SAT 归约的基本原则。基于该原则实现 Transalg 工具，专门考虑基于 SAT 的密码分析需求。作者用 Transalg 构造了对多种密码函数的攻击，其中部分达到当时最优水平；还将该工具功能与其他领域特定归约工具及符号验证系统 CBMC 比较，并利用近年 SAT 竞赛优胜求解器给出大量实验数据。
In the present paper, we propose a technology for translating algorithmic descriptions of discrete functions to SAT. The proposed technology is aimed at applications in algebraic cryptanalysis. We describe how cryptanalysis problems are reduced to SAT in such a way that it should be perceived as natural by the cryptographic community. In~the theoretical part of the paper we justify the main principles of general reduction to SAT for discrete functions from a class containing the majority of functions employed in cryptography. Then, we describe the Transalg software tool developed based on these principles with SAT-based cryptanalysis specifics in mind. We demonstrate the results of applications of Transalg to construction of a number of attacks on various cryptographic functions. Some of the corresponding attacks are state of the art. We compare the functional capabilities of the proposed tool with that of other domain-specific software tools which can be used to reduce cryptanalysis problems to SAT, and also with the CBMC system widely employed in symbolic verification. The paper also presents vast experimental data, obtained using the SAT solvers that took first places at the SAT competitions in the recent several years.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-1805-07239,
title = {Translation of Algorithmic Descriptions of Discrete Functions to SAT with Applications to Cryptanalysis Problems},
author = {Alexander Semenov and Ilya Otpuschennikov and Irina Gribanova and Oleg Zaikin and Stepan Kochemazov},
journal = {Logical Methods in Computer Science},
volume = {Volume 16, Issue 1},
year = {2020},
doi = {10.23638/lmcs-16(1:29)2020}
}