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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Armando, A., Basin, D. A., Boichut, Y., Chevalier, Y., Compagna, L., Cuellar, J., Drielsma, P.H., Heám, P.-C., Kouchnarenko, O., Mantovani, J., Mödersheim, S., von Oheimb, D., Rusinowitch, M., Santiago, J., Turuani, M., Viganò, L., Vigneron, L.: The AVISPA tool for the automated validation of internet security protocols and applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 281–285. Springer, Heidelberg (2005)
Armando, A., Carbone, R., Compagna, L.: LTL Model Checking for Security Protocols. Journal of Applied Non-Classical Logics, special issue on Logic and Information Security, 403–429 (2009)
AVANTSSAR. Deliverable 5.3: AVANTSSAR Library of validated problem cases (2010), http://www.avantssar.eu
AVANTSSAR. Deliverable 2.3 (update): ASLan++ specification and tutorial (2011), http://www.avantssar.eu
AVISPA Project, http://www.avispa-project.org
Becker, M.Y., Fournet, C., Gordon, A.D.: Security Policy Assertion Language (SecPAL), http://research.microsoft.com/en-us/projects/SecPAL/
Bhargavan, K., Fournet, C., Gordon, A.D., Pucella, R.: TulaFale: A security tool for web services. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2003. LNCS, vol. 3188, pp. 197–222. Springer, Heidelberg (2004)
Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: Proceedings of CSFW 2001, pp. 82–96. IEEE Computer Society Press, Los Alamitos (2001)
Burrows, M., Abadi, M., Needham, R.: A Logic of Authentication. ACM Transactions on Computer Systems 8(1), 18–36 (1990)
Chevalier, Y., Compagna, L., Cuéllar, J., Hankes Drielsma, P., Mantovani, J., Mödersheim, S., Vigneron, L.: A High Level Protocol Specification Language for Industrial Security-Sensitive Protocols. In: Automated Software Engineering. Proc. SAPS 2004 Workshop, pp. 193–205. Austrian Computer Society (2004)
Ciobâca, S., Cortier, V.: Protocol composition for arbitrary primitives. In: Proceedings of CSF, pp. 322–336 (2010)
Comon-Lundh, H., Cortier, V.: New decidability results for fragments of first-order logic and application to cryptographic protocols. Technical Report LSV-03-3, Laboratoire Specification and Verification, ENS de Cachan, France (2003)
Cremers, C.: The scyther tool: Verification, falsification, and analysis of security protocols. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 414–418. Springer, Heidelberg (2008)
De Nicola, R., Ferrari, G., Pugliese, R.: KLAIM: a kernel language for agents interaction and mobility. IEEE TSE 24(5), 315–330 (1998)
Durgin, N., Lincoln, P., Mitchell, J., Scedrov, A.: Undecidability of bounded security protocols. In: Proceedings of the Workshop on Formal Methods and Security Protocols (1999)
Escobar, S., Meadows, C., Meseguer, J.: Maude-npa: Cryptographic protocol analysis modulo equational properties. In: FOSAD, pp. 1–50 (2007)
Gao, H., Nielson, F., Nielson, H.R.: Protocol stacks for services. In: Proc. of the Workshop on Foundations of Computer Security, FCS (July 2009)
Gurevich, Y., Neeman, I.: Distributed-Knowledge Authorization Language (DKAL), http://research.microsoft.com/~gurevich/DKAL.htm
Mödersheim, S.: Abstraction by Set-Membership—Verifying Security Protocols and Web Services with Databases. In: Proceedings of 17th CCS. ACM Press, New York (2010)
Mödersheim, S., Viganò, L.: The Open-source Fixed-point Model Checker for Symbolic Analysis of Security Protocols. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) Fosad 2007-2008-2009. LNCS, vol. 5705, pp. 166–194. Springer, Heidelberg (2009)
Rusinowitch, M., Turuani, M.: Protocol insecurity with finite number of sessions is NP-complete. In: CSFW, p. 174. IEEE Computer Society, Los Alamitos (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
von Oheimb, D., Mödersheim, S. (2011). ASLan++ — A Formal Security Specification Language for Distributed Systems. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds) Formal Methods for Components and Objects. FMCO 2010. Lecture Notes in Computer Science, vol 6957. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-25271-6_1
Download citation
DOI: https://doi.org/10.1007/978-3-642-25271-6_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-25270-9
Online ISBN: 978-3-642-25271-6
eBook Packages: Computer ScienceComputer Science (R0)