AnBx: Automatic Generation and Verification of Security Protocols Implementations

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    105 Downloads (Pure)

    Abstract

    The AnBx compiler is a tool for automatic generation of Java implementations of security protocols specified in a simple and abstract model that can be formally verified. In our model-driven development approach, protocols are described in AnBx, an extension of the Alice & Bob notation. Along with the synthesis of consistency checks, the tool analyses the security goals and produces annotations that allow the verification of the generated implementation with ProVerif.
    Original languageEnglish
    Title of host publicationFoundations and Practice of Security
    EditorsJoaquín García-Alfaro, Evangelos Kranakis, Guillaume Bonfante
    PublisherSpringer
    Pages156-173
    Number of pages18
    Volume9482
    DOIs
    Publication statusE-pub ahead of print - 25 Feb 2016
    Event8th International Symposium on Foundations and Practice of Security - Clermont-Ferrand, France
    Duration: 26 Oct 201528 Oct 2015

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer

    Conference

    Conference8th International Symposium on Foundations and Practice of Security
    Abbreviated titleFPS 2015
    Country/TerritoryFrance
    CityClermont-Ferrand
    Period26/10/1528/10/15

    Fingerprint

    Dive into the research topics of 'AnBx: Automatic Generation and Verification of Security Protocols Implementations'. Together they form a unique fingerprint.

    Cite this