Encoding Cryptographic Functions to SAT Using Transalg System
원문 초록
In this paper we propose the technology for constructing propositional encodings of discrete functions. It is aimed at solving inversion problems of considered functions using state-of-the-art SAT solvers. We implemented this technology in the form of the software system called Transalg, and used it to construct SAT encodings for a number of cryptanalysis problems. By applying SAT solvers to these encodings we managed to invert several cryptographic functions. In particular, we used the SAT encodings produced by Transalg to construct the family of two-block MD5 collisions in which the first 10 bytes are zeros. Also we used Transalg encoding for the widely known A5/1 keystream generator to solve several dozen of its cryptanalysis instances in a distributed computing environment. In the paper we compare in detail the functionality of Transalg with that of similar software systems.
함께 살펴볼 논문
공통 태그를 근거로 연결했습니다. 실제 인용 관계나 논문의 우수성을 뜻하지 않습니다.
Correlations Are Ruining Your Gradient Descent
SacFL: Self-Adaptive Federated Continual Learning for Resource-Constrained End Devices
Tree-Guided $L_1$-Convex Clustering
Distributed LLMs and Multimodal Large Language Models: A Survey on Advances, Challenges, and Future Directions
Benchmarking Dynamic SLO Compliance in Distributed Computing Continuum Systems
Distributed Mixture-of-Agents for Edge Inference with Large Language Models
토론
이 논문과 연결된 포럼 글이 아직 없습니다.