Effective sequential protocol composition in Maude-NPA

S Santiago, S Escobar, C Meadows… - arXiv preprint arXiv …, 2016 - arxiv.org
arXiv preprint arXiv:1603.00087, 2016arxiv.org
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 …
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.
arxiv.org
以上显示的是最相近的搜索结果。 查看全部搜索结果