An Improved Calculus for Secure Dynamic Services Composition

With the increased interest in the Web services composition, more and more enterprises and businesses depend on this paradigm. Open, distributed and dynamic properties of the schema, there is a pressing need for secure services in daily transactions. Orchestration and choreography language provide basic services standards and interaction, collaboration, and negotiation standards among services, but they are not give any secure manners or secure operation styles and specifications. Despite the interest of such security mechanisms, a formal module of them is still lacking. For giving general guide to implement secure orchestration and choreography language, we give a formal approach to carry out those goals. To this target, we emphasize on those by designing an extension of the Spi calculus with Secure Global Calculus. The Spi calculus precisely identifies orchestration secure properties of each principal from a local viewpoint. The secure global calculus describes an interaction secure choreography scenario from a vantage point of view. We called our method SpiG4WSC calculus. We believe that the combination of strong practical needs for dynamic secure Web services composition and the theoretical foundations will lead to a bridge between practice and theories. The contribution of this paper are (1) giving the syntax and semantic of SpiG4WSC calculus; (2)applying the calculus to give a model to presenting the secure orchestration, emphasizing on the formal basis for secure services; (3)describing the secure choreography, giving the formal frame for interaction processes.