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 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.
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.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Anlauff, M., Pavlovic, D., Waldinger, R., Westfold, S.: Proving authentication properties in the protocol derivation assistant. In: Proc. of Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis (2006)
Canetti, R., Lindell, Y., Ostrovsky, R., Sahai, A.: Universally composable two-party and multi-party secure computation. In: STOC, pp. 494–503 (2002)
Capkun, S., Hubaux, J.P.: Secure positioning in wireless networks. IEEE Journal on Selected Areas in Communication 24(2) (February 2006)
Cervesato, I., Meadows, C., Pavlovic, D.: An encapsulated authentication logic for reasoning about key establishment protocols. In: IEEE Computer Security Foundations Workshop (2005)
Cortier, V., Delaune, S.: Safely composing security protocols. Formal Methods in System Design 34(1), 1–36 (2009)
Datta, A., Derek, A., Mitchell, J.C., Pavlovic, D.: Secure protocol composition. In: Proc. Mathematical Foundations of Programming Semantics. ENTCS, vol. 83 (2003)
Desmedt, Y.: Major security problems with the “unforgeable” (Feige-)Fiat-Shamir Proofs of identity and how to overcome them. In: Securicom 88, 6th Worldwide Congress on Computer and Communications Security and Protection, Paris, France, March 1988, pp. 147–159 (1988)
Doghim, S., Guttman, J., Thayer, F.J.: Searching for Shapes in Cryptographic Protocols. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 523–537. Springer, Heidelberg (2007)
Durgin, N., Mitchell, J., Pavlovic, D.: A Compositional Logic for Program Correctness. In: Fifteenth Computer Security Foundations Workshop — CSFW-14, Cape Breton, NS, Canada, June 11-13, IEEE Computer Society Press, Los Alamitos (2001)
Escobar, S., Meadows, C., Meseguer, J.: A rewriting-based inference system for the NRL Protocol Analyzer and its meta-logical properties. Theor. Comput. Sci. 367(1-2), 162–202 (2006)
Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA: Cryptographic protocol analysis modulo equational properties. In: FOSAD 2008/2009 Tutorial Lectures, vol. 5705, pp. 1–50. Springer, Heidelberg (2009)
Escobar, S., Meadows, C., Meseguer, J., Santiago, S.: Sequential Protocol Composition in Maude-NPA. Technical Report DSIC-II/06/10, Universidad Politécnica de Valencia (June 2010)
Thayer Fabrega, F.J., Herzog, J., Guttman, J.: Strand Spaces: What Makes a Security Protocol Correct? Journal of Computer Security 7, 191–230 (1999)
Gong, L., Syverson, P.: Fail-stop protocols: An approach to designing secure protocols. In: Proc. of the 5th IFIP International Working Conference on Dependable Computing for Critical Applications, pp. 79–99. IEEE Computer Society Press, Los Alamitos (1998)
Guttman, J.: Security protocol design via authentication tests. In: Proc. Computer Security Foundations Workshop. IEEE Computer Society Press, Los Alamitos (2001)
Guttman, J.D., Herzog, J.C., Swarup, V., Thayer, F.J.: Strand spaces: From key exchange to secure location. In: Workshop on Event-Based Semantics (2008)
Guttman, J.D., Thayer, F.J.: Protocol independence through disjoint encryption. In: CSFW, pp. 24–34 (2000)
Harkins, D., Carrel, D.: The Internet Key Exchange (IKE), IETF RFC 2409 (November 1998)
Lowe, G.: Breaking and fixing the Needham-Schroeder public key protocol using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 147–166. Springer, Heidelberg (1996)
Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theor. Comput. Sci. 96(1), 73–155 (1992)
Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 18–61. Springer, Heidelberg (1998)
TeReSe (ed.): Term Rewriting Systems. Cambridge University Press, Cambridge (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Escobar, S., Meadows, C., Meseguer, J., Santiago, S. (2010). Sequential Protocol Composition in Maude-NPA. In: Gritzalis, D., Preneel, B., Theoharidou, M. (eds) Computer Security – ESORICS 2010. ESORICS 2010. Lecture Notes in Computer Science, vol 6345. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15497-3_19
Download citation
DOI: https://doi.org/10.1007/978-3-642-15497-3_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15496-6
Online ISBN: 978-3-642-15497-3
eBook Packages: Computer ScienceComputer Science (R0)