A Formal Model for Security-Aware dynamic Web Services Composition

Recently, there are imminent requirements to security policies in dynamic Web services composition, so there appear many security specifications. The requirements of security characters are not always constant and the security specifications will need to modify according to the security requirements, however, there is no a uniform formal foundation to support numerous security specifications, it will block the application of these security policies, which have not been deeply investigated so far. To solve these problems, in this paper, we advocate to apply Spi calculus to describe and reason the security properties, for convenience describe and reason we separate security into security enhancing capability and security limiting constraint. Meanwhile we find the original Spi calculus can´t completely to solve the properties in security-aware Web service composition. In success, we extend the syntax and semantic of Spi calculus, named SpiWeb calculus, to adapt the security-aware dynamic web service composition. Finally as a case study, the online banking system, we apply the SpiWeb calculus to describe and analysis the security features of this system.