A trace semantics for Positive Core XPath

    Research output: Book/ReportReportProfessional

    4 Citations (Scopus)
    35 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).