Abstraction by Set-Membership: Verifying Security Protocols and Web Services with Databases

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

    247 Downloads (Pure)

    Abstract

    The abstraction and over-approximation of protocols and web services by a set of Horn clauses is a very successful method in practice. It has however limitations for protocols and web services that are based on databases of keys, contracts, or even access rights, where revocation is possible, so that the set of true facts does not monotonically grow with the transitions. We extend the scope of these over-approximation methods by defining a new way of abstraction that can handle such databases, and we formally prove that the abstraction is sound. We realize a translator from a convenient specification language to standard Horn clauses and use the verifier ProVerif and the theorem prover SPASS to solve them. We show by a number of examples that this approach is practically feasible for wide variety of verification problems of security protocols and web services.
    Original languageEnglish
    Title of host publicationProceedings of the 17th ACM Conference on Computer and Communications Security
    Number of pages9
    Place of PublicationNew York
    PublisherAssociation for Computing Machinery
    Publication date2010
    Pages351-360
    ISBN (Print)978-1-4503-0244-9
    Publication statusPublished - 2010
    EventACM Conference on Computer and Communications Security - Chicago, USA
    Duration: 1 Jan 2010 → …
    Conference number: 17

    Conference

    ConferenceACM Conference on Computer and Communications Security
    Number17
    CityChicago, USA
    Period01/01/2010 → …

    Keywords

    • Automated verification, abstract interpretation, revocation, web services, APIs

    Cite this