Specifying authentication using signal events in CSP

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.

Document Downloads