Towards a Formal Framework for Developing Secure Web Services

In this paper, we experiment with use of a formal framework for developing secure Web services (WSs) from components. The framework focuses on separating security requirements from the functional ones. For each component, the approach makes use of two complementary models: one is state-based, described in Z, and the other is event-based, expressed in Hoare\´s communicating sequential processes (CSP) process algebra. The former is particularly useful to capture persistent data and model "back-end" operations whereas the latter is particularly useful to model behaviour, and in particular, "front-end" interactions and communications. The whole system can then be seen in Z as a combination of the constituent components. In CSP the software architecture of the whole system could be viewed as a parallel composition of appropriate customization of the behaviour of relevant components. The CSP descriptions can be implemented as Web services using current technologies such as Java 2 Enterprise Edition (J2EE) and Microsoft\´s .NET framework. We illustrate this approach with a case study for a conference management system. With this approach, it is possible to specify the core functionalities of a system independently from the security mechanisms. Authentication and authorization are viewed as components which are carefully integrated with the global system