×

Deducibility constraints and blind signatures. (English) Zbl 1360.94298

Summary: Deducibility constraints represent in a symbolic way the infinite set of possible executions of a finite protocol. Solving a deducibility constraint amounts to finding all possible ways of filling the gaps in a proof. For finite local inference systems, there is an algorithm that reduces any deducibility constraint to a finite set of solved forms. This allows one to decide any trace security property of cryptographic protocols. We investigate here the case of infinite local inference systems, through the case study of blind signatures. We show that, in this case again, any deducibility constraint can be reduced to finitely many solved forms (hence we can decide trace security properties). We sketch also another example to which the same method can be applied.

MSC:

94A60 Cryptography
68M12 Network protocols
94A62 Authentication, digital signatures and secret sharing
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abadi, M.; Fournet, C., Mobile values, new names, and secure communication, (POPL (2001)), 104-115 · Zbl 1323.68398
[2] Basin, D.; Ganzinger, H., Automated complexity analysis based on ordered resolution, J. Assoc. Comput. Mach., 48, 1, 70-109 (January 2001)
[3] Bernat, V.; Comon-Lundh, H., Normal proofs in intruder theories, (Proceedings of the 11th Asian Computing Science Conference. Proceedings of the 11th Asian Computing Science Conference, ASIAN’06. Proceedings of the 11th Asian Computing Science Conference. Proceedings of the 11th Asian Computing Science Conference, ASIAN’06, Lect. Notes Comput. Sci., vol. 4435 (2008), Springer)
[4] Bursuc, S.; Delaune, S.; Comon-Lundh, H., Deducibility constraints, (Proceedings of the 13th Asian Computing Science Conference. Proceedings of the 13th Asian Computing Science Conference, ASIAN’09. Proceedings of the 13th Asian Computing Science Conference. Proceedings of the 13th Asian Computing Science Conference, ASIAN’09, Lect. Notes Comput. Sci., vol. 5913 (2009), Springer), 24-38 · Zbl 1273.03103
[5] Chaum, D., Blind signature system, (Chaum, D., CRYPTO (1983), Plenum Press: Plenum Press New York), 153 · Zbl 1487.94151
[6] Chevalier, Y.; Kuester, R.; Rusinowitch, M.; Turuani, M., An NP decision procedure for protocol insecurity with XOR, (Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science. Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science, LICS’03 (2003), IEEE Computer Society Press)
[7] Chevalier, Y.; Küsters, R.; Rusinowitch, M.; Turuani, M., Deciding the security of protocols with Diffie-Hellman exponentiation and products in exponents, (Proceedings of the 23rd Conference on Foundations of Software Technology and Theoretical Computer Science. Proceedings of the 23rd Conference on Foundations of Software Technology and Theoretical Computer Science, FST&TCS’03. Proceedings of the 23rd Conference on Foundations of Software Technology and Theoretical Computer Science. Proceedings of the 23rd Conference on Foundations of Software Technology and Theoretical Computer Science, FST&TCS’03, Lect. Notes Comput. Sci., vol. 2914 (2003), Springer) · Zbl 1205.94078
[8] Chevalier, Y.; Rusinowitch, M., Symbolic protocol analysis in the union of disjoint intruder theories: combining decision procedures, Theor. Comput. Sci., 411, 10, 1261-1282 (2010) · Zbl 1187.68204
[9] Comon, H.; Lescanne, P., Equational problems and disunification, J. Symb. Comput., 7, 371-425 (1989) · Zbl 0678.68093
[10] Comon-Lundh, H.; Cortier, V.; Zalinescu, E., Deciding security properties of cryptographic protocols. Application to key cycles, ACM Trans. Comput. Log., 11, 2 (2010) · Zbl 1351.94035
[11] Comon-Lundh, H.; Shmatikov, V., Intruder deductions, constraint solving and insecurity decision in preence of exclusive or, (Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science. Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science, LICS’03 (2003), IEEE Computer Society Press)
[12] Delaune, S.; Kremer, S.; Ryan, M. D., Symbolic bisimulation for the applied pi calculus, J. Comput. Secur., 18, 2, 317-377 (Mar. 2010)
[13] Delaune, S.; Lafourcade, P.; Lugiez, D.; Treinen, R., Symbolic protocol analysis for monoidal equational theories, Inf. Comput., 206, 2-4, 312-351 (2008) · Zbl 1148.68325
[14] Fujioka, A.; Okamoto, T.; Ohta, K., A practical secret voting scheme for large scale elections, (Seberry, J.; Zheng, Y., AUSCRYPT. AUSCRYPT, Lect. Notes Comput. Sci., vol. 718 (1992), Springer), 244-251 · Zbl 1096.68612
[15] Kremer, S.; Ryan, M. D., Analysis of an electronic voting protocol in the applied pi-calculus, (Proceedings of the 14th European Symposium on Programming. Proceedings of the 14th European Symposium on Programming, ESOP’05. Proceedings of the 14th European Symposium on Programming. Proceedings of the 14th European Symposium on Programming, ESOP’05, Lect. Notes Comput. Sci., vol. 3444 (2005), Springer), 186-200 · Zbl 1108.68462
[16] McAllester, D., Automatic recognition of tractability in inference relations, J. ACM, 40, 2 (1993) · Zbl 0770.68106
[17] Millen, J.; Shmatikov, V., Constraint solving for bounded-process cryptographic protocol analysis, (Proceedings of the 8th ACM Conference on Computer and Communications Security (2001))
[18] Millen, J.; Shmatikov, V., Symbolic protocol analysis with an abelian group operator or Diffie-Hellman exponentiation, J. Comput. Secur., 13, 3, 515-564 (2005)
[19] Rusinowitch, M.; Turuani, M., Protocol insecurity with finite number of sessions is np-complete, (Proceedings of the 14th Computer Security Foundations Workshop. Proceedings of the 14th Computer Security Foundations Workshop, CSFW’01 (2001), IEEE Computer Society Press)
[20] Rusinowitch, M.; Turuani, M., Protocol insecurity with a finite number of sessions, composed keys is NP-complete, Theor. Comput. Sci., 1-3, 299, 451-475 (2003) · Zbl 1042.68009
[21] Shmatikov, V., Decidable analysis of cryptographic protocols with products and modular exponentiation, (Proceedings of the 13th European Symposium on Programming. Proceedings of the 13th European Symposium on Programming, ESOP’04. Proceedings of the 13th European Symposium on Programming. Proceedings of the 13th European Symposium on Programming, ESOP’04, Lect. Notes Comput. Sci., vol. 2986 (2004), Springer) · Zbl 1126.94341
[22] Tiu, A.; Goré, R.; Dawson, J. E., A proof theoretic analysis of intruder theories, Log. Methods Comput. Sci., 6, 3 (2010) · Zbl 1201.68052
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.