libFES : Fast Exhaustive Search for Polynomial Systems over F2

Charles Bouillaguet set up a nice shiny website for libFES the library for exhaustive search on polynomial systems over . The library has a Sage interface, so it’s easy to get started. It’s also integrated in Charles’ upcoming one-stop boolean system solving patch.

He calls his benchmarketing “bragging rights” … and boy has he earned those rights! Check it out, libFES is fast!

Slides of Talk on Sage & Algebraic Techniques

The slides of my Icebreak talk on Sage and algebraic techniques for (lazy) cryptographers are now available (LaTeX sources here).

SAT Solvers for Sage

One of the most efficient techniques for solving polynomial systems over is to convert the problem to a satisfiability problem and to use a standard SAT solver. In the past, I have used CryptoMiniSat and either my own ANF to CNF converter scripts based on Gregory Bard’s ideas or PolyBoRi’s script.

However, this setup leaves much to be desired:

1. It’s all based on string parsing which has some overhead.
2. Usually the instances produced using PolyBoRi’s conversion method are faster to solve. However, as the number of variables per equation increase this method becomes essentially exponentially more expensive. Hence, a compromise between the two techniques is needed.
3. We don’t have access to learnt clauses and conflict clauses.
4. It all feels a bit duct taped and fragile, partly because the code is not shipped with Sage.

At #418 I just finished a much nicer interface to various SAT solvers. Here are some features.