×

Tree automata for detecting attacks on protocols with algebraic cryptographic primitives. (English) Zbl 1347.94020

Habermehl, P. (ed.) et al., Proceedings of the 8th, 9th, and 10th international workshops on verification of infinite-state systems (INFINITY 2006, 2007, 2008), Bonn, Germany, August 26, 2006, Lisbon, Portugal, September 8, 2007, Toronto, Canada, August 23, 2008. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 239, 57-72 (2009).
Summary: This paper extends a rewriting approximations-based theoretical framework in which the security problem – secrecy preservation against an active intruder – may be semi-decided through a reachability analysis. In a recent paper, we have shown how to semi-decide whether a security protocol using algebraic properties of cryptographic primitives is safe. In this paper, we investigate the dual – insecurity – problem: we explain how to semi-decide whether a protocol using cryptographic primitive algebraic properties is unsafe. This improvement offers us to draw automatically a complete diagnostic of a security protocol with an unbounded number of sessions. Furthermore, our approach is supported by the tool TA4SP successfully applied for analysing the NSPK-xor protocol and the Diffie-Hellman protocol.
For the entire collection see [Zbl 1279.68013].

MSC:

94A60 Cryptography
68Q42 Grammars and rewriting systems
68Q45 Formal languages and automata

Software:

Maude-NPA; AVISPA; Timbuk
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Armando, A.; Basin, D.; Boichut, Y.; Chevalier, Y.; Compagna, L.; Cuellar, J.; Hankes Drielsma, P.; Héam, P.-C.; Kouchnarenko, O.; Mantovani, J.; Mödersheim, S.; von Oheimb, D.; Rusinowitch, M.; Santos Santiago, J.; Turuani, M.; Viganò, L.; Vigneron, L., The AVISPA Tool for the automated validation of internet security protocols and applications, (17th International Conference on Computer Aided Verification, Proceedings. 17th International Conference on Computer Aided Verification, Proceedings, CAV 2005. 17th International Conference on Computer Aided Verification, Proceedings. 17th International Conference on Computer Aided Verification, Proceedings, CAV 2005, LNCS, volume 3576 (2005), Springer), 281-285 · Zbl 1081.68523
[2] Blanchet, B., An efficient cryptographic protocol verifier based on prolog rules, (14th IEEE Computer Security Foundations Workshop, Proceedings. 14th IEEE Computer Security Foundations Workshop, Proceedings, CSFW 2001 (2001), IEEE Computer Society Press), 82-96
[3] Blanchet, Bruno; Abadi, Martín; Fournet, Cédric, Automated verification of selected equivalences for security protocols, Journal of Logic and Algebraic Programming, 75, 1, 3-51 (February-March 2008)
[4] Boichut, Y.; Courbis, R.; Héam, P. C.; Kouchnarenko, O., Handling left-quadratic rules when completing tree automata, Electronic Notes in Theoretical Computer Science, 223, 61-70 (2008) · Zbl 1337.68165
[5] Y. Boichut, P.-C. Héam, and O. Kouchnarenko. Automatic Verification of Security Protocols Using Approximations. Technical Report RR-5727, INRIA, 2005; Y. Boichut, P.-C. Héam, and O. Kouchnarenko. Automatic Verification of Security Protocols Using Approximations. Technical Report RR-5727, INRIA, 2005
[6] Boichut, Y.; Héam, P.-C.; Kouchnarenko, O., Handling algebraic properties in automatic analysis of security protocols, (Int. Col. on Theorical Aspects of Computing. Int. Col. on Theorical Aspects of Computing, ICTAC-06. Int. Col. on Theorical Aspects of Computing. Int. Col. on Theorical Aspects of Computing, ICTAC-06, LNCS, volume 4281 (2006), Springer: Springer Berlin/Heidelberg), 153-167 · Zbl 1168.68378
[7] Bond, M., Attacks on cryptoprocessor transaction sets, (International Workshop on Cryptographic Hardware and Embedded Systems, Proceedings. International Workshop on Cryptographic Hardware and Embedded Systems, Proceedings, CHES 2001. International Workshop on Cryptographic Hardware and Embedded Systems, Proceedings. International Workshop on Cryptographic Hardware and Embedded Systems, Proceedings, CHES 2001, Lecture Notes on Computer Science (2001), Springer Verlag), 220-234 · Zbl 1007.68993
[8] Bozga, L.; Lakhnech, Y.; Perin, M., Pattern-based abstraction for verifying secrecy in protocols, (9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Proceedings. 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Proceedings, TACAS 2003. 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Proceedings. 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Proceedings, TACAS 2003, LNCS, volume 2619 (2003), Springer-Verlag) · Zbl 1031.94512
[9] Y. Chevalier, L. Compagna, J. Cuellar, P. Hankes Drielsma, J. Mantovani, S. Mödersheim, and L. Vigneron. A high level protocol specification language for industrial security-sensitive protocols. In Workshop on Specification and Automated Processing of Security Requirements, SAPS 2004, Proceedings; Y. Chevalier, L. Compagna, J. Cuellar, P. Hankes Drielsma, J. Mantovani, S. Mödersheim, and L. Vigneron. A high level protocol specification language for industrial security-sensitive protocols. In Workshop on Specification and Automated Processing of Security Requirements, SAPS 2004, Proceedings
[10] Comon, H.; Dauchet, M.; Gilleron, R.; Jacquemard, F.; Lugiez, D.; Tison, S.; Tommasi, M., Tree Automata Techniques and Applications (2002)
[11] Cortier, V.; Delaune, S.; Lafourcade, P., A survey of algebraic properties used in cryptographic protocols, Journal of Computer Security, 14, 1-43 (2006)
[12] V. Cortier, G. Keighren, and G. Steel. Automatic analysis of the security of xor-based key management schemes. In the 13 th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2007, Proceedings; V. Cortier, G. Keighren, and G. Steel. Automatic analysis of the security of xor-based key management schemes. In the 13 th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2007, Proceedings · Zbl 1186.68180
[13] Cortier, V.; Millen, J. K.; Rueß, H., Proving secrecy is easy enough, (14th IEEE Computer Security Foundations Workshop, Proceedings. 14th IEEE Computer Security Foundations Workshop, Proceedings, CSFW 2001 (June 2001), IEEE), 97-110
[14] C.J.F. Cremers. Scyther - Semantics and Verification of Security Protocols; C.J.F. Cremers. Scyther - Semantics and Verification of Security Protocols
[15] C.J.F. Cremers and P. Lafourcade. Comparing state spaces in security protocol analysis. In In Proc. of AVoCS’07; C.J.F. Cremers and P. Lafourcade. Comparing state spaces in security protocol analysis. In In Proc. of AVoCS’07 · Zbl 1242.94022
[16] Dolev, D.; Yao, A., On the Security of Public-Key Protocols, IEEE Transactions on Information Theory, 2, 29 (1983) · Zbl 0502.94005
[17] Escobar, S.; Meadows, C.; Meseguer, J., Equational cryptographic reasoning in the maude-NRL protocol analyzer, Electr. Notes Theor. Comput. Sci., 171, 4, 23-36 (2007)
[18] Feuillade, G.; Genet, Th.; VietTriemTong, V., Reachability analysis over term rewriting systems, Journal of Automated Reasonning, 33, 3-4 (2004)
[19] Genet, Th.; Klay, F., Rewriting for Cryptographic Protocol Verification, (Proceedings of CADE. Proceedings of CADE, LNCS, volume 1831 (2000), Springer-Verlag), 271-290 · Zbl 0963.94016
[20] C. Meadows. The NRL protocol analyser: An overview. Journal of Logic Programming; C. Meadows. The NRL protocol analyser: An overview. Journal of Logic Programming · Zbl 0871.68052
[21] Monniaux, D., Abstracting cryptographic protocols with tree automata, (Proceedings of SAS. Proceedings of SAS, LNCS, volume 1694 (1999), Springer-Verlag) · Zbl 1047.68066
[22] Ohsaki, H.; Takai, T., ACTAS: A system design for associative and commutative tree automata theory, Electr. Notes Theor. Comput. Sci, 124, 1, 97-111 (2005)
[23] Paulson, L. C., The inductive approach to verifying cryptographic protocols, Journal of Computer Security, 6, 1, 85-128 (1998)
[24] Song, D., Athena: A new efficient automatic checker for security protocol analysis, (12th IEEE Computer Security Foundations Workshop, Proceedings. 12th IEEE Computer Security Foundations Workshop, Proceedings, CSFW 1999 (1999), IEEE Computer Society Press), 192-202
[25] Turuani, M., The cl-atse protocol analyser, (17 th International Conference on Rewriting Techniques and Applications, Proceedings. 17 th International Conference on Rewriting Techniques and Applications, Proceedings, RTA 2006. 17 th International Conference on Rewriting Techniques and Applications, Proceedings. 17 th International Conference on Rewriting Techniques and Applications, Proceedings, RTA 2006, LNCS, volume 4098 (2006), Springer-Verlag), 277-286 · Zbl 1151.68454
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.