Deciding Indistinguishability
This work provides a foundational advance for cryptographers and verification experts by offering a decidable method to automate security proofs, though it is incremental as it builds on existing axiomatic approaches.
The paper tackled the problem of proving computational indistinguishability in cryptography by developing a decidable set of first-order axioms, achieving a theoretical result that enables automated verification of security protocols.
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.