Decidability of a Sound Set of Inference Rules for Computational Indistinguishability

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 [7, 8], axiomatizing what an adversary cannot distinguish. We prove the decidability of a set of first-order axioms that are computationally sound, though incomplete, for protocols with a bounded number of sessions whose security is based on an IND-CCA2 encryption scheme. Alternatively, our result can be viewed as the decidability of a family of cryptographic game transformations. Our proof relies on term rewriting and automated deduction techniques.