On cryptographic attacks using backdoors for SAT

Alexander Semenov, Oleg Zaikin, Ilya Otpuschennikov, Stepan Kochemazov, Alexey Ignatiev

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

31 Citations (Scopus)


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.

Original languageEnglish
Title of host publicationThe Thirty-Second AAAI Conference on Artificial Intelligence
EditorsSheila McIlraith, Kilian Weinberger
Place of PublicationPalo Alto CA USA
PublisherAssociation for the Advancement of Artificial Intelligence (AAAI)
Number of pages8
ISBN (Electronic)9781577358008
Publication statusPublished - 2018
Externally publishedYes
EventAAAI Conference on Artificial Intelligence 2018 - New Orleans, United States of America
Duration: 2 Feb 20187 Feb 2018
Conference number: 32nd


ConferenceAAAI Conference on Artificial Intelligence 2018
Abbreviated titleAAAI 2018
Country/TerritoryUnited States of America
CityNew Orleans
Internet address


  • Satisfiability
  • Backdoors
  • Cryptanalysis
  • Guess-and-determine attack

Cite this