\myheading{\emph{Professional} cryptography}

\leveldown{}

Let's back to the method we previously used (\ref{symbolic_exec}) to construct expressions using running Python function.

We can try to build expression for the output of XXTEA encryption algorithm:

\lstinputlisting[style=custompy]{crypto/xxtea.py}

A key is chosen according to input data, and, obviously, we can't know it during symbolic execution,
so we leave expression like \TT{k[...]}.

Now results for just one round, for each of 4 outputs:

\lstinputlisting{crypto/1round.txt}

Somehow, the size of the expression for each subsequent output is bigger.
I hope I haven't been mistaken?
And this is just for 1 round.
For 2 rounds, size of all 4 expression is $\approx 970KB$.
For 3 rounds, this is $\approx 115MB$.
For 4 rounds, I have not enough RAM on my computer.
Expressions \emph{exploding} exponentially.
And there are 19 rounds.
You can weigh it.

Perhaps, you can simplify these expressions: there are a lot of excessive parenthesis,
but I'm highly pessimistic, cryptoalgorithms constructed in such a way to not have any spare operations.

In order to crack it, you can use these expressions as system of equation and try to solve it using SMT-solver.
This is called ``algebraic attack''.

In other words, theoretically, you can build a system of equation like this: $MD5(x)=12341234...$,
but expressions are so huge so it's impossible to solve them.
Yes, cryptographers are fully aware of this and one of the goals of the successful cipher is
to make expressions as big as possible, using reasonable time and size of algorithm.

Nevertheless, you can find numerous papers about breaking these cryptosystems with reduced number of rounds:
when expression isn't \emph{exploded} yet, sometimes it's possible.
This cannot be applied in practice, but such an experience has some interesting theoretical uses.

\myheading{Attempts to break ``serious'' crypto}

CryptoMiniSat itself exist to support XOR operation, which is ubiquitous in cryptography.

\begin{itemize}
\item Bitcoin mining with CBMC and SAT solver: \url{http://jheusser.github.io/2013/02/03/satcoin.html}, \url{https://github.com/msoos/sha256-sat-bitcoin}.

\item \href{http://2015.phdays.ru/program/dev/40400/}{Alexander Semenov, attempts to break A5/1, etc. (Russian presentation)}

\item \href{https://yurichev.com/mirrors/SAT_SMT_crypto/thesis-output.pdf}{Vegard Nossum - SAT-based preimage attacks on SHA-1}

\item \href{https://yurichev.com/mirrors/SAT_SMT_crypto/166.pdf}{Algebraic Attacks on the Crypto-1 Stream Cipher in MiFare Classic and Oyster Cards}

\item \href{https://yurichev.com/mirrors/SAT_SMT_crypto/Attacking-Bivium-Using-SAT-Solvers.pdf}{Attacking Bivium Using SAT Solvers}

\item \href{https://yurichev.com/mirrors/SAT_SMT_crypto/Extending_SAT_2009.pdf}{Extending SAT Solvers to Cryptographic Problems}

\item \href{https://yurichev.com/mirrors/SAT_SMT_crypto/sat-hash.pdf}{Applications of SAT Solvers to Cryptanalysis of Hash Functions}

\item \href{https://yurichev.com/mirrors/SAT_SMT_crypto/slidesC2DES.pdf}{Algebraic-Differential Cryptanalysis of DES}

\item Attempt to break Speck cipher: \url{https://github.com/TechSecCTF/z3_splash_class}.
\end{itemize}

\levelup{}