Sequential Protocol Composition in Maude-NPA
Title | Sequential Protocol Composition in Maude-NPA |
Publication Type | Conference Paper |
Year of Publication | 2010 |
Authors | Santiago Escobar, Universidad Politécnica de Valencia, Spain, Catherine Meadows, Naval Research Laboratory, Jose Meseguer, University of Illinois at Urbana-Champaign, Sonia Santiago, Universidad Politécnica de Valencia, Spain |
Conference Name | 15th European Conference on Research in Computer Security (ESORICS 2010) |
Publisher | Springer |
Conference Location | Athens, Greece |
Keywords | UIUC |
Abstract | 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 sepa- rately 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 transforma- tion with respect to the extended operational semantics, and illustrate our results on some examples. |
URL | http://publish.illinois.edu/science-of-security-lablet/files/2014/06/Sequentional-Protocol-Compositi... |
Citation Key | node-23407 |
Attachment | Size |
---|---|
bytes |