A "Brutus" model checking of a spi-calculus dialect (Extended Abstract)

This paper proposes a preliminary framework in which protocols, expressed in a dialect of the spi-calculus, can be verified using model checking algorithms. In particular we define a formal semantics for a dialect of the spi-calculus based on labeled transition systems in such a way that the model checking environment developed by Clarke Marrero and Jha, can be re-used. Recently this environment has been extended with both a first order linear temporal logic, used to specify security properties, and partial order reduction techniques. These two new results make our approach interesting and effective for automatic verification.