  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.
