zbMATH — the first resource for mathematics

Polybori: A framework for Gröbner-basis computations with Boolean polynomials. (English) Zbl 1186.68571
Summary: This work presents a new framework for Gröbner-basis computations with Boolean polynomials. Boolean polynomials can be modelled in a rather simple way, with both coefficients and degree per variable lying in \(\{0,1\}\). The ring of Boolean polynomials is, however, not a polynomial ring, but rather the quotient ring of the polynomial ring over the field with two elements modulo the field equations \(x^{2}=x\) for each variable \(x\). Therefore, the usual polynomial data structures seem not to be appropriate for fast Gröbner-basis computations. We introduce a specialised data structure for Boolean polynomials based on zero-suppressed binary decision diagrams, which are capable of handling these polynomials more efficiently with respect to memory consumption and also computational speed. Furthermore, we concentrate on high-level algorithmic aspects, taking into account the new data structures as well as structural properties of Boolean polynomials. For example, a new useless-pair criterion for Gröbner-basis computations in Boolean rings is introduced. One of the motivations for our work is the growing importance of formal hardware and software verification based on Boolean expressions, which suffer-besides from the complexity of the problems -from the lack of an adequate treatment of arithmetic components. We are convinced that algebraic methods are more suited and we believe that our preliminary implementation shows that Gröbner-bases on specific data structures can be capable of handling problems of industrial size.

68W30 Symbolic computation and algebraic computation
13P10 Gröbner bases; other bases for ideals and modules (e.g., Janet and border bases)
Full Text: DOI
[1] Albrecht, M., 2006. Algebraic Attacks on the Courtois Toy Cipher. Universität Bremen. Diplomarbeit · Zbl 1248.94049
[2] Bachmann, O.; Schönemann, H., Monomial representations for Gröbner bases computations, (), 309-316 · Zbl 0924.68104
[3] Bard, G.V., 2006. Accelerating cryptanalysis with the method of four Russians. Cryptology ePrint Archive, Report 2006/251 http://eprint.iacr.org/
[4] Becker, T.; Weispfennig, V., Gröbner bases, a computational approach to commutative algebra, ()
[5] Bérard, B.; Bidoit, M.; Laroussine, F.; Petit, A.; Petrucci, L.; Schoenebelen, P.; McKenzie, P., Systems and software verification: model-checking techniques and tools, (1999), Springer-Verlag New York, Inc. New York, NY, USA
[6] Bosma, W.; Cannon, J.; Playoust, C., The magma algebra system I, Journal of symbolic computation, 24, 3/4, 235-265, (1997) · Zbl 0898.68039
[7] Brickenstein, M., 2006. Slimgb: Gröbner Bases with Slim Polynomials. In: Rhine Workshop on Computer Algebra. pp. 55-66. Proceedings of RWCA’06, Basel, March 2006
[8] Brickenstein, M., Dreyer, A., Greuel, G.-M., Wedler, M., Wienand, O., New developments in the theory of Gröbner bases and applications to formal verification. In: Theoretical Effectivity and Practical Effectivity of Groebner Bases. Journal of Pure and Applied Algebra, in press (doi:10.1016/j.jpaa.2008.11.043) (special issue) · Zbl 1164.68019
[9] Bryant, R.E., Graph-based algorithms for Boolean function manipulation, IEEE transactions on computers, 35, 8, 677-691, (1986) · Zbl 0593.94022
[10] Buchberger, B., A criterion for detecting unnecessary reductions in the construction of a Gröbner basis, () · Zbl 0417.68029
[11] Buchberger, B., 1965. Ein Algorithmus zum Auffinden der Basiselemente des Restklassenrings nach einem nulldimensionalen Polynomideal. Dissertation. Universität Innsbruck · Zbl 1245.13020
[12] Bulygin, S., Small-scale variant (examples) of the Advanced Encryption Standard (AES), private communication
[13] Chai, F., Gao, X.-S., Yuan, C., 2008. A characteristic set method for solving Boolean equations and applications in cryptanalysis of stream ciphers. MM-Preprints 26. URL: http://www.mmrc.iss.ac.cn/pub/mm26.pdf/4-csz2-mm.pdf · Zbl 1201.94080
[14] Cid, C.; Murphy, S.; Robshaw, M.J.B., Small scale variants of the AES, (), 145-162 · Zbl 1140.94330
[15] Clegg, M.; Edmonds, J.; Impagliazzo, R., Using the Groebner basis algorithm to find proofs of unsatisfiability, (1996), pp. 174-183 · Zbl 0938.68825
[16] Collart, S.; Kalkbrener, M.; Mall, D., Converting bases with the Gröbner walk, Journal of symbolic computation, 24, 465-469, (1997) · Zbl 0908.13020
[17] Coudert, O., Madre, J.C., 1992. Implicit and incremental computation of primes and essential primes of Boolean functions. In: Design Automation Conference. pp. 36-39
[18] Courtois, N., 2006. How fast can be algebraic attacks on block ciphers? Cryptology ePrint Archive, Report 2006/168. URL: http://eprint.iacr.org/2006/168.pdf
[19] Eén, N.; Sörensson, N., An extensible SAT-solver, (), 502-518 · Zbl 1204.68191
[20] Faugère, J.-C., Algebraic cryptanalysis of hidden field equation (HFE) cryptosystems using Gröbner bases, (), 44-60 · Zbl 1122.94371
[21] Faugère, J.-C., A new efficient algorithm for computing Gröbner bases (\(F_4\)), Journal of pure and applied algebra, 139, 1-3, 61-88, (1999) · Zbl 0930.68174
[22] Ghasemzadeh, M., 2005. A new algorithm for the quantified satisfiability problem, based on zero-suppressed binary decision diagrams and memoization. Ph.D. Thesis, University of Potsdam, Potsdam, Germany URL: http://opus.kobv.de/ubp/volltexte/2006/637/
[23] Giovini, A.; Mora, T.; Niesi, G.; Robbiano, L.; Traverso, C., One sugar cube, please or selection strategies in buchberger algorithms, (), 49-54 · Zbl 0933.68161
[24] Greuel, G.-M., Pfister, G., Schönemann, H., 2005. SINGULAR 3.0. A Computer Algebra System for Polynomial Computations. Centre for Computer Algebra, University of Kaiserslautern. URL: http://www.singular.uni-kl.de
[25] Greuel, G.-M.; Pfister, G., A SINGULAR introduction to commutative algebra, (2002), Springer Verlag
[26] Hachtel, G.D.; Somenzi, F., Logic synthesis and verification algorithms, (1996), Kluwer Academic · Zbl 0861.94035
[27] Hansen, O.M., Michon, J.-F., 2006. Boolean Gröbner basis. In: Michon, J.-F., Valarcher, P., Yunès, J.-B. (Eds.). Proceedings of BFCA’06 Conference, March 13-15, 2006, Rouen, France. pp. 185-201
[28] Hoos, H.H.; Stützle, T., SATLIB: an online resource for research on SAT, (), 283-292 · Zbl 0979.68128
[29] Kunz, W.; Marques-Silva, J.; Malik, S., SAT and ATPG: algorithms for Boolean decision problems, (2002), p. 309-341
[30] McMillan, K.L., Symbolic model checking, (1993), Kluwer Academic Publishers Norwell, MA, USA · Zbl 1132.68474
[31] Michon, J.-F.; Valarcher, P.; Yunès, J.-B., HFE and BDDs: A practical attempt at cryptanalysis, (), 237-246 · Zbl 1060.94023
[32] Minato, S., 1995. Implicit manipulation of polynomials using zero-suppressed BDDs. In: Proc. of IEEE The European Design and Test Conference, ED&TC’95. pp. 449-454
[33] National Institute of Standards and Technology,, 2001. Advanced encryption standard (AES). FIPS-197, U.S. DoC/National Institute of Standards and Technology
[34] Rossum, G.V.; Drake, F.L., The python language reference manual, (2006), Network Theory Ltd. Bristol, United Kingdom
[35] Somenzi, F., 2005. CUDD: CU decision diagram package. University of Colorado at Boulder, Release 2.4.1. URL: http://vlsi.colorado.edu/ fabio/CUDD/
[36] Steel, A., 2004. Allan Steel’s Gröbner basis timings page.Website. URL: http://magma.maths.usyd.edu.au/users/allan/gb/
[37] Stepanov, A.A., Lee, M., 1994. The Standard Template Library. Tech. Rep. X3J16/940095, WG21/N0482
[38] Toli, I.; Zanoni, A., An algebraic interpretation of AES-128, (), 84-97 · Zbl 1117.94337
[39] Wedler, M., Formal verification of multipliers (examples), private communication · Zbl 0483.68074
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.