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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
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
Abadi, M., Blanchet, B.: Analyzing security protocols with secrecy types and logic programs. Journal of the ACM 52(1), 102–146 (2005)
Abadi, M., Blanchet, B.: Computer-assisted verification of a protocol for certified email. Science of Computer Programming 58(1-2), 3–27 (2005)
Abadi, M., Blanchet, B., Fournet, C.: Just Fast Keying in the pi calculus. ACM Transactions on Information and System Security (to appear, 2007)
Abadi, M., Cortier, V.: Deciding knowledge in security protocols under equational theories. Theoretical Computer Science 367(1-2), 2–32 (2006)
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)
Abadi, M., Fournet, C.: Private authentication. Theoretical Computer Science 322(3), 427–476 (2004)
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)
Abadi, M., Needham, R.: Prudent engineering practice for cryptographic protocols. IEEE Transactions on Software Engineering 22(1), 6–15 (1996)
Abadi, M., Rogaway, P.: Reconciling two views of cryptography (The computational soundness of formal encryption). Journal of Cryptology 15(2), 103–127 (2002)
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)
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)
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)
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)
Aura, T.: Strategies against replay attacks. In: 10th IEEE Computer Security Foundations Workshop, pp. 59–68 (1997)
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)
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)
Baudet, M.: Sécurité des protocoles cryptographiques: aspects logiques et calculatoires. PhD thesis, Ecole Normale Supérieure de Cachan (2007)
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)
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)
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)
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)
Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: 14th IEEE Computer Security Foundations Workshop, pp. 82–96 (June 2001)
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)
Blanchet, B.: Automatic proof of strong secrecy for security protocols. In: 2004 IEEE Symposium on Security and Privacy, pp. 86–100 (May 2004)
Blanchet, B.: A computationally sound mechanized prover for security protocols. In: 2006 IEEE Symposium on Security and Privacy, pp. 140–154 (May 2006)
Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. Journal of Logic and Algebraic Programming (to appear, 2007)
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)
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)
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)
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)
Bodei, C.: Security Issues in Process Calculi. PhD thesis, Università di Pisa (January 2000)
Bolignano, D.: Towards a mechanization of cryptographic protocol verification. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 131–142. Springer, Heidelberg (1997)
Boreale, M., De Nicola, R., Pugliese, R.: Proof techniques for cryptographic processes. SIAM J. Comput. 31(3), 947–986 (2001)
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)
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)
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)
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)
Datta, A., Derek, A., Mitchell, J.C., Roy, A.: Protocol composition logic (PCL). Electronic Notes in Theoretical Computer Science 172(1), 311–358 (2007)
DeMillo, R.A., Lynch, N.A., Merritt, M.: Cryptographic protocols. In: 14th Annual ACM Symposium on Theory of Computing, pp. 383–400 (1982)
Denning, D.E., Sacco, G.M.: Timestamps in key distribution protocols. Communications of the ACM 24(7), 533–535 (1981)
Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Transactions on Information Theory IT-29(12), 198–208 (1983)
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)
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)
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)
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
Goldwasser, S., Micali, S.: Probabilistic encryption. Journal of Computer and System Sciences 28, 270–299 (1984)
Gordon, A.D.: Provable implementations of security protocols. In: 21st Annual IEEE Symposium on Logic in Computer Science (LICS 2006), pp. 345–346 (2006)
Gordon, A.D., Jeffrey, A.: Authenticity by typing for security protocols. In: 14th IEEE Computer Security Foundations Workshop, pp. 145–159 (June 2001)
Gordon, A.D., Jeffrey, A.: Types and effects for asymmetric cryptographic protocols. In: 15th IEEE Computer Security Foundations Workshop, pp. 77–91 (June 2002)
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)
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)
Harkins, D., Carrel, D.: RFC 2409: The Internet Key Exchange (IKE) (November 1998), http://www.ietf.org/rfc/rfc2409.txt
Hüttel, H.: Deciding framed bisimilarity. In: 4th International Workshop on Verification of Infinite-State Systems (INFINITY 2002), pp. 1–20 (August 2002)
Kemmerer, R.A., Meadows, C., Millen, J.K.: Three systems for cryptographic protocol analysis. Journal of Cryptology 7(2), 79–130 (1994)
Kohl, J., Neuman, C.: RFC 1510: The Kerberos network authentication service (v5) (September 1993), ftp://ftp.isi.edu/in-notes/rfc1510.txt
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)
Lampson, B.W.: Protection. In: 5th Princeton Conference on Information Sciences and Systems, pp. 437–443 (1971)
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)
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)
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)
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)
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)
Lynch, N.: I/O automaton models and proofs for shared-key communication systems. In: 12th IEEE Computer Security Foundations Workshop, pp. 14–29 (1999)
Menezes, A.J., van Oorschot, P.C., Vanstone, S.A.: Handbook of Applied Cryptography. CRC Press, Boca Raton (1996)
Merritt, M.J.: Cryptographic Protocols. PhD thesis, Georgia Institute of Technology (February 1983)
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)
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)
Milner, R.: Communicating and Mobile Systems: the π-Calculus. Cambridge University Press, Cambridge (1999)
Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, parts I and II. Information and Computation, 100, 1–40, 41–77 (1992)
Mitchell, J.C., Shmatikov, V., Stern, U.: Finite-state analysis of SSL 3.0. In: 7th USENIX Security Symposium, pp. 201–216 (January 1998)
Monniaux, D.: Abstracting cryptographic protocols with tree automata. Science of Computer Programming 47(2-3), 177–202 (2003)
Needham, R.M.: Logic and over-simplification. In: 13th Annual IEEE Symposium on Logic in Computer Science, pp. 2–3 (1998)
Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Communications of the ACM 21(12), 993–999 (1978)
Needham, R.M., Schroeder, M.D.: Authentication revisited. Operating Systems Review 21(1), 7 (1987)
Paulson, L.C.: The inductive approach to verifying cryptographic protocols. Journal of Computer Security 6(1-2), 85–128 (1998)
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)
Schneider, S.: Security properties and CSP. In: 1996 IEEE Symposium on Security and Privacy, pp. 174–187 (1996)
Syverson, P.: Limitations on design principles for public key protocols. In: 1996 IEEE Symposium on Security and Privacy, pp. 62–73 (1996)
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)
Woo, T.Y.C., Lam, S.S.: Authentication for distributed systems. Computer 25(1), 39–52 (1992)
Woo, T.Y.C., Lam, S.S.: A lesson on authentication protocol design. Operating Systems Review 28(3), 24–37 (1994)
Yao, A.C.: Theory and applications of trapdoor functions. In: 23rd Annual Symposium on Foundations of Computer Science (FOCS 1982), pp. 80–91 (1982)
Author information
Authors and Affiliations
Editor information
Rights 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)