Verifying authentication protocols with CSP

This paper presents a general approach for analysis and verification of authentication properties in the language of Communicating Sequential Processes (CSP). It is illustrated by an examination of the Needham-Schroeder public-key protocol. The contribution of this paper is to develop a specific theory appropriate to the analysis of authentication protocols, built on top of the general CSP semantic framework. This approach aims to combine the ability to express such protocols in a natural and precise way with the facility to reason formally about the properties they exhibit. 1 Introduction Authentication comes in a number of flavours. For example, Gollmann [6] has identified four different varieties of authentication, which raises the question for any particular authentication protocol as to which kind of authentication the protocol was designed for, and which kinds it actually provides. The aim of the CSP approach is to reduce questions about security protocols and properties to ques..