Title: A logic-based verification framework for authentication protocols

Authors: Shahabuddin Muhammad, Zeeshan Furqan, Ratan K. Guha

Addresses: School of Electrical Engineering and Computer Science, University of Central Florida, Orlando, FL 32816, USA. ' School of Electrical Engineering and Computer Science, University of Central Florida, Orlando, FL 32816, USA. ' School of Electrical Engineering and Computer Science, University of Central Florida, Orlando, FL 32816, USA

Abstract: 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.

Keywords: security protocols; authentication protocols; distributed temporal protocol logic; DTPL; SVO logic; logic-based verification; security; source association; public key protocols.

DOI: 10.1504/IJITST.2007.014834

International Journal of Internet Technology and Secured Transactions, 2007 Vol.1 No.1/2, pp.49 - 80

Published online: 10 Aug 2007 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article