Formal Proofs of Cryptographic Security of Diffie-Hellman-Based Protocols

  • Arnab Roy
  • Anupam Datta
  • John C. Mitchell
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4912)


We present axioms and inference rules for reasoning about Diffie-Hellman-based key exchange protocols and use these rules to prove authentication and secrecy properties of two important protocol standards, the Diffie-Hellman variant of Kerberos, and IKEv2, the revised standard key management protocol for IPSEC. The new proof system is sound for an accepted semantics used in cryptographic studies. In the process of applying our system, we uncover a deficiency in Diffie-Hellman Kerberos that is easily repaired.


Encryption Scheme Signature Scheme Random Oracle Random Oracle Model Honest Party 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    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
  2. 2.
    Adão, P., Bana, G., Scedrov, A.: Computational and information-theoretic soundness and completeness of formal encryption. In: Proc. of the 18th IEEE Computer Security Foudnations Workshop, pp. 170–184 (2005)Google Scholar
  3. 3.
    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 Trans. Inf. Syst. Security 7(4), 1–30 (2004)Google Scholar
  4. 4.
    Backes, M., Cervesato, I., Jaggard, A.D., Scedrov, A., Tsay, J.-K.: Cryptographically sound security proofs for basic and public-key Kerberos. In: Proceedings of 11th European Symposium on Research in Computer Security (to appear, 2006)Google Scholar
  5. 5.
    Backes, M., Pfitzmann, B.: Limits of the cryptographic realization of XOR. In: Proc. of the 10th European Symposium on Research in Computer Security, Springer, Heidelberg (2005)Google Scholar
  6. 6.
    Backes, M., Pfitzmann, B.: Relating symbolic and cryptographic secrecy. In: Proc. IEEE Symposium on Security and Privacy, pp. 171–182. IEEE Computer Society Press, Los Alamitos (2005)Google Scholar
  7. 7.
    Backes, M., Pfitzmann, B., Waidner, M.: A universally composable cryptographic library. Cryptology ePrint Archive, Report 2003/015 (2003)Google Scholar
  8. 8.
    Backes, M., Pfitzmann, B., Waidner, M.: Limits of the reactive simulatability/UC of Dolev-Yao models with hashes. In: Gollmann, D., Meier, J., Sabelfeld, A. (eds.) ESORICS 2006. LNCS, vol. 4189, pp. 404–423. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  9. 9.
    Bella, G., Paulson, L.C.: Kerberos version IV: Inductive analysis of the secrecy goals. In: Quisquater, J.-J., Deswarte, Y., Meadows, C., Gollmann, D. (eds.) ESORICS 1998. LNCS, vol. 1485, pp. 361–375. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  10. 10.
    Bellare, M., Boldyreva, A., Micali, S.: Public-key encryption in a multi-user setting: Security proofs and improvements. In: Preneel, B. (ed.) EUROCRYPT 2000. LNCS, vol. 1807, pp. 259–274. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  11. 11.
    Bellare, M., Namprempre, C.: Authenticated encryption: Relations among notions and analysis of the generic composition paradigm. In: Okamoto, T. (ed.) ASIACRYPT 2000. LNCS, vol. 1976, pp. 531–545. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  12. 12.
    Bellare, M., Rogaway, P.: Random oracles are practical: A paradigm for designing efficient protocols. In: ACM Conference on Computer and Communications Security, pp. 62–73 (1993)Google Scholar
  13. 13.
    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
  14. 14.
    Boldyreva, A., Kumar, V.: Provable-security analysis of authenticated encryption in Kerberos. In: Proc. IEEE Security and Privacy (2007)Google Scholar
  15. 15.
    Bresson, E., Lakhnech, Y., Mazare, L., Warinschi, B.: A Generalization of DDH with Applications to Protocol Analysis and Computational Soundness. In: Menezes, A. (ed.) CRYPTO 2007. LNCS, vol. 4622, Springer, Heidelberg (2007)CrossRefGoogle Scholar
  16. 16.
    Butler, F., Cervesato, I., Jaggard, A.D., Scedrov, A.: Verifying confidentiality and authentication in Kerberos. In: ISSS, vol. 5, pp. 1–24 (2003)Google Scholar
  17. 17.
    Canetti, R., Fischlin, M.: Universally composable commitments. In: Kilian, J. (ed.) CRYPTO 2001. LNCS, vol. 2139, pp. 19–40. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  18. 18.
    Canetti, R., Herzog, J.: Universally composable symbolic analysis of mutual authentication and key-exchange protocols. In: Halevi, S., Rabin, T. (eds.) TCC 2006. LNCS, vol. 3876, pp. 380–403. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  19. 19.
    Cervesato, I., Jaggard, A., Scedrov, A., Tsay, J.-K., Walstad, C.: Breaking and fixing public-key Kerberos. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol. 4435, pp. 167–181. Springer, Heidelberg (2008)Google Scholar
  20. 20.
    Cervesato, I., Meadows, C., Pavlovic, D.: An encapsulated authentication logic for reasoning about key distribution protocols. In: CSFW, pp. 48–61 (2005)Google Scholar
  21. 21.
    Chevassut, O., Fouque, P.-A., Gaudry, P., Pointcheval, D.: Key derivation and randomness extraction. Cryptology ePrint Archive, Report 2005/061 (2005),
  22. 22.
    Cortier, V., Warinschi, B.: Computationally sound, automated proofs for security protocols. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 157–171. Springer, Heidelberg (2005)Google Scholar
  23. 23.
    Datta, A., Derek, A., Mitchell, J., Ramanathan, A., Scedrov, A.: Games and the impossibility of realizable ideal functionality. In: TCC, pp. 360–379 (2006)Google Scholar
  24. 24.
    Datta, A., Derek, A., Mitchell, J.C., Pavlovic, D.: A derivation system and compositional logic for security protocols. Journal of Computer Security 13, 423–482 (2005)Google Scholar
  25. 25.
    Datta, A., Derek, A., Mitchell, J.C., Roy, A.: Protocol Composition Logic (PCL). Electronic Notes in Theoretical Computer Science 172, 311–358 (2007)CrossRefMathSciNetGoogle Scholar
  26. 26.
    Datta, A., Derek, A., Mitchell, J.C., Shmatikov, V., Turuani, M.: Probabilistic polynomial-time semantics for a protocol security logic. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 16–29. Springer, Heidelberg (2005)Google Scholar
  27. 27.
    Datta, A., Derek, A., Mitchell, J.C., Warinschi, B.: Computationally sound compositional logic for key exchange protocols. In: Proceedings of 19th IEEE Computer Security Foundations Workshop, pp. 321–334. IEEE Computer Society Press, Los Alamitos (2006)Google Scholar
  28. 28.
    Diffie, W., Hellman, M.E.: New directions in cryptography. IEEE Transactions on Information Theory IT-22(6), 644–654 (1976)CrossRefMathSciNetGoogle Scholar
  29. 29.
    He, C., Sundararajan, M., Datta, A., Derek, A., Mitchell, J.C.: A modular correctness proof of IEEE 802.11i and TLS. In: ACM Conference on Computer and Communications Security, pp. 2–15 (2005)Google Scholar
  30. 30.
    Herzog, J.: The Diffie-Hellman key-agreement scheme in the strand-space model. In: Proceedings of 16th IEEE Computer Security Foundations Workshop, pp. 234–247. IEEE Computer Society Press, Los Alamitos (2003)CrossRefGoogle Scholar
  31. 31.
    Herzog, J.: Computational Soundness for Standard Assumptions of Formal Cryptography. PhD thesis, MIT (2004)Google Scholar
  32. 32.
    Janvier, R., Mazare, L., Lakhnech, Y.: Completing the picture: Soundness of formal encryption in the presence of active adversaries. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 172–185. Springer, Heidelberg (2005)Google Scholar
  33. 33.
    Katz, J., Yung, M.: Unforgeable encryption and chosen ciphertext secure modes of operation. In: Schneier, B. (ed.) FSE 2000. LNCS, vol. 1978, pp. 284–299. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  34. 34.
    Kaufman, C.: Internet Key Exchange (IKEv2) Protocol, RFC (2005)Google Scholar
  35. 35.
    Kohl, J., Neuman, B.: The kerberos network authentication service, RFC (1991)Google Scholar
  36. 36.
    Lakhnech, Y., Mazaré, L.: Computationally sound verifiation of security protocols using Diffie-Hellman exponentiation. Cryptology ePrint Archive: Report 2005/097 (2005)Google Scholar
  37. 37.
    Micciancio, D., Warinschi, B.: Completeness theorems for the Abadi-Rogaway logic of encrypted expressions. Journal of Computer Security 12(1), 99–129 (2004). Preliminary version in WITS 2002Google Scholar
  38. 38.
    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
  39. 39.
    Roy, A., Datta, A., Derek, A., Mitchell, J.C.: Inductive proofs of computational secrecy. In: Biskup, J., López, J. (eds.) ESORICS 2007. LNCS, vol. 4734, pp. 219–234. Springer, Heidelberg (2007), CrossRefGoogle Scholar
  40. 40.
    Roy, A., Datta, A., Derek, A., Mitchell, J.C.: Inductive trace properties for computational security. In: WITS (2007),
  41. 41.
    Roy, A., Datta, A., Derek, A., Mitchell, J.C., Seifert, J.-P.: Secrecy analysis in Protocol Composition Logic. In: Proceedings of 11th Annual Asian Computing Science Conference (to appear, 2006)Google Scholar
  42. 42.
    Roy, A., Datta, A., Mitchell, J.C.: Formal proofs of cryptographic security of Diffie-Hellman-based protocols. Manuscript (2007),
  43. 43.
    Zhu, L., Tung, B.: Public Key Cryptography for Initial Authentication in Kerberos (PKINIT). RFC 4556 (Proposed Standard) (June 2006)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Arnab Roy
    • 1
  • Anupam Datta
    • 2
  • John C. Mitchell
    • 1
  1. 1.Stanford UniversityStanford 
  2. 2.Carnegie Mellon UniversityPittsburgh 

Personalised recommendations