Advertisement

A Survey of Name-Passing Calculi and Crypto-Primitives

  • Michele Bugliesi
  • Giuseppe Castagna
  • Silvia Crafa
  • Riccardo Forcardi
  • Vladimiro Sassone
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2946)

Abstract

The paper surveys the literature on high-level name-passing process calculi, and their extensions with cryptographic primitives. The survey is by no means exhaustive, for essentially two reasons. First, in trying to provide a coherent presentation of different ideas and techniques, one inevitably ends up leaving out the approaches that do not fit the intended roadmap. Secondly, the literature on the subject has been growing at very high rate over the years. As a consequence, we decided to concentrate on few papers that introduce the main ideas, in the hope that discussing them in some detail will provide sufficient insight for further reading.

Keywords

Type System Security Level Operational Semantic Security Protocol Typing Rule 
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.: Secrecy by typing security protocols. Journal of the ACM 46(5), 749–786 (1999)zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Abadi, M.: Security protocols and specifications. In: Thomas, W. (ed.) FOSSACS 1999. LNCS, vol. 1578, pp. 1–13. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  3. 3.
    Abadi, M., Blanchet, B.: Secrecy types for asymmetric communication. In: Honsell, F., Miculan, M. (eds.) FOSSACS 2001. LNCS, vol. 2030, pp. 25–41. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  4. 4.
    Abadi, M., Fournet, C.: Mobile values, new names and secure communication. In: Proceedings of POPL 2001, pp. 104–115. ACM Press, New York (2001)Google Scholar
  5. 5.
    Abadi, M., Gordon, A.D.: A calculus of cryptographic protocols: the spi calculus. In: Fourth ACM Conference on Computer and Communication Security, pp. 36–47 (1997)Google Scholar
  6. 6.
    Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: the spi calculus. Technical Report 149, Digital Equipment Corporation Systems Reasearch Center (January 1998)Google Scholar
  7. 7.
    Abadi, M., Fournet, C., Gonthier, G.: Secure implementation of channel abstractions. In: Proceedings of LICS 1998, July 1998, IEEE Computer Society Press, Los Alamitos (1998)Google Scholar
  8. 8.
    Abadi, M., Fournet, C., Gonthier, G.: A top-down look at a secure message. In: Pandu Rangan, C., Raman, V., Sarukkai, S. (eds.) FST TCS 1999. LNCS, vol. 1738, pp. 122–141. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  9. 9.
    Abadi, M., Fournet, C., Gonthier, G.: Authentication primitives and their compilation. In: Proceedings of POPL 2000, January 2000, pp. 302–315. ACM, New York (2000)Google Scholar
  10. 10.
    Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: The Spi calculus. Journal of Information and Computation 148(1), 1–70 (1999)zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    Boreale, M., Fournet, C., Laneve, C.: Bisimulations for the join-calculus. In: Gries, D., de Roever, W.-P. (eds.) Proceedings of PROCOMET 1998, IFIP (1998)Google Scholar
  12. 12.
    Boudol, G.: Asynchrony and the π-calculus (note). Rapport de Recherche 1702, INRIA Sophia-Antipolis (May 1992)Google Scholar
  13. 13.
    Cardelli, L., Ghelli, G., Gordon, A.D.: Secrecy and group creation. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 365–379. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  14. 14.
    Fournet, L.M.C., Laneve, C., Rḿy, D.: Implicit typing à la ML for the join-calculus. In: Proc. of the 1997 8th International Conference on Concurrency Theory, Springer, Heidelberg (1997)Google Scholar
  15. 15.
    Conchon, S.: Analyse modulaire de flot d’information pour les calculs sq́uentiels et concurrents. PhD thesis, École Polytechnique (2002)Google Scholar
  16. 16.
    Conchon, S., Le Fessant, F.: Jocaml: Mobile agents for Objective-Caml. In: First International Symposium on Agent Systems and Applications and Third International Symposium on Mobile Agents (ASA/MA 1999). Palm Springs, California (1999)Google Scholar
  17. 17.
    Conchon, S., Pottier, F.: JOIN(X): Constraint-based type inference for the join-calculus. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, pp. 221–236. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  18. 18.
    De Nicola, R., Hennessy, M.: Testing equivalences for processes. Theoretical Computer Science 34, 83–133 (1984)zbMATHCrossRefMathSciNetGoogle Scholar
  19. 19.
    Denning, D.E., Denning, P.J.: Certification of programs for secure information flow. Communications of the ACM 20, 504–513 (1977)zbMATHCrossRefGoogle Scholar
  20. 20.
    Durante, A., Focardi, R., Gorrieri, R.: A compiler for analysing cryptographic protocols using non-interference. ACM Transactions on Software Engineering and Methodology 9(4), 489–530 (2000)CrossRefGoogle Scholar
  21. 21.
    Durante, A., Focardi, R., Gorrieri, R.: CVS: A compiler for the analysis of cryptographic protocols. In: Proceedings of CSFW 1999, pp. 203–212. IEEE press, Los Alamitos (1999)Google Scholar
  22. 22.
    Durante, A., Focardi, R., Gorrieri, R.: CVS at Work: A report on new failures upon some cryptographic protocol. In: Gorodetski, V.I., Skormin, V.A., Popyack, L.J. (eds.) MMM-ACNS 2001. LNCS, vol. 2052, Springer, Heidelberg (2001)Google Scholar
  23. 23.
    Focardi, R., Ghelli, A., Gorrieri, R.: Using non interference for the analysis of security protocols. In: Proceedings of DIMACS Workshop on Design and Formal Verification of Security Protocols (1997)Google Scholar
  24. 24.
    Focardi, R., Gorrieri, R.: A classification of security properties for process algebras. Journal of Computer Security 3(1), 5–33 (1995)Google Scholar
  25. 25.
    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
  26. 26.
    Focardi, R., Gorrieri, R., Martinelli, F.: Non Interference for the Analysis of Cryptographic Protocols. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol. 1853, pp. 744–755. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  27. 27.
    Focardi, R., Martinelli, F.: A uniform approach 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
  28. 28.
    Fournet, C., Gonthier, G., Lévy, J.-J., Maranget, L., Rémy, D.: A calculus of mobile agents. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 406–421. Springer, Heidelberg (1996)Google Scholar
  29. 29.
    Fournet, C., Gonthier, G.: The reflexive chemical abstract machine and the join-calculus. In: Proceedings of the 23rd ACM Symposium on Principles of Programming Languages, St. Petersburg Beach, Florida, January 21-24, pp. 372–385. ACM, New York (1996)Google Scholar
  30. 30.
    Fournet, C., Gonthier, G., Lévy, J.-J., Maranget, L., Rémy, D.: A calculus of mobile agents. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 406–421. Springer, Heidelberg (1996)Google Scholar
  31. 31.
    Fournet, C., Gonthier, G., Lévy, J.-J., Maranget, L., Rémy, D.: A calculus of mobile agents. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 406–421. Springer, Heidelberg (1996)Google Scholar
  32. 32.
    Goguen, J.A., Meseguer, J.: Security policy and security models. In: Proceedings of Symposium on Secrecy and Privacy, April 1982, pp. 11–20. IEEE Computer Society, Los Alamitos (1982)Google Scholar
  33. 33.
    Hennessy, M., Riely, J.: Information flow vs resource access in the asynchronous π-calculus (extended abstract). In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol. 1853, pp. 415–427. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  34. 34.
    Hennessy, M., Riely, J.: Information flow vs. resource access in the asynchronous pi-calculus. Computer Science Technical Report 2000:03, School of Cognitive and Computing Sciences, University of Sussex (2000)Google Scholar
  35. 35.
    Honda, K., Vasconcelos, V.T., Yoshida, N.: Secure information flow as typed process behaviour. In: Smolka, G. (ed.) ESOP 2000. LNCS, vol. 1782, pp. 180–199. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  36. 36.
    Honda, K., Tokoro, M.: An object calculus for asynchronous communication. In: America, P. (ed.) ECOOP 1991. LNCS, vol. 512, pp. 133–147. Springer, Heidelberg (1991)CrossRefGoogle Scholar
  37. 37.
    Igarashi, A., Kobayashi, N.: A generic type system for the π-calculus. In: Proceedings of POPL 2001, pp. 128–141. ACM Press, New York (2000)Google Scholar
  38. 38.
    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. 146–166. Springer, Heidelberg (1996)Google Scholar
  39. 39.
    Marrero, W., Clarke, E., Jha, S.: A model checker for authentication protocols. In: Proc. of DIMACS Workshop on Design and Formal Verification of Security Protocols, September 1997, Rutgers University (1997)Google Scholar
  40. 40.
    Merro, M., Sangiorgi, D.: On asynchrony in name-passing calculi. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 856–867. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  41. 41.
    Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)zbMATHGoogle Scholar
  42. 42.
    Milner, R.: Sorts in the π-calculus (extended abstract). In: Best, E., Rozenberg, G. (eds.) Proceedings of the 3rd Workshop on Concurrency and Compositionality, GMD Bonn, St. Augustin. GMD-Studien, vol. 191 (1991), Also available as Report 6/91 from University of HildesheimGoogle Scholar
  43. 43.
    Milner, R.: The polyadic π-calculus: A tutorial. In: Bauer, F.L., Brauer, W., Schwichtenberg, H. (eds.) Logic and Algebra of Specification. F. NATO ASI, vol. 94. Springer, Heidelberg (1993), Available as Technical Report ECS-LFCS-91-180, University of Edinburgh (October 1991)Google Scholar
  44. 44.
    Milner, R.: The π-calculus. Undergraduate lecture notes. Cambridge University Press, Cambridge (1995)Google Scholar
  45. 45.
    Milner, R.: Communicating and Mobile Systems: the π-Calculus. Cambridge University Press, Cambridge (May 1999)Google Scholar
  46. 46.
    Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, part I/II. Journal of Information and Computation 100, 1–77 (1992)zbMATHCrossRefMathSciNetGoogle Scholar
  47. 47.
    Pierce, B., Sangiorgi, D.: Typing and subtyping for mobile processes. Mathematical Structures in Compoter Sciences 6(5), 409–454 (1996); An extended abstract in Proc. LICS, vol. 93. IEEE Computer Society Press, Los AlamitosGoogle Scholar
  48. 48.
    Focardi, R., Martinelli, F.: A uniform approach for the analysis of cryptographic protocols. In: Persiano, G. (ed.) Conference on Security in Communication Networks, SCN 1999 (1999)Google Scholar
  49. 49.
    Focardi, R., Gorrieri, R., Martinelli, F.: Secrecy in security protocols as non interference. In: Schneider, S., Ryan, P. (eds.) Proceedings of DERA/ RHULWorkshop on Secure Architectures and Information Flow. ENTCS, vol. 32. Elsevier, Amsterdam (1999)Google Scholar
  50. 50.
    Focardi, R., Gorrieri, R., Martinelli, F.: Message authentication through non interference. In: Rus, T. (ed.) AMAST 2000. LNCS, vol. 1816, pp. 258–272. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  51. 51.
    Roscoe, A.W., Woodcock, J.C.P., Wulf, L.: Non-interference through determinism. In: Gollmann, D. (ed.) ESORICS 1994. LNCS, vol. 875, pp. 33–53. Springer, Heidelberg (1994)Google Scholar
  52. 52.
    Ryan, P.Y.A., Schneider, S.A.: Process algebra and non-interference. In: Proceedings of 12th IEEE Computer Security Foundation Workshop, pp. 214–227. IEEE press, Los Alamitos (1999)CrossRefGoogle Scholar
  53. 53.
    Sabelfeld, A., Sands, D.: Probabilistic noninterference for multi-threaded programs. In: Proceedings of the 13th IEEE Computer Security Foundation Workshop, Cambridge, UK, IEEE press, Los Alamitos (2000)Google Scholar
  54. 54.
    Sangiorgi, D., Walker, D.: The π-calculus: A Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)Google Scholar
  55. 55.
    Smith, G., Volpano, D.: Secure information flow in a multi-threaded imperative language. In: Proceedings of POPL 1998, January 1988, pp. 355–364. ACM Press, New York (1988)Google Scholar
  56. 56.
    Volpano, D., Smith, G., Irvine, C.: A sound type system for secure flow analysis. Journal of Computer Security 4(3), 167–187 (1996)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Michele Bugliesi
    • 1
  • Giuseppe Castagna
    • 2
  • Silvia Crafa
    • 1
  • Riccardo Forcardi
    • 1
  • Vladimiro Sassone
    • 3
  1. 1.Università “Ca’ Foscari”Venezia
  2. 2.Ecole Normale SuperieureParis
  3. 3.University of Sussex 

Personalised recommendations