Abstract
Automation of semantic web service composition is one of the most promising challenges in semantic web service research area, in which security research on service composition has attracted more attention. In this paper, we present a model of Action labeled Kripke Transition System, namely AKTS which can abstract interaction behaviors involved in service composition and turn them into logic symbols, then propose a secure conversation mode with constraints based on WS-Trust and WS-SecureConversation to ensure the security of service composition. At last, the problem of determining the security of service composition is verified by deterministic propositional logic.