Advertisement

Security Protocols: Principles and Calculi

Tutorial Notes
  • Martín Abadi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, 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.

Keywords

Function Symbol Authentication Protocol Security Protocol Security Property Horn Clause 
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.: 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. 2.
    Abadi, M., Blanchet, B.: Analyzing security protocols with secrecy types and logic programs. Journal of the ACM 52(1), 102–146 (2005)CrossRefMathSciNetGoogle Scholar
  3. 3.
    Abadi, M., Blanchet, B.: Computer-assisted verification of a protocol for certified email. Science of Computer Programming 58(1-2), 3–27 (2005)zbMATHCrossRefMathSciNetGoogle Scholar
  4. 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. 5.
    Abadi, M., Cortier, V.: Deciding knowledge in security protocols under equational theories. Theoretical Computer Science 367(1-2), 2–32 (2006)zbMATHCrossRefMathSciNetGoogle Scholar
  6. 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. 7.
    Abadi, M., Fournet, C.: Private authentication. Theoretical Computer Science 322(3), 427–476 (2004)zbMATHCrossRefMathSciNetGoogle Scholar
  8. 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)CrossRefMathSciNetGoogle Scholar
  9. 9.
    Abadi, M., Needham, R.: Prudent engineering practice for cryptographic protocols. IEEE Transactions on Software Engineering 22(1), 6–15 (1996)CrossRefGoogle Scholar
  10. 10.
    Abadi, M., Rogaway, P.: Reconciling two views of cryptography (The computational soundness of formal encryption). Journal of Cryptology 15(2), 103–127 (2002)zbMATHMathSciNetGoogle Scholar
  11. 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)CrossRefGoogle Scholar
  12. 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)CrossRefGoogle Scholar
  13. 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)CrossRefGoogle Scholar
  14. 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. 15.
    Aura, T.: Strategies against replay attacks. In: 10th IEEE Computer Security Foundations Workshop, pp. 59–68 (1997)Google Scholar
  16. 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. 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. 18.
    Baudet, M.: Sécurité des protocoles cryptographiques: aspects logiques et calculatoires. PhD thesis, Ecole Normale Supérieure de Cachan (2007)Google Scholar
  19. 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. 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. 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)CrossRefGoogle Scholar
  22. 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. 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. 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)CrossRefGoogle Scholar
  25. 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. 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. 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. 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. 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)CrossRefGoogle Scholar
  30. 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. 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)zbMATHCrossRefGoogle Scholar
  32. 32.
    Bodei, C.: Security Issues in Process Calculi. PhD thesis, Università di Pisa (January 2000)Google Scholar
  33. 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. 34.
    Boreale, M., De Nicola, R., Pugliese, R.: Proof techniques for cryptographic processes. SIAM J. Comput. 31(3), 947–986 (2001)CrossRefMathSciNetGoogle Scholar
  35. 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. 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)CrossRefGoogle Scholar
  37. 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)zbMATHMathSciNetCrossRefGoogle Scholar
  38. 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. 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)CrossRefMathSciNetGoogle Scholar
  40. 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. 41.
    Denning, D.E., Sacco, G.M.: Timestamps in key distribution protocols. Communications of the ACM 24(7), 533–535 (1981)CrossRefGoogle Scholar
  42. 42.
    Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Transactions on Information Theory IT-29(12), 198–208 (1983)CrossRefMathSciNetGoogle Scholar
  43. 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. 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)CrossRefGoogle Scholar
  45. 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)CrossRefGoogle Scholar
  46. 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. 47.
    Goldwasser, S., Micali, S.: Probabilistic encryption. Journal of Computer and System Sciences 28, 270–299 (1984)zbMATHCrossRefMathSciNetGoogle Scholar
  48. 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. 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. 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. 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. 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. 53.
    Harkins, D., Carrel, D.: RFC 2409: The Internet Key Exchange (IKE) (November 1998), http://www.ietf.org/rfc/rfc2409.txt
  54. 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. 55.
    Kemmerer, R.A., Meadows, C., Millen, J.K.: Three systems for cryptographic protocol analysis. Journal of Cryptology 7(2), 79–130 (1994)zbMATHCrossRefGoogle Scholar
  56. 56.
    Kohl, J., Neuman, C.: RFC 1510: The Kerberos network authentication service (v5) (September 1993), ftp://ftp.isi.edu/in-notes/rfc1510.txt
  57. 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. 58.
    Lampson, B.W.: Protection. In: 5th Princeton Conference on Information Sciences and Systems, pp. 437–443 (1971)Google Scholar
  59. 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. 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. 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. 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. 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. 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. 65.
    Menezes, A.J., van Oorschot, P.C., Vanstone, S.A.: Handbook of Applied Cryptography. CRC Press, Boca Raton (1996)Google Scholar
  66. 66.
    Merritt, M.J.: Cryptographic Protocols. PhD thesis, Georgia Institute of Technology (February 1983)Google Scholar
  67. 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. 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. 69.
    Milner, R.: Communicating and Mobile Systems: the π-Calculus. Cambridge University Press, Cambridge (1999)Google Scholar
  70. 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. 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. 72.
    Monniaux, D.: Abstracting cryptographic protocols with tree automata. Science of Computer Programming 47(2-3), 177–202 (2003)zbMATHCrossRefMathSciNetGoogle Scholar
  73. 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. 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)zbMATHCrossRefGoogle Scholar
  75. 75.
    Needham, R.M., Schroeder, M.D.: Authentication revisited. Operating Systems Review 21(1), 7 (1987)CrossRefGoogle Scholar
  76. 76.
    Paulson, L.C.: The inductive approach to verifying cryptographic protocols. Journal of Computer Security 6(1-2), 85–128 (1998)Google Scholar
  77. 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. 78.
    Schneider, S.: Security properties and CSP. In: 1996 IEEE Symposium on Security and Privacy, pp. 174–187 (1996)Google Scholar
  79. 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. 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. 81.
    Woo, T.Y.C., Lam, S.S.: Authentication for distributed systems. Computer 25(1), 39–52 (1992)CrossRefGoogle Scholar
  82. 82.
    Woo, T.Y.C., Lam, S.S.: A lesson on authentication protocol design. Operating Systems Review 28(3), 24–37 (1994)CrossRefGoogle Scholar
  83. 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

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • Martín Abadi
    • 1
  1. 1.Microsoft Research, and University of California, Santa Cruz 

Personalised recommendations