Verification of security protocols using Casper and FDR

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.  

hosted by