2009 22nd IEEE Computer Security Foundations Symposium (2009)
Port Jefferson, New York
July 8, 2009 to July 10, 2009
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/CSF.2009.12
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.
definite clauses, protocol verification, security protocols, authenticity
R. Vigo and G. Filè, "Expressive Power of Definite Clauses for Verifying Authenticity," 2009 22nd IEEE Computer Security Foundations Symposium(CSF), Port Jefferson, New York, 2009, pp. 251-265.