arXiv · 2507.21731
Modelling Arbitrary Computations in the Symbolic Model using an Equational Theory for Bounded Binary Circuits
Abstract
In this work, we propose a class of equational theories for bounded binary circuits that have the finite variant property. These theories could serve as a building block to specify cryptographic primitive implementations and automatically discover attacks as binary circuits in the symbolic model. We provide proofs of equivalence between this class of equational theories and Boolean logic up to circuit size 3 and we provide the variant complexities and performance benchmarks using Maude-NPA. This is the first result in this direction and follow-up research is needed to improve the scalability of the approach.
Explore related subjects
Keep this discovery
Michiel Marcus, Frank Westers, Anne Nijsten. 2025-07-29. Modelling Arbitrary Computations in the Symbolic Model using an Equational Theory for Bounded Binary Circuits. https://arxiv.org/abs/2507.21731
Cite the original work for its findings. Save a collection to share your selection of sources.