Verification of Access Control Requirements in Web Services Choreography

Web services choreography is used to design peer-to-peer applications where each peer is potentially a Web service. It defines the required behavior of participating Web services along with their interactions through message exchanges. Implementing a complex system described by a choreography requires selecting actual Web services whose individual behaviors are compatible with the overall behavior described by the choreography. Although the selected Web services implement the specified behavior, they may not be able to interact due to the policies they enforce to protect their resources. A Web service' resource can be an operation or a credential type to be submitted to be able to invoke an operation. In this paper, we propose a novel approach to determine at design time whether a choreography can be implemented by a set of Web services based on their access control policies and the disclosure policies regulating the release of their credentials. We model both Web services and Web services choreography as transition systems and represent Web services credential disclosure policies as directed graphs. We then verify that all possible conversations of the Web services choreography can be implemented by matching credential disclosure policies of the invoker Web service with the access control policy of the Web services being invoked. We propose a resource release graph to enable this verification.