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

TL;DR

This paper introduces B2Scala, a Scala-based tool embedding a Linda-like language called Bach, enabling formal security protocol verification with asynchronous communication and logic-based execution restrictions, demonstrated on the Needham-Schroeder protocol.

Contribution

It presents a novel Scala embedding of Bach with a logic for restricting executions, facilitating security protocol analysis within the Scala ecosystem.

Findings

Successfully rediscovered the man-in-the-middle attack on Needham-Schroeder

Demonstrated the integration of Bach in Scala with security-focused logic

Enabled formal verification of security protocols using asynchronous communication

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.