Models and Proofs of Protocol Security: A Progress Report

  • Martín Abadi
  • Bruno Blanchet
  • Hubert Comon-Lundh
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5643)


This paper discusses progress in the verification of security protocols. Focusing on a small, classic example, it stresses the use of program-like representations of protocols, and their automatic analysis in symbolic and computational models.


Security Protocol Security Property Cryptographic Protocol Cryptographic Operation Process Calculus 
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.


  1. 1.
    Abadi, M.: Security protocols: Principles and calculi. In: Aldini, A., Gorrieri, R. (eds.) FOSAD 2007. LNCS, vol. 4677, pp. 1–23. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  2. 2.
    Abadi, M., Blanchet, B.: Analyzing security protocols with secrecy types and logic programs. Journal of the ACM 52(1), 102–146 (2005)MathSciNetCrossRefzbMATHGoogle 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)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Abadi, M., Blanchet, B., Fournet, C.: Just Fast Keying in the pi calculus. ACM Transactions on Information and System Security 10(3), 1–59 (2007)CrossRefzbMATHGoogle Scholar
  5. 5.
    Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: 28th ACM Symposium on Principles of Programming Languages, pp. 104–115 (2001)Google Scholar
  6. 6.
    Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: The spi calculus. Information and Computation 148(1), 1–70 (1999); An extended version appeared as Digital Equipment Corporation Systems Research Center report No. 149 (January 1998)Google Scholar
  7. 7.
    Abadi, M., Rogaway, P.: Reconciling two views of cryptography (The computational soundness of formal encryption). Journal of Cryptology 15(2), 103–127 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    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
  9. 9.
    Backes, M., Maffei, M., Unruh, D.: Zero-knowledge in the applied pi-calculus and automated verification of the direct anonymous attestation protocol. In: Proceedings of the 2008 IEEE Symposium on Security and Privacy, pp. 202–215 (2008)Google Scholar
  10. 10.
    Baudet, M.: Sécurité des protocoles cryptographiques: aspects logiques et calculatoires. PhD thesis, Ecole Normale Supérieure de Cachan (2007)Google Scholar
  11. 11.
    Bellare, M., Namprempre, C.: Authenticated encryption: Relations among notions and analysis of the generic composition paradigm. Journal of Cryptology 21(4), 469–491 (2008)MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    Bhargavan, K., Fournet, C., Corin, R., Zalinescu, E.: Cryptographically verified implementations for TLS. In: Proceedings of the 15th ACM Conference on Computer and Communications Security, pp. 459–468 (2008)Google Scholar
  13. 13.
    Bhargavan, K., Fournet, C., Gordon, A.D.: Verifying policy-based security for web services. In: ACM Conference on Computer and Communications Security, pp. 268–277 (2004)Google Scholar
  14. 14.
    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
  15. 15.
    Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: 14th IEEE Computer Security Foundations Workshop, pp. 82–96 (2001)Google Scholar
  16. 16.
    Blanchet, B.: Automatic proof of strong secrecy for security protocols. In: 2004 IEEE Symposium on Security and Privacy, pp. 86–100 (2004)Google Scholar
  17. 17.
    Blanchet, B.: A computationally sound mechanized prover for security protocols. In: 2006 IEEE Symposium on Security and Privacy, pp. 140–154 (2006)Google Scholar
  18. 18.
    Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. Journal of Logic and Algebraic Programming 75(1) (February-March 2008)Google Scholar
  19. 19.
    Blanchet, B., Chaudhuri, A.: Automated formal analysis of a protocol for secure file sharing on untrusted storage. In: 2008 IEEE Symposium on Security and Privacy, pp. 417–431 (2008)Google Scholar
  20. 20.
    Blanchet, B., Podelski, A.: Verification of cryptographic protocols: Tagging enforces termination. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol. 2620, pp. 136–152. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  21. 21.
    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
  22. 22.
    Bodei, C.: Security Issues in Process Calculi. PhD thesis, Università di Pisa (January 2000)Google Scholar
  23. 23.
    Boreale, M., Nicola, R.D., Pugliese, R.: Proof techniques for cryptographic processes. SIAM Journal on Computing 31(3), 947–986 (2001)MathSciNetCrossRefzbMATHGoogle Scholar
  24. 24.
    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)CrossRefGoogle Scholar
  25. 25.
    Burrows, M., Abadi, M., Needham, R.: A logic of authentication. Proceedings of the Royal Society of London A 426, 233–271 (1989); A preliminary version appeared as Digital Equipment Corporation Systems Research Center report No. 39 (February 1989)Google Scholar
  26. 26.
    Comon-Lundh, H., Cortier, V.: Computational soundness of observational equivalence. In: Proceedings of the 15th ACM Conference on Computer and Communications Security, pp. 109–118 (2008)Google Scholar
  27. 27.
    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)CrossRefGoogle Scholar
  28. 28.
    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
  29. 29.
    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
  30. 30.
    Freier, A.O., Karlton, P., Kocher, P.C.: The SSL protocol: Version 3.0 (November 1996),
  31. 31.
    Goldwasser, S., Micali, S.: Probabilistic encryption. Journal of Computer and System Sciences 28, 270–299 (1984)MathSciNetCrossRefzbMATHGoogle Scholar
  32. 32.
    Gordon, A.D.: Provable implementations of security protocols. In: 21st Annual IEEE Symposium on Logic in Computer Science, pp. 345–346 (2006)Google Scholar
  33. 33.
    Gordon, A.D., Jeffrey, A.: Types and effects for asymmetric cryptographic protocols. In: 15th IEEE Computer Security Foundations Workshop, pp. 77–91 (2002)Google Scholar
  34. 34.
    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)CrossRefGoogle Scholar
  35. 35.
    He, C., Sundararajan, M., Datta, A., Derek, A., Mitchell, J.C.: A modular correctness proof of IEEE 802.11i and TLS. In: Proceedings of the 12th ACM Conference on Computer and Communications Security, pp. 2–15 (2005)Google Scholar
  36. 36.
    Hüttel, H.: Deciding framed bisimilarity. In: 4th International Workshop on Verification of Infinite-State Systems, pp. 1–20 (2002)Google Scholar
  37. 37.
    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)CrossRefGoogle 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. 147–166. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  39. 39.
    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
  40. 40.
    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)CrossRefGoogle Scholar
  41. 41.
    Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, parts I and II. Information and Computation 100, 1–77 (1992)Google Scholar
  42. 42.
    Morrissey, P., Smart, N.P., Warinschi, B.: A modular security analysis of the TLS handshake protocol. In: Pieprzyk, J. (ed.) ASIACRYPT. LNCS, vol. 5350, pp. 55–73. Springer, Heidelberg (2008)Google Scholar
  43. 43.
    Needham, R.M.: The changing environment for security protocols. IEEE Network 11(3), 12–15 (1997)CrossRefGoogle Scholar
  44. 44.
    Paulson, L.C.: Inductive analysis of the internet protocol TLS. ACM Transactions on Information and System Security 2(3), 332–351 (1999)CrossRefGoogle Scholar
  45. 45.
    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)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Martín Abadi
    • 1
    • 2
  • Bruno Blanchet
    • 3
    • 4
    • 5
  • Hubert Comon-Lundh
    • 5
    • 6
    • 7
  1. 1.Microsoft ResearchSilicon Valley
  2. 2.University of CaliforniaSanta Cruz
  3. 3.CNRSFrance
  4. 4.École Normale SupérieureFrance
  5. 5.INRIAFrance
  6. 6.École Normale Supérieure de CachanFrance
  7. 7.Research Center for Information SecurityAdvanced Industrial Science and TechnologyJapan

Personalised recommendations