=Paper=
{{Paper
|id=None
|storemode=property
|title=Formalizing and Verifying Authenticity over Assertion Changes for An Interaction Protocol
|pdfUrl=https://ceur-ws.org/Vol-651/paper6.pdf
|volume=Vol-651
}}
==Formalizing and Verifying Authenticity over Assertion Changes for An Interaction Protocol==
https://ceur-ws.org/Vol-651/paper6.pdf
Formalizing and Verifying Authenticity over
Assertion Changes for An Interaction Protocol
Xiaolie Ye and Lejian Liao
School of Computer Science and Technology, Beijing Institute of Technology,
5 South Zhongguancun Street, Haidian District, Beijing, China
Abstract. The Semantic Web techniques, like OWL1 , bring more se-
mantic 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 se-
curity of interactions of Web services, we should solve such problems like
how to describe interactive behaviors, static information, and the secu-
rity properties required in the ontological layer, and how to validate those
properties by a reasonable reduction method. As well-known, a knowl-
edge 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 asser-
tions(assertion changes)that describe the update and erasure in instance
level for a knowledge base, we propose an approach to conceptualize tran-
sitions 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.
Keywords: Ontology Change, Interaction Protocol, Temporal Logic, Authen-
ticity
1 Introduction
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 Needham-
Schroeder 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.
2
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 .
Alice → Server : (a, N oncea )Ks
Server → Alice : (N onces , N oncea )Ka
Alice → Server : (N onces )Ks
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 pro-
tocol 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 match-
making. 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 representa-
tion into the SOAP-base encapsulation, the implicit and hidden information in
the semantic layer will not be preserved completely. Perhaps, it will cause ignor-
ing 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 prop-
erties 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.
3
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 oc-
curs 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 sta-
ble and is defined to conceptualize the domain of intense, the extension level,
frequently changing, can be used to represent possible models. And also, to-
wards 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 min-
imal 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 in-
vocations 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 post-
condition (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 computa-
tional complexity of satisfiability of executability and projection under uncondi-
tional or conditional actions, with or without occlusions. Therefore, following the
vein above, we propose to use an assert change-based formalism to model in-
teractions 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 OWL Ontology based Past-LTL and Reasoning
2.1 The ALCQIO f ragment of OWL
With the consideration on the decidability for ontology-based context reason-
ing, it is necessary to limit the expressive capability of OWL and use a frag-
4
ment of that to implement context reasoning. In DLs, ALCQIO(that is based
on ALC 4 ), allows for these constructors including Negation, Conjunction, Dis-
junction, Existential and Universal restrictions, Qualified number restriction(Q),
Inverse role(I), and Nominal(O)[2]. For conveniens, the subset of the OWL cor-
responding 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 di-
rect 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 C C
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 C I , 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 Conceptualizing Assertion Change
For formalizing an interaction protocol, we present a concept assertion change(AC)
that describes a change from a source f ragment ontology into another.
Definition 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 inter-
pretations 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.
Definition 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 Comple-
ments is the basis of many expressive Description Logics.
5
http://www.w3.org/TR/2009/REC-owl2-direct-semantics-20091027/
5
transition(ALT ) noted with I1 →α I2 , such that the semantic of I1 →α I2 is in-
ductively defined through (1) and (2) for classes and object properties in O.
AI2 = (AI1 ∪ {aI1 |a : A ∈ α}\{bI1 |b : ¬A ∈ α}) (1)
rI2 = (rI1 ∪ {(aI1 , bI1 )|(a, b) : r ∈ α}\{(cI1 , dI1 )|(c, d) : ¬r ∈ α}) (2)
And, according to Def.2 above, we propose another definition ALT path as the
following:
Definition 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,
ρ= (3)
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.
Definition 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:
Definition 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.
6
2.3 Reducing
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, respect-
ing the time point i, the minimization of changes on named elements can be
described in a direct way through Λred i , while the minimization of changes on
unnamed elements is achieved through a suitable encoding of T in Γired . As men-
tioned 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
i of the reduced assertions that consists of the initial assertions, the AC
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 ∈ ∂, Γi
red
⊔ Λred
i |= Λφi ;
As shown in (4)[4], ΓiN is defined as a set that contains a single equivalence
class axiom for a named class N and a conjunction of all nominal classes, in
which, n stands for the size of the set of nominal classes aj for an input Ξ.
Furthermore, TkA in (5) stands for the equivalent class to the interception of the
atomic class A after the k th transition. As shown in the right side of the formula
(5)[4], the unionOf ⊔ constructor connects two parts: the first, expressing named
elements and the second, expressing the unnamed elements. For same reason, the
equivalent class to the interception of each named class, such as TkC⊔D , TkC⊓D ,
Tk¬C , Tk∃r.C , Tk∀r.C ,Tk≥nr.C , and Tk≤nr.C in Sub can be inductively defined by
the semantics of constructors(details in [1]). Finally, we can get a set ΓkSub of
equivalent class axioms. In addition, as shown in (6), besides the axioms reduced
7
from nominal and AC, Γired also contains others axioms reduced from initial
equivalent class axioms in O, and the object property domain and range axioms
w.r.t Ξ.
⊔
ΓiN = {N ≡ {aj }} (4)
0≤j≤n
TkA ≡ (N ⊓ Ak ) ⊔ (¬N ⊓ A0 ), A ∈ Sub, (5)
⊔
Γired = ΓiN ⊔ ( (ΓkSub ⊔ {TkA ≡ TkE |(A ≡ E) ∈ O}
0≤k≤i
(6)
⊔ {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 (7), be φi , or
a, b : ri , or a, b : ¬ri at time point i, respectively.
C
a : Ti ), if φ = a : C
φi = (a, b) : ri , if φ = a, b : r (7)
(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 (8).
Λinit = {φ0 |φ ∈ Λ} (8)
So, the set Λred
i of reduced assertions is defined inductively as follows(9 - 14):
¬A
ΛA
0 = Λ0 = Λr0 = Λ¬r
0 =Λ
init
(9)
k =Λk−1 ∪ {a : Ak−1 → Ak |a ∈ NI , and a : Ak−1 ∈ Λk−1 }
ΛA A A
(10)
∪ {a : Ak |a : A ∈ fAC (ρ, k)}, if 1 ≤ k ≤ i.
Λ¬A ¬A
k =Λk−1 ∪ {a : ¬Ak−1 → ¬Ak |a ∈ NI , and
(11)
a : ¬Ak−1 ∈ Λ¬A
k−1 } ∪ {a : ¬Ak |a : ¬A ∈ fAC (ρ, k)}, if 1 ≤ k ≤ i.
8
Λrk =Λrk−1 ∪ {a : (∃rk−1 {b} → ∃rk .{b})|a, b ∈ NI , and (a, b : rk−1 ) ∈ Λrk−1 }
∪ {a, b : rk |a, b : r ∈ fAC (ρ, k)}, if 1 ≤ k ≤ i.
(12)
Λ¬r ¬r ¬r
k =Λk−1 ∪ {a : (∀rk−1 ¬{b} → ∀rk .¬{b})|a, b ∈ NI , and (a, b : ¬rk−1 ) ∈ Λk−1 }
∪ {a, b : ¬rk |a, b : ¬r ∈ fAC (ρ, k)}, if 1 ≤ k ≤ i.
(13)
¬A
i ∪ Λi
Λred = ΛA ∪ Λri ∪ Λ¬r
i (14)
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 (15-18), ∂
is a set of sets of Past-LTL formulae with an initial status ∂ = {{φi }}, φ0 = φ.
′′
In ∨Rule, the set β ′ and β is defined in (19-20) And, in U − Rule, Ωk is defined
as (21).
Λ ∈ ∂ ∧ (φ ∧ ϕ)i ∈ Λ
∧Rule (15)
Λ := (Λ\{(φ ∧ ϕ)i }) ∪ {φi , ϕi }
Λ ∈ ∂ ∧ (φ ∨ ϕ)i ∈ Λ
∨Rule (16)
∂ := (∂\{Λ}) ∪ {Ω ′ , Ω ′′ }
Λ ∈ ∂ ∧ (Y φ)i ∈ Λ, 0 ≤ i ≤ #ρ
Y Rule (17)
Λ := (Λ\{(Y φ)i }) ∪ {φi−1 }
Λ ∈ ∂ ∧ (φU − ϕ)i ∈ Λ, 0 ≤ i ≤ #ρ −
U Rule (18)
∂ := (∂\{Λ}) ∪ {Ωi , Ωi−1 , . . . , Ω0 }
′
Ω = (Λ\{(φ ∨ ϕ)i }) ∪ {φi } (19)
′′
Ω = (Λ\{(φ ∨ ϕ)i }) ∪ {ϕi } (20)
Ωk = (Λ\{(φU − ϕ)i }) ∪ {φi , φi−1 , . . . , ϕi−k , 0 ≤ k ≤ i} (21)
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 ∪ Λred
i .
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 (4-5), Γired is obtained as a set of reduced
defining axioms; and through (9-14), Λredi as a set of reduced asserting axioms.
Likewise, through (15-18) w.r.t Ξ, ∂ is obtained as a set of sets of assertions
for φ. Then, (ρ, i) |= φ if and only if Γired ∪ Λred
i is consistent and ∃Λφ i ∈ ∂,
φ
Γi ∪ Λi |= Λi .
red red
9
Table 1. Conceptualizing Authentication Events in F ragment
F ragment Abbreviation Statement
:Role CR a participant.
:Session CS a session.
N
:Nonce C random value.
:Begin(End)Init C BI begin or end in an initiator.
:RunInit C RI run an authentication in an initiator.
:Begin(End)Response C BR begin or end in a responser.
RR
:RunResponse C run an authentication in a responser.
w
:who r range over participants.
:session rs range over sessions.
n
:nonce r range over random value.
:parter rp 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 ontolo-
gies (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 Authenticity in Past-LTL
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 authen-
ticity in Past-LTL. Usually, the correspondence or non-injection in the authen-
tication 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 C BI , C RI , C EI ,
C BR , C RR , and C ER in Tab.1 with other classes and object properties related.
And, as to (22), we can obtain the concrete event assertion only if each E is
substituted by one of C BI , C RI , C EI , C BR , C RR , and C ER .
.
e : E(i, p, s, n) =((e : E) ∧ (e, i : rw ) ∧ (p : rp ) · ∧(s : rs ) ∧ (e, n : rn )·
(22)
∧ (i : C R ) ∧ (p : C R ) · ∧(s : C S ) ∧ (n : C N )
Given a collection of individual variables a, b, s, and n and two event individuals
e0 , e1 , a Past-LTL formula (23) with a universal quantification ∀(a : C R , b :
C R , s : C S , n : C N ), represents the authenticity within an interacting protocol.
10
(Note that ⊙ is the ’Once’ operator and ⊙φ is as (⊤U − φ), and ϕ → φ is as
¬ϕ ∨ φ.)
∀(a : C R , b : C R , s : C S , n : C N ) · (e0 : C ER (b, a, s, n) →
(23)
⊙ (e1 : C RI (a, b, s, n)))
As a result, given an abbreviated Past-LTL formula ∀νδ as (23) and an input Ξ,
the authenticity is hold in ρ such that for every instantiation of the individual
variables a, b, s, and n, ρ |= δ w.r.t Ξ. (Note that ρ |= is the abbreviation of
(ρ, #ρ) |=.)
4 Related Works
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-LiteF S 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 SOAP-
based 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 so-
lution 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 poli-
cies within a dynamic context, such as the composition of services, the reasoning
11
mechanism is limited to check the satisfaction of static security properties since
the absence of semantics of interactions (actions).
5 Conclusions and Future Works
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 ax-
ioms reduced from a path entails the one unfolded from the Past-LTL formula
for the temporal properties. For more clarity, some algorithms has been pro-
posed 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.
References
1. Baader, F., Lutz, C., Milicic, M., Sattler, U., Wolter, F.: A description logic based
approach to reasoning about web services. In: The WWW 2005 Workshop on Web
Service Semantics (WSS2005). Chiba City, Japan (2005)
2. Baader, F.: Description logics. In: 5th International Summer School on Reasoning
Web: Semantic Technologies for Information Systems, August 30, 2009 - September
4, 2009. vol. 5689 LNCS, pp. 1–39. Theoretical Computer Science, TU Dresden,
Germany, Springer Verlag, Brixen-Bressanone, Italy (2009)
3. Baader, F., Liu, H., ul Mehdi, A.: Integrate Action Formalisms into Linear Tem-
poral Description Logics. LTCS-Report LTCS-09-03, Chair for Automata Theory,
Institute for Theoretical Computer Science, Dresden University of Technology, Ger-
many (2009), see http://lat.inf.tu-dresden.de/research/reports.html.
4. Baader, F., Lutz, C., Milicic, M., Sattler, U., Wolter, F.: Integrating description
logics and action formalisms: First results. In: 20th National Conference on Ar-
tificial Intelligence and the 17th Innovative Applications of Artificial Intelligence
Conference, AAAI-05/IAAI-05, July 9, 2005 - July 13, 2005. vol. 2, pp. 572–577.
American Association for Artificial Intelligence (2005)
12
5. Bhargavan, K., Fournet, C., Gordon, A.D.: A semantics for web services authenti-
cation. In: POPL 2004: 31st ACM SIGPLAN-SIGACT Symposium on Principles
of Programming Languages, 14-16 Jan. 2004. vol. 39, pp. 198–209. Microsoft Res.,
Cambridge, UK, ACM, USA (01 2004)
6. Bhargavan, K., Fournet, C., Gordon, A.D., Pucella, R.: Tulafale: A security tool
for web services. In: International Symposium on Formal Methods for Components
and Objects (FMCO’ 03), Volume 3188 of LNCS. pp. 197–222. Springer (2004)
7. Carminati, B., Ferrari, E., Bishop, R., Hung, P.C.K.: Security conscious web service
composition. In: 4th IEEE International Conference on Web Services (ICWS. pp.
489–496. IEEE Computer Society (2006)
8. Corin, R., Saptawijaya, A.: A logic for constraint-based security protocol analysis.
In: 2006 IEEE Symposium on Security and Privacy, 21-24 May 2006. p. 14. Twente
Univ., Netherlands, IEEE Comput. Soc, Los Alamitos, CA, USA (2006)
9. FLOURIS, G., MANAKANATAS, D., KONDYLAKIS, H., PLEXOUSAKIS, D.,
ANTONIOU, G.: Ontology change: classification and survey. The Knowledge En-
gineering Review 23, 2 pp. 117–152 (2008)
10. Flouris, G., Plexousakis, D., Antoniou, G.: A classification of ontology change. In:
In Proc. of the 3rd Italian Semantic Web Workshop: Semantic Web Applications
and Perspectives (SWAP 2006) (2006)
11. Giacomo, G.D., Lenzerini, M., Poggi, A., Rosati, R.: On instance-level update and
erasure in description logic ontologies. Journal of Logic and Computation 19(5),
745–770 (2009)
12. Gutierrez, C., Hurtado, C., Vaisman, A.: The meaning of erasing in rdf under the
katsuno-mendelzon approach. In: In Proc. of the 9th Int. Workshop on the Web
and Databases (WebDB 2006) (2006)
13. Halaschek-Wiener, C., Parsia, B., Sirin, E., Kalyanpur, A.: Description logic rea-
soning for dynamic aboxes. In: In Proc. of the 2006 Description Logic Workshop
(DL 2006). vol. 189 (2006)
14. Kagal, L., Finin, T., Joshi, A.: A policy based approach to security for the semantic
web. In: The SemanticWeb - ISWC 2003. pp. 402–418. Springer Berlin (2003)
15. Katsuno, H., Mendelzon, A.O.: On the difference between updating a knowledge
base and revising it. pp. 387–394. Morgan Kaufmann
16. Kleiner, E., Roscoe, A.W.: On the relationship between web services security and
traditional protocols. In: Mathematical Foundations of Programming Semantics
(MFPS XXI (2005)
17. Levesque, H., Reiter, R., Lesperance, Y., Lin, F., Scherl, R.: Golog: a logic pro-
gramming language for dynamic domains. Journal of Logic Programming 31(1-3),
59 – 83 (1997/04/)
18. Liu, H., Lutz, C., Milicic, M., Wolter, F.: Updating description logic aboxes. In: In
International Conference of Principles of Knowledge Representation and Reason-
ing(KR. pp. 46–56 (2006)
19. Lowe, G.: An attack on the needham-schroeder public-key authentication protocol.
Information Processing Letters 56(3), 131 – 3 (1995/11/10)
20. Meadows, C.A.: Formal verification of cryptographic protocols: A survey. pp. 133–
150. Springer-Verlag (1995)
21. Reiter, R.: Knowledge in Action. MIT Press (2001)
22. Winslett, M.: Reasoning about action using a possible models approach UIUCDCS-
R-88-1428, 17 – (1988/05/)
23. Woo, T.Y.C., Lam, S.S.: A semantic model for authentication protocols. In: IEEE
Symposium on Research in Security and Privacy, 24-26 May 1993. pp. 178–194.
13
Dept. of Comput. Sci., Texas Univ., Austin, TX, USA, IEEE Comput. Soc. Press,
Los Alamitos, CA, USA (1993)
24. Ye, X., Liao, L.: Security of composed interaction for web services. Journal of
Software 4(10), 1160–1168 (2009)