Paper Info
Title
Effective Sequential Protocol Composition in Maude-NPA.
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 its 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, as well as improving, in terms of both performance and ease of specification, on an earlier composition extension we presented in [18]. We show how compositions can be defined and executed symbolically in Maude-NPA using the compositional syntax and semantics. We also provide an experimental analysis of the performance of Maude-NPA using the compositional syntax and semantics, and compare it to the performance of a syntax and semantics for composition developed in earlier research. Finally, in the conclusion we give some lessons learned about the best ways of extending narrowing-based state reachability tools, as well as comparison with related work and future plans.
Year
Venue
Field
2016
arXiv: Cryptography and Security
Operational semantics,Programming language,Cryptographic protocol,Computer science,Theoretical computer science,Reachability,Syntax,Semantics
DocType
Volume
Citations 
Journal
abs/1603.00087
2
PageRank 
References 
Authors
0.38
16
4
Name
Order
Citations
PageRank
S. Santiago1544.45
Santiago Escobar2435.08
Catherine Meadows392889.05
José Meseguer49533805.39