Deciding Security for a Fragment of ASLan

    Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

    Abstract

    ASLan is the input language of the verification tools of the AVANTSSAR platform, and an extension of the AVISPA Intermediate Format IF. One of ASLan's core features over IF is to integrate a transition system with Horn clauses that are evaluated at every state. This allows for modeling many common situations in security such as the interaction between the workflow of a system with its access control policies. While even the transition relation is undecidable for ASLan in general, we show the security problem is decidable for a large and useful fragment that we call TASLan, as long as we bound the number of steps of honest participants. The restriction of TASLan is that all messages and predicates must be in a certain sense unambiguous in their interpretation, excluding “type-confusions” similar to some tagging results for security protocols.
    Original languageEnglish
    Title of host publicationComputer Security – ESORICS 2012 : 17th European Symposium on Research in Computer Security, Pisa, Italy, September 10-12, 2012. Proceedings
    PublisherSpringer
    Publication date2012
    Pages127-144
    ISBN (Print)978-3-642-33166-4
    ISBN (Electronic)978-3-642-33167-1
    DOIs
    Publication statusPublished - 2012
    Event17th European Symposium on Research in Computer Security (ESORICS 2012) - Pisa, Italy
    Duration: 10 Sep 201214 Sep 2012
    http://www.iit.cnr.it/esorics2012/

    Conference

    Conference17th European Symposium on Research in Computer Security (ESORICS 2012)
    CountryItaly
    CityPisa
    Period10/09/201214/09/2012
    Internet address
    SeriesLecture Notes in Computer Science
    Volume7459
    ISSN0302-9743

    Fingerprint Dive into the research topics of 'Deciding Security for a Fragment of ASLan'. Together they form a unique fingerprint.

    Cite this