Deciding Indistinguishability

TL;DR

This paper introduces a decidable, axiomatic framework for computational indistinguishability in cryptography, enabling automated reasoning about security properties using term rewriting and deduction techniques.

Contribution

It formalizes a set of axioms for indistinguishability, proving their decidability and computational soundness, advancing automated cryptographic protocol analysis.

Findings

Decidability of a first-order axiomatization for indistinguishability.

Framework is both computationally sound and expressive.

Enables automated reasoning about cryptographic security properties.

Abstract

Computational indistinguishability is a key property in cryptography and verification of security protocols. Current tools for proving it rely on cryptographic game transformations. We follow Bana and Comon's approach, axiomatizing what an adversary cannot distinguish. We prove the decidability of a set of first-order axioms that are both computationally sound and expressive enough. This can be viewed as the decidability of a family of cryptographic game transformations. Our proof relies on term rewriting and automated deduction techniques.