×

Easy intruder deduction problems with homomorphisms. (English) Zbl 1184.68459

Summary: We present complexity results for the verification of security protocols. Since the perfect cryptography assumption is unrealistic for cryptographic primitives with visible algebraic properties, we extend the classical Dolev-Yao model by permitting the intruder to exploit these properties. More precisely, we are interested in theories such as Exclusive or and Abelian groups in combination with the homomorphism axiom. We show that the intruder deduction problem is in PTIME in both cases, improving the EXPTIME complexity results of Lafourcade, Lugiez and Treinen.

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68P25 Data encryption (aspects in computer science)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abadi, M.; Cortier, V., Deciding knowledge in security protocols under (many more) equational theories, (Proc. 18th IEEE Computer Security Foundations Workshop (CSFW’05), Aix-en-Provence, France (2005), IEEE Comp. Soc. Press), 62-76
[2] Aschenbrenner, M., Ideal membership in polynomial rings over the integers, J. Amer. Math. Soc., 17, 407-441 (2004) · Zbl 1099.13045
[3] J. Benaloh, Verifiable secret ballot elections, PhD thesis, Yale University, 1987; J. Benaloh, Verifiable secret ballot elections, PhD thesis, Yale University, 1987 · Zbl 1344.68029
[4] Chevalier, Y.; Küsters, R.; Rusinowitch, M.; Turuani, M., Deciding the security of protocols with Diffie-Hellman exponentiation and product in exponents, (Proc. 23rd Conf. Foundations of Software Technology and Theoretical Computer Science (FST&TCS’03), Mumbai, India. Proc. 23rd Conf. Foundations of Software Technology and Theoretical Computer Science (FST&TCS’03), Mumbai, India, Lecture Notes in Comput. Sci., vol. 2914 (2003), Springer: Springer Berlin), 124-135 · Zbl 1205.94078
[5] Chevalier, Y.; Küsters, R.; Rusinowitch, M.; Turuani, M., An NP decision procedure for protocol insecurity with XOR, (Proc. of 18th Annual IEEE Symp. Logic in Computer Science (LICS’03), Ottawa, Canada (2003), IEEE Comp. Soc. Press.), 261-270
[6] Comon-Lundh, H.; Treinen, R., Easy intruder deductions, (Verification: Theory & Practice, Essays Dedicated to Zohar Manna on the Occasion of his 64th Birthday. Verification: Theory & Practice, Essays Dedicated to Zohar Manna on the Occasion of his 64th Birthday, Lecture Notes in Comput. Sci., vol. 2772 (2003), Springer: Springer Berlin), 225-242 · Zbl 1201.68049
[7] V. Cortier, S. Delaune, P. Lafourcade, A survey of algebraic properties used in cryptographic protocols, J. Comput. Security (2005), in press; V. Cortier, S. Delaune, P. Lafourcade, A survey of algebraic properties used in cryptographic protocols, J. Comput. Security (2005), in press
[8] Dolev, D.; Yao, A., On the security of public key protocols, IEEE Trans. Inform. Theory, 29, 2, 198-208 (1983) · Zbl 0502.94005
[9] Kaltofen, E.; Krishnamoorthy, M. S.; Saunders, B. D., Fast parallel computation of Hermite and Smith forms of polynomial matrices, SIAM J. Algebr. Discrete Methods, 8, 4, 683-690 (1987) · Zbl 0655.65069
[10] Lafourcade, P.; Lugiez, D.; Treinen, R., Intruder deduction for AC-like equational theories with homomorphisms, (Proc. 16th Internat. Conf. Rewriting Techniques and Applications (RTA’05), Nara, Japan. Proc. 16th Internat. Conf. Rewriting Techniques and Applications (RTA’05), Nara, Japan, Lecture Notes in Comput. Sci., vol. 3467 (2005), Springer: Springer Berlin), 308-322 · Zbl 1078.68034
[11] P. Lafourcade, D. Lugiez, R. Treinen, Intruder deduction for the equational theory of exclusive-or with distributive encryption, Research Report LSV-05-19, Laboratoire Spécification et Vérification, ENS Cachan, France, 2005; P. Lafourcade, D. Lugiez, R. Treinen, Intruder deduction for the equational theory of exclusive-or with distributive encryption, Research Report LSV-05-19, Laboratoire Spécification et Vérification, ENS Cachan, France, 2005 · Zbl 1112.68048
[12] McAllester, D. A., Automatic recognition of tractability in inference relations, J. ACM, 40, 2, 284-303 (1993) · Zbl 0770.68106
[13] Nutt, W., Unification in monoidal theories, (Proc. 10th Internat. Conf. Automated Deduction (CADE’90), Kaiserslautern, Germany. Proc. 10th Internat. Conf. Automated Deduction (CADE’90), Kaiserslautern, Germany, Lecture Notes in Comput. Sci., vol. 449 (1990), Springer: Springer Berlin), 618-632 · Zbl 1509.03045
[14] Schrijver, A., Theory of Linear and Integer Programming (1986), Wiley: Wiley New York · Zbl 0665.90063
[15] Tatebayashi, M.; Matsuzaki, N.; Newman, D. B., Key distribution protocol for digital mobile communication systems, (Proc. 9th Annual Internat. Cryptology Conference (CRYPTO’89), Santa Barbara, CA, USA. Proc. 9th Annual Internat. Cryptology Conference (CRYPTO’89), Santa Barbara, CA, USA, Lecture Notes in Comput. Sci., vol. 435 (1989), Springer: Springer Berlin), 324-333
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.