License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DagSemProc.10271.3
URN: urn:nbn:de:0030-drops-27894
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2010/2789/
Go to the corresponding Portal

Brickenstein, Michael ; Dreyer, Alexander

Network-driven Boolean Normal Forms

pdf-format:
10271.DreyerAlexander.Paper.2789.pdf (0.3 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{brickenstein_et_al:DagSemProc.10271.3,
  author =	{Brickenstein, Michael and Dreyer, Alexander},
  title =	{{Network-driven Boolean Normal Forms}},
  booktitle =	{Verification over discrete-continuous boundaries},
  pages =	{1--8},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10271},
  editor =	{Bernd Becker and Luca Cardelli and Holger Hermanns and Sofiene Tahar},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2010/2789},
  URN =		{urn:nbn:de:0030-drops-27894},
  doi =		{10.4230/DagSemProc.10271.3},
  annote =	{Keywords: Groebner, normal forms, Boolean polynomials, cryptanalysis, verification}
}

Keywords: Groebner, normal forms, Boolean polynomials, cryptanalysis, verification
Collection: 10271 - Verification over discrete-continuous boundaries
Issue Date: 2010
Date of publication: 02.11.2010

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI