Sequential protocol composition in Maude-NPA

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

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


Protocols do not work alone, but together, one protocol relying on another to provide needed services. Many of the problems in cryptographic protocols arise when such composition is done incorrectly or is not well understood. In this paper we discuss an extension to the Maude-NPA syntax and operational semantics to support dynamic sequential composition of protocols, so that protocols can be specified separately and composed when desired. This allows one to reason about many different compositions with minimal changes to the specification. Moreover, we show that, by a simple protocol transformation, we are able to analyze and verify this dynamic composition in the current Maude-NPA tool. We prove soundness and completeness of the protocol transformation with respect to the extended operational semantics, and illustrate our results on some examples.

Original languageEnglish (US)
Title of host publicationComputer Security, ESORICS 2010 - 15th European Symposium on Research in Computer Security, Proceedings
Number of pages16
ISBN (Print)3642154964, 9783642154966
StatePublished - 2010
Event15th European Symposium on Research in Computer Security, ESORICS 2010 - Athens, Greece
Duration: Sep 20 2010Sep 22 2010

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6345 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other15th European Symposium on Research in Computer Security, ESORICS 2010

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Sequential protocol composition in Maude-NPA'. Together they form a unique fingerprint.

Cite this