Journal article
CaPiTo: protocol stacks for services
Computer Science and Engineering, Department of Informatics and Mathematical Modeling, Technical University of Denmark1
Department of Informatics and Mathematical Modeling, Technical University of Denmark2
Language-Based Technology, Department of Informatics and Mathematical Modeling, Technical University of Denmark3
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.
Language: | English |
---|---|
Publisher: | Springer-Verlag |
Year: | 2011 |
Pages: | 541-565 |
Journal subtitle: | Applicable Formal Methods |
ISSN: | 1433299x and 09345043 |
Types: | Journal article |
DOI: | 10.1007/s00165-011-0174-7 |
ORCIDs: | Nielson, Flemming and Nielson, Hanne Riis |