On the Decidability of (ground) Reachability Problems for Cryptographic Protocols (extended version)

TL;DR

This paper introduces a transformation algorithm for cryptographic protocol analysis within a symbolic model, establishing conditions under which the ground reachability problem is decidable, and extends this to non-ground problems with a new criterion.

Contribution

It presents a novel transformation algorithm for deduction systems with the finite variant property and identifies a new condition for decidability of non-ground reachability problems.

Findings

Transformation algorithm terminates for systems with finite variant property

Decidability of ground reachability is achieved under the proposed conditions

A new criterion is provided for the decidability of non-ground problems

Abstract

Analysis of cryptographic protocols in a symbolic model is relative to a deduction system that models the possible actions of an attacker regarding an execution of this protocol. We present in this paper a transformation algorithm for such deduction systems provided the equational theory has the finite variant property. the termination of this transformation entails the decidability of the ground reachability problems. We prove that it is necessary to add one other condition to obtain the decidability of non-ground problems, and provide one new such criterion.