Abstract
When formalizing security protocols, different specification languages support very different reasoning methodologies, whose results are not directly or easily comparable. Therefore, establishing clear mappings among different frameworks is highly desirable, as it permits various methodologies to cooperate by interpreting theoretical and practical results of one system in another. In this paper, we examine the non-trivial relationship between two general verification frameworks: multiset rewriting (MSR) and a process algebra (PA) inspired to CCS and the π-calculus. Although defining a simple and general bijection between MSR and PA appears difficult, we show that the sublanguages needed to specify a large class of cryptographic protocols (immediate decryption protocols) admits an effective translation that is not only bijective and trace-preserving, but also induces a weak form of bisimulation across the two languages. In particular, the correspondence sketched in this abstract permits transferring several important trace-based properties such as secrecy and many forms of authentication.
Bistarelli was partially supported by MIUR project “Constraint Based Verification of Reactive Systems” (COVER), and by the MIUR project “Network Aware Programming: Object, Languages, Implementation” (NAPOLI). Cervesato was partially supported by NRL under contract N00173-00-C-2086. Lenzini was supported by the MIUR-CNR Project SP4. Martinelli was partially supported by MIUR project “Constraint Based Verification of Reactive Systems” (COVER), by MIUR project “MEFISTO”, by Microsoft Research and by the CSP project “SeTAPS II”.
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
Abadi, M., Blanchet, B.: Analyzing Security Protocols with Secrecy Types and Logic Programs. ACM SIGPLAN Notices 31(1), 33–44 (2002); Proc. of the 29th ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages (POPL 2002)
Abadi, M., Gordon, A.D.: Reasoning about Cryptographic Protocols in the Spi Calculus. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 59–73. Springer, Heidelberg (1997)
Abadi, M., Gordon, A.D.: A Bisimulation Methods for Cryptographic Protocols. In: Hankin, C. (ed.) ESOP 1998. LNCS, vol. 1381, p. 12. Springer, Heidelberg (1998)
Bistarelli, S., Cervesato, I., Lenzini, G., Martinelli, F.: Relating multiset rewriting and process algebras for security protocol analysis. Technical report, ISTI-CNR (2003), available at http://matrix.iei.pi.cnr.it/lenzini/pub/msr.ps
Bistarelli, S., Cervesato, I., Lenzini, G., Martinelli, F.: Relating Process Algebras and Multiset Rewriting for Security Protocol Analysis. In: Gorrieri, R. (ed.) Third Workshop on Issues in the Theory of Security — WITS 2003, Warsaw, Poland (2003)
Burrows, M., Abadi, M., Needham, R.: A logic of authentication. In: Houbak, N. (ed.) SIL - a Simulation Language. LNCS, vol. 426, pp. 233–271. Springer, Heidelberg (1989)
Cervesato, I., Durgin, N.A., Lincoln, P.D., Mitchell, J.C., Scedrov, A.: A Meta- Notation for Protocol Analysis. In: Proc. of the 12th IEEE Computer Security Foundations Workshop (CSFW 1999). IEEE Computer Society Press, Los Alamitos (1999)
Cervesato, I., Durgin, N.A., Lincoln, P.D., Mitchell, J.C., Scedrov, A.: Relating strands and multiset rewriting for security protocol analysis. In: Proc. of the 13th IEEE Computer Security Foundations Workshop (CSFW 2000), pp. 35–51. IEEE, Los Alamitos (2000)
Clarke, E.M., Jha, S., Marrero, W.: A Machine Checkable Logic of Knowledge for Protocols. In: Proc. of Workshop on Formal Methods and Security Protocols (1998)
Crazzolara, F., Winskel, G.: Events in security protocols. In: Proceedings of the 8th ACM conference on Computer and Communications Security, pp. 96–105. ACM Press, New York (2001)
Denker, G., Millen, J.: Capsl integrated protocol environment. In: Proc. of DARPA Information Survivability Conference (DISCEX 2000), pp. 207–221. IEEE Computer Society, Los Alamitos (2000)
Denker, G., Millen, J.K., Grau, A., Filipe, J.K.: Optimizing protocol rewrite rules of CIL specifications. In: CSFW, pp. 52–62 (2000)
Dolev, D., Yao, A.: On the security of public-key protocols. IEEE Transaction on Information Theory 29(2), 198–208 (1983)
Fiore, M., Abadi, M.: Computing Symbolic Models for Verifying Cryptographic Protocols. In: Proc. of the 14th Computer Security Foundation Workshop (CSFW- 14), pp. 160–173. IEEE Computer Society Press, Los Alamitos (2001)
Focardi, R., Gorrieri, R.: The Compositional Security Checker: A tool for the Verification of Information Flow Security Properties. IEEE Transactions on Software Engineering 23(9), 550–571 (1997)
Focardi, R., Gorrieri, R., Martinelli, F.: NonInterference for the Analysis of Cryyptographic Protocols. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol. 1853, p. 354. Springer, Heidelberg (2000)
Focardi, R., Martinelli, F.: A Uniform Approch for the Definition of Security Properties. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 794–813. Springer, Heidelberg (1999)
Gordon, A.D., Jeffrey, A.: Authenticity by Typing for Security Protocols. In: Proc. 14th IEEE Computer Security Foundations Workshop (CSFW 2001), pp. 145–159. IEEE Computer Society, Los Alamitos (2001)
Meadows, C.A.: The NRL protocol analyzer: an overview. In: Proc. of the 2nd International Conference on the Practical Application of PROLOG (1994)
Miller, D.: Higher-order quantification and proof search. In: Proceedings of the AMAST confrerence. LNCS. Springer, Heidelberg (2002)
Milner, R.: Communication and Concurrency. In: International Series in Computer Science. Prentice Hall, Englewood Cliffs (1989)
Milner, R.: Communicating and Mobile Systems: the π-Calculus. Cambridge University Press, Cambridge (2000)
Milner, R., Parrow, J., Walker, D.: A Calculus of Mobile Processes, I and II. Information and Computation 100(1), 1–40 (1992)
Schneider, S.: Security properties and CSP. In: Proc. of the IEEE Symposium on Research in Security and Privacy, pp. 174–187 (1996)
Schneider, S.: Verifying Authentication Protocols in CSP. IEEE Transaction on Sofware Engineering 24(8), 743–758 (1998)
Thayer, J., Herzog, J., Guttman, J.: Honest ideals on strand spaces. In: Proc of the 11th IEEE Computer Security Foundations Workshop (CSFW 1998), Washington,Brussels, Tokyo, pp. 66–78. IEEE, Los Alamitos (1998)
Thayer, J., Herzog, J., Guttman, J.: Strand spaces: Why is a security protocol correct?. In: Proc. of the 19th IEEE Computer Society Symposium on Research in Security and Privacy (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bistarelli, S., Cervesato, I., Lenzini, G., Martinelli, F. (2003). Relating Process Algebras and Multiset Rewriting for Immediate Decryption Protocols. In: Gorodetsky, V., Popyack, L., Skormin, V. (eds) Computer Network Security. MMM-ACNS 2003. Lecture Notes in Computer Science, vol 2776. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45215-7_7
Download citation
DOI: https://doi.org/10.1007/978-3-540-45215-7_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40797-3
Online ISBN: 978-3-540-45215-7
eBook Packages: Springer Book Archive