Expressive Power of Definite Clauses for Verifying Authenticity

Thanks to the work of Bruno Blanchet definite clauses are an established technique for verifying security properties of communication protocols. We investigate the expressive power of this approach with respect to verifying authenticity. A translation from protocols into definite clauses is given, and direct proofs for correctness and completeness of the authenticity verification based on these clauses are shown. These proofs are new, and in particular the completeness result is surprising. These results, beside their intrinsic value, shed light on some interesting issues about existing proposals for exploiting definite clauses in protocols verification.