A Logic-Based Verification Framework For Authentication Protocols

Designing authentication protocols is an error-prone process. In this paper, we develop a deductive style proof-based framework to verify authentication protocols. The proposed framework clearly represents authentication protocols and concisely proves their security properties. We utilise Distributed Temporal Protocol Logic (DTPL) to capture temporal aspects of distributed events. We formalise essential features for achieving authentication. We also extend the notion of source association for public-key protocols. The resulting framework demonstrates the ease with which a protocol is analysed. It also demonstrates DTPL\u27s suitability to be used as a meta-level tool to benefit from different formalisms. Copyright © 2007 Inderscience Enterprises Ltd