On the Verification of Security-Aware E-services

Web services providing E-commerce capabilities to support business transactions over the Internet are more and more widespread. The development of such services involves several security issues ranging from authentication to the management of the access to shared resources according to a given business model. The capability of validating designs against fast evolving requirements is of paramount importance for the adaptation of business models to changing regulations and rapidly evolving market needs. So, techniques for the specification and automated analysis of web services to be used in security-sensitive applications are crucial in the development of these systems. In this paper, we propose an extension of the relational transducers introduced by Abiteboul, Vianu, Fordham, and Yesha for the specification of the transaction protocols of web services and their security properties. We investigate the decidability of relevant verification problems such as goal reachability (for the validation of use-case scenarios) and log validation (for detecting frauds) and provide sufficient conditions for their decidability. The extension we propose is two-fold. First, we add constraints to specify the algebraic structure of the resources manipulated by the transducers. Second, recursion is allowed (only) in policy rules to express important policy idioms such as delegation. Technically, decidability is obtained by a reduction to a decidable class of first-order formulae and fix-point computation to handle recursion.