Skip to main content
SpringerLink
Log in
Book cover

International School on Foundations of Security Analysis and Design

International School on Foundations of Security Analysis and Design

FOSAD 2007, FOSAD 2006: Foundations of Security Analysis and Design IV pp 1–23Cite as

Security Protocols: Principles and Calculi

Tutorial Notes

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNSC,volume 4677))

Abstract

This paper is a basic introduction to some of the main themes in the design and analysis of security protocols. It includes a brief explanation of the principles of protocol design and of a formalism for protocol analysis. It is intended as a written counterpart to a tutorial given at the 2006 International School on Foundations of Security Analysis and Design.

This is a preview of subscription content, 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abadi, M.: Security protocols: Principles and calculi. Lectures at 6th International School on Foundations of Security Analysis and Design (September 2006), Slides at http://www.sti.uniurb.it/events/fosad06/papers/Abadi-fosad06.pdf

  2. Abadi, M., Blanchet, B.: Analyzing security protocols with secrecy types and logic programs. Journal of the ACM 52(1), 102–146 (2005)

    Article  MathSciNet  Google Scholar 

  3. Abadi, M., Blanchet, B.: Computer-assisted verification of a protocol for certified email. Science of Computer Programming 58(1-2), 3–27 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  4. Abadi, M., Blanchet, B., Fournet, C.: Just Fast Keying in the pi calculus. ACM Transactions on Information and System Security (to appear, 2007)

    Google Scholar 

  5. Abadi, M., Cortier, V.: Deciding knowledge in security protocols under equational theories. Theoretical Computer Science 367(1-2), 2–32 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  6. Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: 28th ACM Symposium on Principles of Programming Languages (POPL 2001), pp. 104–115 (January 2001)

    Google Scholar 

  7. Abadi, M., Fournet, C.: Private authentication. Theoretical Computer Science 322(3), 427–476 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  8. Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: The spi calculus (An extended version appeared as Digital Equipment Corporation Systems Research Center report No. 149, January 1998). Information and Computation 148(1), 1–70 (1998)

    Article  MathSciNet  Google Scholar 

  9. Abadi, M., Needham, R.: Prudent engineering practice for cryptographic protocols. IEEE Transactions on Software Engineering 22(1), 6–15 (1996)

    Article  Google Scholar 

  10. Abadi, M., Rogaway, P.: Reconciling two views of cryptography (The computational soundness of formal encryption). Journal of Cryptology 15(2), 103–127 (2002)

    MATH  MathSciNet  Google Scholar 

  11. Aiello, W., Bellovin, S.M., Blaze, M., Canetti, R., Ioannidis, J., Keromytis, A.D., Reingold, O.: Just Fast Keying: Key agreement in a hostile internet. ACM Transactions on Information and System Security 7(2), 242–273 (2004)

    Article  Google Scholar 

  12. Amadio, R., Lugiez, D.: On the reachability problem in cryptographic protocols. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 380–395. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  13. Amadio, R., Prasad, S.: The game of the name in cryptographic tables. In: Thiagarajan, P.S., Yap, R.H.C. (eds.) ASIAN 1999. LNCS, vol. 1742, pp. 15–27. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  14. Anderson, R., Needham, R.: Robustness principles for public key protocols. In: Coppersmith, D. (ed.) CRYPTO 1995. LNCS, vol. 963, pp. 236–247. Springer, Heidelberg (1995)

    Google Scholar 

  15. Aura, T.: Strategies against replay attacks. In: 10th IEEE Computer Security Foundations Workshop, pp. 59–68 (1997)

    Google Scholar 

  16. Backes, M., Pfitzmann, B., Waidner, M.: A composable cryptographic library with nested operations. In: 10th ACM conference on Computer and Communications security (CCS 2003), pp. 220–230 (October 2003)

    Google Scholar 

  17. Baldamus, M., Parrow, J., Victor, B.: Spi calculus translated to pi-calculus preserving may-tests. In: 19th Annual IEEE Symposium on Logic in Computer Science (LICS 2004), pp. 22–31 (July 2004)

    Google Scholar 

  18. Baudet, M.: Sécurité des protocoles cryptographiques: aspects logiques et calculatoires. PhD thesis, Ecole Normale Supérieure de Cachan (2007)

    Google Scholar 

  19. Bellare, M., Rogaway, P.: Entity authentication and key distribution. In: Stinson, D.R. (ed.) CRYPTO 1993. LNCS, vol. 773, pp. 232–249. Springer, Heidelberg (1994)

    Google Scholar 

  20. Bhargavan, K., Fournet, C., Gordon, A.D.: Verifying policy-based security for web services. In: ACM Conference on Computer and Communications Security (CCS 2004), pp. 268–277 (October 2004)

    Google Scholar 

  21. Bhargavan, K., Fournet, C., Gordon, A.D.: Verified reference implementations of WS-security protocols. In: Bravetti, M., Núñez, M., Zavattaro, G. (eds.) WS-FM 2006. LNCS, vol. 4184, pp. 88–106. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  22. Bhargavan, K., Fournet, C., Gordon, A.D., Pucella, R.: TulaFale: A security tool for web services. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2003. LNCS, vol. 3188, pp. 197–222. Springer, Heidelberg (2004)

    Google Scholar 

  23. Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: 14th IEEE Computer Security Foundations Workshop, pp. 82–96 (June 2001)

    Google Scholar 

  24. Blanchet, B.: From secrecy to authenticity in security protocols. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 342–359. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  25. Blanchet, B.: Automatic proof of strong secrecy for security protocols. In: 2004 IEEE Symposium on Security and Privacy, pp. 86–100 (May 2004)

    Google Scholar 

  26. Blanchet, B.: A computationally sound mechanized prover for security protocols. In: 2006 IEEE Symposium on Security and Privacy, pp. 140–154 (May 2006)

    Google Scholar 

  27. Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. Journal of Logic and Algebraic Programming (to appear, 2007)

    Google Scholar 

  28. Blanchet, B., Podelski, A.: Verification of cryptographic protocols: Tagging enforces termination. In: Gordon, A.D. (ed.) ETAPS 2003 and FOSSACS 2003. LNCS, vol. 2620, pp. 136–152. Springer, Heidelberg (2003)

    Google Scholar 

  29. Blanchet, B., Pointcheval, D.: Automated security proofs with sequences of games. In: Dwork, C. (ed.) CRYPTO 2006. LNCS, vol. 4117, pp. 537–554. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  30. Blum, M., Micali, S.: How to generate cryptographically strong sequences of pseudo random bits. In: 23rd Annual Symposium on Foundations of Computer Science (FOCS 1982), pp. 112–117 (1982)

    Google Scholar 

  31. Bodei, C., Degano, P., Nielson, F., Nielson, H.: Flow logic for Dolev-Yao secrecy in cryptographic processes. Future Generation Computer Systems 18(6), 747–756 (2002)

    Article  MATH  Google Scholar 

  32. Bodei, C.: Security Issues in Process Calculi. PhD thesis, Università di Pisa (January 2000)

    Google Scholar 

  33. Bolignano, D.: Towards a mechanization of cryptographic protocol verification. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 131–142. Springer, Heidelberg (1997)

    Google Scholar 

  34. Boreale, M., De Nicola, R., Pugliese, R.: Proof techniques for cryptographic processes. SIAM J. Comput. 31(3), 947–986 (2001)

    Article  MathSciNet  Google Scholar 

  35. Borgström, J., Briais, S., Nestmann, U.: Symbolic bisimulation in the spi calculus. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 161–176. Springer, Heidelberg (2004)

    Google Scholar 

  36. Borgström, J., Nestmann, U.: On bisimulations for the spi calculus. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol. 2422, pp. 287–303. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  37. Burrows, M., Abadi, M., Needham, R.: A logic of authentication (A preliminary version appeared as Digital Equipment Corporation Systems Research Center report No. 39, February 1989). Proceedings of the Royal Society of London A 426, 233–271 (1989)

    Article  MATH  MathSciNet  Google Scholar 

  38. Datta, A., Derek, A., Mitchell, J.C., Pavlovic, D.: A derivation system and compositional logic for security protocols. Journal of Computer Security 13(3), 423–482 (2005)

    Google Scholar 

  39. Datta, A., Derek, A., Mitchell, J.C., Roy, A.: Protocol composition logic (PCL). Electronic Notes in Theoretical Computer Science 172(1), 311–358 (2007)

    Article  MathSciNet  Google Scholar 

  40. DeMillo, R.A., Lynch, N.A., Merritt, M.: Cryptographic protocols. In: 14th Annual ACM Symposium on Theory of Computing, pp. 383–400 (1982)

    Google Scholar 

  41. Denning, D.E., Sacco, G.M.: Timestamps in key distribution protocols. Communications of the ACM 24(7), 533–535 (1981)

    Article  Google Scholar 

  42. Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Transactions on Information Theory IT-29(12), 198–208 (1983)

    Article  MathSciNet  Google Scholar 

  43. Durante, L., Sisto, R., Valenzano, A.: A state-exploration technique for spi-calculus testing-equivalence verification. In: Formal Techniques for Distributed System Development, FORTE/PSTV. IFIP Conference Proceedings, vol. 183, pp. 155–170. Kluwer, Dordrecht (2000)

    Google Scholar 

  44. Durante, L., Sisto, R., Valenzano, A.: Automatic testing equivalence verification of spi calculus specifications. ACM Transactions on Software Engineering and Methodology 12(2), 222–284 (2003)

    Article  Google Scholar 

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

  46. Freier, A.O., Karlton, P., Kocher, P.C.: The SSL protocol: Version 3.0 (November 1996), http://www.mozilla.org/projects/security/pki/nss/ssl/draft302.txt

  47. Goldwasser, S., Micali, S.: Probabilistic encryption. Journal of Computer and System Sciences 28, 270–299 (1984)

    Article  MATH  MathSciNet  Google Scholar 

  48. Gordon, A.D.: Provable implementations of security protocols. In: 21st Annual IEEE Symposium on Logic in Computer Science (LICS 2006), pp. 345–346 (2006)

    Google Scholar 

  49. Gordon, A.D., Jeffrey, A.: Authenticity by typing for security protocols. In: 14th IEEE Computer Security Foundations Workshop, pp. 145–159 (June 2001)

    Google Scholar 

  50. Gordon, A.D., Jeffrey, A.: Types and effects for asymmetric cryptographic protocols. In: 15th IEEE Computer Security Foundations Workshop, pp. 77–91 (June 2002)

    Google Scholar 

  51. Goubault-Larrecq, J., Parrennes, F.: Cryptographic protocol analysis on real C code. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 363–379. Springer, Heidelberg (2005)

    Google Scholar 

  52. Gray III, J.W., Ip, K.F.E., Lui, K.-S.: Provable security for cryptographic protocols—exact analysis and engineering applications. In: 10th IEEE Computer Security Foundations Workshop, pp. 45–58 (1997)

    Google Scholar 

  53. Harkins, D., Carrel, D.: RFC 2409: The Internet Key Exchange (IKE) (November 1998), http://www.ietf.org/rfc/rfc2409.txt

  54. Hüttel, H.: Deciding framed bisimilarity. In: 4th International Workshop on Verification of Infinite-State Systems (INFINITY 2002), pp. 1–20 (August 2002)

    Google Scholar 

  55. Kemmerer, R.A., Meadows, C., Millen, J.K.: Three systems for cryptographic protocol analysis. Journal of Cryptology 7(2), 79–130 (1994)

    Article  MATH  Google Scholar 

  56. Kohl, J., Neuman, C.: RFC 1510: The Kerberos network authentication service (v5) (September 1993), ftp://ftp.isi.edu/in-notes/rfc1510.txt

  57. Kremer, S., Ryan, M.D.: Analysis of an electronic voting protocol in the applied pi calculus. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 186–200. Springer, Heidelberg (2005)

    Google Scholar 

  58. Lampson, B.W.: Protection. In: 5th Princeton Conference on Information Sciences and Systems, pp. 437–443 (1971)

    Google Scholar 

  59. Laud, P.: Symmetric encryption in automatic analyses for confidentiality against active adversaries. In: 2004 IEEE Symposium on Security and Privacy, pp. 71–85 (May 2004)

    Google Scholar 

  60. Laud, P.: Secrecy types for a simulatable cryptographic library. In: 12th ACM Conference on Computer and Communications Security (CCS 2005), pp. 26–35 (November 2005)

    Google Scholar 

  61. Lincoln, P., Mitchell, J., Mitchell, M., Scedrov, A.: A probabilistic poly-time framework for protocol analysis. In: 5th ACM Conference on Computer and Communications Security (CCS 1998), pp. 112–121 (1998)

    Google Scholar 

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

    Google Scholar 

  63. Lux, K.D., May, M.J., Bhattad, N.L., Gunter, C.A.: WSEmail: Secure internet messaging based on web services. In: ICWS 2005: Proceedings of the IEEE International Conference on Web Services, pp. 75–82 (2005)

    Google Scholar 

  64. Lynch, N.: I/O automaton models and proofs for shared-key communication systems. In: 12th IEEE Computer Security Foundations Workshop, pp. 14–29 (1999)

    Google Scholar 

  65. Menezes, A.J., van Oorschot, P.C., Vanstone, S.A.: Handbook of Applied Cryptography. CRC Press, Boca Raton (1996)

    Google Scholar 

  66. Merritt, M.J.: Cryptographic Protocols. PhD thesis, Georgia Institute of Technology (February 1983)

    Google Scholar 

  67. Micciancio, D., Warinschi, B.: Soundness of formal encryption in the presence of active adversaries. In: Naor, M. (ed.) TCC 2004. LNCS, vol. 2951, pp. 133–151. Springer, Heidelberg (2004)

    Google Scholar 

  68. Miller, S.P., Neuman, B.C., Schiller, J.I., Saltzer, J.H.: Kerberos authentication and authorization system, Project Athena technical plan, section E.2.1. Technical report. MIT (July 1987)

    Google Scholar 

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

    Google Scholar 

  70. Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, parts I and II. Information and Computation, 100, 1–40, 41–77 (1992)

    Google Scholar 

  71. Mitchell, J.C., Shmatikov, V., Stern, U.: Finite-state analysis of SSL 3.0. In: 7th USENIX Security Symposium, pp. 201–216 (January 1998)

    Google Scholar 

  72. Monniaux, D.: Abstracting cryptographic protocols with tree automata. Science of Computer Programming 47(2-3), 177–202 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  73. Needham, R.M.: Logic and over-simplification. In: 13th Annual IEEE Symposium on Logic in Computer Science, pp. 2–3 (1998)

    Google Scholar 

  74. Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Communications of the ACM 21(12), 993–999 (1978)

    Article  MATH  Google Scholar 

  75. Needham, R.M., Schroeder, M.D.: Authentication revisited. Operating Systems Review 21(1), 7 (1987)

    Article  Google Scholar 

  76. Paulson, L.C.: The inductive approach to verifying cryptographic protocols. Journal of Computer Security 6(1-2), 85–128 (1998)

    Google Scholar 

  77. Ramanathan, A., Mitchell, J., Scedrov, A., Teague, V.: Probabilistic bisimulation and equivalence for security analysis of network protocols. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol. 2987, pp. 468–483. Springer, Heidelberg (2004)

    Google Scholar 

  78. Schneider, S.: Security properties and CSP. In: 1996 IEEE Symposium on Security and Privacy, pp. 174–187 (1996)

    Google Scholar 

  79. Syverson, P.: Limitations on design principles for public key protocols. In: 1996 IEEE Symposium on Security and Privacy, pp. 62–73 (1996)

    Google Scholar 

  80. Javier Thayer Fábrega, F., Herzog, J.C., Guttman, J.D.: Strand spaces: Why is a security protocol correct? In: 1998 IEEE Symposium on Security and Privacy, pp. 160–171 (May 1998)

    Google Scholar 

  81. Woo, T.Y.C., Lam, S.S.: Authentication for distributed systems. Computer 25(1), 39–52 (1992)

    Article  Google Scholar 

  82. Woo, T.Y.C., Lam, S.S.: A lesson on authentication protocol design. Operating Systems Review 28(3), 24–37 (1994)

    Article  Google Scholar 

  83. Yao, A.C.: Theory and applications of trapdoor functions. In: 23rd Annual Symposium on Foundations of Computer Science (FOCS 1982), pp. 80–91 (1982)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Microsoft Research, and University of California, Santa Cruz,  

    Martín Abadi

Authors
  1. Martín Abadi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Alessandro Aldini Roberto Gorrieri

Rights and permissions

Reprints and permissions

Copyright information

© 2007 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Abadi, M. (2007). Security Protocols: Principles and Calculi. In: Aldini, A., Gorrieri, R. (eds) Foundations of Security Analysis and Design IV. FOSAD FOSAD 2007 2006. Lecture Notes in Computer Science, vol 4677. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74810-6_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-74810-6_1

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-74809-0

  • Online ISBN: 978-3-540-74810-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation