Verifying authentication protocols in CSP

Author

Schneider, Steve

Author_Institution

Dept. of Comput. Sci., R. Holloway Univ. of London, Egham, UK

Volume

24

Issue

9

fYear

1998

fDate

9/1/1998 12:00:00 AM

Firstpage

741

Lastpage

758

Abstract

This paper presents a general approach for analysis and verification of authentication properties using the theory of Communicating Sequential Processes (CSP). The paper aims 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 ability to reason formally about the properties they exhibit. The theory is illustrated by an examination of the Needham-Schroeder (1978) public key protocol. The protocol is first examined with respect to a single run and then more generally with respect to multiple concurrent runs

Keywords

communicating sequential processes; formal verification; message authentication; protocols; public key cryptography; CSP; Communicating Sequential Processes; Needham-Schroeder protocol; authentication protocol verification; public key protocol; semantic framework; Authentication; Computer Society; Digital signatures; IEC standards; ISO standards; Logic; Protocols; Public key; Security;

fLanguage

English

Journal_Title

Software Engineering, IEEE Transactions on

Publisher

ieee

ISSN

0098-5589

Type

jour

DOI

10.1109/32.713329

Filename

713329