Advertisement

Relating Process Algebras and Multiset Rewriting for Immediate Decryption Protocols

  • Stefano Bistarelli
  • Iliano Cervesato
  • Gabriele Lenzini
  • Fabio Martinelli
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2776)

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.

Keywords

Security Protocol Security Property Parallel Composition Process Algebra Cryptographic Protocol 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    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)CrossRefGoogle Scholar
  2. 2.
    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)Google Scholar
  3. 3.
    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)CrossRefGoogle Scholar
  4. 4.
    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
  5. 5.
    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)Google Scholar
  6. 6.
    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)Google Scholar
  7. 7.
    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)Google Scholar
  8. 8.
    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)CrossRefGoogle Scholar
  9. 9.
    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)Google Scholar
  10. 10.
    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)CrossRefGoogle Scholar
  11. 11.
    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)Google Scholar
  12. 12.
    Denker, G., Millen, J.K., Grau, A., Filipe, J.K.: Optimizing protocol rewrite rules of CIL specifications. In: CSFW, pp. 52–62 (2000)Google Scholar
  13. 13.
    Dolev, D., Yao, A.: On the security of public-key protocols. IEEE Transaction on Information Theory 29(2), 198–208 (1983)zbMATHCrossRefMathSciNetGoogle Scholar
  14. 14.
    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)Google Scholar
  15. 15.
    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)CrossRefGoogle Scholar
  16. 16.
    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)CrossRefGoogle Scholar
  17. 17.
    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)CrossRefGoogle Scholar
  18. 18.
    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)CrossRefGoogle Scholar
  19. 19.
    Meadows, C.A.: The NRL protocol analyzer: an overview. In: Proc. of the 2nd International Conference on the Practical Application of PROLOG (1994)Google Scholar
  20. 20.
    Miller, D.: Higher-order quantification and proof search. In: Proceedings of the AMAST confrerence. LNCS. Springer, Heidelberg (2002)Google Scholar
  21. 21.
    Milner, R.: Communication and Concurrency. In: International Series in Computer Science. Prentice Hall, Englewood Cliffs (1989)Google Scholar
  22. 22.
    Milner, R.: Communicating and Mobile Systems: the π-Calculus. Cambridge University Press, Cambridge (2000)Google Scholar
  23. 23.
    Milner, R., Parrow, J., Walker, D.: A Calculus of Mobile Processes, I and II. Information and Computation 100(1), 1–40 (1992)zbMATHCrossRefMathSciNetGoogle Scholar
  24. 24.
    Schneider, S.: Security properties and CSP. In: Proc. of the IEEE Symposium on Research in Security and Privacy, pp. 174–187 (1996)Google Scholar
  25. 25.
    Schneider, S.: Verifying Authentication Protocols in CSP. IEEE Transaction on Sofware Engineering 24(8), 743–758 (1998)Google Scholar
  26. 26.
    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)Google Scholar
  27. 27.
    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)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Stefano Bistarelli
    • 1
    • 2
  • Iliano Cervesato
    • 3
  • Gabriele Lenzini
    • 4
  • Fabio Martinelli
    • 1
  1. 1.Istituto di Informatica e Telematica – CNRPisaItaly
  2. 2.Dipartimento di ScienzeUniversità “D’Annunzio” di Chieti-PescaraPescaraItaly
  3. 3.Advanced Engineering and Science DivisionITT Industries Inc.AlexandriaUSA
  4. 4.Istituto di Scienza e Tecnologie dell’Informazione — CNRPisaItaly

Personalised recommendations