The B2Scala Tool: Integrating Bach in Scala with Security in Mind

Process algebras have been widely used to verify security protocols in a formal manner.However they mostly focus on synchronous communication based on the exchange of messages.We present an alternative approach relying on asynchronous communication obtained through information available on a shared space.More precisely this paper first proposes an embedding in Scala of a Linda-like language, called Bach.It consists of a Domain Specific Language, internal to Scala, that allows us to experiment programs developed in Bach while benefiting from the Scala eco-system, in particular from its type system as well as program fragments developed in Scala.Moreover, we introduce a logic that allows to restrict the executions of programs to those meeting logic formulae.Our work is illustrated on the Needham-Schroeder security protocol, for which we manage to automatically rediscover the man-in-the-middle attack first put in evidence by G. Lowe.