离散函数算法描述到 SAT 的翻译及其在密码分析问题中的应用
计算机科学中的逻辑
2023-06-22 v5 人工智能
密码学与安全
摘要
在本文中，我们提出一种将离散函数的算法描述翻译为 SAT 的技术。所提技术旨在应用于代数密码分析。我们描述了如何将密码分析问题归约为 SAT，以使密码学界视为自然。在本文的理论部分，我们针对包含密码学中使用的多数函数的一类离散函数，论证了归约到 SAT 的一般原则。随后，我们描述了基于这些原则并顾及基于 SAT 的密码分析特性而开发的 Transalg 软件工具。我们展示了 Transalg 在构造针对多种密码函数的一系列攻击中的应用结果。其中部分相应攻击处于当前最优水平。我们将所提工具的功能与其他可用于将密码分析问题归约为 SAT 的专用软件工具，以及广泛用于符号验证的 CBMC 系统进行比较。本文还给出了使用近年来 SAT 竞赛中名列前茅的 SAT 求解器所获取的大量实验数据。
引用
@article{arxiv.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= {arXiv preprint arXiv:1805.07239},
year = {2023}
}