Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
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)
Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: 14th IEEE CSFW, June 2001, IEEE Computer Society Press, Los Alamitos (2001)
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)
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)
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)
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)
Herzog, J.: The Diffie-Hellman protocol in the strand space model. In: Proc. 16th IEEE CSFW, IEEE Computer Society Press, Los Alamitos (2003)
Kaufman, C.: Internet key exchange (IKEv2) protocol. draft-ietf-ipsec-kev2-14.txt (January 2004), Available at http://www.watersprings.org/pub/id/draft-ietfipsec-ikev2-14.txt
Lynch, C., Meadows, C.: On the relative soundness of the free algebra model for public key encryption. In: WITS 2004 (April 2004) (to appear)
Lynch, C., Morawska, B.: Basic syntactic mutation. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 471–485. Springer, Heidelberg (2002)
Meadows, C.: The NRL Protocol Analyzer: an overview. Journal of Logic Programming 26(2), 113–131 (1995)
Meadows, C.: Towards a hierarchy of cryptographic protocol specifications. In: Proc. FMSE 2003: Formal Methods in Security Engineering, ACM Press, New York (2003)
Millen, J.: On the freedom of decryption. Information Processing Letters 86(6), 329–333 (2003)
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)
Song, D., Berizin, S., Perrig, A.: Athena: a novel approach to efficient automatic security analysis. Journal of Computer Security 9(1), 47–74 (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lynch, C., Meadows, C. (2004). Sound Approximations to Diffie-Hellman Using Rewrite Rules. In: Lopez, J., Qing, S., Okamoto, E. (eds) Information and Communications Security. ICICS 2004. Lecture Notes in Computer Science, vol 3269. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30191-2_21
Download citation
DOI: https://doi.org/10.1007/978-3-540-30191-2_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23563-7
Online ISBN: 978-3-540-30191-2
eBook Packages: Springer Book Archive