The B2Scala Tool: Integrating Bach in Scala with Security in Mind
Doha Ouardi, Manel Barkallah, Jean-Marie Jacquet
TL;DR
This work addresses formal verification of security protocols in asynchronous settings by embedding the Bach coordination language into Scala as an internal DSL, B2Scala, and by introducing a bsL constraint logic to prune executions. The approach leverages Bach’s Linda-like shared-space semantics within Scala’s type system and libraries, enabling concrete coding of protocols like Needham–Schroeder and automated discovery of Lowe’s man-in-the-middle attack. Key contributions include a practical Scala-based embedding of Bach, a concrete store-based interpretation of Bach agents, and a formal bsL calculus controlling constrained executions. The work demonstrates that asynchronous network models can be effectively analyzed in a familiar programming language, with potential for extended protocol analysis and integration with Scala tooling and model-checking ideas.
Abstract
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.