On the relationship between strand spaces and multi-agent systems

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.

REFERENCES

• 1: B. Alpern and F. B. Schneider. Defining liveness. Information Processing Letters, 21:181-185, 1985.
• 2: N. Asokan, V. Shoup, and M. Waidner. Asynchronous protocols for optimistic fair exchange. In Proceedings of the IEEE Symposium on Research in Security and Privacy, pages 86-99. IEEE Computer Society Press, 1998.
• 3: M. Ben-Or, O. Goldreich, S. Micali, and R. L. Rivest. A fair protocol for signing contracts. IEEE Transactions on Information Theory, 36(1):40-46, 1990.
• 4: Michael Burrows , Martin Abadi , Roger Needham, A logic of authentication, ACM Transactions on Computer Systems (TOCS), v.8 n.1, p.18-36, Feb. 1990 [doi>10.1145/77648.77649]
• 5: Nadia Busi , Roberto Gorrieri, Distributed Conflicts in Communicating Systems, Selected papers from the ECOOP'94 Workshop on Models and Languages for Coordination of Parallelism and Distribution, Object-Based Models and Languages for Concurrent Systems, p.49-65, July 05, 1994
• 6: Nancy Durgin , Patrick Lincoln , John Mitchell , Andre Scedrov , Iliano Cervesato, Relating Strands and Multiset Rewriting for Security Protocol Analysis, Proceedings of the 13th IEEE Computer Security Foundations Workshop (CSFW'00), p.35, July 03-05, 2000
• 7: Ronald Fagin , Joseph Y. Halpern , Moshe Y. Vardi , Yoram Moses, Reasoning about knowledge, MIT Press, Cambridge, MA, 1995
• 8: James W. Gray, III , Paul F. Syverson, A logical approach to multilevel security of probabilistic systems, Distributed Computing, v.11 n.2, p.73-90, April 1998 [doi>10.1007/s004460050043]
• 9: Adam J. Grove, Naming and identity in epistemic logic part II: a first-order logic for naming, Artificial Intelligence, v.74 n.2, p.311-350, April 1995 [doi>10.1016/0004-3702(95)98593-D]
• 10: A. J. Grove and J. Y. Halpern. Naming and identity in propositional logics, Part I: the propositional case. Journal of Logic and Computation, 3(4):345-378, 1993.
• 11: Joseph Y. Halpern, A note on knowledge-based programs and specifications, Distributed Computing, v.13 n.3, p.145-153, July 2000 [doi>10.1007/PL00008916]
• 12: Joseph Halpern , Yjoram Moses , Mark Tuttle, A knowledge-based analysis of zero knowledge, Proceedings of the twentieth annual ACM symposium on Theory of computing, p.132-147, May 02-04, 1988, Chicago, Illinois, United States [doi>10.1145/62212.62224]
• 13: J. McLean. Security models. In J. Marciniak, editor, Encyclopedia of Software Engineering. Wiley Press, 1994.
• 14: Catuscia Palamidessi, Comparing the expressive power of the synchronous and the asynchronous &pgr;-calculus, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.256-265, January 15-17, 1997, Paris, France [doi>10.1145/263699.263731]
• 15: V. Shmatikov and J. C. Mitchell. Analysis of a fair exchange protocol. In Seventh Annual Symposium on Network and Distributed System Security (NDSS 2000), pages 119-128, 2000.
• 16: Einer Snekkenes, Roles in Cryptographic Protocols, Proceedings of the 1992 IEEE Symposium on Security and Privacy, p.105, May 04-06, 1992
• 17: Stuart G. Stubblebine , Rebecca N. Wright, An authentication logic supporting synchronization, revocation, and recency, Proceedings of the 3rd ACM conference on Computer and communications security, p.95-105, March 14-15, 1996, New Delhi, India [doi>10.1145/238168.238195]
• 18: P. Syverson. A logic for the analysis of cryptographic protocols. NRL Report 9305, Naval Research Laboratory, 1990.
• 19: P. Syverson. Towards a strand semantics for authentication logic. Electronic Notes in Theoretical Computer Science, 20, 1999.
• 20: F. Javier Thayer , Jonathan C. Herzog , Joshua D. Guttman, Mixed Strand Spaces, Proceedings of the 1999 IEEE Computer Security Foundations Workshop, p.72, June 28-30, 1999
• 21: F. Javier Thayer Fábrega, Strand spaces: proving security protocols correct, Journal of Computer Security, v.7 n.2-3, p.191-230, Jan. 1999

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.6 SIMULATION AND MODELING
      I.6.5 Model Development
          Subjects: Modeling methodologies

Additional Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
        I.2.11 Distributed Artificial Intelligence
            Subjects: Multiagent systems
  I.6 SIMULATION AND MODELING
      I.6.4 Model Validation and Analysis

General Terms:
Algorithms, Design, Security