# Logical Cryptanalysis as a SAT Problem

@article{Massacci2004LogicalCA, title={Logical Cryptanalysis as a SAT Problem}, author={Fabio Massacci and Laura Marraro}, journal={Journal of Automated Reasoning}, year={2004}, volume={24}, pages={165-203} }

Cryptographic algorithms play a key role in computer security and the formal analysis of their robustness is of utmost importance. Yet, logic and automated reasoning tools are seldom used in the analysis of a cipher, and thus one cannot often get the desired formal assurance that the cipher is free from unwanted properties that may weaken its strength.In this paper, we claim that one can feasibly encode the low-level properties of state-of-the-art cryptographic algorithms as SAT problems and… Expand

#### Figures, Tables, and Topics from this paper

#### 122 Citations

Complete SAT based Cryptanalysis of RC5 Cipher

- Computer Science
- 2020

This article presents a wide analysis and new experimental results of SATbased, direct cryptanalysis of the RC5 cipher, that uses logical encoding and uses SAT-solvers for checking the satisfiability of the Boolean formulas. Expand

Towards Complete SAT-based Cryptanalysis of RC5 Cipher

- Computer Science
- 2019 IEEE 15th International Scientific Conference on Informatics
- 2019

This paper shows investigations and new experimental results in the case of SAT-based, direct cryptanalysis of the RC5 cipher, and uses and compares several SAT solvers, one of the used and efficient ways to investigate important properties of some symmetric ciphers. Expand

Encoding Hash Functions as a SAT Problem

- Computer Science
- 2012 IEEE 24th International Conference on Tools with Artificial Intelligence
- 2012

The SATisfiability Problem is a core problem in mathematical logic and computing theory. In the last years, progresses have led it to be a great and competitive approach to practically solve a wide… Expand

Applications of SAT Solvers in Cryptanalysis: Finding Weak Keys and Preimages

- Mathematics, Computer Science
- J. Satisf. Boolean Model. Comput.
- 2014

An efficient, generic and automated method for generating SAT instances encoding a wide range of cryptographic computations is introduced and this method can be used to automate the first step of algebraic attacks, i.e. the generation of a system ofgebraic equations. Expand

CDCL(Crypto) and Machine Learning based SAT Solvers for Cryptanalysis

- Computer Science
- 2020

An approach called CDCL(Crypto) is described to tailor the internal subroutines of the CDCL SAT solver with domain-specific knowledge about cryptographic primitives, and a formulation of SAT into Bayesian moment matching to address heuristic initialization problem in SAT solvers is used. Expand

Extending SAT Solvers to Cryptographic Problems

- Computer Science
- SAT
- 2009

A new approach to solving cryptographic problems by adapting both the problem description and the solver synchronously instead of tweaking just one of them is presented, which was able to solve a well-researched stream cipher 26 times faster than was previously possible. Expand

An efficient SAT-based algorithm for finding short cycles in cryptographic algorithms

- Computer Science
- 2018 IEEE International Symposium on Hardware Oriented Security and Trust (HOST)
- 2018

The presented algorithm can handle cryptographic algorithms with very large state spaces, including important ciphers such as Trivium and Grain-128, and is found to contain short cycles whose existence, to the best knowledge, was previously unknown. Expand

Use of SAT Solvers in Cryptanalysis

- 2016

SAT solvers are a universal tool for finding solutions to boolean satisfiability problems. In the past they have also been used for cryptographic problems, such as finding preimages for hash… Expand

Satisfiability-based Framework for Enabling Side-channel Attacks on Cryptographic Software

- Computer Science
- Proceedings of the Design Automation & Test in Europe Conference
- 2006

A new framework for performing side-channel attacks is proposed by formulating the analysis phase as a search problem that can be solved using modern Boolean analysis techniques such as satisfiability solvers, which can substantially enhance the scope of side- channel attacks. Expand

On Finding Short Cycles in Cryptographic Algorithms

- 2017

We show how short cycles in the state space of a cryptographic algorithm can be used to mount a fault attack on its implementation which results in a full secret key recovery. The attack is based on… Expand

#### References

SHOWING 1-10 OF 66 REFERENCES

A New Challenge for Automated Reasoning: Veriication and Cryptanalysis of Cryptographic Algorithms

- 1999

The veriication of security properties is one of the key issues of computer science and automated reasoning tools play a key role in the high level veriication of cryptographic protocols. Yet almost… Expand

Using Walk-SAT and Rel-Sat for Cryptographic Key Search

- Computer Science
- IJCAI
- 1999

Two state-of-the-art AI search algorithms have been tested on the encoding of the Data Encryption Standard, to see whether they are up the task, and what lesson can be learned from the analysis on this benchmark to improve SAT solvers are discussed. Expand

The Inductive Approach to Verifying Cryptographic Protocols

- Computer Science
- J. Comput. Secur.
- 1998

Informal arguments that cryptographic protocols are secure can be made rigorous using inductive definitions. The approach is based on ordinary predicate calculus and copes with infinite-state… Expand

A Computing Procedure for Quantification Theory

- Computer Science
- JACM
- 1960

In the present paper, a uniform proof procedure for quantification theory is given which is feasible for use with some rather complicated formulas and which does not ordinarily lead to exponentiation. Expand

Automated Analysis of Cryptographic Protocols Using Mur '

- 1997

A methodology is presented for using a general-purpose state enumeration tool, Mur', to analyze cryptographic and security-related protocols. We illustrate the feasibility of the approach by… Expand

The First Experimental Cryptanalysis of the Data Encryption Standard

- Computer Science
- CRYPTO
- 1994

An improved version of linear cryptanalysis is described and its application to the first, successful computer experiment in breaking the full 16-round DES with high success probability if 243 random plaintexts and their ciphertexts are available. Expand

Automated analysis of cryptographic protocols using Mur/spl phi/

- Computer Science
- Proceedings. 1997 IEEE Symposium on Security and Privacy (Cat. No.97CB36097)
- 1997

The efficiency of Mur/spl phi/ allows us to examine multiple terms of relatively short protocols, giving us the ability to detect replay attacks, or errors resulting from confusion between independent execution of a protocol by independent parties. Expand

Programming Satan's Computer

- Computer Science
- Computer Science Today
- 1995

The task is to program a computer which gives answers which are subtly and maliciously wrong at the most inconvenient possible moment. Expand

SATO: An Efficient Propositional Prover

- Computer Science
- CADE
- 1997

Two techniques that are found eeective to improve SATO performance are discussed, one is about splitting rules; the other is about connict analysis. Expand

The complexity of satisfiability problems

- Computer Science, Mathematics
- STOC
- 1978

An infinite class of satisfiability problems is considered which contains these two particular problems as special cases, and it is shown that every member of this class is either polynomial-time decidable or NP-complete. Expand