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 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.

• Type: Conference
• Year: 1995
• Where: CSFW
• Authors: A. W. Roscoe
• Keywords: CSFW 1995, Forces Careful Consideration, Key-exchange Protocols, Model-checking Tool Fdr, Security Privacy