Verifying authentication protocols with CSP

Author

Schneider, Steve

Author_Institution

Dept. of Comput. Sci., London Univ., UK

fYear

1997

fDate

10-12 Jun 1997

Firstpage

3

Lastpage

17

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

Keywords

authorisation; communicating sequential processes; formal verification; message authentication; program verification; protocols; public key cryptography; Needham-Schroeder public key protocol; authentication properties; authentication protocol verification; communicating sequential processes; formal reasoning; general CSP semantic framework; Authentication; Computer science; Cryptographic protocols; Public key; Public key cryptography; Security; Standards development;

fLanguage

English

Publisher

ieee

Conference_Titel

Computer Security Foundations Workshop, 1997. Proceedings., 10th

Conference_Location

Rockport, MA

ISSN

1063-6900

Print_ISBN

0-8186-7990-5

Type

conf

DOI

10.1109/CSFW.1997.596775

Filename

596775