CaPiTo: protocol stacks for services

Han Gao, Flemming Nielson, Hanne Riis Nielson

    Research output: Contribution to journalJournal articleResearchpeer-review

    Abstract

    CaPiTo allows the modelling of service-oriented applications using process algebras at three levels of abstraction. The abstract level focuses on the key functionality of the services; the plug-in level shows how to obtain security using standardised protocol stacks; finally, the concrete level allows to consider how security is obtained using asymmetric and symmetric cryptographic primitives. The CaPiTo approach therefore caters for a variety of developers that need to cooperate on designing and implementing service-oriented applications. We show how to formally analyse CaPiTo specifications for ensuring the absence of security flaws. The method used is based on static analysis of the corresponding LySa specifications. We illustrate the development on two industrial case studies; one taken from the banking sector and the other a single sign-on protocol.
    Original languageEnglish
    JournalFormal Aspects of Computing
    Volume23
    Issue number4
    Pages (from-to)541-565
    ISSN0934-5043
    DOIs
    Publication statusPublished - 2011

    Keywords

    • Process algebras
    • Communication protocols
    • Standardised protocol stacks
    • Formal verification

    Fingerprint

    Dive into the research topics of 'CaPiTo: protocol stacks for services'. Together they form a unique fingerprint.

    Cite this