Verifying authentication protocols with CSP

This paper presents a general approach for analysis and veri cation 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 speci c 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.

• Type: Conference
• Year: 1997
• Where: CSFW
• Authors: Steve Schneider
• Keywords: Communicating Sequential Processes, CSFW 1997, CSP Semantic Framework, Needham-Schroeder Public-Key Protocol, Security Privacy