Verifying authentication protocols with CSP

Abstract

The 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 (R. Needham and M. Schroeder, 1978). The contribution of the article 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.