# On Cryptographic Attacks Using Backdoors for SAT

arXiv: https://arxiv.org/abs/1803.04646 · HTML: https://mlsanity.com/paper/1803.04646/

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 13 Mar 2018.

## Built on by (most cited first, 6 of 6)

- [Learning Pseudo-Backdoors for Mixed Integer Programs](https://mlsanity.com/paper/2106.05080/) (2021)
- [A Parameterized Theory of PAC Learning](https://mlsanity.com/paper/2304.14058/) (2023)
- [ML Supported Predictions for SAT Solvers Performance](https://mlsanity.com/paper/2112.09438/) (2021)
- [Inverting Cryptographic Hash Functions via Cube-and-Conquer](https://mlsanity.com/paper/2212.02405/) (2022)
- [Decomposing Hard SAT Instances with Metaheuristic Optimization](https://mlsanity.com/paper/2312.10436/) (2023)
- [Efficient Parallel Algorithm for Decomposing Hard CircuitSAT Instances](https://mlsanity.com/paper/2602.17130/) (2026)

## Abstract (arXiv)

Propositional satisfiability (SAT) is at the nucleus of state-of-the-art approaches to a variety of computationally hard problems, one of which is cryptanalysis. Moreover, a number of practical applications of SAT can only be tackled efficiently by identifying and exploiting a subset of formula's variables called backdoor set (or simply backdoors). This paper proposes a new class of backdoor sets for SAT used in the context of cryptographic attacks, namely guess-and-determine attacks. The idea is to identify the best set of backdoor variables subject to a statistically estimated hardness of the guess-and-determine attack using a SAT solver. Experimental results on weakened variants of the renowned encryption algorithms exhibit advantage of the proposed approach compared to the state of the art in terms of the estimated hardness of the resulting guess-and-determine attacks.