Web services are software systems that support distributed applications composed of independent processes which communicate by message passing. To realize the full potential of web services, the authors need to compose existent web services in order to get more functionality. However the composition of web services should be secure. In this paper, they propose an automatic formal approach to monitor the execution of choreography of web services and they prove its correctness. They introduce the syntax and semantic rules of a new operator which takes as input choreography and a security policy and produces as output a secure version of this choreography which behaves like the original one and does not violate the security policy.