Abstract
Automatic methods developed so far for analysis of security protocols only model a limited set of cryptographic primitives (often, only encryption and concatenation) and abstract from low-level features of cryptographic algorithms. This paper is an attempt towards closing this gap. We propose a symbolic technique and a decision method for analysis of protocols based on modular exponentiation, such as Diffie-Hellman key exchange. We introduce a protocol description language along with its semantics. Then, we propose a notion of symbolic execution and, based on it, a verification method. We prove that the method is sound and complete with respect to the language semantics.
This work has been partially supported by EU within the FET – Global Computing initiative, projects MIKADO and PROFUNDIS and by MIUR project NAPOLI.
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.
References
Abadi, M., Fournet, C.: Mobile Values, New Names, and Secure Communication. In: Conf. Rec. of POPL 2001 (2001)
Amadio, R.M., Lugiez, S.: On the reachability problem in cryptographic protocols. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, p. 380. Springer, Heidelberg (2000)
Boreale, M.: Symbolic Trace Analysis of Cryptographic Protocols. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, p. 667. Springer, Heidelberg (2001)
Boreale, M., Buscemi, M.: Experimenting with STA, a Tool for Automatic Analysis of Security Protocols. In: SAC 2002. ACM Press, New York (2002)
Boreale, M., Buscemi, M.: A Framework for the Analysis of Security Protocol. In: Brim, L., Jančar, P., Křetínský, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, p. 483. Springer, Heidelberg (2002)
Boreale, M., Buscemi, M.: On the Symbolic Analysis of Low-Level Cryptographic Primitives: Modular Exponentiation and the Diffie-Hellman Protocol. To appear in Proc. of FCS 2003, ENTS Series. Elsevier Science (2003)
Chevalier, Y., Kuesters, R., Rusinowitch, M., Turuani, M.: An NP Decision Procedure for Protocol Insecurity with Xor. In: Proc. of LICS 2003. IEEE Computer Society Press, Los Alamitos (2003)
Comon, H., Cortier, V., Mitchell, J.: Tree automata with one memory, set constraints and ping-pong protocols. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, p. 682. Springer, Heidelberg (2001)
Comon-Lundh, H., Shmatikov, V.: Intruder Deductions, Constraint Solving and Insecurity Decision in Presence of Exclusive or. In: Proc. LICS 2003. IEEE Computer Society Press, Los Alamitos (2003)
Diffie, W., Hellman, M.: New Directions in Cryptography. IEEE Transactions on Information Theory 22(6), 644–654 (1976)
Dolev, D., Yao, A.: On the security of public-key protocols. IEEE Transactions on Information Theory 29(2), 198–208 (1983)
Kapur, D., Narendran, P., Wang, L.: An E-unification Algorithm for Analyzing Protocols that Use Modular Exponentiation. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706. Springer, Heidelberg (2003)
Lowe, G.: Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055. Springer, Heidelberg (1996)
Millen, J., Shmatikov, V.: Constraint solving for bounded-process cryptographic protocol analysis. In: Proc. of 8th ACM Conference on Computer and Communication Security. ACM Press, New York (2001)
Millen, J., Shmatikov, V.: Symbolic Protocol Analysis with Products and Diffie-Hellman Exponentiation. In: Proc. of 16th IEEE Computer Security Foundations Workshop. IEEE Computer Society Press, Los Alamitos (2003)
Vanackère, V.: The TRUST Protocol Analyser, Automatic and Efficient Verification of Cryptographic Protocols. In: Proc. of Verify 2002 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Boreale, M., Buscemi, M.G. (2003). Symbolic Analysis of Crypto-Protocols Based on Modular Exponentiation. In: Rovan, B., Vojtáš, P. (eds) Mathematical Foundations of Computer Science 2003. MFCS 2003. Lecture Notes in Computer Science, vol 2747. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45138-9_21
Download citation
DOI: https://doi.org/10.1007/978-3-540-45138-9_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40671-6
Online ISBN: 978-3-540-45138-9
eBook Packages: Springer Book Archive