Sound Approximations to Diffie-Hellman Using Rewrite Rules

  • Christopher Lynch
  • Catherine Meadows
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3269)


The commutative property of exponentiation that is necessary to model the Diffie-Hellman key exchange can lead to inefficiency when reasoning about protocols that make use of that cryptographic construct. In this paper we discuss the feasibility of approximating the commutative rule for exponentiation with a pair of rewrite rules, for which in unification-based systems, the complexity of the unification algorithm changes from at best exponential to at worst quadratic in the number of variables. We also derive and prove conditions under which the approximate model is sound with respect to the original model. Since the conditions make the protocol easier to reason about and less prone to error, they often turn out to be in line with generally accepted principles for sound protocol design.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Backes, M., Pfitzmann, B., Waidner, M.: A composable cryptographic library with nested operations (extended abstract). In: Proc. 10th ACM Conference on Computer and Communications Security (CCS), October 2003, ACM, New York (2003)Google Scholar
  2. 2.
    Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: 14th IEEE CSFW, June 2001, IEEE Computer Society Press, Los Alamitos (2001)Google Scholar
  3. 3.
    Cervesato, I., Durgin, N., Lincoln, P., Mitchell, J., Scedrov, A.: Relating strands and multiset rewriting for security protocol analysis. In: Proc. 13th IEEE CSFW, IEEE Computer Society Press, Los Alamitos (2000)Google Scholar
  4. 4.
    Cervesato, I., Meadows, C., Syverson, P.: Dolev-Yao is no better than Machiavelli. In: First Workshop on Issues in the Theory of Security - WITS 2000 (2000)Google Scholar
  5. 5.
    Thayer Fábrega, F., Herzog, J., Guttman, J.: Strand spaces: Why is a security protocol correct? In: Proc. 1998 IEEE Symposium on Security and Privacy, May 1998, pp. 160–171. IEEE Computer Society Press, Los Alamitos (1998)Google Scholar
  6. 6.
    Heather, J., Schneider, S., Lowe, G.: How to prevent type flaw attacks on security protocols. In: Proc. 13th CSFW, IEEE Computer Society Press, Los Alamitos (2000)Google Scholar
  7. 7.
    Herzog, J.: The Diffie-Hellman protocol in the strand space model. In: Proc. 16th IEEE CSFW, IEEE Computer Society Press, Los Alamitos (2003)Google Scholar
  8. 8.
    Kaufman, C.: Internet key exchange (IKEv2) protocol. draft-ietf-ipsec-kev2-14.txt (January 2004), Available at
  9. 9.
    Lynch, C., Meadows, C.: On the relative soundness of the free algebra model for public key encryption. In: WITS 2004 (April 2004) (to appear)Google Scholar
  10. 10.
    Lynch, C., Morawska, B.: Basic syntactic mutation. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 471–485. Springer, Heidelberg (2002)Google Scholar
  11. 11.
    Meadows, C.: The NRL Protocol Analyzer: an overview. Journal of Logic Programming 26(2), 113–131 (1995)CrossRefGoogle Scholar
  12. 12.
    Meadows, C.: Towards a hierarchy of cryptographic protocol specifications. In: Proc. FMSE 2003: Formal Methods in Security Engineering, ACM Press, New York (2003)Google Scholar
  13. 13.
    Millen, J.: On the freedom of decryption. Information Processing Letters 86(6), 329–333 (2003)zbMATHCrossRefMathSciNetGoogle Scholar
  14. 14.
    Millen, J., Shmatikov, V.: Constraint solving for bounded process cryptographic protocol analysis. In: Proc. 8th ACM Conference on Computer and Communications Security (CCS 2001), pp. 166–175. ACM Press, New York (2001)CrossRefGoogle Scholar
  15. 15.
    Song, D., Berizin, S., Perrig, A.: Athena: a novel approach to efficient automatic security analysis. Journal of Computer Security 9(1), 47–74 (2001)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Christopher Lynch
    • 1
  • Catherine Meadows
    • 2
  1. 1.Department of Mathematics and Computer ScienceClarkson UniversityPotsdamUSA
  2. 2.Naval Research LaboratoryCenter for High Assurance Computer SystemsWashingtonUSA

Personalised recommendations