Abstract
In the analysis of cryptographic protocols, a treacherous set of terms is one from which an intruder can get access to what was intended to be secret, by adding on to the top of a sequence of elements of this set, a cap formed of symbols legally part of his/her knowledge. In this paper, we give sufficient conditions on the rewrite system modeling the intruder’s abilities, such as using encryption and decryption functions, to ensure that it is decidable if such caps exist. The following classes of intruder systems are studied: linear, dwindling, Δ-strong, and optimally reducing; and depending on the class considered, the cap problem (“find a cap for a given set of terms”) is shown respectively to be in P, NP-complete, decidable, and undecidable.
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
Abadi, M., Cortier, V.: Deciding knowledge in security protocols under equational theories. Theor. Comput. Sci. 367(1-2), 2–32 (2006)
Amadio, R., Lugiez, D., Vanackère, V.: On the symbolic reduction of processes with cryptographic functions. Theor. Comput. Sci. 290(1), 695–740 (2003)
S. Anantharaman, P. Narendran, M. Rusinowitch. Intruders with Caps, http://www.univ-orleans.fr/lifo/prodsci/rapports/RR/RR2007/RR-2207-02.ps
Armando, A., Compagna, L.: SATMC: a SAT-based Model Checker for Security Protocols. In: Alferes, J.J., Leite, J.A. (eds.) JELIA 2004. LNCS (LNAI), vol. 3229, pp. 730–733. Springer, Heidelberg (2004)
Baudet, M.: Deciding security of protocols against off-line guessing attacks. In: Proc. of ACM Conference on Computer and Communications Security, pp. 16–25 (2005)
Book, R.V., Jantzen, M., Wrathall, C.: Monadic thue systems. Theor. Comput. Sci. 19, 231–251 (1982)
Book, R.V., Otto, F.: The verifiability of two-party protocols. In: EUROCRYPT, pp. 254–260 (1985)
Chevalier, Y., Vigneron, L.: A Tool for Lazy Verification of Security Protocols. In: Proc. of the Automated Software Engineering Conference (ASE 2001), IEEE Computer Society Press, Washington, DC, USA (2001)
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., Treinen, R.: Easy Intruder Deductions. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol. 2772, pp. 225–242. Springer, Heidelberg (2004)
Delaune, S., Jacquemard, F.: A decision procedure for the verification of security protocols with explicit destructors. In: Proc. of ACM Conference on Computer and Communications Security, pp. 278–287 (2004)
Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Transactions on Information Theory 29(2), 198–207 (1983)
Durgin, N.A., Lincoln, P.D., Mitchell, J.G., Scedrov, A.: Multiset rewriting and the complexity of bounded security protocols. Journal of Computer Security 12(1), 677–722 (2004)
Gilleron, R., Tison, S.: Regular tree languages and rewrite systems. Fundamenta Informaticae 24, 157–176 (1995)
Huet, G.P.: Confluent reductions: Abstract properties and applications to term rewriting systems. Journal of the ACM 27(4), 797–821 (1980)
Narendran, P., Pfenning, F., Statman, R.: On the unification problem for Cartesian Closed Categories. Journal of Symbolic Logic 62(2), 636–647 (1997)
Nesi, M., Rucci, G.: Formalizing and analyzing the Needham-Schroeder symmetric-key protocol by rewriting. Electr. Notes Theor. Comput. Sci. 135(1), 95–114 (2005)
Weidenbach, C.: Towards an automatic analysis of security protocols. In: Ganzinger, H. (ed.) Automated Deduction - CADE-16. LNCS (LNAI), vol. 1632, pp. 378–382. Springer, Heidelberg (1999)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Anantharaman, S., Narendran, P., Rusinowitch, M. (2007). Intruders with Caps. In: Baader, F. (eds) Term Rewriting and Applications. RTA 2007. Lecture Notes in Computer Science, vol 4533. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73449-9_4
Download citation
DOI: https://doi.org/10.1007/978-3-540-73449-9_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73447-5
Online ISBN: 978-3-540-73449-9
eBook Packages: Computer ScienceComputer Science (R0)