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.
Due to the importance of security for Web services, the dynamic aspects of interactive services should be formalized and verified for the satisfaction of some security requirement, such as the compliance of authentication, authorization and privacy policy. In particular, if a cryptographic protocol is designated to perform the authentication in the composition of services, we should abstract the relevant interactions and verify it. Respecting authenticity, the intuitional explanation is that an event e authenticates an agent a such that e can occurs only if a previous message was send by a [23]. For example, given the NeedhamSchroeder Public Key protocol [19] as follows, when Server authenticates Alice 1 Web Ontology Language , at http://www.w3.org/TR/owl-guide/ 2 It is the variant of LTL that only concern the temporal relations in the past time, such as yesterday and until in history. with N onces, Server should detect whether a correspondence assertion[23] is true: once Server accepts N onces encrypted by Ks , it should ensure the event corresponding has occurred in the past, namely, that Server created N onces and sent N onces encrypted by Ka.
So that, one agent should become sure of the identity of the other. Usually, the authenticity is represented as a temporal relationship of events occurring in an interaction protocol of Web services. In the relevant studies [20, 6, 24], authors mainly concern using the grounding messages and operators for the security protocol analysis in the SOAP-based layer. Meanwhile, the relevant techniques of Semantic Web bring more semantics to the functionality and non-functionality of Web services and composition, and perform reasoning tasks for semantic matchmaking. The Web Ontology Language(OWL) and OWL-S 3 have been widely accepted in practice. Respecting OWL-S, to describe their functionality, services are viewed as processes that have pre-conditions and effects. Further, it leads to the consideration about representing interactions of Web services in the OWL and reasoning for the satisfaction of requirement.
However, towards faithfully unrevealing the dynamic aspects of services, it is beyond the expressiveness and reasoning capability of the OWL. Even if we obtain the conversational interactions of processes described in the OWL-S, none of the approaches in [20, 6], is adoptable for us to verify security properties in the semantic layer. That is because that, after mapping the ontological representation into the SOAP-base encapsulation, the implicit and hidden information in the semantic layer will not be preserved completely. Perhaps, it will cause ignoring potential flaws. On the other hand, the formalism and reasoning mechanism in [20, 6] are based on the Closed W orld Assumption(the unknown is false by default), but, the basic logics of the OWL, like the Description Logics(DLs), is on the Open W orld Assumption. Generally speaking, we should consider how to describe interactive behaviors, changes of information, and the security properties required in the ontology-based semantic layer, and how to validate those properties by a reasonable reduction method.
Moreover, our issue is relevant to the well-known f rame problem [22](how to handle the consequence of actions and those facts that remain unaffected by actions), and the reasoning task for inconsistency has to be performed under incomplete knowledge of the world. In recent years, Ontology Evolution, as the generalized case of inconsistent problems, has been classified as one subfield of the relevant research about Ontology Change [9]. In essence, it addresses how to represent the reaction for changing an ontology in order to reflect a change in the domain of interest. As mentioned in [11], there is a pair of changing operations, 3 Ontology Web Language for Services to provide the building blocks for encoding rich semantic service descriptions, http://www.w3.org/Submission/OWL-S. update and erasure, which revise the intensional level of the ontology or the extensional, or both, e.g. making effect on both ABox and T Box of a knowledge base in Description Logics(DL)[2]. There, the special case that changes only occurs in the extensional level of ontology is so-called assertion change, which is similar as other notations, like ABox update in [18], and instance level update and erasure in [11]. As we know, while the intension level of ontology is stable and is defined to conceptualize the domain of intense, the extension level, frequently changing, can be used to represent possible models. And also, towards designating a set of assert changes as a semantic transition, some studies related to assertion change in [18, 11, 1], are compliant with the strategy of minimal change(the change should be as little as possible on a possible model)[22]. Respecting the application related to interactions of services, as mentioned in [21] and [17], the situation calculus and GOLOG are applied to formalize the dynamic aspects of Web services and describe their composition. In particular, Franz Baader, et. al. [1], integrate the action theory[21] with DLs to model invocations of services and present an approach to reasoning for composition. In [1], an atomic service is defined as an action that has a pre-condition and postcondition (a set of effects), described using the assertions of ontology changes. And, the common knowledge base is a set of possible states for the world. As a result, the composability of Web services is reduced into the consistency of a knowledge base in DLs. Furthermore, Franz Baader, et. al. [3], integrate action formalisms into a linear temporal description logics and discuss the computational complexity of satisfiability of executability and projection under unconditional or conditional actions, with or without occlusions. Therefore, following the vein above, we propose to use an assert change-based formalism to model interactions of Web services and reason for the verification of temporal properties, such as authenticity, in the ontological layer.
For convenience, we only concern the case interactions of atomic services and simplify an action with removing pre-conditions and occlusions. In this paper, we propose an OWL-based Past-Linear Temporal Logic (Past-LTL) to formulate temporal properties along a sequence of ontology changes (caused by a sequence of the execution of atomic services), and present the refined method reasoning for the validity of the formulae in an interaction protocol from the semantic layer. As a result, we present a Past-LTL formulae to formally describe authenticity in an interaction protocol of Web services.
In the paper, the rest is organized as follows: Section 2 presents Past-LTL and a skeleton of the reduction approach. In Section 3, we express the authenticity in an interacting protocol as a Past-LTL formula. Finally, we present the related works in Section 4 and give some conclusions in Section 5. 2 2.1
The ALCQIO f ragment of OWL With the consideration on the decidability for ontology-based context reasoning, it is necessary to limit the expressive capability of OWL and use a fragment of that to implement context reasoning. In DLs, ALCQIO(that is based on ALC4), allows for these constructors including Negation, Conjunction, Disjunction, Existential and Universal restrictions, Qualified number restriction(Q), Inverse role(I), and Nominal(O)[2]. For conveniens, the subset of the OWL corresponding to ALCQIO is so-called the ALCQIO f ragment (f ragment) in this paper. Furthermore, for presenting semantics in the f ragment, we take the direct model-theoretic semantics in OWL 25 and simplify those for the f ragment. Namely, given a 4-tuple < ∆I , ·C , ·OP , ·I > as an interpretation I , in which ∆I is a non-empty set of object domains and ·C is a mapping to assign a subset CC of ∆I to each class C, ·OP is a mapping to assign a subset rOP of ∆I × ∆I to each object property r, and ·I is a mapping to assign a subset aI of ∆I to each individual a. Without confusion, an atomic class A, or a class C, or an object property r, or an individual a with a superscript I is as the abbreviation of the result set AI , or CI , or rI , or aI through the corresponding mappings in the model I. And also, we call an interpretation I as a model such that I satisfies an ontology O if all of conditions resulted from each axiom in O are satisfied by I, noted with I |= O(I possibly with subscription to indicate a time point.). One of the most important relationships between two ontologies is the entailment. Namely, let O1 and O2 be two ontologies, O1 entails O2, noted with O1 |= O2, such that for every interpretation I, I |= O1 implies I |= O2 . Likewise, let φ be an f ragment axiom, then O1 |= O2 if and only if for every φ ∈ O2, O1 |= φ. In a f ragment ontology, every class expression is restricted to contain only a simple object property. So that, the inference, e.g. the ontology entailment, is decidable. 2.2
For formalizing an interaction protocol, we present a concept assertion change(AC) that describes a change from a source f ragment ontology into another. De nition 1. (Assertion Change) The assertion change is a set α of atomic assertions (e.g. class assertion, object property assertion, and negative object property assertion axioms) that describe a change on a f ragment ontology. Supposed that we follow the constant domain assumption, (namely, all interpretations share the same set of individuals within a common domain, let I1 and I2 be the different models for a f ragment ontology, then domain((·I )I1 ) = domain((·I )I2 ).), we present Def.2 to express a transition from one model to another.
De nition 2. (AC-Labelled Transition) Let α be AC that puts effect on a model
I1 w.r.t a f ragment ontology O, and products another model I2, and A be
an atomic class, and r be an object property. We call that an AC − labelled
4 The prototypical Description Logics Attributive Concept Language with
Complements is the basis of many expressive Description Logics.
5 http://www.w3.org/TR/2009/REC-owl2-direct-semantics-20091027/
(
AI2 = (AI1 ∪ {aI1 |a : A ∈ α}\{bI1 |b : ¬A ∈ α}) rI2 = (rI1 ∪ {(aI1 , bI1 )|(a, b) : r ∈ α}\{(cI1 , dI1 )|(c, d) : ¬r ∈ α}) And, according to Def.2 above, we propose another definition ALT path as the following: De nition 3. (ALT Path) The ALT P ath(path) is defined as a sequence ρ of AC − labelled transitions, noted with follows: ( Note that a subscription i indicates the order in ρ.) ρ = {
I0, i = 0,
I0 →α1 I1 →α2 . . . →αi Ii, i ≥ 0.
Given a path ρ and 0 ≤ i ≤ #ρ, let α = fAC (ρ, i) be a function to obtain an AC α at the position i in ρ.
Furthermore, through combining some past temporal operators with assertions in a f ragment ontology, we could obtain Past-LTL formulae as defined in Def.4. And, each of the past temporal operators, such as Y (Yesterday), and U −( until in history), only appears in front of an assertion.
De nition 4. (Past-LTL Formula) Given a f ragment ontology O, a Past-LTL formula is inductively defined as follows: 1. F oreveryφ ∈ O, φ is a Past-LTL formula. 2. If either of φ and ψ is a Past-LTL formula, then φ ∧ ψ,φ ∨ ψ, Y φ, and φU −ψ, are also Past-LTL formulae.
Then, as to a Past-LTL formula, back along a path, the validity is defined as follows: De nition 5. (Validity along a path) Given a Past-LTL formula φ and a path ρ from an initial f ragment ontology O, the validity of a Past-LTL formula φ, back from a time point i along ρ, noted with (ρ, i) |= φ, is inductively defined as follows: (ρ, i) |= φ, iff for the interpretation Ii, Ii |= φ and φ is an assertion axiom; (ρ, i) |= φ ∧ ψ, iff (ρ, i) |= φ and (ρ, i) |= ψ; (ρ, i) |= φ ∨ ψ, iff (ρ, i) |= φ or (ρ, i) |= ψ; (ρ, i) |= ¬φ, iff (ρ, i) ̸|= φ; (ρ, i) |= Y φ, iff (ρ, i − 1) |= φ, i > 0; Otherwise, false; (ρ, i) |= φU −ψ, iff ∃k 0 ≤ k ≤ i, (ρ, k) |= ψ, implies ∀j k ≤ j ≤ i, (ρ, j) |= φ;
Each interpretation in a path can be one of the possible worlds as similar as in first order logics. So, a Past-LTL formula can be used to express some temporal properties for a sequence of behaviors that change the possible world.
We refine the reducing method in [4, 3] and propose an OWL-based approach for validating a Past-LTL formula φ along a path ρ from a f ragment ontology O. Supposed that each Past-LTL formula φ has been the Negative Normal Form, Ξ stands for a triple < O, ρ, φ > as an input that consists of a f ragment ontology O , a path ρ, and a Past-LTL formula φ. Let Sub be a set of all class expressions occurring in Ξ, and Λ a set of assertion axioms in O. And, A, r, and T is an atomic class expression (an named class), an object property or a negative object property expression, and a class expression for an AC, respectively. Syntactically, either of names and expressions is possibly with a subscript that indicates a time point i or k with 0 ≤ k ≤ i in a path; and, it is also with a superscript that indicates which constructor the conceptualization is related to. For example, given the classes C and D, TkC⊔D stands for the reduced class from the class C ⊔ D.
Following the strategy in [22], changes between two interpretations should be little as possible while still satisfying all post-conditions. Intuitively, respecting the time point i, the minimization of changes on named elements can be described in a direct way through Λred, while the minimization of changes on i unnamed elements is achieved through a suitable encoding of T in Γired. As mentioned in [1], since the interpretation of a defined class is uniquely determined by the interpretation of an atomic class and role names, it is sufficient to impose this minimization of change condition on named classes and roles.
Given a time point i in a path for the input Ξ, the reducing skeleton is as the following steps: 1. Due to the meaning of ALT in Def.2, we can define a set Γired of some equivalent class axioms to conceptualize the minimization of changes on individuals, classes, and axioms at each transition in ρ from O. 2. In a path ρ, the changes on the named objects will be guaranteed by a set Λred of the reduced assertions that consists of the initial assertions, the AC i assertions in ρ , and the preserving assertions; 3. The Past-LTL formula φ will be transformed into a set ∂ of sets of assertion axioms by a set of reducing tableaux rules; 4. Finally, φ is valid such that ∃Λiφ, Λiφ ∈ ∂, Γired ⊔ Λired |= Λiφ;
As shown in (
ΓiN = {N ≡
⊔ T A
k ≡ (N ⊓ Ak) ⊔ (¬N ⊓ A0), A ∈ Sub, Γired = ΓiN ⊔ (
⊔ (ΓkSub ⊔ {TkA ≡ TkE |(A ≡ E) ∈ O} ⊔ {Domain(rk, TkC )|Domain(r, C) ∈ O} ⊔ {Range(rk, TkC )|Range(r, C) ∈ O})) In this paper, we only discuss the case adding new assertions(possibly a negative object property). And also, with the addition of domain and range axioms, our approach avoids producing too many reduced assertions to affect the availability.
Given an input Ξ, with reducing each of class expressions, we also need to
reduce the assertions related. For all assertions w.r.t Ξ, at a time point i or
after a transition, each class expression occurring within a class assertion or
object property axiom should be replaced with the reduced one. Let φ be a class
assertion a : C, or an object property assertion a, b : r, or a negative object
property assertion a, b : ¬r , then the reduced one, as shown in (
φi = a : TiC ),
if φ = a : C
(a, b) : ri, if φ = a, b : r
(a, b) : ¬ri, if φ = a, b : ¬r
Given Λ as an initial set of all assertions w.r.t Ξ, Λini is a set of the results
through (
Λinit = {φ0|φ ∈ Λ}
So, the set Λred of reduced assertions is defined inductively as follows(
0 0 ΛkA =ΛkA−1 ∪ {a : Ak−1 → Ak|a ∈ NI , and a : Ak−1 ∈ ΛkA−1}
∪ {a : Ak|a : A ∈ fAC (ρ, k)}, if 1 ≤ k ≤ i.
Λk¬A =Λk¬−A1 ∪ {a : ¬Ak−1 → ¬Ak|a ∈ NI , and
a : ¬Ak−1 ∈ Λk¬−A1} ∪ {a : ¬Ak|a : ¬A ∈ fAC (ρ, k)}, if 1 ≤ k ≤ i.
(
Λred = ΛiA ∪ Λi¬A ∪ Λir ∪ Λi¬r
As to a Past-LTL formula φ, through a tableaux approach refereing to that in [3],
φ is unfolded into a set Λiφ of assertions w.r.t Ξ. In the tableaux rules (
Λ ∈ ∂ ∧ (φ ∨ ϕ)i ∈ Λ ∂ := (∂\{Λ}) ∪ {Ω′ , Ω′′ } ∨Rule
Λ := (Λ\{(Y φ)i}) ∪ {φi−1} Λ ∈ ∂ ∧ (Y φ)i ∈ Λ, 0 ≤ i ≤ #ρ
Y Rule ∧Rule Λ ∈ ∂ ∧ (φU −ϕ)i ∈ Λ, 0 ≤ i ≤ #ρ ∂ := (∂\{Λ}) ∪ {Ωi, Ωi−1, . . . , Ω0}
U −Rule Ω′ = (Λ\{(φ ∨ ϕ)i}) ∪ {φi} Ω′′ = (Λ\{(φ ∨ ϕ)i}) ∪ {ϕi} Ωk = (Λ\{(φU −ϕ)i}) ∪ {φi, φi−1, . . . , ϕi−k, 0 ≤ k ≤ i}
Finally, The rules above are applied exhaustively on ∂ to get rid of any temporal operator in φ. And, we can take a set Λiφ from ∂, which should be as candidates to check the entailment relationship with the reduced ontology Γired ∪ Λired.
Theorem 1. Let Ξ be an input as a triple (O, ρ, φ) and O, ρ, and φ, be an
initial f ragment ontology, a path, and a Past-LTL formula, respectively. Then,
given a time point i in ρ, through (
i
Likewise, through (
:RunInit :Begin(End)Response :RunResponse
:who :session :nonce :parter
CR CS CN CBI CRI CBR CRR rw rs rn rp
Statement a participant.
a session.
random value.
begin or end in an initiator. run an authentication in an initiator.
begin or end in a responser. run an authentication in a responser.
range over participants.
range over sessions. range over random value. range over participants.
In summary, the validity of a Past-LTL formula w.r.t the input is transformed into the problem checking the entailment relationship between two OWL ontologies (two sets of axioms). Since our approach is based on the ALCQIO fragment of OWL and is approximatively the ALCQIO-case under unconditional actions without occlusions in [3], the whole commotional complexity is NExpTime for the Lemma.12 in [3]. 3
The authenticity is an essential property for interacting protocols always as a
temporal property [23, 5, 8]. So, we represent the property related to the
authenticity in Past-LTL. Usually, the correspondence or non-injection in the
authentication is expressed in a temporal logic based on such events, e.g. beginning
an initial request, ending an initial request, etc[8]. So, we follow it but express
them as a Past-LTL formula in a f ragment, so as to conceptualize each event
occurring in an authentication procedure. There are six events CBI , CRI , CEI ,
CBR, CRR, and CER in Tab.1 with other classes and object properties related.
And, as to (
e : E(i, p, s, n) =.((e : E) ∧ (e, i : rw) ∧ (p : rp) · ∧(s : rs) ∧ (e, n : rn)·
∧ (i : CR) ∧ (p : CR) · ∧(s : CS ) ∧ (n : CN )
(
As the foundation of reasoning under a dynamic and open environment(with incomplete knowledge of the world), the research about Ontology Change has widely carried out[10] in recent years. Specially, many works fucus on update of assertive axioms, or update in the instance level of ontology. In [13], the authors present an algorithm for updating completion graphs under both the addition and removal of ABox assertions. On the contrary, both [12] and [18] adopt a semantic notion of update and erasure. In [12], erasure is studied for RDF, under the same semantics we use in the present paper, namely the Katsuno-Mendelson semantics [15]. In [4, 18], the authors propose a formal semantics for updates in DLs, and present interesting results on various aspects related to computing updates. In [11], authors introduce DL-LiteFS that minimally extends DL-LiteF and is closed with respect to instance-level update, and also present a polynomial algorithm for computing instance-level update in this logic. In this paper, we are inspired mainly by the reducing method in [4, 18] and refine it for the validation of the Past-LTL formulae.
Respecting the security verification for Web services, in [6], authors propose a specification language T ulaF ale for writing machine-checkable descriptions of SOAP-based security protocols and their properties, which can be complied into the applied pi calculus, and be verified using Blanchet’s resolution-based protocol verifier. Moreover, authors in [16] propose a method for mapping interacting messages to abstract symbols in the style of Dolev-Yao, and Casper notation and formally analyze WS-Security and WS-Secure Conversation. While these approaches mainly consider how to specify, model and verify security of SOAPbased interactions between Web services, our approach is such a solution in an ontology-based semantic layer that be more suitable for open environment.
For the security aspects of composing services, Barbara Carminati et al put efforts on security constraint-based Web services composition [7]. Moreover, Lalana Kagal et al present some ontology of policy language and a distributed solution for policy management to enhance the traditional identification and access control framework so as to realize the dynamic and non-center management[14]. Although these works discuss the enforcement of ontology-based security policies within a dynamic context, such as the composition of services, the reasoning mechanism is limited to check the satisfaction of static security properties since the absence of semantics of interactions (actions). 5
With the help of the action theory and OWL, we can formalize a sequence of state changes caused by the invocations of atomic Semantic Web services and check the salification of temporal properties under incomplete knowledge of world. In particular, Authenticity as a concrete temporal property, has been expressed as an OWL-base Past-LTL formula. According to the approach, the validity of temporal properties in an interaction protocol has been reduced into obtaining an entailment relationship, namely, detecting whether a set of the axioms reduced from a path entails the one unfolded from the Past-LTL formula for the temporal properties. For more clarity, some algorithms has been proposed for reducing a path and unfolding a Past-LTL based on the result of the former. As a concrete application, we have represented the mechanism marking events in a f ragment for checking the non-injective agreement and reduce the authenticating procedure into a path. As a result, verifying the authenticity in an interacting protocol has been reduced into the validity of a Past-LTL formula in a path.
Since the result is archived on only concerning atomic services, we will extend the approach into the application of complex services. In this case, more control constructors, such as choice and iteration, will be considered and need to enhance the reducing method. Moreover, we plan to use more simple fragment of OWL to semantically describe the interactions of Web services, such as OWL-Lite, so as to promote the performance of checking the entailment relationship of reduced ontologies.