Partial model checking for the verification and synthesis of secure service compositions*

Abstract

Security is one of the main aspects of Web Services composition. In this paper we describe a logical approach based on partial model checking technique and open system analysis for the verification and synthesis of secure service orchestrators. Indeed through this framework we are able to specify a system with a possible intruder and verify whether the whole system is secure, i.e., whether the system satisfies a given temporal logic formula that describes a correct behavior (security property). Moreover we are able to define an orchestrator operator able to orchestrate several services in such a way to guarantee both functional and security requirements.