We consider two complementary formal approaches for describing services and their interactive behaviour.

The first approach is based on the notion of contracts. Contracts are
CCS-like processes that contain a description of the external observable behavior of a service. A notion of compliace has been introduced allowing
to check whether the interaction between two parties terminate or gets stuck. The second proposal is based on λ-req, a core calculus for services, with primitives for expressing security policies and for composing services in a call-by-contract fashion.
In the dissertation we express CCS contracts via λ-req expressions and we prove that the proposed transformation preserves compliance of contracts, by exploiting the security mechanism of λ-req.

The transformation enjoys further properties.
Multi-party and secure contracts are naturally handled. Moreover, the resulting notion of compliance is compositional: one can substitute a service with an equivalent one without breaking the security of the composition.