Abstract
Web services send and receive messages in XML syntax with some parts hashed, encrypted or signed, according to the WS-Security standard. In this paper we introduce a model to formally describe the protocols that underly these services, their security properties and the rewriting attacks they might be subject to. Unlike other protocol models (in symbolic analysis) ours can handle non-deterministic receive/send actions and unordered sequence of XML nodes. Then to detect the attacks we have to consider the services as combining multiset operators and cryptographic ones and we have to solve specific satisfiability problems in the combined theory. By non-trivial extension of the combination techniques of [3] we obtain a decision procedure for insecurity of Web services with messages built using encryption, signature, and other cryptographic primitives. This combination technique allows one to decide insecurity in a modular way by reducing the associated constraint solving problems to problems in simpler theories.
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
Bhargavan, K., Fournet, C., Gordon, A.D., Pucella, R.: Tulafale: A security tool for web services. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2003. LNCS, vol. 3188, pp. 197–222. Springer, Heidelberg (2004)
Cervesato, I., Durgin, N.A., Lincoln, P., Mitchell, J.C., Scedrov, A.: A meta-notation for protocol analysis. In: CSFW, pp. 55–69 (1999)
Chevalier, Y., Rusinowitch, M.: Combining intruder theories. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 639–651. Springer, Heidelberg (2005)
Basin, D.A., Mödersheim, S., Viganò, L.: Algebraic intruder deductions. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 549–564. Springer, Heidelberg (2005)
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, Springer, Heidelberg (2005)
Goubault-Larrecq, J., Roger, M., Verma, K.N.: Abstraction and resolution modulo ac: How to verify diffie-hellman-like protocols automatically. J. Log. Algebr. Program. 64(2), 219–251 (2005)
Baader, F., Schulz, K.U.: Unification in the union of disjoint equational theories. J. Symb. Comput. 21(2), 211–243 (1996)
Thayer, F.J., Herzog, J.C., Guttman, J.D.: Strand spaces: Proving security protocols correct. Journal of Computer Security 7(1) (1999)
Chevalier, Y., Lugiez, D., Rusinowitch, M.: Towards an Automatic Analysis of Web Service Security. Technical report, INRIA (2007), http://www.inria.fr/rrrt/liste-2007.html
Dolev, D., Yao, A.: On the Security of Public-Key Protocols. IEEE Transactions on Information Theory 2(29) (1983)
Weidenbach, C.: Towards an automatic analysis of security protocols in first-order logic. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 314–328. Springer, Heidelberg (1999)
Dershowitz, N., Jouannaud, J.P.: Rewrite systems. In: Handbook of Theoretical Computer Science, vol. B, pp. 243–320. Elsevier, Amsterdam (1990)
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)
Millen, J., Shmatikov, V.: Symbolic protocol analysis with an abelian group operator or Diffie-Hellman exponentiation. Journal of Computer Security (2005)
Chevalier, Y., Kuesters, R., Rusinowitch, M., Turuani, M.:An NP Decision Procedure for Protocol Insecurity with XOR. In: Proceedings of the Logic In Computer Science Conference, LICS 2003 (2003)
Chevalier, Y., Kourjieh, M.: A symbolic intruder model for hash-collision attacks. In: 11th Annual Asian Computing Science Conference. LNCS, Springer, Heidelberg (2006), ftp://ftp.irit.fr/IRIT/LILAC/main.pdf
Bursuc, S., Comon-Lundh, H., Delaune, S.: Associative-commutative deducibility constraints. In: Thomas, W., Weil, P. (eds.) STACS 2007. LNCS, vol. 4393, pp. 634–645. Springer, Heidelberg (2007)
Rusinowitch, M., Turuani, M.: Protocol insecurity with finite number of sessions is NP-complete. In: Proc.14th IEEE Computer Security Foundations Workshop, Cape Breton, Nova Scotia (2001)
Armando, A., et al.: 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)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chevalier, Y., Lugiez, D., Rusinowitch, M. (2007). Towards an Automatic Analysis of Web Service Security. In: Konev, B., Wolter, F. (eds) Frontiers of Combining Systems. FroCoS 2007. Lecture Notes in Computer Science(), vol 4720. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74621-8_9
Download citation
DOI: https://doi.org/10.1007/978-3-540-74621-8_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-74620-1
Online ISBN: 978-3-540-74621-8
eBook Packages: Computer ScienceComputer Science (R0)