A formal framework for secure and complying services

Internet is offering a variety of services that are assembled to accomplish requests made by clients. While serving a request, security of the communications and of the data exchanged among services is crucial. Since communications occur along specific channels, it is equally important to guarantee that the interactions between a client and a server never get blocked because either cannot access a selected channel. We address here both these problems, from a formal point of view. A static analysis is presented, guaranteeing that a composition of a client and of possibly nested services respects both security policies for access control, and compliance between clients and servers.