Modelling and verifying key-exchange protocols using CSP and FDR
- 19 November 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- No. 10636900,p. 98-107
- https://doi.org/10.1109/csfw.1995.518556
Abstract
We discuss the issues involved in modelling and verifying key-exchange protocols within the framework of CSP and its model-checking tool FDR. Expressing such protocols within a process algebra forces careful consideration of exception handling, and makes it natural to consider the closely connected issues of commitment and no-loss-of service. We argue that it is often better to specify key exchange mechanisms in the context of an enclosing system rather than in isolation.Keywords
This publication has 5 references indexed in Scilit:
- A system for the specification and analysis of key management protocolsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Exploring the BAN approach to protocol analysisPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- CSP and determinism in security modellingPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- A logic of authenticationACM Transactions on Computer Systems, 1990
- Using encryption for authentication in large networks of computersCommunications of the ACM, 1978