  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.
