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. } }