Abstract
We consider deducibility constraints, which are equivalent to particular Diophantine systems, arising in the automatic verification of security protocols, in presence of associative and commutative symbols. We show that deciding such Diophantine systems is, in general, undecidable. Then, we consider a simple subclass, which we show decidable. Though the solutions of these problems are not necessarily semi-linear sets, we show that there are (computable) semi-linear sets whose minimal solutions are not too far from the minimal solutions of the system. Finally, we consider a small variant of the problem, for which there is a much simpler decision algorithm.
This work was partly supported by the RNTL project PROUVÉ 03V360, ACI-SI Rossignol, and EPSRC project EP/E029833.
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
Blanchet, B., Podelski, A.: Verification of Cryptographic Protocols: Tagging Enforces Termination. Theoretical Computer Science 333(1-2), 67–90 (2005)
Chevalier, Y., et al.: Deciding the security of protocols with Diffie-Hellman exponentiation and product in exponents. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol. 2914, pp. 124–135. Springer, Heidelberg (2003)
Chevalier, Y., et al.: An NP decision procedure for protocol insecurity with XOR. In: Proc. 18th IEEE Symp. Logic in Computer Science (LICS’03), pp. 261–270. IEEE Computer Society Press, Los Alamitos (2003)
Chevalier, Y., Rusinowitch, M.: Hierarchical combination of intruder theories. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 108–122. Springer, Heidelberg (2006)
Comon, H., Cortier, V.: Tree automata with one memory, set constraints and cryptographic protocols. Theoretical Computer Science 331(1), 143–214 (2005)
Comon-Lundh, H., Delaune, S.: The finite variant property: How to get rid of some algebraic properties. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 294–307. Springer, Heidelberg (2005)
Comon-Lundh, H., Shmatikov, V.: Intruder deductions, constraint solving and insecurity decision in presence of exclusive or. In: Proc. 18th IEEE Symp. Logic in Computer Science (LICS’03), pp. 271–280. IEEE Computer Society Press, Los Alamitos (2003)
Davis, M., Matijasevich, Y., Robinson, J.: Hilbert’s tenth problem, Diophantine equations: positive aspects of a negative solution. In: Proc. of Symposia in Pure Maths, pp. 323–378 (1976)
Delaune, S.: Vérification des protocoles cryptographiques et propriétés algébriques. Thèse de doctorat, ENS Cachan, France (2006)
Delaune, S., et al.: Symbolic protocol analysis in presence of a homomorphism operator and exclusive or. In: Bugliesi, M., et al. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 132–141. Springer, Heidelberg (2006)
Karianto, W., Krieg, A., Thomas, W.: On intersection problems for polynomially generated sets. In: Bugliesi, M., et al. (eds.) ICALP 2006. LNCS, vol. 4052, Springer, Heidelberg (2006)
Lowe, G.: Towards a completeness result for model checking of security protocols. J. Computer Security 7(2–3), 89–146 (1999)
Millen, J., Shmatikov, V.: Symbolic protocol analysis with an abelian group operator or Diffie-Hellman exponentiation. J. Computer Security 13(3), 515–564 (2005)
Ramanujam, R., Suresh, S.P.: Decidability of context-explicit security protocols. J. Computer Security 13(1) (2005)
Rusinowitch, M., Turuani, M.: Protocol insecurity with finite number of sessions is NP-complete. In: Proc.14th IEEE Computer Security Foundations Workshop, IEEE Computer Society Press, Los Alamitos (2001)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Bursuc, S., Comon-Lundh, H., Delaune, S. (2007). Associative-Commutative Deducibility Constraints. In: Thomas, W., Weil, P. (eds) STACS 2007. STACS 2007. Lecture Notes in Computer Science, vol 4393. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-70918-3_54
Download citation
DOI: https://doi.org/10.1007/978-3-540-70918-3_54
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-70917-6
Online ISBN: 978-3-540-70918-3
eBook Packages: Computer ScienceComputer Science (R0)