Security protocols are relatively small and need to be right. One can interpret these protocols as messages exchanged between agents that might be intercepted or altered by an intruder. Therefore, a security protocol can be represented as a system of parallel CSP processes that correspond to the agents and intruder.

Secrecy and authentication requirements can be expressed as trace properties. In order to show that a security protocol meets its security requirements thus amounts to verification of the trace properties of the corresponding CSP system.

Casper, a tool developed by Gavin Lowe, helps translating transaction based protocol descriptions into CSP. FDR, a model checker for CSP developed by Bill Roscoe et al., can be used to check the required trace properties. We illustrate the use of these tools for a few simple protocols.