Analysing Security Protocols using CSP
Lowe Gavin · IOS Press eBooks · 2011
In this chapter we describe an approach to analysing security protocols using the process algebra CSP and the model checker FDR. The basic approach is to build a CSP model of a small system running the protocol, together with the most general intruder who can interact with the protocol. We then use the model checker FDR to explore the state space, looking for insecure states. In the second half of the chapter, we extend this approach so as to be able to analyse an arbitrary system running the protocol.