Advertisement

ASLan++ — A Formal Security Specification Language for Distributed Systems

  • David von Oheimb
  • Sebastian Mödersheim
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6957)

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.

Keywords

services security specification language formal analysis 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    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)CrossRefGoogle Scholar
  2. 2.
    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)Google Scholar
  3. 3.
    AVANTSSAR. Deliverable 5.3: AVANTSSAR Library of validated problem cases (2010), http://www.avantssar.eu
  4. 4.
    AVANTSSAR. Deliverable 2.3 (update): ASLan++ specification and tutorial (2011), http://www.avantssar.eu
  5. 5.
  6. 6.
    Becker, M.Y., Fournet, C., Gordon, A.D.: Security Policy Assertion Language (SecPAL), http://research.microsoft.com/en-us/projects/SecPAL/
  7. 7.
    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)CrossRefGoogle Scholar
  8. 8.
    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)Google Scholar
  9. 9.
    Burrows, M., Abadi, M., Needham, R.: A Logic of Authentication. ACM Transactions on Computer Systems 8(1), 18–36 (1990)CrossRefzbMATHGoogle Scholar
  10. 10.
    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)Google Scholar
  11. 11.
    Ciobâca, S., Cortier, V.: Protocol composition for arbitrary primitives. In: Proceedings of CSF, pp. 322–336 (2010)Google Scholar
  12. 12.
    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)Google Scholar
  13. 13.
    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)CrossRefGoogle Scholar
  14. 14.
    De Nicola, R., Ferrari, G., Pugliese, R.: KLAIM: a kernel language for agents interaction and mobility. IEEE TSE 24(5), 315–330 (1998)Google Scholar
  15. 15.
    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)Google Scholar
  16. 16.
    Escobar, S., Meadows, C., Meseguer, J.: Maude-npa: Cryptographic protocol analysis modulo equational properties. In: FOSAD, pp. 1–50 (2007)Google Scholar
  17. 17.
    Gao, H., Nielson, F., Nielson, H.R.: Protocol stacks for services. In: Proc. of the Workshop on Foundations of Computer Security, FCS (July 2009)Google Scholar
  18. 18.
    Gurevich, Y., Neeman, I.: Distributed-Knowledge Authorization Language (DKAL), http://research.microsoft.com/~gurevich/DKAL.htm
  19. 19.
    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)Google Scholar
  20. 20.
    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)Google Scholar
  21. 21.
    Rusinowitch, M., Turuani, M.: Protocol insecurity with finite number of sessions is NP-complete. In: CSFW, p. 174. IEEE Computer Society, Los Alamitos (2001)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • David von Oheimb
    • 1
  • Sebastian Mödersheim
    • 2
  1. 1.Siemens Corporate TechnologyIT SecurityMunichGermany
  2. 2.DTU InformaticsTechnical University of DenmarkLyngbyDenmark

Personalised recommendations