Verifying authentication protocols with CSP
- 1 January 1997
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
This paper presents a general approach for analysis and veri cation of authentication properties in the language of Communicating Sequential Processes CSP It is il lustrated 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 analy sis of authentication protocols built on top of the gen eral CSP semantic framework This approach aims to combine the ability to express such protocols in a natu ral and precise way with the facility to reason formally about the properties they exhibiKeywords
This publication has 16 references indexed in Scilit:
- A calculus of mobile processes, IPublished by Elsevier ,2004
- Intensional specifications of security protocolsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- What do we mean by entity authentication?Published by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Modelling and verifying key-exchange protocols using CSP and FDRPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- The Interrogator modelPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Recursion induction for real-time processesFormal Aspects of Computing, 1993
- Authentication and authenticated key exchangesDesigns, Codes and Cryptography, 1992
- Applying Formal Methods to the Analysis of a Key Management ProtocolJournal of Computer Security, 1992
- On the security of public key protocolsIEEE Transactions on Information Theory, 1983
- Using encryption for authentication in large networks of computersCommunications of the ACM, 1978