On the Relationship between Strand Spaces and Multi-Agent Systems

TL;DR

This paper investigates the formal relationship between strand spaces and multi-agent systems, revealing differences in agent modeling and limitations in expressiveness, and proposes extensions to strand spaces for broader applicability.

Contribution

It provides a formal translation between strand spaces and multi-agent systems and identifies expressiveness limitations in strand spaces, suggesting extensions for improved modeling.

Findings

Not all multi-agent systems can be represented as strand spaces.

A family of translations from strand spaces to multi-agent systems is provided.

Strand spaces lack explicit agent modeling, limiting their expressiveness.

Abstract

Strand spaces are a popular framework for the analysis of security protocols. Strand spaces have some similarities to a formalism used successfully to model protocols for distributed systems, namely multi-agent systems. We explore the exact relationship between these two frameworks here. It turns out that a key difference is the handling of agents, which are unspecified in strand spaces and explicit in multi-agent systems. We provide a family of translations from strand spaces to multi-agent systems parameterized by the choice of agents in the strand space. We also show that not every multi-agent system of interest can be expressed as a strand space. This reveals a lack of expressiveness in the strand-space framework that can be characterized by our translation. To highlight this lack of expressiveness, we show one simple way in which strand spaces can be extended to model more systems.