CaPiTo: protocol stacks for services

    Research output: Contribution to journalJournal articleResearchpeer-review


    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
    Issue number4
    Pages (from-to)541-565
    Publication statusPublished - 2011


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

    Cite this