Abstract
In this paper we extend the approximation based theoretical framework in which the security problem – secrecy preservation against an intruder – may be semi-decided through a reachability verification.
We explain how to cope with algebraic properties for an automatic approximation-based analysis of security protocols. We prove that if the initial knowledge of the intruder is a regular tree language, then the security problem may by semi-decided for protocols using cryptographic primitives with algebraic properties. More precisely, an automatically generated approximation function enables us 1) an automatic normalization of transitions, and 2) an automatic completion procedure. The main advantage of our approach is that the approximation function makes it possible to verify security protocols with an arbitrary number of sessions.
The concepts are illustrated on an example of the view-only protocol using a cryptographic primitive with the exclusive or algebraic property.
This work has been supported by the European project AVISPA IST-2001-39252 and the French projects RNTL PROUVE and ACI SATIN.
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
Smartright technical white paper v1.0. Technical report, Thomson (October 2001), http://www.smartright.org
Armando, A., Basin, D., Boichut, Y., Chevalier, Y., Compagna, L., Cuellar, J., Drielsma, P.H., Heám, P.C., Kouchnarenko, O., Mantovani, J., Mödersheim, S., von Oheimb, D., Rusinowitch, M., Santiago, J., Turuani, M., Viganò, L., Vigneron, L.: The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 281–285. Springer, Heidelberg (2005)
Armando, A., Basin, D., Bouallagui, M., Chevalier, Y., Compagna, L., Mödersheim, S., Rusinowitch, M., Turuani, M., Viganò, L., Vigneron, L.: The AVISS Security Protocol Analysis Tool. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 349–354. Springer, Heidelberg (2002)
AVISPA. Deliverable 2.1: The High-Level Protocol Specification Language (2003), available at: http://www.avispa-project.org
AVISPA. Deliverable 7.2: Assessment of the AVISPA tool v. 1 (2003), available at: http://www.avispa-project.org
Boichut, Y., Héam, P.-C., Kouchnarenko, O.: Automatic Verification of Security Protocols Using Approximations. Research Report RR-5727, INRIA-CASSIS Project (October 2005)
Boichut, Y., Héam, P.-C., Kouchnarenko, O., Oehl, F.: Improvements on the Genet and Klay technique to automatically verify security protocols. In: Proc. AVIS 2004, joint to ETAPS 2004, pp. 1–11 (April 2004) (to appear in ENTCS)
Bozga, L., Lakhnech, Y., Périn, M.: HERMES: An automatic tool for verification of secrecy in security protocols. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 219–222. Springer, Heidelberg (2003)
Chevalier, Y., Compagna, L., Cuellar, J., Hankes Drielsma, P., Mantovani, J., Mödersheim, S., Vigneron, L.: A high level protocol specification language for industrial security-sensitive protocols. In: Proceedings of SAPS 2004, Linz, Austria, vol. 180 (September 2004)
Chevalier, Y., Kusters, R., Rusinowitch, M., Turuani, M.: An NP decision procedure for protocol insecurity with XOR. Theoretical Computer Science 338 (2005)
Cibrario, I., Durante, L., Sisto, R., Valenzano, A.: Automatic detection of attacks on cryptographic protocols: A case study. In: Julisch, K., Krügel, C. (eds.) DIMVA 2005. LNCS, vol. 3548, pp. 69–84. Springer, Heidelberg (2005)
Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications (2002), http://www.grappa.univ-lille3.fr/tata/
Comon-Lundh, H., Cortier, V.: Tree automata with one memory, set constraints and cryptographic protocols. Theoretical Computer Science 331(1), 143–214 (2005)
Cortier, V., Delaune, S., Lafourcade, P.: A survey of algebraic properties used in cryptographic protocols. Journal of Computer Security (2005)
Durgin, N.A., Lincoln, P.D., Mitchell, J.C., Scedrov, A.: Undecidability of bounded security protocols. In: Proc. FMSP 1999, Italy, Trento (August 1999)
Feuillade, G., Genet, T., Viet Triem Tong, V.: Reachability analysis of term rewriting systems. Journal of Automated Reasonning 33 (2004)
Genet, T., Klay, F.: Rewriting for cryptographic protocol verification. In: McAllester, D. (ed.) CADE 2000. LNCS, vol. 1831, pp. 271–290. Springer, Heidelberg (2000)
Genet, T., Tang-Talpin, Y.-M., Viet Triem Tong, V.: Verification of copy-protection cryptographic protocol using approximations of term rewriting systems. In: Proc. of WITS 2003 (2003)
Monniaux, D.: Abstracting cryptographic protocols with tree automata. In: Cortesi, A., Filé, G. (eds.) SAS 1999. LNCS, vol. 1694, p. 149. Springer, Heidelberg (1999)
Ohsaki, H., Takai, T.: Actas: A system design for associative and commutative tree automata theory. In: Proc. of RULE 2004 (June 2004) (to appear in ENTCS)
Rusinowitch, M., Turuani, M.: Protocol insecurity with finite number of sessions is NP-complete. In: Proc. of CSFW 2001, pp. 174–190. IEEE, Los Alamitos (2001)
Truderung, T.: Regular protocols and attacks with regular knowledge. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS, vol. 3632, pp. 377–391. Springer, Heidelberg (2005)
Zunino, R., Degano, P.: Handling exp, x (and timestamps) in protocol analysis. In: Aceto, L., Ingólfsdóttir, A. (eds.) FOSSACS 2006. LNCS, vol. 3921, pp. 413–427. Springer, Heidelberg (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Boichut, Y., Héam, P.C., Kouchnarenko, O. (2006). Handling Algebraic Properties in Automatic Analysis of Security Protocols. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds) Theoretical Aspects of Computing - ICTAC 2006. ICTAC 2006. Lecture Notes in Computer Science, vol 4281. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11921240_11
Download citation
DOI: https://doi.org/10.1007/11921240_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-48815-6
Online ISBN: 978-3-540-48816-3
eBook Packages: Computer ScienceComputer Science (R0)