The B2Scala Tool: Integrating Bach in Scala with Security in Mind
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866917866153967616 |
|---|---|
| author | Ouardi, Doha Barkallah, Manel Jacquet, Jean-Marie |
| author_facet | Ouardi, Doha Barkallah, Manel Jacquet, Jean-Marie |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2412_08235 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | The B2Scala Tool: Integrating Bach in Scala with Security in Mind Ouardi, Doha Barkallah, Manel Jacquet, Jean-Marie Programming Languages Multiagent Systems Symbolic Computation D.1.3; D.2.4; D.3.3 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. |
| title | The B2Scala Tool: Integrating Bach in Scala with Security in Mind |
| topic | Programming Languages Multiagent Systems Symbolic Computation D.1.3; D.2.4; D.3.3 |
| url | https://arxiv.org/abs/2412.08235 |