B2Scala 工具：面向安全的 Bach 在 Scala 中的集成
编程语言
2024-12-12 v1 多智能体系统
符号计算
摘要
过程代数已被广泛用于形式化方式验证安全协议。然而它们大多 focus on 基于消息交换的同步通信。我们提出了一种替代方法，依赖于通过共享空间中可用信息获得的异步通信。更准确地说，本文首先提出了将类似 Linda 的语言 Bach 嵌入 Scala 的方法。这包括一个内置于 Scala 的域特定语言（DSL），允许我们在受益于 Scala 生态系统（特别是其类型系统以及由 Scala 开发的程序片段）的同时实验在 Bach 中开发的程序。此外，我们引入了一个逻辑，用于限制满足逻辑公式的程序执行。我们以 Needham-Schroeder 安全协议为例，成功地自动重现了 G. Lowe 首次发现的中间人攻击。
引用
@article{arxiv.2412.08235,
title = {The B2Scala Tool: Integrating Bach in Scala with Security in Mind},
author = {Doha Ouardi and Manel Barkallah and Jean-Marie Jacquet},
journal= {arXiv preprint arXiv:2412.08235},
year = {2024}
}
备注
In Proceedings ICE 2024, arXiv:2412.07570