Modelling and Verifying Key-Exchange Protocols using CSP and FDR

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 nat-ural to consider the closely connected issues of commit-ment and no-loss-of service. We argue that it is often better to specify key exchange mechanisms in the con-text of an enclosing system rather than in isolation.