As a guest user you are not logged in or recognized by your IP address. You have
access to the Front Matter, Abstracts, Author Index, Subject Index and the full
text of Open Access publications.
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.
loading subjects...
