A logic-based verification framework for authentication protocols
Shahabuddin Muhammad, Zeeshan Furqan, Ratan Kumar Guha · International Journal of Internet Technology and Secured Transactions · 2007
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's suitability to be used as a meta-level tool to benefit from different formalisms.