The Modelling and Analysis of Security Protocols: the CSP Approach

9.9. The inductive approach

In 1996 Paulson [70] introduced the inductive approach with automated support provided by his Isabelle proof assistant. In several respects the underlying, conceptual framework is similar to that of the CSP approach. The key elements are traces: sequences of events that could occur as the protocol agents execute in a hostile environment. Traces are defined inductively from a set of rules that correspond to the possible actions of the agents, including spies. The approach does not involve state enumeration and so the numbers of agents and spies can be regarded as unbounded – and indeed each agent can be allowed to play multiple roles simultaneously.

Security properties such as secrecy and authentication can be stated ...