Modelling Arbitrary Computations in the Symbolic Model using an Equational Theory for Bounded Binary Circuits

TL;DR

This paper introduces equational theories for bounded binary circuits with the finite variant property, enabling symbolic cryptographic analysis and attack discovery, with initial proofs and benchmarks demonstrating its potential.

Contribution

It presents a novel class of equational theories for bounded binary circuits with the finite variant property, linking Boolean logic and cryptographic primitive specification.

Findings

Proved equivalence between theories and Boolean logic up to circuit size 3

Provided variant complexities and performance benchmarks using Maude-NPA

First result establishing this approach in cryptographic circuit analysis

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.