Bosphorus is an ANF simplification and solving tool. It takes as input an ANF over GF(2) and can simplify and solve it. It uses many different algorithms, including XL, SAT, Brickenstein's ANF-to-CNF conversion, Gauss-Jordan elimination, etc. to simplify and solve ANFs.

The main use of the system is to simplify and solve ANF problems. It should give you highly optimised ANFs and CNFs that it can solve. Its ANF simplifications should be useful is many areas, not just direct ANF-to-SAT solving. For example, it could be useful for helping to break post-quantum cryptograpy problems.

This work was done by Davin Choo and Kian Ming A. Chai from DSO National Laboratories Singapore, and Mate Soos and Kuldeep Meel from the National University of Singapore (NUS). If you use Bosphorus, please cite our paper (bibtex) published at DATE 2019. Some of the code was generously donated by Security Research Labs, Berlin.

Please use the release binaries or Nix: install nix and then:

nix shell github:meelgroup/bosphorus

Then you will have the bosphorus binary available and ready to use.

Advanced users who want to build from source should follow the steps of the GitHub Actions build workflow:

Suppose we have a system of two equations:

x1 ⊕ x2 ⊕ x3 = 0
x1 * x2 ⊕ x2 * x3 + 1 = 0

Put this in the ANF file test.anf:

$ cat test.anf
x1 + x2 + x3
x1*x2 + x2*x3 + 1

or, you can use the more detailed description:

$ cat test-detail.anf
x(1) + x(2) + x(3)
x(1)*x(2) + x(2)*x(3) + 1

Bosphorus takes an input and at most one output file, and tells ANF from CNF by the .anf/.cnf extension; inputs may be gzipped (.anf.gz, .cnf.gz). Without an output file it solves:

$ ./bosphorus test.anf              # simplify and solve
$ ./bosphorus test.anf out.cnf      # simplify and write the CNF

To write both the simplified ANF and CNF, and solve and write the solution:

$ ./bosphorus test.anf out.anf --cnfwrite out.cnf --solvewrite solution

The simplified ANF is in out.anf:

$ cat out.anf
x(2) + 1
x(3) + x(1) + 1
c UNSAT : false

The simplified CNF is in out.cnf:

3 0
2 4 0
-2 -4 0

This CNF represents all the solutions to the ANF, i.e. it's equivalent to the ANF.

A solution to the problem is in solution:

$ cat solution
v -0 1 2 -3

This means x0 is false, x1 is true, x2 is true and x3 is false.

Complete bases come from Bosphorus's own matrix-F4 engine (--gbengine 1, M4RI over squarefree 64-bit monomials, deterministic budgets --gbsteps and --gbmaxcells); --gbengine 0 uses BRiAl's symmGB_F2 [8] and --gbengine 2 a Matrix-F5 [4] variant (with a MutantXL [9] step: rows that fell in degree are multiplied up again before the next degree) that is faster on random quadratic systems and slower on structured ones. Both engines stop as soon as the linear basis members fix every variable. A step whose matrix would exceed --gbmaxcells (default 250 MB) is not built: the system is split on a variable instead (gb-split, up to --gbsplit levels, --gbsplitrows matrix rows in total), so memory stays bounded and the degree stays low.

Small polynomials are converted directly (Brickenstein's algorithm [10]), and small equations that share variables, such as those of one S-box, are encoded jointly. Larger ones are linearised: nonlinear parts become XORed CNF variables, with small combinations such as x*y + x folded into one variable (the partner strategies of Jovanovic and Kreuzer [11]). A product of linear factors becomes one clause over one XOR-defined variable per factor. XORs are cut into short pieces, or written as CryptoMiniSat's native XOR clauses.

A projection set in the ANF becomes a c p show line in the CNF, so solution counts over it agree.

Post-quantum multivariate schemes reduce to quadratic systems over GF(2). Bosphorus reads Fukuoka MQ challenge files and Magma polynomial lists such as the HFE systems of Allan Steel through converters in utils/, and can generate random MQ systems with a planted solution. A system with few enough variables is solved by its Gröbner basis alone, without any SAT solving.

To reproduce a row of the table below:

python3 utils/mqgen.py 24 48 1 > mq24.anf   # n=24, m=48, seed 1
./build/bosphorus mq24.anf                  # F4; --gbengine 2 for F5

The degree of regularity of such a system is 4 up to n = 27 and 5 from n = 28, and a degree-5 matrix has five times the columns of a degree-4 one; gb-split fixes one variable (two for n = 30, three for n = 32), which brings every branch back to degree 4, and combines the branches. Memory in parentheses.

HFE systems (secret degree 96): Magma's F4 solved them in 2004 on hardware roughly 20-30x slower than a current core; Bosphorus finds the same solutions:

To find all solutions to myfile.anf:

./bosphorus myfile.anf --allsol
[...]
s ANF-SATISFIABLE
v x(0) x(1)+1 x(2) x(3)
s ANF-SATISFIABLE
v x(0) x(1)+1 1+x(2) 1+x(3)
s ANF-UNSATISFIABLE
c Number of solutions found: 2

Where x(0) means x(0) must be FALSE and x(1)+1 means x(1) must be TRUE. This enumerates one solution per SAT call and does not scale beyond some 10000 solutions; count larger solution sets with ApproxMC as below.

When there are too many solutions to list (say 2**40), count them on the CNF with ApproxMC. The ANF line c p show ... END sets the projection set; it becomes c p show ... 0 in the CNF:

$ cat count.anf
c p show x1 x2 x3 x4 END
x1*x2 + x3 + 1
x3*x5 + x6
$ ./bosphorus count.anf out.cnf
$ ./approxmc out.cnf
[...]
c [appmc] Number of solutions is: 4*2**0*2
s mc 8

If the number of solutions is low (say, less than 1000) you can also use CryptoMiniSat to do the counting:

./cryptominisat5 --maxsol 100000 out.cnf
[...]
c Number of solutions found until now:      8
s UNSATISFIABLE

Write the CNF together with a solution map, solve the CNF with any SAT solver, and map the model back to the ANF's variables:

./bosphorus test.anf test.cnf --solmap solution_map
./cryptominisat5 test.cnf > cnf_solution
./scripts/map_solution.py solution_map cnf_solution
s ANF-SATISFIABLE
v x(0) 1+x(1) 1+x(2) x(3)

x(0) means x(0) is FALSE and 1+x(1) means x(1) is TRUE.

• PolyBoRi cannot handle ring of sizes over approx 1 million (1048574). Do not run bosphorus on instances with over a million variables.

1. J. W. Freeman, Improvements to propositional satisfiability search algorithms, PhD thesis, University of Pennsylvania, 1995.
2. M. Soos, K. S. Meel, Arjun: an efficient independent support computation technique and its applications to counting and sampling, ICCAD 2022.
3. J.-C. Faugère, A new efficient algorithm for computing Gröbner bases (F4), J. Pure Appl. Algebra 139, 1999.
4. J.-C. Faugère, A new efficient algorithm for computing Gröbner bases without reduction to zero (F5), ISSAC 2002.
5. M. Bardet, J.-C. Faugère, B. Salvy, On the complexity of the F5 Gröbner basis algorithm, J. Symb. Comput. 70, 2015.
6. N. Courtois, A. Klimov, J. Patarin, A. Shamir, Efficient algorithms for solving overdefined systems of multivariate polynomial equations, EUROCRYPT 2000.
7. N. Courtois, P. Sepehrdad, P. Sušil, S. Vaudenay, ElimLin algorithm revisited, FSE 2012.
8. M. Brickenstein, A. Dreyer, PolyBoRi: a framework for Gröbner-basis computations with Boolean polynomials, J. Symb. Comput. 44, 2009.
9. J. Ding, J. Buchmann, M. S. E. Mohamed, W. S. A. Mohamed, R.-P. Weinmann, MutantXL, SCC 2008.
10. M. Brickenstein, Boolean Gröbner bases: theory, algorithms and applications, PhD thesis, TU Kaiserslautern, 2010.
11. P. Jovanovic, M. Kreuzer, Algebraic attacks using SAT-solvers, Groups Complex. Cryptol. 2, 2010.