Automated Analysis of Infinite Scenarios

Mikael Buchholtz

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

    Abstract

    The security of a network protocol crucially relies on the scenario in which the protocol is deployed. This paper describes syntactic constructs for modelling network scenarios and presents an automated analysis tool, which can guarantee that security properties hold in all of the (infinitely many) instances of a scenario. The tool is based on control flow analysis of the process calculus LySa and is applied to the Bauer, Berson, and Feiertag protocol where is reveals a previously undocumented problem, which occurs in some scenarios but not in other.
    Original languageEnglish
    Title of host publicationTrustworthy Global Computing
    Place of PublicationBerlin
    PublisherSpringer-verlag Berlin
    Publication date2005
    Pages334-352
    ISBN (Print)3-540-30007-4
    DOIs
    Publication statusPublished - 2005
    EventInternational Symposium on Trustworthy Global Computing - Edinburgh, United Kingdom
    Duration: 7 Apr 20059 Apr 2005

    Conference

    ConferenceInternational Symposium on Trustworthy Global Computing
    CountryUnited Kingdom
    CityEdinburgh
    Period07/04/200509/04/2005
    SeriesLecture Notes in Computer Science
    Volume3705
    ISSN0302-9743

    Fingerprint Dive into the research topics of 'Automated Analysis of Infinite Scenarios'. Together they form a unique fingerprint.

    Cite this