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 thesis, we discuss an extension to the current syntax and operational semantics of the Maude-NPA, a protocol specification and analysis tool, 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 without any modification to the tool. We prove soundness and completeness of the protocol transformation with respect to the extended operational semantics, for protocol composition. Finally, we illustrate our work on some examples of protocol composition and provide some experimental results.