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
CS09.pdf - Accepted Version
Available under License : See the attached licence file.
Plain Text (licence)
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.
|Divisions :||Faculty of Engineering and Physical Sciences > Computing Science|
|Date :||July 2009|
|Identification Number :||10.1016/j.cose.2008.10.001|
|Uncontrolled Keywords :||Authentication, Security protocols, CSP, Formal specification, Kerberos, CRYPTOGRAPHIC PROTOCOLS, ENTITY AUTHENTICATION, SPECIFICATIONS, NETWORKS|
|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.|
|Depositing User :||Symplectic Elements|
|Date Deposited :||01 Dec 2011 13:48|
|Last Modified :||23 Sep 2013 18:45|
Actions (login required)
Downloads per month over past year