Towards Model Checking a Spi-Calculus Dialect

We present a model checking framework for a spi-calculus dialect which uses a linear time temporal logic for expressing security properties. We have provided our spi-calculus dialect, called SPID, with a semantics based on labeled transition systems (LTS), where the intruder is modeled in the Dolev-Yao style as an active environment controlling the communication and able to compose new messages by pairing, splitting encryption or decryption. The LTS coming from protocols specification usually infinite state because of the intruder's capability to generate an infinite amount of messages, are the models over which the satisfiability of the logic formulae has been defined. As a logic we have used the one defined by Clarke, Jha and Marrero, for their BRUTUS model checker. We call it BRUTUS logic, which is known to be suitable to express a wide class of security properties, such as secrecy, integrity, authenticity some weak form of anonymity and general safety properties. Although providing a satisfiability procedure over models coming from SPID protocols is the main contribution of this paper, we also have, as long term target the development of an automatic verification tool. In this case we need finite models, and in this paper as a first solution we have limited in the transition rules defining the transitions of our LTS, the length of messages the intruder can generate. Although simple, this strategy suffices for obtaining finite models using which it is possible to discover known attacks over protocols commonly used as test cases.