A trace semantics for Positive Core XPath

Research output: Book/ReportReportProfessional

4 Citations (Scopus)
34 Downloads (Pure)

Abstract

We provide a novel trace semantics for positive core XPath that exposes all intermediate nodes visited by the query engine. This enables a detailed analysis of all information relevant to the query. We give two examples of such analyses in the form of access control policies. We translate positive core XPath into Linear Temporal Logic, showing that branching structures can be linearised effectively. The translation is proved correct. We use the SPIN model checker in a proof of concept implementation to resolve the queries, and to perform the access control. The performance of the implementation is shown to be competitive.
Original languageUndefined
Place of PublicationEnschede
PublisherDistributed and Embedded Security (DIES)
Number of pages12
Publication statusPublished - Jan 2005

Publication series

NameCTIT Technical Report Series
PublisherUniversity of Twente, Centre for Telematics and Information Technology (CTIT)
No.TR-CTIT-05-03
ISSN (Print)1381-3625

Keywords

  • SCS-Cybersecurity
  • METIS-248120
  • EWI-5751
  • IR-57010

Cite this

Hartel, P. H. (2005). A trace semantics for Positive Core XPath. (CTIT Technical Report Series; No. TR-CTIT-05-03). Enschede: Distributed and Embedded Security (DIES).
Hartel, Pieter H. / A trace semantics for Positive Core XPath. Enschede : Distributed and Embedded Security (DIES), 2005. 12 p. (CTIT Technical Report Series; TR-CTIT-05-03).
@book{55b8556f8b344007843f3efff67397d7,
title = "A trace semantics for Positive Core XPath",
abstract = "We provide a novel trace semantics for positive core XPath that exposes all intermediate nodes visited by the query engine. This enables a detailed analysis of all information relevant to the query. We give two examples of such analyses in the form of access control policies. We translate positive core XPath into Linear Temporal Logic, showing that branching structures can be linearised effectively. The translation is proved correct. We use the SPIN model checker in a proof of concept implementation to resolve the queries, and to perform the access control. The performance of the implementation is shown to be competitive.",
keywords = "SCS-Cybersecurity, METIS-248120, EWI-5751, IR-57010",
author = "Hartel, {Pieter H.}",
note = "Imported from CTIT",
year = "2005",
month = "1",
language = "Undefined",
series = "CTIT Technical Report Series",
publisher = "Distributed and Embedded Security (DIES)",
number = "TR-CTIT-05-03",

}

Hartel, PH 2005, A trace semantics for Positive Core XPath. CTIT Technical Report Series, no. TR-CTIT-05-03, Distributed and Embedded Security (DIES), Enschede.

A trace semantics for Positive Core XPath. / Hartel, Pieter H.

Enschede : Distributed and Embedded Security (DIES), 2005. 12 p. (CTIT Technical Report Series; No. TR-CTIT-05-03).

Research output: Book/ReportReportProfessional

TY - BOOK

T1 - A trace semantics for Positive Core XPath

AU - Hartel, Pieter H.

N1 - Imported from CTIT

PY - 2005/1

Y1 - 2005/1

N2 - We provide a novel trace semantics for positive core XPath that exposes all intermediate nodes visited by the query engine. This enables a detailed analysis of all information relevant to the query. We give two examples of such analyses in the form of access control policies. We translate positive core XPath into Linear Temporal Logic, showing that branching structures can be linearised effectively. The translation is proved correct. We use the SPIN model checker in a proof of concept implementation to resolve the queries, and to perform the access control. The performance of the implementation is shown to be competitive.

AB - We provide a novel trace semantics for positive core XPath that exposes all intermediate nodes visited by the query engine. This enables a detailed analysis of all information relevant to the query. We give two examples of such analyses in the form of access control policies. We translate positive core XPath into Linear Temporal Logic, showing that branching structures can be linearised effectively. The translation is proved correct. We use the SPIN model checker in a proof of concept implementation to resolve the queries, and to perform the access control. The performance of the implementation is shown to be competitive.

KW - SCS-Cybersecurity

KW - METIS-248120

KW - EWI-5751

KW - IR-57010

M3 - Report

T3 - CTIT Technical Report Series

BT - A trace semantics for Positive Core XPath

PB - Distributed and Embedded Security (DIES)

CY - Enschede

ER -

Hartel PH. A trace semantics for Positive Core XPath. Enschede: Distributed and Embedded Security (DIES), 2005. 12 p. (CTIT Technical Report Series; TR-CTIT-05-03).