Abstract
We demonstrate that the symbolic trace reachability problem for cryptographic protocols is decidable in the presence of an Abelian group operator and modular exponentiation from arbitrary bases. We represent the problem as a sequence of symbolic inference constraints and reduce it to a system of linear Diophantine equations. For a finite number of protocol sessions, this result enables fully automated, sound and complete analysis of protocols that employ primitives such as Diffie-Hellman exponentiation and modular multiplication without imposing any bounds on the size of terms created by the attacker, but taking into account the relevant algebraic properties.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Amadio, R., Lugiez, D.: On the reachability problem in cryptographic protocols. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 380–394. Springer, Heidelberg (2000)
Baader, F., Snyder, W.: Unification theory. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 8, vol. 1, pp. 445–532. Elsevier Science, Amsterdam (2001)
Boreale, M.: Symbolic trace analysis of cryptographic protocols. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, pp. 667–681. Springer, Heidelberg (2001)
Boreale, M., Buscemi, M.: On the symbolic analysis of low-level cryptographic primitives: modular exponentiation and the Diffie-Hellman protocol. In: Proc. Workshop on the Foundations of Computer Security, FCS (2003)
Chevalier, Y., Küsters, R., Rusinowitch, M., Turuani, M.: Deciding the security of protocols with Diffie-Hellman exponentiation and products in exponents. Technical Report IFI-Report 0305, CAU Kiel (2003)
Comon-Lundh, H., Shmatikov, V.: Intruder deductions, constraint solving and insecurity decision in presence of exclusive or. In: Proc. 18th Annual IEEE Symposium on Logic in Computer Science (LICS 2003), pp. 271–280 (2003)
Contejean, E., Devie, H.: An efficient algorithm for solving systems of Diophantine equations. Information and Computation 113(1), 143–172 (1994)
Durgin, N., Lincoln, P.D., Mitchell, J.C., Scedrov, A.: Undecidability of bounded security protocols. In: Proc. FLOC Workshop on Formal Methods in Security Protocols (1999)
Fiore, M., Abadi, M.: Computing symbolic models for verifying cryptographic protocols. In: Proc. 14th IEEE Computer Security Foundations Workshop, pp. 160–173 (2001)
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, pp. 165–179. Springer, Heidelberg (2003)
Meadows, C., Narendran, P.: A unification algorithm for the group Diffie- Hellman protocol. In: Proc. Workshop of Issues in Theory of Security, WITS (2002)
Menezes, A., van Oorschot, P., Vanstone, S.: Handbook of Applied Cryptography. CRC Press, Boca Raton (1997)
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 (2001)
Millen, J., Shmatikov, V.: Symbolic protocol analysis with products and Diffie- Hellman exponentiation. In: Proc. 16th IEEE Computer Security Foundations Workshop, pp. 47–61 (2003)
Paulson, L.: Mechanized proofs for a recursive authentication protocol. In: Proc. 10th IEEE Computer Security Foundations Workshop, pp. 84–95 (1997)
Pereira, O., Quisquater, J.-J.: A security analysis of the Cliques protocols suites. In: Proc. 14th IEEE Computer Security Foundations Workshop, pp. 73–81 (2001)
Rusinowitch, M., Turuani, M.: Protocol insecurity with finite number of sessions is NP-complete. In: Proc. 14th IEEE Computer Security Foundations Workshop, pp. 174–190 (2001)
Ryan, P., Schneider, S.: An attack on a recursive authentication protocol: A cautionary tale. Information Processing Letters 65(1), 7–10 (1998)
Steiner, M., Tsudik, G., Waidner, M.: Diffie-Hellman key distribution extended to group communication. In: Proc. 3rd ACM Conference on Computer and Communications Security (CCS 1996), pp. 31–37 (1996)
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
Shmatikov, V. (2004). Decidable Analysis of Cryptographic Protocols with Products and Modular Exponentiation. In: Schmidt, D. (eds) Programming Languages and Systems. ESOP 2004. Lecture Notes in Computer Science, vol 2986. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24725-8_25
Download citation
DOI: https://doi.org/10.1007/978-3-540-24725-8_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21313-0
Online ISBN: 978-3-540-24725-8
eBook Packages: Springer Book Archive