Verifying Security of Composed Interaction for Web Services

Abstract

SOAP-based complex interactions of multiple end points in Web Services mostly consist of sub-processes or sub-protocols, which are reused as modules and need to comply with corresponding standards and proposals. However, the consistency of local and global properties of interactions is important for practical applications with high security requirement. Therefore, a method is proposed to formally describe composed interactions by the definition of basic and composed interaction models for Web Services. Furthermore, the semantic of interactions, is presented as a path of transitions in Action-based Kripke Transition System, on which some properties, such as secrecy and authentication, are described and verified as formulae in Past Linear Temporal Logic. Then a scenario of composed interactions for Web Services is given and some formal properties corresponding to security are more effectively checked by our approach.