Skip to main content
SpringerLink
Log in

A Survey of Name-Passing Calculi and Crypto-Primitives

  • Conference paper
Foundations of Security Analysis and Design II (FOSAD 2001)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2946))

Included in the following conference series:

  • 251 Accesses

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.

Research supported by ‘MyThS: Models and Types for Security in Mobile Distributed Systems’, EU FET-GC IST-2001-32617.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abadi, M.: Secrecy by typing security protocols. Journal of the ACM 46(5), 749–786 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  2. Abadi, M.: Security protocols and specifications. In: Thomas, W. (ed.) FOSSACS 1999. LNCS, vol. 1578, pp. 1–13. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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. 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. 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. 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. 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)

    Chapter  Google Scholar 

  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. Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: The Spi calculus. Journal of Information and Computation 148(1), 1–70 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  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. Boudol, G.: Asynchrony and the π-calculus (note). Rapport de Recherche 1702, INRIA Sophia-Antipolis (May 1992)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  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. Conchon, S.: Analyse modulaire de flot d’information pour les calculs sq́uentiels et concurrents. PhD thesis, École Polytechnique (2002)

    Google Scholar 

  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. 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)

    Chapter  Google Scholar 

  18. De Nicola, R., Hennessy, M.: Testing equivalences for processes. Theoretical Computer Science 34, 83–133 (1984)

    Article  MATH  MathSciNet  Google Scholar 

  19. Denning, D.E., Denning, P.J.: Certification of programs for secure information flow. Communications of the ACM 20, 504–513 (1977)

    Article  MATH  Google Scholar 

  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)

    Article  Google Scholar 

  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. 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. 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. Focardi, R., Gorrieri, R.: A classification of security properties for process algebras. Journal of Computer Security 3(1), 5–33 (1995)

    Google Scholar 

  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)

    Article  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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. 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. 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. 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. 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. 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)

    Chapter  Google Scholar 

  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. 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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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. 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. 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. 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)

    Chapter  Google Scholar 

  41. Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)

    MATH  Google Scholar 

  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 Hildesheim

    Google Scholar 

  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. Milner, R.: The π-calculus. Undergraduate lecture notes. Cambridge University Press, Cambridge (1995)

    Google Scholar 

  45. Milner, R.: Communicating and Mobile Systems: the π-Calculus. Cambridge University Press, Cambridge (May 1999)

    Google Scholar 

  46. Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, part I/II. Journal of Information and Computation 100, 1–77 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  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 Alamitos

    Google Scholar 

  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. 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. 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)

    Chapter  Google Scholar 

  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. 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)

    Chapter  Google Scholar 

  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. Sangiorgi, D., Walker, D.: The π-calculus: A Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)

    Google Scholar 

  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. 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 

Download references

Author information

Authors and Affiliations

  1. Università “Ca’ Foscari”, Venezia

    Michele Bugliesi, Silvia Crafa & Riccardo Forcardi

  2. Ecole Normale Superieure, Paris

    Giuseppe Castagna

  3. University of Sussex,  

    Vladimiro Sassone

Authors
  1. Michele Bugliesi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Giuseppe Castagna
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Silvia Crafa
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Riccardo Forcardi
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Vladimiro Sassone
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dipartimento di Informatica, Università Ca’Foscari di Venezia,  

    Riccardo Focardi

  2. Dipartimento di Scienze dell’Informazione, Università di Bologna, Mura A. Zamboni, 7, 40127, Bologna, Italy

    Roberto Gorrieri

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bugliesi, M., Castagna, G., Crafa, S., Forcardi, R., Sassone, V. (2004). A Survey of Name-Passing Calculi and Crypto-Primitives. In: Focardi, R., Gorrieri, R. (eds) Foundations of Security Analysis and Design II. FOSAD 2001. Lecture Notes in Computer Science, vol 2946. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24631-2_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-24631-2_3

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-20955-3

  • Online ISBN: 978-3-540-24631-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation