Specifying authentication using signal events in CSP

Shaikh, SA, Bush, VJ and Schneider, SA (2009) Specifying authentication using signal events in CSP Computers and Security, 28 (5). 310 - 324. ISSN 0167-4048

Preview	PDF CS09.pdf - Accepted Version Available under License : See the attached licence file. Download (327Kb)
	Plain Text (licence) licence.txt Download (1516b)

Abstract

The formal analysis of cryptographic protocols has developed into a comprehensive body of knowledge, building on a wide variety of formalisms and treating a diverse range of security properties, foremost of which is authentication. The formal specification of authentication has long been a subject of examination. In this paper, we discuss the use of correspondence to formally specify authentication and focus on Schneider's use of signal events in the process algebra Communicating Sequential Processes (CSP) to specify authentication. The purpose of this effort is to strengthen this formalism further. We develop a formal structure for these events and use them to specify a general authentication property. We then develop specifications for recentness and injectivity as sub-properties, and use them to refine authentication further. Finally, we use signal events to specify a range of authentication definitions and protocol examples to clarify their use and make explicit related theoretical issues. our work is motivated by the desire to effectively analyse and express security properties in formal terms, so as to make them precise and clear. (C) 2008 Elsevier Ltd. All rights reserved.

Item Type:	Article
Additional Information:	NOTICE: this is the author’s version of a work that was accepted for publication in Computers and Security. Changes resulting from the publishing process, such as peer review, editing, corrections, structural formatting, and other quality control mechanisms may not be reflected in this document. Changes may have been made to this work since it was submitted for publication. A definitive version was subsequently published in Computers and Security, 28(5), July 2009, DOI 10.1016/j.cose.2008.10.001.
Uncontrolled Keywords:	Authentication, Security protocols, CSP, Formal specification, Kerberos, CRYPTOGRAPHIC PROTOCOLS, ENTITY AUTHENTICATION, SPECIFICATIONS, NETWORKS
Divisions:	Faculty of Engineering and Physical Sciences > Computing Science
Depositing User:	Symplectic Elements
Date Deposited:	01 Dec 2011 13:48
Last Modified:	23 Sep 2013 18:45
URI:	http://epubs.surrey.ac.uk/id/eprint/7246

Actions (login required)

View Item

Downloads