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.

翻译：进程代数已被广泛用于以形式化方法验证安全协议。然而，它们主要关注基于消息交换的同步通信。本文提出了一种替代方法，该方法依赖于通过共享空间上的可用信息实现的异步通信。具体而言，本文首先提出了一种在Scala中嵌入类Linda语言（称为Bach）的方案。该方案包含一个Scala内部的领域特定语言，使我们能够在利用Scala生态系统（特别是其类型系统以及用Scala开发的程序片段）的同时，对Bach开发的程序进行实验。此外，我们引入了一种逻辑，可将程序执行限制为满足逻辑公式的执行。我们的工作以Needham-Schroeder安全协议为例进行说明，通过该协议我们成功自动重现了G. Lowe首次揭示的中间人攻击。