Abstract
Based on a concise domain analysis we develop a formal semantics of security protocols. Its main virtue is that it is a generic model, in the sense that it is parameterized over e.g. the intruder model. Further characteristics of the model are a straightforward handling of parallel execution of multiple protocols, locality of security claims, the binding of local constants to role instances, and explicitly defined initial intruder knowledge. We validate our framework by analysing the Needham-Schroeder-Lowe protocol.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Commun. ACM 21, 993–999 (1978)
Burrows, M., Abadi, M., Needham, R.: A logic of authentication. ACM Transactions on Computer Systems 8, 18–36 (1990)
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)
Mauw, S., Wiersma, W.T., Willemse, T.A.C.: Language-driven system design. International Journal of Software Engineering and Knowledge Engineering (2004) (to appear)
Dolev, D., Yao, A.: On the security of public key protocols. IEEE Transactions on Information Theory IT-29, 198–208 (1983)
Engels, A.G., Mauw, S., Reniers, M.A.: A hierarchy of communication models for Message Sequence Charts. Science of Computer Programming 44, 253–292 (2002)
Plotkin, G.: A structural approach to operational semantics. Technical Report DIAMI FN-19, Computer Science Department, Aarhus University (1981)
Cremers, C., Mauw, S., de Vink, E.: Defining authentication in a trace model. In: Dimitrakos, T., Martinelli, F., eds.: FAST 2003, Proceedings of the first international Workshop on Formal Aspects in Security and Trust, Pisa, IITT-CNR technical report, 131–145 (2003)
Roscoe, A.W.: Intensional Specifications of Security Protocols. In: Proc. 9th Computer Security Foundations Workshop, pp. 28–38. IEEE, Los Alamitos (1996)
Lowe, G.: Casper: A compiler for the analysis of security protocols. In: Proc. 10th Computer Security Foundations Workshop, pp. 18–30. IEEE, Los Alamitos (1997)
Lowe, G.: A hierarchy of authentication specifications. In: Proc. 10th Computer Security Foundations Workshop, pp. 31–44. IEEE, Los Alamitos (1997)
Thayer Fábrega, F., Herzog, J., Guttman, J.: Strand spaces: Why is a security protocol correct? In: Proc. 1998 IEEE Symposium on Security and Privacy, Oakland, California, pp. 66–77 (1998)
Abadi, M., Gordon, A.: A calculus for cryptographic protocols: The spi calculus. Inf. Comput. 148, 1–70 (1999)
Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, i. Inf. Comput. 100, 1–40 (1992)
Bodei, C., Degano, P., Focardi, R., Priami, C.: Primitives for authentication in process algebras. Theor. Comput. Sci. 283, 271–304 (2002)
Martinelli, F.: Analysis of security protocols as open systems. Theor. Comput. Sci. 290, 1057–1106 (2003)
Cremers, C., Mauw, S.: Checking secrecy by means of partial order reduction. In: Amyot, D., Williams, A.W. (eds.) SAM 2004. LNCS, vol. 3319, pp. 177–194. Springer, Heidelberg (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cremers, C., Mauw, S. (2005). Operational Semantics of Security Protocols. In: Leue, S., Systä, T.J. (eds) Scenarios: Models, Transformations and Tools. Lecture Notes in Computer Science, vol 3466. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11495628_4
Download citation
DOI: https://doi.org/10.1007/11495628_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-26189-6
Online ISBN: 978-3-540-32032-6
eBook Packages: Computer ScienceComputer Science (R0)