Strand spaces with choice via a process Algebra semantics

Fan Yang, Santiago Escobar, Catherine Meadows, José Meseguer, Sonia Santiago

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Roles in cryptographic protocols do not always have a linear execution, but may include choice points causing the protocol to continue along different paths. In this paper we address the problem of representing choice in the strand space model of cryptographic protocols, particularly as it is used in the Maude-NPA cryptographic protocol analysis tool. To achieve this goal, we develop and give formal semantics to a process algebra for cryptographic protocols that supports a rich taxonomy of choice primitives for composing strand spaces. In our taxonomy, deterministic and non-deterministic choices are broken down further. Non-deterministic choice can be either explicit, i.e., one of two paths is chosen, or implicit, i.e. the value of a variable is chosen non-deterministically. Likewise, deterministic choice can be either an (explicit) if-then-else choice, i.e. one path is chosen if a predicate is satisfied, while the other is chosen if it is not, or implicit deterministic choice, i.e. execution continues only if a certain pattern is matched. We have identified a class of choices which includes finite branching and some cases of infinite branching, which we address in this paper. Our main theoretical results are two bisimulation results: one proving that the formal semantics of our process algebra is bisimilar to the forwards execution semantics of its associated strands, and another showing that it is also bisimilar with respect to the symbolic backwards semantics of the strands such as that supported by Maude-NPA. At the practical level, we present a prototype implementation of our process algebra in Maude-NPA, illustrate its expres-sive power and naturalness with various examples, and show how it can be effectively used in formal analysis.

Original languageEnglish (US)
Title of host publicationProceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, PPDP 2016
PublisherAssociation for Computing Machinery, Inc
Pages76-89
Number of pages14
ISBN (Electronic)9781450341486
DOIs
StatePublished - Sep 5 2016
Event18th International Symposium on Principles and Practice of Declarative Programming, PPDP 2016 - Edinburgh, United Kingdom
Duration: Sep 5 2016Sep 7 2016

Publication series

NameProceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, PPDP 2016

Other

Other18th International Symposium on Principles and Practice of Declarative Programming, PPDP 2016
CountryUnited Kingdom
CityEdinburgh
Period9/5/169/7/16

Keywords

  • Cryptographic protocol analysis
  • Narrowing-based reachability analysis
  • Process algebra
  • Rewriting-based model checking

ASJC Scopus subject areas

  • Software
  • Computational Theory and Mathematics
  • Computer Science Applications

Fingerprint Dive into the research topics of 'Strand spaces with choice via a process Algebra semantics'. Together they form a unique fingerprint.

  • Cite this

    Yang, F., Escobar, S., Meadows, C., Meseguer, J., & Santiago, S. (2016). Strand spaces with choice via a process Algebra semantics. In Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, PPDP 2016 (pp. 76-89). (Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, PPDP 2016). Association for Computing Machinery, Inc. https://doi.org/10.1145/2967973.2968609