Verifying Authenticity in Interactive Behaviors of SemanticWeb Services

Due to the importance of security within Semantic Web services, every interaction protocol embedded in dynamic behaviors of composed services should be formally modeled and verified for the satisfaction of some security requirement, such as the compliance of authentication, authorization and privacy policy. Our purpose is to model interactive behaviors and verifying security properties in the ontology-base semantic layer. Towards the aim, we present an OWL-based Past Linear Temporal Logic (Past-LTL) to describe temporal properties within interactions of Semantic Web services and refine some algorithms to reduce the validity of an OWL-based Past-LTL formula into the entailment relationship in OWL. With the help of the action theory on describing dynamic aspect of Semantic Web services, we propose an approach to transform the verification of the authenticity in interactive behaviors of Semantic Web services into the validity of the OWL-based Past-LTL formula corresponding.