Deciding a Fragment of (α , β )-Privacy.

We show how to automate fragments of the logical framework (α, β)privacy which provides an alternative to bisimilarity-based and tracebased definitions of privacy goals for security protocols. We consider the so-called message-analysis problem, which is at the core of (α, β)-privacy: given a set of concrete messages and their structure, which models can the intruder rule out? While in general this problem is undecidable, we give a decision procedure for a standard class of algebraic theories.