Publication
ASLan++ — A formal security specification language for distributed systems
Formal Methods for Components and Objects (FMCO 2010)
Author(s): David von Oheimb and Sebastian Mödersheim
Year: 2010
Publisher: Springer
Editors: Bernhard Aichernig and Frank de Boer and Marcello Bonsangue
Keywords: services, security, specification language, formal analysis
Abstract:
This paper introduces ASLan++, the AVANTSSAR Specification Language.
ASLan++ has been designed for formally specifying dynamically composed security-sensitive
web services and service-oriented architectures, their associated security policies,
as well as their security properties, at both communication and application level.
We introduce the main concepts of ASLan++ at a small but very instructive running example,
abstracted form a company intranet scenario, that features non-linear and inter-dependent
workflows, communication security at different abstraction levels including an explicit
credentials-based authentication mechanism, dynamic access control policies, and the related
security goals. This demonstrates the flexibility and expressiveness of the language,
and that the resulting models are logically adequate, while on the other hand they are clear
to read and feasible to construct for system designers who are not experts in formal methods.
Copyright © 2010 AVANTSSAR consortium
Preprint; official download
Slides
BibTeX entry:
@inproceedings{ASLan++-FMCO10,
author = {David von Oheimb and Sebastian M\"odersheim},
title = {{ASLan++} --- A formal security specification language for distributed systems},
booktitle = {Formal Methods for Components and Objects, FMCO 2010, Graz, Austria},
editor = {Aichernig, B. and de Boer, F. and Bonsangue, M.},
publisher = {Springer},
series = {LNCS},
volume = {6957},
pages = {1--22},
isbn = {978-3-642-25270-9},
ee = {http://dx.doi.org/10.1007/978-3-642-25271-6},
year = 2010,
month = Dec,
location = {Graz, Austria},
note = {\url{http://ddvo.net/papers/FMCO2010.html}},
abstract = {
This paper introduces ASLan++, the AVANTSSAR Specification Language.
ASLan++ has been designed for formally specifying dynamically composed security-sensitive
web services and service-oriented architectures, their associated security policies,
as well as their security properties, at both communication and application level.
We introduce the main concepts of ASLan++ at a small but very instructive running example,
abstracted form a company intranet scenario, that features non-linear and inter-dependent
workflows, communication security at different abstraction levels including an explicit
credentials-based authentication mechanism, dynamic access control policies, and the related
security goals. This demonstrates the flexibility and expressiveness of the language,
and that the resulting models are logically adequate, while on the other hand they are clear
to read and feasible to construct for system designers who are not experts in formal methods.
}
}