We apply the PolyBoRi framework for Groebner bases computations

with Boolean polynomials to bit-valued problems from algebraic

cryptanalysis and formal verification.

First, we proposed zero-suppressed binary decision

diagrams (ZDDs) as a suitable data structure for Boolean polynomials.

Utilizing the advantages of ZDDs we develop new

reduced normal form algorithms for

linear lexicographical lead rewriting systems.

The latter play an important role in modeling bit-valued components of

digital systems.

Next, we reorder the variables in Boolean polynomial rings with respect

to the topology of digital components. This brings computational algebra

to digital circuits and small scale crypto systems in the first place. We

additionally propose an optimized topological ordering, which tends to

keep the intermediate results small. Thus, we successfully applied the

linear lexicographical lead techniques to non-trivial examples from

formal verification of digital systems.

Finally, we evaluate the performance using benchmark examples from

formal verification and cryptanalysis including equivalence checking of a

bit-level formulation of multiplier components. Before we introduced

topological orderings in PolyBoRi, state of the art for the algebraic approach

was a bit-width of 4 for each factor. By combining our techniques we raised

this bound to 16, which is an important step towards real-world applications.