TY - GEN
T1 - Sequential protocol composition in Maude-NPA
AU - Escobar, Santiago
AU - Meadows, Catherine
AU - Meseguer, José
AU - Santiago, Sonia
N1 - Funding Information:
S. Escobar and S. Santiago have been partially supported by the EU (FEDER) and the Spanish MEC/MICINN under grant TIN 2007-68093-C02-02. J. Meseguer has been supported by NSF Grants CNS 07-16638 and CNS 09-04749.
PY - 2010
Y1 - 2010
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=78049354833&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=78049354833&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-15497-3_19
DO - 10.1007/978-3-642-15497-3_19
M3 - Conference contribution
AN - SCOPUS:78049354833
SN - 3642154964
SN - 9783642154966
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 303
EP - 318
BT - Computer Security, ESORICS 2010 - 15th European Symposium on Research in Computer Security, Proceedings
PB - Springer
T2 - 15th European Symposium on Research in Computer Security, ESORICS 2010
Y2 - 20 September 2010 through 22 September 2010
ER -