Formalizing and verifying authenticity over assertion changes for an interaction protocol

The Semantic Web techniques, like OWL1, bring more semantic to the static information about functionalities and non-functionalities of Web services. However, it is not smooth to faithfully describe some dynamic aspects and support reasoning tasks. When discussing the security of interactions of Web services, we should solve such problems like how to describe interactive behaviors, static information, and the security properties required in the ontological layer, and how to validate those properties by a reasonable reduction method. As well-known, a knowledge base (e.g. that contains assertive axioms in OWL), can be used to represent the possible states of a world. Then, using a set of the assertions( assertion changes)that describe the update and erasure in instance level for a knowledge base, we propose an approach to conceptualize transitions of states for modeling interactions of Web services. Furthermore, we present an OWL-based Past Linear Temporal Logic (Past-LTL)2 to describe temporal properties within a finite sequence of interactions and refine some algorithms to reduce the validity of an OWL-based Past-LTL formula into the entailment relationship in OWL.