Tailoring the Dolev-Yao abstraction to Web Services realities - A comprehensive wish list

Abstract

Web Services are an important series of standards for adding semantics to web-based and XML-based communication. For analyzing the security of Web Services protocols composed of these standards, it is tempting to exploit their similarity to traditional security protocols by first transforming them into the Dolev-Yao absion, where cryptographic operators are treated symbolically as constructors of a free algebra, and as a second step by applying existing symbolic techniques for machine-assisted or even fully automated protocol verification within this absion. We show in this paper that this approach tends to ignore intrinsic aspects of Web Services standards and protocols and to hence be too coarse-grained for capturing Web Services security in all its facets. We identify a series of such aspects both on the conceptual level and on the level of concrete Web Services protocols: service requestors and providers have additional properties independent of the protocol under consideration and hence offer additional attack possibilities, protocol behaviors can be defined by explicit Web Services policies and complex message parsings which do not necessarily follow the common Dolev-Yao-style parsing conventions, etc. We sketch in a series of examples how to exploit these aspects for mounting successful attacks against Web Services protocols, and we discuss possibilities to circumvent these attacks. In particular, this exemplifies the need for tailoring Dolev-Yao absions specifically to Web Services idiosyncrasies, which go beyond the standard Dolev-Yao assumptions. Copyright 2005 ACM.