↑ Return to Frederic Lafitte


This package allows for the user to generate, manipulate, and solve SAT instances encoding cryptographic algorithms of the ARX family (Addition, Rotation, eXclusive or) that make use of bitwise Boolean functions and S-Boxes. Currently supported algorithms include the compression function of the obsolete hash algorithm MD4, the stream cipher ZUC used in 4G LTE, and the key schedule of block ciphers WIDEA and MESH. The package can be easily extended in order to support other algorithms.
System requirements: Linux, g++, little-endian platform.